Sequentiality in orthogonal term rewriting systems
Term rewriting systems can be used for computing with equations. A term rewriting system is called orthogonal if it is (1) left-linear (no variable appears more than once in a left hand side of a rule) and (2) non-overlapping (no left-hand side of a rule is unifyable with a non- variable subterm of a left-hand side of a rule). This property is very useful since it guaranties confluence: no term can be rewritten to two different normal forms. But, there may be a term which can be rewritten to a normal form and at the same time it is the starting point of an infinite rewriting sequence. So it is of great importance to develop a rewriting strategy that avoids infinite computations whenever possible. Huet and Lévy have defined a subclass of orthogonal term rewriting systems, called strongly sequential rewriting systems, that allow for such a strategy: For any term \(t\) one can compute a `needed redex', that is a subterm \(t_ 0\) of \(t\) that has to be rewritten in any rewriting sequence starting with \(t\) and ending in the normal form of \(t\). Now, the rewriting strategy is just to rewrite in each step a needed redex. Huet and Lévy have proved that it is decidable whether an orthogonal rewriting system is strongly sequential, but their proof is highly complex and in essence it is a correctness proof of some algorithm. The aim of the paper is to analyse the notation of a strongly sequential term rewriting system and so to arrive at a conceptually much simpler proof of the decidability result. The resulting decision algorithm is of high computational complexity, so a second algorithm is given that has a computational complexity comparable to the algorithm of Huet and Lévy. It is also proved that strong sequentiality in a modular property, i.e. the disjoint union of two strongly sequential term rewriting systems is again strongly sequential.
- Semantics and strong sequentiality of priority term rewriting systems
- Strongly sequential and inductively sequential term rewriting systems
- Semantics and strong sequentially of priority term rewriting systems
- Formalizing the confluence of orthogonal rewriting systems
- Completeness and confluence of order-sorted term rewriting
- A formalization of sequential, parallel, and continuous rewriting
- Sequentiality in an extensional framework
- scientific article; zbMATH DE number 176122
- Bounded, strongly sequential and forward-branching term rewriting systems
- Transfinite reductions in orthogonal term rewriting systems
- A refinement of strong sequentiality for term rewriting with constructors
- Computing in systems described by equations
- Conditional rewrite rules: Confluence and termination
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- scientific article; zbMATH DE number 3988695 (Why is no real title available?)
- scientific article; zbMATH DE number 4037164 (Why is no real title available?)
- scientific article; zbMATH DE number 4074466 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- Implementation of an interpreter for abstract equations
- Minimal and Optimal Computations of Recursive Programs
- Modular properties of conditional term rewriting systems
- Needed reduction and spine strategies for the lambda calculus
- On the Church-Rosser property for the direct sum of term rewriting systems
- Sequential evaluation strategies for parallel-or and related reduction systems
- Strong and NV-sequentiality of constructor systems
- A hybrid programming scheme combining fuzzy-logic and functional-logic resources
- A refinement of strong sequentiality for term rewriting with constructors
- Semantics and strong sequentiality of priority term rewriting systems
- Constructor equivalent term rewriting systems are strongly sequential: A direct proof
- Decidable call-by-need computations in term rewriting
- Sequential evaluation strategies for parallel-or and related reduction systems
- Normalization, approximation, and semantics for combinator systems
- Sequentiality, monadic second-order logic and tree automata.
- Context-sensitive rewriting strategies
- Rules + strategies for transforming lazy functional logic programs
- On term-graph rewrite strategies
- Strongly sequential and inductively sequential term rewriting systems
- Root-neededness and approximations of neededness
- A Needed Rewriting Strategy for Data-Structures with Pointers
- NV-Sequentiality: A Decidable Condition for Call-by-Need Computations in Term-Rewriting Systems
- scientific article; zbMATH DE number 1761894 (Why is no real title available?)
- The geometry of orthogonal reduction spaces
- scientific article; zbMATH DE number 2090086 (Why is no real title available?)
- Optimal solutions to pattern matching problems
- Optimal normalization in orthogonal term rewriting systems
- Decidable approximations of term rewriting systems
- Semantics and strong sequentially of priority term rewriting systems
- Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic Programs
- Decidable call by need computations in term rewriting (extended abstract)
- Lazy productivity via termination
- A sequential reduction strategy
- Constructor equivalent term rewriting systems
This page was built for publication: Sequentiality in orthogonal term rewriting systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1186735)
