
In the last few decades, term rewriting systems have played a fundamental role in the analysis and implementation of abstract data type specifications, decidability of word problems, theorem proving, computability theory, design of functional programming languages (e.g. Miranda), integration of functional programming and logic programming paradigms, termination of logic programs, etc. Termination and confluence are two fundamental properties of term rewriting systems. In this paper, we study confluence properties. To be precise, we obtain a number of results relating different notions of confluence. A rewrite step \(C[l \sigma] \Rightarrow C[r \sigma]\) with rewrite rule \(l \to r\) is an innermost reduction step if no proper subterm of \(l \sigma\) is reducible. A term rewriting system is innermost-confluent if its innermost rewrite relation is confluent. The study of innermost confluence is interesting since denotational semantics is often defined by a kind of innermost evaluation procedure, which is similar to innermost rewriting. A reduction step \(C[l \sigma] \Rightarrow C[r \sigma]\) with rewrite rule \(l \to r\) is an outermost reduction step if no position above \(l \sigma\) is a redex position, i.e., there is no subterm \(s\) of \(C[l\sigma]\) and no rule \(l' \to r'\) such that (i) \(l \sigma\) is a proper subterm of \(s\) and (ii) \(s\) is an instance of \(l'\). A term rewriting system \({\mathcal R}({\mathcal F}, R)\) is outermost-confluent if its outermost rewrite relation is confluent. Outermost-confluence is interesting because outermost reduction corresponds to lazy evaluation. If a system is outermost-confluent, that means that the lazy semantics is well-defined, regardless of the order in which outermost reductions are done and regardless of which rules are applied. Also, nonterminating outermost-confluent systems are those for which a semantics based on infinite terms seems most natural, since lazy evaluation for nonterminating programs can lead to infinite structures. It is easy to observe that confluence of terminating systems implies innermost-confluence and outermost-confluence as every innermost/outermost derivation terminates. However, a terminating system can be innermost or outermost-confluent without being confluent. A nonterminating system can be confluent but not innermost (outermost) confluent and vice versa. The following results are established in the paper. 1. A weakly innermost normalizing overlay system is innermost-confluent if and only if it is confluent. 2. A weakly innermost normalizing system is innermost-confluent if it is confluent. But the converse is not true. 3. strongly innermost normalizing system is innermost-confluent if \(s\theta\) and \(t \theta\) are joinable by innermost rewriting for every overlay critical pair \(\langle s, t \rangle\) and a substitution \(\theta\) which replaces variables by irreducible terms. 4. Let \(R\) be a weakly outermost normalizing left-linear overlay system with the property: if the right-hand side \(r_1\) of a rule unifies with a non-variable proper subterm of the left-hand side \(l_2\) of a rule then \(l_2\) does not unify with the left-hand side of any other rule in \(R\). Then \(R\) is confluent if and only if it is outermost-confluent. 5. A weakly outermost normalizing system is outermost-confluent if it is confluent. But the converse is not true. 6. Every weakly normalizing almost orthogonal system is outermost-confluent. A strongly outermost normalizing left-linear overlay system is confluent if and only if it is outermost-confluent.
confluence, Grammars and rewriting systems, Semantics in the theory of computing, lazy evaluation, term rewriting systems, denotational semantics
confluence, Grammars and rewriting systems, Semantics in the theory of computing, lazy evaluation, term rewriting systems, denotational semantics
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
