Transforming conditional rewrite systems with extra variables into unconditional systems

DOI10.1007/3-540-48242-3_8MaRDI QIDQ4938421zbMATH OpenFDO

Authors Enno Ohlebusch

Publication date 23 February 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48242-3_8

zbMATH Keywords

conditional term rewriting systemsfunctional logic programming

Mathematics Subject Classification ID

Logic programming (68N17) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Review text

This paper investigates properties of certain transformations on Conditional Term Rewriting Systems (CTRSs), having applications into the field of functional logic programming. As a first result (inspired by the approach of M. Marchiori -- 1996), the author shows how every deterministic CTRS \(R\) can be transformed into an unconditional TRS \(U(R)\), such that the termination of \(U(R)\) implies quasi-reductivity of \(R\). This result is interesting because standard methods for proving the termination of TRSs can be employed to infer quasi-reductivity automatically. The main theorem of the paper states that quasi-reductivity of the CTRS \(R\) implies the innermost termination of the corresponding unconditional TRS \(U(R)\). These results have (at least) two interesting applications : (1) Quasi-reductivity is modular for non-overlapping syntactically deterministic composable CTRSs. (2) The proposed two-stage transformation approach to proving termination of an LR-well-moded logic program can be automated, and provides certain advantages over the direct transformation. For the entire collection see [Zbl 0921.00037].

Recommendations

• Elimination of conditions
• Notes on structure-preserving transformations of conditional term rewrite systems
• Transformations of Conditional Rewrite Systems Revisited
• Transformation for refining unraveled conditional term rewriting systems
• scientific article; zbMATH DE number 4092755

Cited in

(9)

• Operational termination of conditional term rewriting systems
• Applications and extensions of context-sensitive rewriting
• scientific article; zbMATH DE number 1696594 (Why is no real title available?)
• Extra variables can be eliminated from functional logic programs
• Formalizing soundness and completeness of unravelings
• Complexity of conditional term rewriting
• Semi-inversion of conditional constructor term rewriting systems
• Notes on structure-preserving transformations of conditional term rewrite systems
• Characterizing and proving operational termination of deterministic conditional term rewriting systems

This page was built for publication: Transforming conditional rewrite systems with extra variables into unconditional systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4938421)