Publications in Scientific Journals:
F. Schernhammer, B. Gramlich:
"Characterizing and Proving Operational Termination of Deterministic Conditional Term Rewriting Systems";
Journal of Logic and Algebraic Programming,
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
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.