Relating confluence, innermost-confluence and outermost-confluence properties of term rewriting system (Q1901710)

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.