[Back]

F. Schernhammer, B. Gramlich:
"Characterizing and Proving Operational Termination of Deterministic Conditional Term Rewriting Systems";
Journal of Logic and Algebraic Programming, 79 (2010), 7; 659 - 688.

We investigate the practically crucial property of operational termination of deterministic conditional term rewriting systems (DCTRSs), an important declarative programming paradigm. We show that operational termination can be equivalently characterized by the newly introduced notion of context-sensitive quasi-reductivity. Based on this characterization and an unraveling transformation of DCTRSs into context-sensitive (unconditional) rewrite systems (CSRSs), context-sensitive quasi-reductivity of a DCTRS is shown to be equivalent to termination of the resulting CSRS on original terms. This result enables both proving and disproving operational termination of given DCTRSs via transformation into CSRSs. A concrete procedure for this restricted termination analysis (on original terms) is proposed and encouraging benchmarks obtained by the termination tool VMTL, that utilizes this approach, are presented. Finally, we show that the context-sensitive unraveling transformation is sound and complete for collapse-extended termination, thus solving an open problem of [Duran et al. 2008].

Conditional term rewriting; Operational termination; Transforming conditional rewrite systems; Collapse extended termination; Dependency pair framework

http://dx.doi.org/10.1016/j.jlap.2009.08.001

http://publik.tuwien.ac.at/files/PubDat_194519.pdf