Proving termination properties of conditional rewrite systems

Abstract

Conditional Term Rewriting Systems (CTRSs) extend Term Rewriting Systems (TRSs) conditional part c to each rewrite rule l → r, thus obtaining a conditional rewrite rule l → r ⇐ c. The addition of such conditional parts c substantially increases the expressiveness of programming languages that use them and often clarifies the purpose of the rules to make programs more readable and self-explanatory. Computations with CTRSs are defined by means of an Inference System where each rewriting step s →R t requires a proof. This proof-theoretical definition of the operational semantics suggests a natural definition of the termination behavior of R as the absence of infinite proof trees. The notion of operational termination captures this idea, meaning that, given an initial goal, an interpreter will either succeed in finite time in producing a closed proof tree, or will fail in finite time, not being able to close or extend further any of the possible proof trees, after exhaustively searching all such proof trees. Besides implying termination in the usual ‘horizontal’ sense (i.e., as the absence of infinite sequences of rewrite steps), operational termination also captures a ‘vertical’ dimension of the termination behavior which is missing in the usual “without infinite reduction sequences” definition of termination. In [1] we define the notion of V-termination, which captures such a vertical dimension of the termination behavior of CTRSs. We provide a uniform definition of termination and V-termination of CTRSs as the absence of specific kinds of infinite proof trees. We prove that operational termination is just the conjunction of termination and V-termination. We use these results to develop a methodology to prove or disprove termination, V-termination, and operational termination of CTRSs by extending the Dependency Pair (DP) approach for TRSs and generalize the DP approach to all aforementioned termination properties of CTRSs.