On the correspondence between two classes of reduction systems
We consider the relationship between two classes of term rewriting systems. In one class, there is a sharp distinction between data constructors and computable functions, which is absent, in the other. Both classes contain systems described by sets of left-linear rules without critical pairs in the sense of Knuth-Bendix. We show that although the class based on constructors appears to be a special case, it is in fact powerful enough to simulate the larger class, and thus certain problems such as sequentiality in the larger class can be reduced via simulation to the technically simpler environment of constructor systems.
- Constructor equivalent term rewriting systems
- Constructor equivalent term rewriting systems are strongly sequential: A direct proof
- scientific article; zbMATH DE number 4045104
- Efficient simulation of forward-branching systems with constructor systems
- Implementing first-order rewriting with constructor systems
- A Machine-Oriented Logic Based on the Resolution Principle
- Abstract Implementations and Their Correctness Proofs
- Computing in systems described by equations
- scientific article; zbMATH DE number 3664336 (Why is no real title available?)
- Implementation of an interpreter for abstract equations
- Initial Algebra Semantics and Continuous Algebras
- Tree-Manipulating Systems and Church-Rosser Theorems
- A refinement of strong sequentiality for term rewriting with constructors
- Implementing first-order rewriting with constructor systems
- Reducible systems and embedding procedures in the canonical formalism
- Constructor equivalent term rewriting systems are strongly sequential: A direct proof
- Interaction systems II: The practice of optimal reductions
- Remarks on Thatte's transformation of term rewriting systems
- Inductive proofs by specification transformations
- Transforming strongly sequential rewrite systems with constructors for efficient parallel execution
- Transformations and confluence for rewrite systems
- Constructor equivalent term rewriting systems
This page was built for publication: On the correspondence between two classes of reduction systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1059392)
