# Confluent reductions: abstract properties and applications to term rewriting systems

Gérard Huet

<figure><img src="image_1.png" /></figure>

## To cite this version:

Gérard Huet. Confluent reductions: abstract properties and applications to term rewriting systems. [Research Report] IRIA-RR-250, IRIA. 1977, pp.17. hal-04716458

HAL Id: hal-04716458

https://inria.hal.science/hal-04716458v1

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
IRIA

laboria

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20

laboratoire de recherche
en informatique
et automatique

<figure><img src="image_3.png" /></figure>

CONFLUENT REDUCTIONS:
ABSTRACT PROPERTIES
AND APPLICATIONS TO
TERM REWRITING SYSTEMS

Gérard HUET

Rapport de Recherche N° 250

Août 1977
CONFLUENT REDUCTIONS:
ABSTRACT PROPERTIES AND APPLICATIONS
TO TERM REWRITING SYSTEMS

Gérard HUET

IRIA / LABORIA

<figure><img src="image_4.png" /></figure>

Résumé :

Cet article présente des résultats concernant les propriétés Church-Rosser de systèmes de réécriture.

La première partie donne des résultats abstraits de confluence, qui ne dépendent que de propriétés axiomatiques d'une relation appelée réduction. Des résultats de divers auteurs, en particulier Newman, sont présentés dans un formalisme commun. Un puissant principe de récurrence est introduit, qui permet de généraliser des résultats de Sethi sur la réduction modulo une relation d'équivalence.

La deuxième partie concerne les systèmes de simplification de termes de premier ordre. Des théorèmes de Rosen et Knuth et Bendix sont étendus, ce qui donne plusieurs nouveaux critères de confluence, en utilisant les résultats de la première partie. On montre alors comment ces résultats peuvent être appliqués à des méthodes de semi-décision efficaces pour les théories équationnelles.

Abstract:

This paper gives new results, and presents old ones in a unified formalism, concerning Church-Rosser theorems for rewriting systems.

Part 1 gives abstract confluence properties, depending solely on axioms for a binary relation called reduction. Results of Newman and others are presented in a unified formalism. Systematic use of a powerful induction principle permits to generalize results of Sethi on reduction modulo equivalence.

Part 2 concerns simplification systems operating on terms of a first-order logic. Results by Rosen and Knuth and Bendix are extended to give several new criteria for confluence of these systems, using the results of part 1. It is then shown how these results yield efficient methods for the mechanization of equational theories.
# I. ABSTRACT REDUCTION PROPERTIES

## I - Generalities

Let $\mathcal{E}$ be an arbitrary set. We shall give in this section some more or less well-known properties of a binary relation $\to$ on $\mathcal{E}$, which we shall call *reduction*. These properties are abstract, in the sense that they depend solely on axioms for the reduction relation.

## Notations

i is the identity relation on $\mathcal{E}$ : $i = \{\langle x, x \rangle \mid x \in \mathcal{E} \}$.

· is relation composition :

$$ \to_1 \cdot \to_2 = \{ \langle x, y \mid \exists z \ x \to_1 z \ \& \ z \to_2 y \} $$

$$ \to^{-1} \text{ is the inverse of relation } \to : \to^{-1} = \{ \langle x, y \mid y \to x \} $$

For any relation $\to$ on $\mathcal{E}$, we now define :

$$ \underline{0} = i $$

$$ \mathcal{E} = \to \cup \mathcal{U} \text{ reflexive closure of } \to $$

$$ i \stackrel{\cdot}{=} \to \cdot \to^{i-1} \forall i > 0 \text{ i-iteration of } \to $$

$$ \dot{\to} = \cup \stackrel{i}{\underset{i>0}{\vee}} \text{ transitive closure of } \to $$

$$ \dot{\to}^* = \dot{\to} \cup \mathcal{U} \text{ transitive-reflexive closure of } \to $$

$$ \dot{\to}^* \leftrightarrow (\to \cup \to^{-1})^* \text{ equivalence closure of } \to. $$

If $x$ is maximal with respect to $\to$, i.e. $\exists y \ x \to y$, we say that $x$ is a normal form, and we let $\eta$ be the set of all such elements. For $x \in \mathcal{E}$, if there exists $y \in \eta$ such that $x \stackrel{*}{\to} y$, we say that $y$ is a normal form of $x$.

For a given relation $\to$, we let :

$$ x \to y \Leftrightarrow \exists z \ x \stackrel{*}{\to} z \ \& \ y \stackrel{*}{\to} z $$

$$ x \to y \Leftrightarrow \exists z \ z \stackrel{*}{\to} x \ \& \ z \stackrel{*}{\to} y $$

$$ \Delta(x) = \max\{i \mid \exists y \ x \stackrel{\underline{i}}{\to} y\} \in \mathbb{N} \cup \{\infty\} $$

$$ \Delta(x) = \{y \mid x \to y\} $$

$$ \Delta^+(x) = \{y \mid x \stackrel{\cdot}{\to} y\}, \Delta^*(x) = \Delta^+(x) \cup \{x\} $$

## Definitions

$\mathcal{D} \to$ is inductive iff for every sequence $x_1 \to x_2 \to \dots \to x_n \to \dots$ there exists $y$ such that $\forall i \ge 1$ $x_i \stackrel{*}{\to} y$.
D2 + is acyclic iff $\vdash$ is irreflexive (and then $\vdash$ is a partial ordering relation).

D3 + is noetherian iff there is no infinite sequence $x_1 \to x_2 \to \dots \to x_n \to \dots$ (then $\vdash$ is well founded).

D4 + is bounded iff $\forall x \Lambda(x) < \infty$ (the finiteness property in [1,15]).

Every bounded relation is noetherian, and every noetherian relation is inductive and acyclic.

Let P be any predicate on $\mathcal{E}$. We say that P is $\rightarrow$-complete iff $\forall x \in \mathcal{E} [\forall y \in \Delta^+(x) P(y)] \Rightarrow P(x)$.

Our interest in noetherian relations stems from the following:

### Principle of noetherian induction

Let $\rightarrow$ be a noetherian relation. Any $\rightarrow$-complete predicate P is universal: $\forall x \in \mathcal{E} P(x)$.

This principle is as powerful as the usual forms of ordinal induction. It presents the advantage of not requiring the construction of the well ordering associated with the partial ordering $\vdash$.

### Definitions

D5 + is locally finite iff $\forall x \in \mathcal{E} \Delta(x)$ is finite.

Let $\rightarrow$ be a locally finite relation. For every $x$ in $\mathcal{E}$, if $\Lambda(x) = \infty$ there exists an infinite sequence $x = x_1 \to x_2 \to \dots \to x_n \to \dots$

Therefore a locally finite relation is bounded iff it is noetherian.

D6 + is globally finite iff $\forall x \in \mathcal{E} \Delta^*(x)$ is finite.

Let $\rightarrow$ be a locally finite relation. For every $x$ in $\mathcal{E}$, if $\Delta^*(x)$ is infinite there exists an infinite sequence $x = x_1 \to x_2 \to \dots \to x_n \to \dots$

Therefore a noetherian locally finite relation is globally finite. Conversely, any acyclic globally finite relation is bounded. Combining all this, we get:

### Koenig's lemma

Let $\rightarrow$ be an acyclic locally finite relation. Then $\rightarrow$ is noetherian iff it is bounded iff it is globally finite. Finally, note that acyclic and noetherian does not imply bounded, as shown by:

<figure><img src="image_5.png" /></figure>

Also, acyclic, inductive and locally finite implies neither noetherian nor globally finite, as shown by the dual example:

<figure><img src="image_6.png" /></figure>

## 2 - Confluence properties

Suppose we are interested in the equivalence $\rightarrow \stackrel{*}{\leftrightarrow}$ generated by a relation $\rightarrow$. We are going to give conditions on $\rightarrow$ that permit to recognize if $x \stackrel{*}{\leftrightarrow} y$, when performing only reductions ($\rightarrow^*$) from x and y.

### Definition

D7 + is confluent iff $\forall x y x \rightarrow y \Rightarrow x \rightarrow y$

We express this property with the diagram:

<figure><img src="image_7.png" /></figure>

The results that follow appear in Newman [8]. They have been rediscovered by several authors in various contexts, where $\rightarrow$ is interpreted as the $\beta$-reduction relation in $\lambda$-calculus, the deduction relation in a formal system, or the operational semantics in a programming language.

**Lemma 1** If $\rightarrow$ is confluent, then the following "Church Rosser" property holds: $\forall x y x \stackrel{*}{\leftrightarrow} y \Rightarrow x + y$.

**Lemma 2** If $\rightarrow$ is confluent, then the normal form of any element, if it exists, is unique.

The converse of this lemma is true, when $\rightarrow$ is such that every element possesses a normal form. This will be the case, for instance, with acyclic inductive relations (using Zorn's lemma).

The two preceding lemmas show the interest of confluent relations. The rest of this section is devoted to finding sufficient conditions for a relation to be confluent. First, it is easy to partially localize the test for confluence:

**Lemma 3** + is confluent iff $\forall x y z x \rightarrow y \& x \stackrel{*}{\leftrightarrow} z \Rightarrow y \rightarrow z$.

In the case of noetherian relations, it is possible to localize completely the confluence test.
### Definition

$D8 \to$ is locally confluent iff

<figure><img src="image_8.png" /></figure>

### Lemma 4

A noetherian relation is confluent iff it is locally confluent.

This lemma appears in the literature in various places, in weaker forms: either the relation is required to be bounded (easy induction on $\Lambda(x)) [1,15]$), or it is assumed to be locally finite [7], or it is proved for a specific noetherian relation [6] (ad hoc induction). Several weaker forms are given in [16]. It appears in its full generality in [8], but with an unnecessarily complex proof. Let us show how noetherian induction permits an easy and natural proof.

### Proof of lemma 4

The only if part is trivial. For the if part, assume $\to$ is a noetherian locally confluent relation. We prove $P(x) : \forall y z \ x \stackrel{*}{\to} y \ \& \ x \stackrel{\to}{\to} z \Rightarrow y \to z$ be noetherian induction, showing that $P$ is $\to$ complete.

Let $x \stackrel{\text{in}}{\to} y$ and $x \stackrel{\text{out}}{\to} z$. We show $\exists t \ y \stackrel{*}{\to} t$ and $z \stackrel{*}{\to} t$.

* if $m = 0$ we choose $t = z$, if $n = 0$ we choose $t = y$.

* otherwise, let $x \to y_1 \stackrel{*}{\to} y$ and $x \to z_1 \stackrel{*}{\to} z$.

By local confluence, $\exists u \ y_1 \stackrel{*}{\to} u$ and $z_1 \stackrel{*}{\to} u$. By induction hypothesis on $y_1$, $\exists v \ y \stackrel{*}{\to} v$ and $u \stackrel{*}{\to} v$. By induction hypothesis on $z_1$, $\exists w \ u \stackrel{*}{\to} w$ and $z \stackrel{*}{\to} w$. Finally, by induction hypothesis on $u$, $\exists t \ v \stackrel{*}{\to} t$ and $w \stackrel{*}{\to} t$, proving $P(x)$.

The induction step of the proof is shown in the diagram of Fig. 1. □

<figure><img src="image_9.png" /><figcaption>Fig. 1</figcaption></figure>

Lemma 4 fails, if we suppose only $\to$ to be inductive and acyclic, as shown by the counter example in Fig. 2, due to Newman.

<figure><img src="image_10.png" /><figcaption>Fig. 2</figcaption></figure>

For the relations that are not noetherian, much stronger local hypotheses are necessary to yield confluence.

### Definition

$D9 \to$ is strongly confluent iff

$$ \forall x y z \ x \to y \ \& \ x \to z \Rightarrow \exists u \ y \stackrel{*}{\to} u \ \& \ z \stackrel{\xi}{\to} u. $$

**Remark 1** : Beware of the symmetry between $y$ and $z$ in the definition above. It is only slightly weaker than to require $y \stackrel{\xi}{\to} u \ \& \ z \stackrel{\xi}{\to} u$. For instance, $\to$ in Fig. 2 is not strongly confluent.

### Lemma 5

Any strongly confluent relation is confluent.

**Proof** It is easy to show, by induction on $n$, that if $\to$ is strongly confluent then $\forall x y z \ x \stackrel{\xi}{\to} y \ \& \ x \stackrel{n}{\to} z \Rightarrow \exists u \ y \stackrel{*}{\to} u \ \& \ z \stackrel{\xi}{\to} u$. The result follows then from lemma 3. □

It may seem that the conditions in definition D9 are too restrictive to be of practical use. However, lemma 5 is the basis of a common method to prove Church Rosser results in Combinatory Logic : one usually constructs, from the reduction relation $\to$, a strongly confluent relation $\rightsquigarrow$ with same transitive closure as $\to$ : $\to = \rightsquigarrow$. Actually, a weaker condition is sufficient : it is enough to show that $\to \to$ is a compatible refinement of $\to$, in the sense of Staples [16].

Various other axiomatic conditions imply confluence, for instance using decompositions of $\to$ as the union of two or more relations. See in particular [8, 14, 16]. For instance, lemma 5 is a consequence of the commutativity lemma in Rosen [14].

### 3 - Reduction modulo equivalence

Our motivation in studying reduction relations stems from practical problems arising in formula manipulation systems such as theorem provers, program optimizers, algebraic simplifiers. The problem is to define some efficient operational semantics for an equational theory. This theory is usually defined by axioms of two forms : "structural" axioms such as associativity and
commutativity of operators, and "simplification rules"
such as "if true then x else y → x". While the latter
usually define a noetherian relation on the terms of
the language, the former can often be taken into account
by a specific data structure used to represent these
terms.

We shall now model this situation by considering a
reduction relation +, to which we adjoin an equivalence
relation ~, in the same manner as Sethi [15].

Definition
---

D10 + is confluent modulo ~ iff

$$
\forall x y x' y' \ x \sim y \ & x \underset{x'}{\oplus} \ x' \ & y \underset{y'}{\oplus} \ y' \Rightarrow \exists \bar{x} \ \bar{y} \ \ x' \underset{\bar{x}}{\oplus} \ \bar{x} \ & \\
\phantom{\forall x y x' y' \ } \ y' \underset{\bar{y}}{\oplus} \ \bar{y} \ & \bar{x} \sim \bar{y}
$$

Remark that this condition is different from +/~ being
confluent in E /~, since we do not allow ~ along the +
- derivations. If + has the property of defining a nor-
mal form for every element, we get a weak form of lem-
ma 2 :

Lemma 6

Let $\to$ normalize $\mathcal{E}$, i.e. $\forall x \in \mathcal{E} \ \exists y \in \mathcal{N} \ x \stackrel{*}{\to} y$. Then $\to$ is confluent modulo $\sim$ iff

$$
\forall x y \in \mathcal{E} \ \forall u v \in \mathcal{N} \ x \equiv y \ & x \underset{x}{\overset{u}{\oplus}} \ u \ & y \underset{v}{\overset{u}{\oplus}} \ u \sim v, \\
\text{where } \equiv \text{ is } (\to \cup \underset{u}{\to} \underset{v}{\to})^*.
$$

We leave the proof of this result to the reader.
We are now going to search for sufficient conditions
for → to be confluent modulo ~. The first step is to
generalize lemma 4, assuming → noetherian. The lemma
below generalizes th. 2.2 of Sethi [15], who requires+
to be bounded. This generalization will be useful prac-
tically since one frequently proves termination results
using lexicographic orderings on terms that are noethe-
rian but not bounded [6]. But the main interest lies
here in the technique of proof, based on noetherian
induction.

Definition
---

D11 → is locally confluent modulo ~ iff conditions α
and β below are satisfied.

$$
\alpha : \forall x y z \quad x \to y \ & x \to z \Rightarrow y \to z
$$

$$
\beta : \forall x y z \quad x \sim y \ & x \to z \Rightarrow y \to z
$$

where $y \overset{\sim}{\to} z \Leftrightarrow \exists u \ v \quad y \underset{u}{\overset{\sim}{\to}} u \ \& \ z \underset{v}{\overset{\sim}{\to}} v$.

<figure><img src="image_11.png" /></figure>

We can now state the generalization of lemma 4.

<figure><img src="image_12.png" /></figure>

Lemma 7

Let → be a noetherian relation. For any equivalence ~,
→ is confluent modulo ~ iff → is locally confluent
modulo ~.

Before giving the proof of this lemma, let us state
a preliminary proposition.

Definition
---

Let $\to$ be any relation on $\mathcal{E}$. We define a relation $\to \in \mathcal{E} \ x \mathcal{E}$ by :

$$
<x, y> \Leftrightarrow <x', y'> \text{ iff :}
$$

- either $x \to x'$ and $(x \to y'$ or $y = y$') \quad (a)$

- or $y \to y'$ and $(x = x'$ or $y \to x$') \quad (b)$

**Proposition 1** if → is noetherian, then → is a noetherian relation in E x E.

Proof
---

Let <xᵢ, yᵢ>, i ≥ 0, be an infinite sequence in E x E,
with <xᵢ, yᵢ> = <xᵢ₊₁, yᵢ₊₁>. There are three cases :

- if from rank k we use only rules of type (a), we get
an infinite sequence x_k → x_{k+1} → x_{k+2} → ...

- if from rank k we use only rules of type (b) : symmetric case.

- we alternate indefinitely between rules (a) and rules (b) :

$$
<x_0, y_0> \underset{(a)}{\stackrel{+}{\rightarrow}} <x_1, y_1> \underset{(b)}{\stackrel{+}{\rightarrow}} <x_2, y_2> \underset{(a)}{\stackrel{+}{\rightarrow}} <x_3, y_3> \dots
$$

In this case we get an infinite sequence :

$$
y_i \underset{i}{\overset{\oplus}{\to}} x_j \underset{j}{\overset{\oplus}{\to}} y_{i+1} \underset{i+1}{\overset{\oplus}{\to}} x_{j+1} \underset{j+1}{\overset{\oplus}{\to}} \dots \text{ which concludes the proof. } \square
$$

Proof of lemma 7

Let → be a noetherian relation locally confluent modu-
lo ~. We shall use noetherian induction in E x E,
applied to → and to property :

$$
P(x,y) : x \sim y \Rightarrow [\forall x', y' \ x \underset{x}{\overset{\sim}{\to}} x' \ \& \ y \underset{y}{\overset{\sim}{\to}} y']
$$
Let us show that P is $\rightarrow$-complete. For that, let $x, y, x', y' \in \mathcal{E}$ such that $x \sim y, x \leq x', y \geq y'$. We show $\exists \bar{x}, \bar{y} : x' \stackrel{*}{=} \bar{x}, y' \stackrel{*}{=} \bar{y}, \bar{x} \sim \bar{y}$.

* if $n = 0$ and $m = 0$, it is trivial.

* otherwise, let us assume without loss of generality that $n > 0$, and let $x \to x_1$. By applying property $\beta$ to $x, y, x_1$, we get $u$ and $v$ such that $x_1 \stackrel{*}{=} u, y \stackrel{*}{=} v, u \sim v$. There are two cases:

a) $m = 0$. Let $\bar{x}', \bar{u}$ and $\bar{v}$ be $\sim$-normal forms of respectively $x'$, $u$ and $v$.

We get $\bar{x}' \sim \bar{u}$ by induction hypothesis $P(x_1,x_1)$ and $\bar{u} \sim \bar{v}$ by induction hypothesis $P(u,v)$, completing the proof of case a); the diagram is shown in fig. 3a.

b) $m > 0$. Let $y \to y_1$. Again there are two cases:

- b1) $v = y$. We apply again property $\beta$ to $y, u, y_1$, getting $w$ and $z$ such that $u \stackrel{*}{=} w, y_1 \stackrel{*}{=} z, w \sim z$. Let $\bar{x}', \bar{u}, \bar{v}, \bar{w}, \bar{z}$ and $\bar{y}'$ be $\sim$-normal forms of respectively $x', w, z$ and $y'$. We get $\bar{x}' \sim \bar{w}$ by hypothesis $P(x_1,x_1)$, $\bar{w} \sim \bar{z}$ by $P(w,z)$ and $\bar{z} \sim \bar{y}'$ by $P(y_1,y_1)$, completing the proof of this case; the diagram is shown in fig. 3b1.

- b2) otherwise, let $y \to t$. We now apply property $\alpha$ to $y, y_1, t$, getting $w$ and $z$ such that $t \stackrel{*}{=} w, y_1 \stackrel{*}{=} z, w \sim z$. Let $\bar{x}', \bar{u}, \bar{v}, \bar{w}, \bar{z}$ and $\bar{y}'$ be normal forms respectively of $x', u, v, w, z$ and $y'$. We get successively $\bar{x}' \sim \bar{u}$ by induction hypothesis $P(x_1,x_1)$, $\bar{u} \sim \bar{v}$ by $P(u,v)$, $\bar{v} \sim \bar{w}$ by $P(t,t)$, $\bar{w} \sim \bar{z}$ by $P(w,z)$, and finally $\bar{z} \sim \bar{y}'$ by $P(y_1,y_1)$ completing the proof of the lemma; the diagram of this last case is shown in fig. 3b2.

We leave it to the reader to check that we used hypothesis $P(\lambda, \mu)$ only when $\langle x, y \rangle \stackrel{\sim}{\rightleftharpoons} \langle \lambda, \mu \rangle$. Actually, the definition of $\stackrel{\sim}{\rightleftharpoons}$ was inspired directly from the diagrams we wished to close, which makes this method a very natural one to use for this sort of proof. $\square$

<figure><img src="image_13.png" /></figure>

(a)

<figure><img src="image_14.png" /></figure>

(b1)

<figure><img src="image_15.png" /></figure>

(b2)

<caption>Fig. 3</caption>

Next, we localize further property $\beta$, when considering $\sim$ as generated by a symmetric relation $\stackrel{\sim}{\rightleftharpoons}$, i.e. $\sim = \stackrel{\sim}{\rightleftharpoons}$.

**Definition** Property $\gamma$:

$V \times y \times z \quad x \stackrel{\sim}{\rightleftharpoons} y \ \& \ x \to z \Rightarrow y \stackrel{\sim}{\rightleftharpoons} z$, with $\sim = \stackrel{\sim}{\rightleftharpoons}$.

<figure><img src="image_16.png" /></figure>

**Definitions**

If $x \sim y$, we define $\rho(x,y)$ as the smallest $k$ such that $x \stackrel{k}{\rightleftharpoons} y$. Similarly to above, we define a relation $\sim$ in $\mathcal{E} \times \mathcal{E}$ by:

$\langle x, y \rangle \stackrel{\sim}{\rightleftharpoons} \langle x', y' \rangle \text{ iff:}$

* either $\langle x, y \rangle \stackrel{\sim}{\rightleftharpoons} \langle x', y' \rangle$ with same definition as above,

* or $x \sim y \sim x' \sim y'$ and $\rho(x,y) > \rho(x',y')$.
**Proposition 2**

if $\to$.~ is noetherian (or, equivalently, if $\to$.~ is noetherian in $\mathcal{E}/\sim$), then $\to$ is a noetherian relation in $\mathcal{E} \times \mathcal{E}$. The proof follows that of proposition 1, but in the quotient set $\mathcal{E}/\sim$. Note that we need a stronger condition than for proposition 1.

**Lemma 8**

Let $\mathcal{I}$ be a symmetric relation, and let $\sim = \mathcal{I}^*$ . Let $\to$ be any relation such that $\to$.~ is noetherian. Then $\to$ is confluent modulo $\sim$ iff properties $\alpha$ and $\gamma$ are verified.

**Proof**

The only if part is obvious. For the if part, let us assume that $\to$.~ is noetherian, and that properties $\alpha$ and $\gamma$ hold. We shall again use noetherian induction in $\mathcal{E} \times \mathcal{E}$, applied to $\mathcal{I} \to$ and the same property $P$ as in the proof of lemma 7.

Let $x, y, x', y' \in \mathcal{E}$ such that $x \sim y, x \underset{\sim}{\overset{\sim}{\vdash}} x', y \underset{\sim}{\overset{\sim}{\vdash}} y'$. We show the existence of $\bar{x}$ and $\bar{y}$ such that $x' \underset{\sim}{\overset{\sim}{\vdash}} \bar{x}, y' \underset{\sim}{\overset{\sim}{\vdash}} \bar{y}$ and $\bar{x} \sim \bar{y}$.

There are two cases :

a) $x = y$

. if $n = 0$ or $m = 0$ it is trivial.

. otherwise, let $x \to u \underset{\sim}{\overset{\sim}{\vdash}} x'$ and $y \to v \underset{\sim}{\overset{\sim}{\vdash}} y'$.

Applying property $\alpha$ to $x, u, v$, we get the existence of $w$ and $z$ such that $u \underset{\sim}{\overset{\sim}{\vdash}} w, v \underset{\sim}{\overset{\sim}{\vdash}} z, w \sim z$. Let $\bar{x}', \bar{w}, \bar{z}$ and $\bar{y}'$ be $\to$-normal forms of respectively $x', w, z$ and $y'$. We get $\bar{x}' \sim \bar{w}$ by induction hypothesis $P(u,u)$, $\bar{w} \sim \bar{z}$ by hypothesis $P(w,z)$, and $\bar{z} \sim \bar{y}'$ by hypothesis $P(v,v)$, completing the proof of a) according to the diagram in Fig. 4a.

b) $\rho(x,y) > 0$.

. if $n = 0$ and $m = 0$ it is trivial

. otherwise, let us assume without loss of generality that $n > 0$, and let $x \to u \underset{\sim}{\overset{\sim}{\vdash}} x'$. Let us choose $v$ such that

$x \mathcal{I} v \sim y$, with $\rho(v,y) = \rho(x,y)-1$. Applying property $\gamma$ to $x, v, u$, we get $w$ and $z$ such that $u \underset{\sim}{\overset{\sim}{\vdash}} w, v \underset{\sim}{\overset{\sim}{\vdash}} z$ and $w \sim z$. We complete the proof as in a), applying induction hypotheses $P(u,u)$, $P(w,z)$ and $P(v,y)$. Note that we always have $\langle x,y \rangle \mathcal{I}^+ \to \langle w,z \rangle$. This concludes the proof, according to the diagram in Fig. 4b. $\square$

<figure><img src="image_17.png" /></figure>

(a)

<figure><img src="image_18.png" /></figure>

(b)

<caption>Fig. 4</caption>

**Remarks** Sethi's th. 2.3 [15] is similar to lemma 8, in the special case $\mathcal{I} = \sim_1 u \sim_2$, where $\sim_1$ and $\sim_2$ are two equivalence relations. But his conditions are significantly more restrictive : he demands that $\to$ is not bounded, because he constructs explicitly the ordinal of the induction.

Nivat shows in [9] an equivalent of lemma 8, for a reduction relation defined by word rewrites in a free monoid.

Remark the symmetry between properties $\alpha$ and $\gamma$. Both express localizing the confluence check to one application of the generators of respectively $\underset{\sim}{\overset{\sim}{\vdash}}$ and $\sim$.

The rather strong condition that $\to$.~ is noetherian is essential. For instance, Fig. 5 gives an example (inspired from the one in Fig. 2) where $\to$ is noetherian and $\alpha$ and $\gamma$ are verified. Still, $\to$ is not confluent modulo $\sim$. This corresponds to the infinite $\mathcal{I} \to$-sequence of pairs $\langle y, x_1 \rangle$.

<figure><img src="image_19.png" /><figcaption>Fig. 5</figcaption></figure>
## II. APPLICATIONS TO TERM REWRITING SYSTEMS

### I - The lattice $\mathcal{T}$ of first-order terms

We briefly survey properties of the set $\mathcal{C}$ of terms of a first order language, ordered by substitution. Full proofs may be found in [5], and related results in [10], [12] and [13].

Let $v$ be a denumerable set of elements called variables, and noted $x, y, z, ...$ Let $\mathcal{F}$ be a finite or denumerable set, with $\mathcal{F} \cap v = \emptyset$, graded by an *arity* function $\alpha : \mathcal{F} \to \mathbb{N}$. Elements in $\mathcal{F}$ are called *function symbols*, and noted $F, G, H, ...$. We define :

Let $\Sigma = v \cup \mathcal{F}$, $\Sigma^* = \text{the free monoid on } \Sigma$. We define the set $\mathcal{C}$ of terms as the smallest subset of $\Sigma^*$ containing $v$ and closed by operators : $t_1, ..., t_n \in \mathcal{C} \to F t_1 ... t_n \in \mathcal{C}$ for every $F \in \mathcal{F}_n$, $n \ge 0$.

$\mathcal{C}$ is thus isomorphic to the free $\alpha$-graded algebra. For $t \in \mathcal{C}$, we define :

- $v(t) \subset v$: the set of variables of t by :

$$ \begin{cases} v(x) = \{x\} & \forall x \in v \\ v(F t_1 \dots t_n) = \bigcup_{i=1}^{n} v(t_i) & \forall F \in \mathcal{F}_n \end{cases} $$

- $v(t) = |v(t)| \in \mathbb{N}$. If $v(t) = 0$ we say term t is ground.

- $\lambda(t) \ge 1$: the length of t :

$$ \begin{cases} \lambda(x) = 1 & \forall x \in v \\ \lambda(F t_1 \dots t_n) = 1 + \sum_{i=1}^{n} \lambda(t_i) & \forall F \in \mathcal{F}_n \end{cases} $$

- $\theta(t) \ge 0$: the size of t :

$$ \begin{cases} \theta(x) = 0 & \forall x \in v \\ \theta(F t_1 \dots t_n) = 1 + \sum_{i=1}^{n} \theta(t_i) & \forall F \in \mathcal{F}_n \end{cases} $$

- $\mu(t) = \lambda(t) - v(t)$. It is easy to show $\mu(t) \ge \theta(t)$, which shows $\mu(t) \ge 0$, and $\mu(t) = 0 \Leftrightarrow t \in v$.

If $\mu(t) = \theta(t)$, we say that $t$ is *free*; this means that all variable occurrences in $t$ are distinct.

Let $N_+^*$ be the set of sequences of positive integers, $\in$ the empty sequence in $N_+^*$, the concatenation of sequences. We shall call the members of $N_+^*$ *occurrences*, and denote them $u, v, w$. We define the *prefix order* $\prec$ in $N_+^*$ by : $u \prec v \Leftrightarrow \exists w \ v = u, w$; in this case we define: $v/u = w$. Occurrences $u$ and $v$ are said to be *disjoint*, and we note $u|v$, iff $\exists u \prec v$ and $\forall v \prec u$.

For any $t \in \mathcal{C}$, we define its *set of occurrences* as the finite set $\mathcal{O}(t) \subset N_+^*$, and for any $u \in \mathcal{O}(t)$, the *subterm of t at u*, $t/u \in \mathcal{C}$, as follows.

- if $t = x \in v$ then $\mathcal{O}(t) = \{\epsilon\}$, $t/\epsilon = t$.

- if $t = F t_1 \dots t_n$ then $\mathcal{O}(t) = \{\epsilon\} \cup \{iu \mid i \in n, u \in \mathcal{O}(t_i)\}$, $t/\epsilon = t$, $t/iu = t_i/u$.

We say that $u$ is an *occurrence of t/u in t*. Finally, for $t \in \mathcal{C}$, $u \in \mathcal{O}(t)$ and $t' \in \mathcal{C}$, we define $t[u + t'] \in \mathcal{C}$ by :

- $t[\epsilon + t'] = t'$

- $(F t_1 \dots t_n)[iu + t'] =$

$$ F t_1 \dots t_{i-1}(t_i[u + t']) t_{i+1} \dots t_n \quad i \le n $$

These definitions are consistent with [14, 17], and in the rest of the paper we shall make free use of the following proposition, which corresponds to lemmas 4.6 and 4.7 in [14].

### Proposition 3

a) $\forall t_1, t_2 \in \mathcal{C}$, $u \in \mathcal{O}(t_1)$, $v \in \mathcal{O}(t_2)$ :

$$ a-1 - t_1[u + t_2]/u.v = t_2/v \quad \text{embedding} $$

$$ a-2 - t_1[u + t_2[v + t_3]] = t_1[u + t_2][u.v + t_3] \quad \text{associativity} $$

b) $\forall t_1, t_2, t_3 \in \mathcal{C}$, $u, v \in \mathcal{O}(t_1)$, with $u|v$ :

$$ b-1 - t_1[u + t_2]/v = t_1/v \quad \text{persistence} $$

$$ b-2 - t_1[u + t_2][v + t_3] = t_1[v + t_3][u + t_2] \quad \text{commutativity} $$

c) $\forall t_1, t_2 \in \mathcal{C}$, $u, v \in \mathcal{O}(t_1)$, with $v \prec u$ :

$$ c-1 - t_1/u = (t_1/v)/(u/v) \quad \text{cancellation} $$

$$ c-2 - t_1[u + t_2]/v = (t_1/v)[u/v + t_2] \quad \text{distributivity} $$

### Definitions

A *substitution* is a mapping $\sigma$ from $v$ to $\mathcal{C}$, with $\sigma(x)=x$ almost everywhere. Substitutions are noted $\sigma, \rho, \eta$. Substitutions are extended as morphisms of $\mathcal{C}$, by :

$$ \sigma(F t_1 \dots t_n) = F \sigma(t_1) \dots \sigma(t_n). $$

The bijective morphisms are called *permutations*, and are noted $\xi, \zeta', \dots$. We call *domain* of substitution $\sigma$ the finite set $\mathcal{D}(\sigma) = \{x \in v | \sigma(x) \neq x\} \subset v$. For $V \subset v$, we define the restriction $\sigma|_V$ of $\sigma$ to $V$ as :

$$ (\sigma|_V)(x) = \begin{cases} \sigma(x) & \text{if } x \in V \\ x & \text{otherwise} \end{cases} $$

For all $\sigma$, $t$ and $V$, $v(t) \subset V \Rightarrow \sigma(t) = (\sigma|_V)(t)$, and $\mathcal{D}(\sigma) \cap v(t) = \emptyset \Rightarrow \sigma(t) = t$.
We define the quasi ordering $\leq$ of subsumption in $\mathcal{C}$ by :

$$t \leq t' \Leftrightarrow \exists \sigma \ t' = \sigma(t)$$

It can be shown that if such a $\sigma$ exists, $\sigma|_{\mathcal{V}}(t)$ is unique. We call it the match of $t'$ by $t$, and denote it $t'//t$.

We define $t \equiv t' \Leftrightarrow t \leq t'$ and $t' \leq t$. It can be shown that $t \equiv t'$ iff there exists a permutation $\xi$ such that $t' = \xi t$. Remark that $\nu, \lambda$ and $\theta$ are preserved by $\equiv$. Finally, we define :

$$t > t' \Leftrightarrow t' \leq t \text{ & } t \neq t'$$

**Proposition 4** > is a noetherian relation in $\mathcal{C}$.

The proof of this proposition is given in [5], and consists in showing $t > t' \Rightarrow \mu(t) > \mu(t')$.

Let $\varphi$ be any bijection between $\mathcal{C}$ x $\mathcal{C}$ and $\nu$. We define a binary operation $\wedge$ in $\mathcal{C}$ inductively by :

$$\begin{align*}
& F t_1 \dots t_n \wedge F t'_1 \dots t'_n = F(t_1 \wedge t'_1) \dots (t_n \wedge t'_n) \quad \forall F \in \mathfrak{F}_n \\
& t \wedge t' = \varphi(t,t') \text{ in all other cases.}
\end{align*}$$

$t \wedge t'$ is uniquely determined from $\varphi$, and for distinct $\varphi$'s is unique up to $\equiv$.

**Proposition 5** $t \wedge t'$ is a glb of $t$ and $t'$ under the subsumption ordering.

Let $\hat{\mathcal{C}}$ be the quotient set $\mathcal{C}/\equiv$, completed with a maximum element $T$. From propositions 4 and 5 follows directly :

**Theorem 1** $\hat{\mathcal{C}}$ is a complete lattice.

The proof of proposition 5, of theorem 1 and various other results concerning the structure of $\mathcal{C}$ and of its completion by infinite terms, may be found in [5]. See also [10] and [12] for similar constructions.

A direct consequence of theorem 1 is the existence, for any two terms $t$ and $t'$ that have a common instance (i.e. s.t. $\exists \sigma, \sigma'(t) = \sigma'(t')$), of an lub $t \vee t'$, most general such instance. The term $t \vee t'$ is unique modulo $\equiv$, and may be found by the unification algorithm [13]. Efficient ways of unifying terms are described in [5, 18]. If such an lub exists, we write $t \Delta t'$, and say that $t$ and $t'$ are unifiable.

We shall need in the next sections the following technical lemmas, whose proofs are omitted here.

**Proposition 6** $\mathcal{O}(\sigma(t)) = \mathcal{O}(t) \cup \bigcup_{t/u \in \mathcal{V}} \{u.v | v \in \mathcal{O}(\sigma(t/u))\}$.

$\forall u \in \mathcal{O}(t) : \begin{array}{ll} \cdot & \text{if } t/u = t' \notin \mathcal{V} \text{ then } \sigma(t)/u = \sigma(t') \\ \cdot & \text{if } t/u = x \in \mathcal{V} \text{ then } \sigma(t)/u.v = \sigma(x)/v. \\ \forall v \in \mathcal{O}(\sigma(x)) & \end{array}$

**Proposition 7** $\forall t, t' \in \mathcal{C}, \forall u \in \mathcal{O}(t) \ \sigma(t)[u + \sigma(t')] = \sigma(t[u + t'])$.

## 2 - Term rewriting systems and critical pairs

### Definition

We call term rewriting system any set $\mathcal{R}$ of pairs of terms $\langle\gamma, \delta\rangle$, such that $\nu(\delta) \subset \nu(\gamma)$.

We say that $u$ is a redex of $\mathcal{R}$ in term $t$ iff $u \in \mathcal{O}(t)$, and $\exists \langle\gamma, \delta\rangle \in \mathcal{R}$ such that $\gamma \leq t/u$. Taking $\sigma = (t/u) // \gamma$ and $t' = t [u + \sigma(\delta)]$, we say that $t$ reduces to $t'$ in $u$, and we write $t \xrightarrow{\mathcal{R}} t'$ or, when we want to specify the redex, $t [u] \xrightarrow{\mathcal{R}} t'$.

**Example** Let $\mathcal{R} = \{\langle Ix, x\rangle\}$, with $\alpha(I) = 1$.

We have $I I x \xrightarrow{[\epsilon]} I x$, and also $I I x \xrightarrow{[1]} \mathcal{R} I x$.

### Definition

Let $\to$ be a relation over $\mathcal{C}$. We say that $\to$ is :

- stable iff $\forall \sigma \forall t.t' \ t \to t' \Rightarrow \sigma(t) \to \sigma(t')$.

- compatible iff $\forall \bar{\tau} \in \mathcal{C} \forall u \in \mathcal{O}(\bar{\tau}) \forall t,t' \ t \to t' \Rightarrow \bar{\tau}[u + t] \to \bar{\tau}[u + t']$.

It is easy to show, using propositions 3 and 6, that $\mathcal{R} \to$ is the smallest compatible stable relation containing $\mathcal{R}$.

### Proposition 8

Let $\to$ be any compatible relation in $\mathcal{C}$, $\sigma$ and $\sigma'$ be substitutions such that $\begin{cases} \sigma(x) \to \sigma'(x) \\ \sigma(y) = \sigma'(y) \ \forall y \neq x. \end{cases}$

Let $t$ be any term, and $u_1, \dots, u_n \in \mathcal{O}(t)$ be all the occurrences of $x$ in $t$ (assumed to be distinct). Defining $t_o = \sigma(t)$, and $t_i = t_{i-1}[u_i \to \sigma'(x)] \forall i \leq i \leq n$, we have : $t_i \xrightarrow{n-i} \sigma'(t) \ \forall i \ 0 \leq i \leq n$.

We leave the proof of this easy proposition to the reader. Let us now describe a superposition algorithm, used to define critical pairs of terms in a term rewriting system. This algorithm is taken from Knuth and Bendix [6].
## Superposition algorithm

Let $<\gamma_1, \delta_1>$, $<\gamma_2, \delta_2>$ $\in \mathcal{R}$, and $u \in \mathcal{O}(\gamma_1)$ such that $t = \gamma_1/u \notin \mathcal{V}$ and $t \Delta \gamma_2$. Let $t' \equiv t \vee \gamma_2$, such that $\mathcal{V}(t') \cap \mathcal{V}(\gamma_1) = \emptyset$. We say that the superposition of $<\gamma_2, \delta_2>$ on $<\gamma_1, \delta_1>$ in $u$ determines the critical pair $<t_1, t_2>$, defined by:

$$ \begin{cases} t_1 = \sigma_1(\gamma_1) [u + \sigma_2(\delta_2)] \\ t_2 = \sigma_1(\delta_1) \end{cases} $$

where $\sigma_1 = t'//t$ and $\sigma_2 = t'//\gamma_2$.

**Remarks:** For any $<\gamma_1, \delta_1>$, $<\gamma_2, \delta_2>$ and $u$ the critical pair is unique, up to a permutation. We may choose $<\gamma_2, \delta_2> = <\gamma_1, \delta_1>$, as in example c below. But in this case (and in this case only) we shall not consider the case $u = \epsilon$, which gives only trivial critical pairs $<\delta, \delta>$.

## Examples

For convenience, we use parentheses in our examples:

a) $\gamma_1 = F(x, G(x, A))$, $\delta_1 = H(x)$, $\gamma_2 = G(B, x)$, $\delta_2 = K(x)$ with $u = 2$ determine the pair $t_1 = F(B, K(A))$, $t_2 = H(B)$.

b) $\gamma_1 = F(x, H(x'))$, $\delta_1 = P(x', x)$, $\gamma_2 = H(G(x, x'))$, $\delta_2 = Q(x, x')$ with $u = 2$ determine $t_1 = F(x, Q(y, z))$, $t_2 = P(G(y, z), x)$.

c) $\gamma_1 = \gamma_2 = H(H(x))$, $\delta_1 = \delta_2 = K(x)$ with $u = 1$ determine $t_1 = H(K(y))$, $t_2 = K(H(y))$.

**Remark:** The condition $\mathcal{V}(t') \cap \mathcal{V}(\gamma_1) = \emptyset$ may be replaced by the weaker condition: $\mathcal{V}(t') \cap (\mathcal{V}(\gamma_1) - \mathcal{V}(t)) = \emptyset$. The example b) shows why this condition is necessary: choosing the pair $<F(x, Q(x, x'))$, $P(G(x, x'), x)>$ would be strictly less general than the pair $<t_1, t_2>$. If we compute $t'$ by unification of $t$ and $\xi(\gamma_2)$, where $\xi$ is a permutation renaming variables in $\mathcal{V}(\gamma_1) \cap \mathcal{V}(\gamma_2)$, we get $\mathcal{V}(t') \subset (\mathcal{V}(t) \cup \mathcal{V}(\xi(\gamma_2)))$, and the condition above is thus satisfied.

## Proposition 9

Let $<\gamma_1, \delta_1>$, $<\gamma_2, \delta_2> \in \mathcal{R}$ and $u \in \mathcal{O}(\gamma_1)$ such that $t = \gamma_1/u \notin \mathcal{V}$ and there exist $\sigma_1$ and $\sigma_2$ with $\sigma_1(t) = \sigma_2(\gamma_2)$. Then there exist a critical pair $<t_1, t_2>$ of $\mathcal{R}$ and a substitution $\rho$ such that $\sigma_1(\gamma_1) [u + \sigma_2(\gamma_2)] = \rho(t_1)$ and $\sigma_1(\delta_1) = \rho(t_2)$.

We shall omit here, for lack of space, the proof of this proposition, which asserts the correctness of the superposition algorithm.

We are interested in critical pairs because of the following lemma, which shows that the test for local confluence may be restricted to critical pairs.

## Lemma 9

$\tilde{\mathcal{R}}$ is locally confluent iff for every critical pair $<t_1, t_2>$ of $\mathcal{R}$ we have $t_1 + t_2$.

## Proof

We abbreviate below $\tilde{\mathcal{R}}$ in $\cdot$.

Using the notations of the superposition algorithm, a critical pair $<t_1, t_2>$ is such that $\sigma_1(\gamma_1) + t_1$ and $\sigma_1(\gamma_1) + t_2$, which shows the only if part.

For the if part, assume that for every critical pair $<t_1, t_2>$ of $\mathcal{R}$ we have $t_1 + t_2$. Let $t$ be an arbitrary term, $t$ and $t'$ such that $t \xrightarrow{[u_1]} t'$ and $t \xrightarrow{[u_2]} t''$; i.e., there exists $<\gamma_1, \delta_1>$, $<\gamma_2, \delta_2>$ in $\mathcal{R}$ and substitutions $\sigma_1$ and $\sigma_2$, with:

$$ \begin{aligned} t/u_1 &= \sigma_1(\gamma_1), t/u_2 = \sigma_2(\gamma_2), t' &= t[u_1 + \sigma_1(\delta_1)], \\ t'' &= t[u_2 + \sigma_2(\delta_2)]. \end{aligned} $$

There are two cases, according to the relative positions of the two redexes:

a) disjoint redexes: $u_1|u_2$

We have then $t'/u_2 = \sigma_2(\gamma_2)$ by persistence, and similarly $t''/u_1 = \sigma_1(\gamma_1)$. Furthermore, we have $\bar{t} = t'[u_2 + \sigma_2(\delta_2)] = t'[u_1 + \sigma_1(\delta_1)]$ by commutativity, and therefore $t' \to \bar{t}$ and $t'' \to \bar{t}$.

b) prefix redexes.

Let us assume, without loss of generality, that $u_1 \prec u_2$. Let $v = u_2/u_1$. By cancellation, we get $\sigma_1(\gamma_1)/v = \sigma_2(\gamma_2)$ and by distributivity: $t''/u_1 = \sigma_1(\gamma_1)[v + \sigma_2(\delta_2)]$.

Let us show that there exists $\bar{t}$ such that $\sigma_1(\delta_1) \stackrel{\star}{\to} \bar{t}$ and $t''/u_1 \stackrel{\star}{\to} \bar{t}$. It will then follow that $t' \to t''$, by compatibility of $\cdot$. According to proposition 6, there are two cases:

b1) $v = v_1 \cdot v_2 \quad \gamma_1/v_1 = x \in \mathcal{V} \quad \sigma_2(\gamma_2) = \sigma_1(x)/v_2$.

Let us consider substitution $\sigma'_1$ defined by:

$$ \begin{cases} \sigma'_1(x) = \sigma_1(x)[v_2 + \sigma_2(\delta_2)] \\ \sigma'_1(y) = \sigma_1(y) \quad \forall y \neq x. \end{cases} \quad \text{and let } \bar{t} = \sigma'_1(\delta_1). $$

We have $\sigma_1(x) + \sigma'_1(x)$, and by proposition 8 we get $\sigma_1(\delta_1) \stackrel{\star}{\to} \bar{t}$ and $\sigma_1(\gamma_1)[v + \sigma_2(\delta_2)] \stackrel{\star}{\to} \sigma'_1(\gamma_1)$. Since $\cdot$ is stable we get $\sigma'_1(\gamma_1) \to \bar{t}$, which concludes the proof of b1.
b2) $\exists \gamma \ell \nu \ \gamma = \gamma_1/v, \sigma_2(\gamma_2) = \sigma_1(\gamma).$

Using proposition 9, there exists a critical pair <t₁, t₂> and a substitution ρ such that
σ₁(γ₁)[ν + σ₂(δ₂)] = ρ(t₁) and σ₁(δ₁) = ρ(t₂). By
hypothesis, there exists t₃ such that t₁ ⋆ t₃ and
t₂ ⋆ t₃. We may choose t̄ = ρ(t₃), and the result
follows by stability of →. □

**Remark :** Lemma 9 is inspired from Knuth & Bendix [6]. But our proof, contrarily to theirs, does not require → to be noetherian. The corollary to th. 5 in [6] is essentially th.2 below.

**Theorem 2**

Let $\mathcal{R}$ be a term rewriting system such that $\hat{\mathcal{R}}$ is noetherian. Let $\hat{t}$ denote an arbitrary $\hat{\mathcal{R}}$-normal form of $t$, for $t \in \mathcal{G}$. Then $\hat{\mathcal{R}}$ is confluent iff for every critical pair $<t_1, t_2>$ of $\mathcal{R}$ we have $\hat{t}_1 = \hat{t}_2$.

Proof

⇒ For any critical pair <t₁, t₂> of $\mathcal{R}$ , ∃ t $\hat{\mathcal{R}}$ t₁ &
t $\hat{\mathcal{R}}$ t₂. If $\hat{\mathcal{R}}$ is confluent, then by lemma 2 t admits a
unique $\bar{\mathcal{R}}$ -normal form $\hat{t}_1 = \hat{t}_2$. ⇐ $\hat{t}_1 = \hat{t}_2$ implies
$\bar{t}_1 + \bar{t}_2$, and $\bar{\mathcal{R}}$ is locally confluent by lemma 9, and
therefore confluent by lemma 4. []

**Remarks :** If $\bar{\mathcal{R}}$ is noetherian, we may get $\hat{t}$ by an arbitrary sequence of rewritings using rules of $\mathcal{R}$ to $t$, termination being guaranteed. Theorem 2 gives us in this case an effective way of testing the confluence of $\bar{\mathcal{R}}$ provided we have only a finite number of critical pairs $<t_1, t_2>$. This will happen in particular if $\mathcal{R}$ is finite.

Theorem 2 gives also hints on how to complete $\mathcal{R}$ to a confluent system, when it is not : the idea is to include in $\mathcal{R}$, for every $<t_1, t_2>$ such that $\hat{t}_1 \neq \hat{t}_2$, either $<t_1, t_2>$, or $<t_2, t_1>$, or $<t_1, t>$ and $<t_2, t>$ for some term $t$. See [6] and [7]. Of course one must show that the new pairs preserve termination, and there is no guarantee that the "completing" process will terminate. We shall come back to this in section 4.

The main difficulty in using th.2 consists in showing $\bar{\mathcal{R}}$ noetherian. For that, one must find a noetherian, stable, compatible strict partial order $>=$ such that $\gamma > \delta$ for every $<\gamma, \delta>$ in $\mathcal{R}$. Knuth & Bendix propose in [6] a tricky lexicographic ordering for this purpose. A somewhat more general method consists in defining an interpretation $\chi$ of terms over $\mathbb{N}$. To be effective, each $F$ in $\mathbb{F}_n$ will be interpreted as a recursive total func-

tion of n arguments $\chi(F)$. Interpretations being mor-
phisms, compatibility is insured. To prove $\bar{\mathcal{R}}$ noethe-
rian, it suffices to show that, for every $<\gamma, \delta>$ in $\mathcal{R}$,
$\chi(\gamma) > \chi(\delta)$ is identically true for all values of $\chi(x_i)$
This is essentially the method (with $\chi(F)$ being poly-
nomials) used by Lankford in [7]. For instance, the
ten group reduction rules of Knuth & Bendix may be
shown to define a noetherian rewriting system, using
the interpretation :

$$
\begin{cases}
\chi(\cdot) = \lambda \ x \ y. \ x(1+2y) \\
\chi(-) = \lambda \ x. \ x^2 \\
\chi(e) = 2
\end{cases}
\qquad \text{over integers } > 1.
$$

3 - *Free term rewriting systems*

We are now going to give sufficient conditions for
confluence that do not depend on termination conditions.
The idea is to impose on critical pairs <t₁, t₂> of R a
condition stronger than t₁ + t₂, inspired from the
strong confluency condition.

Definition

A term rewriting system $\mathcal{R}$ is $\epsilon$-closed iff, for every
critical pair <t₁, t₂> of $\mathcal{R}$, there exists $t_3$ such that
$t_1 \xrightarrow{\epsilon} \mathcal{R} t_3$ and $t_2 \xrightarrow{\epsilon} \mathcal{R} t_3$.

Remark that this condition alone is not sufficient
to ensure confluence, as shown by the counter-example :

$$
\mathcal{R} = \{ \langle F(x, x), A \rangle, \langle F(x, G(x)), B \rangle, \langle C, G(C) \rangle \}
$$

since the term F(C,C) possesses two distinct normal
forms A and B. Note that $\mathcal{R}$ has no critical pair.

Definition

$\mathcal{R}$ is left-free iff $\forall <\gamma, \delta> \in \mathcal{R} \ \gamma$ is free.

$\mathcal{R}$ is right-free iff $\forall <\gamma, \delta> \in \mathcal{R} \ \delta$ is free.

**Lemma 10**

If $\mathcal{R}$ is a left and right-free $\epsilon$-$\epsilon$ closed term rewriting system, $\bar{\mathcal{R}}$ is strongly confluent.

Proof

Let us assume $\mathcal{R}$ is left and right free and $\epsilon-\epsilon$ closed,
and let us abbreviate $\bar{\mathcal{R}}$ in $\to$. Let $t \xrightarrow{[u_1]} t'$ and $t \xrightarrow{[u_2]} t''$;
i.e., $\exists <\gamma_1, \delta_1>, <\gamma_2, \delta_2> \in \mathcal{R}$, and substitutions $\sigma_1$ and
$\sigma_2$ such that $t/u_1 = \sigma_1(\gamma_1)$, $t' = t[u_1 + \sigma_1(\delta_1)]$,
$t/u_2 = \sigma_2(\gamma_2)$, and $t'' = t[u_2 + \sigma_2(\delta_2)]$. We show there
exists $\bar{t}$ such that $t' \xrightarrow{\xi} \bar{t}$ and $t'' \xrightarrow{\xi} \bar{t}$.
There are two cases, according to the relative positions of redexes $u_1$ and $u_2$; the proof is similar to that of lemma 9.

a) disjoint redexes : $u_1|u_2$
We take $\bar{t} = t'[u_2 + \sigma_2(\delta_2)] = t''[u_1 + \sigma_1(\delta_1)]$.

b) prefix redexes ; let us assume, without loss of generality, that $u_1 < u_2$.
Let $v = u_2/u_1$. We have $\sigma_2(\gamma_2) = \sigma_1(\delta_1)/v$ and $t'' = t[u_1 + \sigma_1(\gamma_1)[v + \sigma_2(\delta_2)]]$.

b1) $\sigma_2(\gamma_2)$ is completely introduced by $\sigma_1$ :
$$ \exists v_1, v_2 \quad v = v_1, v_2, \quad \gamma_1/v_1 = x \in \mathcal{V}, \quad \sigma_1(x)/v_2 = \sigma_2(\gamma_2). $$
We define a substitution $\sigma_3$ by :
$$ \begin{cases} \sigma_3(x) = \sigma_1(x)[v_2 + \sigma_2(\delta_2)]. \\ \sigma_3(y) = \sigma_1(y) \quad \forall y \neq x. \end{cases} $$
and we take $\bar{t} = t[u_1 + \sigma_3(\delta_1)]$.

$\mathcal{R}$ being left-free, $x$ occurs in $\gamma_1$ only in occurrence $v_1$, and we get :

$$ \begin{aligned} \sigma_3(\gamma_1) &= \sigma_1(\gamma_1)[v_1 + \sigma_3(x)] = \sigma_1(\gamma_1)[v_1 + \sigma_1(x)[v_2 + \sigma_2(\delta_2)]] \\ &= \sigma_1(\gamma_1)[v + \sigma_2(\delta_2)], \quad \text{whence } t'' = t[u_1 + \sigma_3(\gamma_1)], \\ \text{which shows } t'' \to \bar{t}. \quad \text{There are again two cases :} \end{aligned} $$

b1-i) $x \notin \mathcal{V}(\delta_1)$
Then trivially $\sigma_3(\delta_1) = \sigma_1(\delta_1)$ and therefore $\bar{t} = t'$.

b1-ii) $\exists w \in \mathcal{O}(\delta_1) \quad \delta_1/w = x$.
$\mathcal{R}$ being right-free, $w$ is the unique occurrence of $x$ in $\delta_1$, and we get :
$$ \begin{aligned} \sigma_3(\delta_1) &= \sigma_1(\delta_1)[w + \sigma_1(x)[v_2 + \sigma_2(\delta_2)]] = \\ &= \sigma_1(\delta_1)[w \cdot v_2 + \sigma_2(\delta_2)]. \end{aligned} $$

Since $\sigma_1(\delta_1)/w \cdot v_2 = \sigma_2(\gamma_2)$, we get $t' \to \bar{t}$, using redex u.w.v_2.

b2) $\sigma_2(\gamma_2)$ partially exists in $\gamma_1$ :
$$ v \in \mathcal{O}(\gamma_1), \gamma = \gamma_1/v \notin \mathcal{V}, \quad \sigma_1(\gamma) = \sigma_2(\gamma_2). $$

According to proposition 9, there exists a critical pair $<t_1, t_2>$ and a substitution $\rho$ such that:
$\rho(t_1) = \sigma_1(\gamma_1)[v + \sigma_2(\delta_2)]$ and $\rho(t_2) = \sigma_1(\delta_1)$, and thus $t' = t[u_1 + \rho(t_2)]$ and $t'' = t[u_1 + \rho(t_1)]$.

By closure hypothesis, there exists $t_3$ such that $t_1 \not\equiv t_3$ and $t_2 \not\equiv t_3$, and therefore $t' \not\equiv \bar{t}$ and $t'' \not\equiv \bar{t}$, with $\bar{t} = t[u_1 + \rho(t_3)]$. □

Using lemma 5 we get :

**Corollary** : If $\mathcal{R}$ is a left and right free $\epsilon-\epsilon$ closed system, $\bar{\mathcal{R}}$ is confluent.

**Remarks** : Without change to the proof above, we could replace the condition "$\epsilon-\epsilon$ closed" by the slightly more general condition : "for every critical pair $<t_1, t_2>$ of $\mathcal{R}$, there exist $t_3$ and $t_4$ such that $t_1 \stackrel{*}{\mathcal{R}} t_3$, $t_2 \stackrel{\xi}{\mathcal{R}} t_3$, $t_1 \stackrel{\xi}{\mathcal{R}} t_4$ and $t_2 \stackrel{*}{\mathcal{R}} t_4$".

If $\mathcal{R}$ is only left-free and $\epsilon-\epsilon$ closed, $\bar{\mathcal{R}}$ is not necessarily confluent, as shown by the following counter-example :

$$ \mathcal{R} = \{ \langle F(A, A), G(B, B) \rangle, \langle A, A' \rangle, \langle F(A', x), F(x, x) \rangle, \\ \langle F(x, A'), F(x, x) \rangle, \langle G(B, B), F(A, A) \rangle, \langle B, B' \rangle, \\ \langle G(B', x), G(x, x) \rangle, \langle G(x, B'), G(x, x) \rangle \} $$

since $F(A', A') \stackrel{*}{\rightleftharpoons} G(B', B')$ and still $F(A', A') + G(B', B')$ is false.

Still, it is very desirable to find sufficient conditions for a term rewriting system to be confluent that do not depend on right-freeness, a rather unnatural condition. One way to do this is to change the closure condition, as we shall see. Let us first give some new definitions.

A reduction relation $\stackrel{\leftrightarrow}{\overline{\mathcal{R}}}$ over $\mathcal{C}$ is said to be a *congruence* iff it is reflexive and it verifies :

$$ t_1 \stackrel{\leftrightarrow}{\to} t'_1 \quad \& \quad \dots \quad \& \quad t_n \stackrel{\leftrightarrow}{\to} t'_n \quad \Rightarrow \quad F \ t_1 \dots t_n \stackrel{\leftrightarrow}{\to} F \ t'_1 \dots t'_n \\ \forall F \in \mathcal{F}_n. $$

For any term rewriting $\mathcal{R}$, we define a relation $\stackrel{\leftrightarrow}{\mathcal{R}}$ (parallel reduction) as follows.

Let $t \in \mathcal{C}$, and $U = \{u_1, \dots, u_n\}$ be a set of mutually disjoint redexes of $\mathcal{R}$ in $t$: $V_i \le n \ t/u_i = \sigma_i(\gamma_i)$, with $\langle \gamma_i, \delta_i \rangle \in \mathcal{R}$. We define $t' = t[u_1 + \sigma_i(\delta_i)] \mid_{i \in n}$ as the term $t[u_1 + \sigma_i(\delta_i)] \dots [u_n + \sigma_n(\delta_n)]$. It is easy to show, by commutativity, that the order in which we reduce redexes is irrelevant. We say that $t$ reduces in parallel to $t'$, which we write $t \stackrel{\leftrightarrow}{\to} t'$. It is easy to show that $\stackrel{\leftrightarrow}{\mathcal{R}}$ is the smallest congruence containing $\bar{\mathcal{R}}$, and that it is stable.
**Proposition 10**

For any substitution $\sigma$ and term $t$:

$$ \sigma(t) = t[u \to \sigma(x)|t/u = x \in \mathcal{V}]. $$

**Proposition 11** Let $\mathcal{H} \to \mathcal{U}$ be any congruence.

Let $U$ be a set of disjoint occurrences in term $t$. Then
$\forall u \in U \quad t'_u \to t''_u \Rightarrow t[u \to t'_u|u \in U] \mathcal{H} \to t[u + t''_u|u \in U].$

Propositions 10 and 11 are easily proved by induction on $t$.

**Definition**

A term rewriting system $\mathcal{R}$ is parallel-0 closed iff, for every critical pair $\langle t_1, t_2 \rangle$ of $\mathcal{R}$ we have $t_1 \mathcal{H} \to t_2$.

**Lemma 11**

If $\mathcal{R}$ is a left-free parallel-0 closed term rewriting system, $\mathcal{H} \to \mathcal{R}$ is strongly confluent.

*Proof* We abbreviate $\mathcal{H} \to \mathcal{R}$ in $\mathcal{H} \to \mathcal{R}$.

Let $\mathcal{H} \to \mathcal{R}$ with set of redexes $U$, and $\mathcal{H} \to \mathcal{R}$ with set $V$.

Let $P = \{u \in U | \exists v \in V \ v \prec u\} \cup \{v \in V | \exists u \in U \ u \prec v\}$
and $Q = [(U \cup V) - P] \cup (U \cap V)$.

$P$ and $Q$ are two sets of mutually disjoint occurrences of $t$. We prove $\exists \bar{t} \ t' \mathcal{H} \to \bar{t} \ \& \ t'' \mathcal{H} \to \bar{t}$ by complete induction on $p(t,U,V) = \sum_{w \in P} \lambda(t/w)$.

1) Let $u$ be any redex in $Q$. We may assume, without loss of generality, that $u \in U$. Let $V_u = \{v \in V|u \prec v\}$. We shall now show the existence of a term $t_u$ such that $t'/u \mathcal{H} \to t_u$ and $t''/u \mathcal{H} \to t_u$.

Let $\langle \gamma, \delta \rangle$ be the rule of $\mathcal{R}$ used in $u$ in the parallel reduction $U$, with substitution $\sigma: t/u = \sigma(\gamma)$ and $t'/u = \sigma(\delta)$.

There are two cases:

a) No $v$ is critical in $u$, i.e. for all $v$ in $V_u$, we have $v/u = w.w'$ with $\gamma/w = x \in \mathcal{V}$. (This covers the case $V_u = \emptyset$).

Conversely, let $x$ be any variable of $\gamma$. $\gamma$ being free by hypothesis, there is a unique $w \in \mathcal{O}(\gamma)$ such that $\gamma/w = x$. Let $W'$ be the set of occurrences in $\sigma(x)$ of redexes of $V: W' = \{v/u.w|u.w \prec v \in V_u\}$. Let $\langle \gamma_i, \delta_i \rangle$ be the rule of $\mathcal{R}$ corresponding to $w'_i$ in the reduction $V$, with substitution $\sigma_i:

$\gamma/w.w'_i = \sigma_i(\gamma_i)$. Let us construct a substitution $\sigma'$ by defining $\sigma'(x) = \sigma(x)[w'_i \to \sigma_i(\delta_i)|w'_i \in W']$, for every $x$ in $\gamma$.

We have $\sigma(x) \mathcal{H} \to \sigma'(x)$, and therefore $\sigma(\delta) \mathcal{H} \to \sigma'(\delta)$, using propositions 10 and 11. But also $t''/u = \sigma'(\gamma)$ by construction, using propositions 3 and 10. We may therefore choose $t_u = \sigma'(\delta)$.

b) Let $v_1$ in $V_u$ be critical in $u$, i.e. $\gamma/w \notin \mathcal{V}$, with $w = v_1/u$.

Let $\langle \gamma_1, \delta_1 \rangle$ be the rule of $\mathcal{R}$ corresponding to $v_1$ in the reduction $V$, with substitution $\sigma_1$. Using proposition 9, there exists a critical pair $\langle t_1, t_2 \rangle$ of $\mathcal{R}$ and a substitution $\rho$ such that $t'/u = \rho(t_2)$ and $\bar{\ell} = t/u[w \to \sigma_1(\delta_1)] = \rho(t_1)$. By closure hypothesis $t_1 \mathcal{H} \to t_2$, and by stability of $\mathcal{H}$ we get $\bar{\ell} \mathcal{H} \to t'/u$. Let $\bar{W}$ be the set of redexes of $\bar{\ell}$ in this reduction.

We have also $\bar{\ell} \mathcal{H} \to t''/u$, using the set of redexes $V' = \{v/u|v \in V_u - \{v_1\}\}$. Furthermore, $p(\bar{\ell}, V', \bar{W}) \le \sum_{v' \in V'} \lambda(t/u, v') < \sum \lambda(t/u) \le p(t, U, V)$ (by cases according to the position of $v'$ relatively to the family $\bar{W}$). We may therefore use the induction hypothesis, showing the existence of $t_u$.

2) We now consider $\bar{\ell} = t[u \to t_u|u \in Q]$. Since $Q$ dominates all the redexes in $U$, we have $\bar{\ell} = t[u \to t'/u|u \in Q]$ and similarly for $t''$. Using proposition 11, we get $\bar{\ell} \mathcal{H} \to \bar{\ell}$ and $t'' \mathcal{H} \to \bar{\ell}$, which concludes the proof. $\square$

Using lemma 5 and the fact that $\mathcal{H} \to \mathcal{R}$, we get:

**Corollary** Any left-free parallel-0 closed term rewriting system is confluent.

This result is important in practice. It can be used for instance to show the consistency of operational semantics for recursive programming languages. It is the generalization to schemas of the main theorem of Rosen [14], which applies only to ground terms, and which requires 1-0 closure. Notice that Rosen's theorem 6.5 gives only a very particular case of lemma 11 (no critical pairs).
### 4 - Confluent equational theories

We shall now use the results of I-3 to extend the applicability of lemma 9.

We suppose that we are interested in an equational first-order theory $\mathcal{K}$. We assume that the rules of inference of substitution of terms for free variables and of replacement of equals are valid.

Suppose we partition $\mathcal{K}$ in $\mathcal{R} \cup \mathcal{E}$, where $\mathcal{R}$ is a term rewriting system and $\mathcal{E}$ is a set of equations. We assume that $\forall \gamma <\gamma_1, \delta_1 \in \mathcal{R} \quad \mathcal{V}(\delta) \subset \mathcal{V}(\gamma)$, and furthermore
$\forall \gamma = \delta \in \mathcal{E} \quad \mathcal{V}(\delta) = \mathcal{V}(\gamma)$.

As before, $\tilde{\mathcal{K}}$ (abbreviated below →) will denote the smallest compatible stable relation containing $\mathcal{R}$. We also define $\tilde{\mathcal{E}}$ (abbreviated below ↕) as the smallest compatible stable symmetric relation containing $\mathcal{E}$. Note that $\mathcal{K} \models t = t' \Leftrightarrow t(\rightarrow u \tilde{=} t' \rightarrow u) \ast t'$.

We say that $\mathcal{K}$ is a confluent equational theory iff → is confluent modulo ↕. In this case, provided → normalizes $\tilde{\mathcal{C}}$, lemma 6 gives us a way of reducing the problem $\mathcal{K} \models t = t'$ to the problem $\tilde{\mathcal{C}} \sim \tilde{\mathcal{E}}'$, where $\tilde{\mathcal{C}}$ and $\tilde{\mathcal{E}}'$ are →-normal forms of respectively t and t', and $\sim = ↕^*$.

We shall now show how lemma 9 can be generalized to confluent equational theories, which will give sufficient conditions for an equational theory to be confluent, using lemma 8.

Let us recall property $\alpha$ of definition D11 :

$$ \alpha : \forall t, t', t'' \quad t \to t' \quad \& \quad t \to t'' \Rightarrow t' \stackrel{\sim}{\to} t'' $$

$$ \text{where } t' \stackrel{\sim}{\to} t'' \Leftrightarrow \exists \tilde{\mathcal{C}}' \in \tilde{\mathcal{C}}' \quad \tilde{\mathcal{C}}'' \quad t' \stackrel{\ast}{\to} \tilde{\mathcal{C}}' \quad \& \quad t'' \stackrel{\ast}{\to} \tilde{\mathcal{C}}'' \quad \& \quad \tilde{\mathcal{C}}' \sim \tilde{\mathcal{C}}'' $$

### Lemma 12

$\langle \mathcal{R}, \mathcal{E} \rangle$ verifies property $\alpha$ iff for every critical pair $\langle t_1, t_2 \rangle$ of $\mathcal{R}$ we have $t_1 \stackrel{\sim}{\to} t_2$.

### Proof

The proof follows closely that of lemma 9. We use the same notation and indicate here only the points that differ.

Parts a and b1 are kept unchanged.

For part b2, let $\langle t_1, t_2 \rangle$ be the critical pair of $\mathcal{R}$ involved.

By hypothesis, there exist $t_3$ and $t_4$ such that $t_1 \stackrel{\ast}{\to} t_3$, $t_2 \stackrel{\ast}{\to} t_4$ and $t_3 \sim t_4$. Let us consider $\tilde{\mathcal{C}}_1 = \rho(t_3)$ and $\tilde{\mathcal{C}}_2 = \rho(t_4)$.

We get here $\sigma_1(\delta_1) = \rho(t_2) \stackrel{\ast}{\to} \tilde{\mathcal{C}}_2$ since → is stable and $t''/u_1 = \rho(t_1) \stackrel{\ast}{\to} \tilde{\mathcal{C}}_3$ since → is stable. Therefore $\sigma_1(\delta_1) \stackrel{\sim}{\to} t''/u_1$, and thus $t' \stackrel{\sim}{\to} t''$ since → and ↕ are compatible, which concludes the proof. □

We want now to get a similar result for property $\gamma$, which we recall here : $\gamma : \forall t, t', t'' \quad t \to t' \quad \& \quad t \to t'' \Rightarrow t' \stackrel{\sim}{\to} t''$.

### Definition

Let $\langle \mathcal{R}, \mathcal{E} \rangle$ be an equational theory. We call *critical pair of* $\mathcal{E}/\mathcal{R}$ any pair $\langle t_1, t_2 \rangle$ as constructed by the superposition algorithm, but now applied to $\gamma_1, \delta_1, \gamma_2, \delta_2$ such that :

* either $\gamma_1 = \delta_1 \in \mathcal{E}$ or $\delta_1 = \gamma_1 \in \mathcal{E}$, and $\langle \gamma_2, \delta_2 \rangle \in \mathcal{R}$

* or $\langle \gamma_1, \delta_1 \rangle \in \mathcal{R}$ and $\gamma_2 = \delta_2 \in \mathcal{E}$ or $\delta_2 = \gamma_2 \in \mathcal{E}$.

### Lemma 13

Let $\langle \mathcal{R}, \mathcal{E} \rangle$ be an equational theory such that $\mathcal{R}$ is left-free. Then property $\gamma$ holds iff for every critical pair $\langle t_1, t_2 \rangle$ of $\mathcal{E}/\mathcal{R}$ we have $t_1 \stackrel{\sim}{\to} t_2$.

### Proof

The proof follows the same general pattern as that of lemma 9.

Using the notations of the superposition algorithm, a critical pair $\langle t_1, t_2 \rangle$ of $\mathcal{E}/\mathcal{R}$ is such that $\sigma_1(\gamma_1) \to t_1$ and $\sigma_1(\gamma_1) \to t_2$, which shows the only if part.

For the if part, assume that for every critical pair $\langle t_1, t_2 \rangle$ of $\mathcal{E}/\mathcal{R}$ : $t_1 \stackrel{\sim}{\to} t_2$.

Let $t$ be an arbitrary term, $t'$ and $t''$ such that :

$$ t \xrightarrow{[u_1]} t' \quad \text{and} \quad t \xrightarrow{[u_2]} t''; $$

i.e. $\exists \gamma_1, \delta_1 \in \mathcal{R}, \gamma_2 = \delta_2 \in \mathcal{E}$, and substitutions $\sigma_1, \sigma_2$ such that $t/u_1 = \sigma_1(\gamma_1), t/u_2 = \sigma_2(\gamma_2)$, $t' = t[u_1 + \sigma_1(\delta_1)], t'' = t[u_2 + \sigma_2(\delta_2)]$ (the symmetric case is obtained in replacing below $\gamma_2$ by $\delta_2$ and conversely throughout).

There are here three cases, according to the relative positions of the two redexes :

a) disjoint redexes : $u_1|u_2$

$$ \text{With } \tilde{\mathcal{C}} = t'[u_2 + \sigma_2(\delta_2)] = t''[u_1 + \sigma_1(\delta_1)] \text{ we get } t' \to \tilde{\mathcal{C}} \text{ and } t'' \to \tilde{\mathcal{C}}, \text{ and therefore } t' \stackrel{\sim}{\to} t'' $$

b) $u_1 < u_2$ - Let $v = u_2/u_1$.

$$ \text{We have } \sigma_1(\gamma_1)/v = \sigma_2(\gamma_2), \text{ and } t''/u_1 = \sigma_1(\gamma_1)[v + \sigma_2(\delta_2)]. \text{ There are two cases :} $$
b1) $v = v_1 \cdot v_2, \gamma_1 / v_1 = x \in \mathcal{V}, \sigma_2(\gamma_2) = \sigma_1(x) / v_2$.

Let us consider substitution $\sigma'_1$ defined by :

$$
\begin{cases}
\sigma'_1(x) = \sigma_1(x) [v_2 + \sigma_2(\delta_2)] \\
\sigma'_1(y) = \sigma_1(y) \quad \forall y \neq x
\end{cases}
\text{and let } \bar{t} = \sigma'_1(\delta_1).
$$

We have $\sigma_1(\delta_1) \stackrel{*}{\rightleftharpoons} \bar{t}$ by the analogue of proposition 8.

Also $\sigma_1(\gamma_1)[v + \sigma_2(\delta_2)] = \sigma'_1(\gamma_1)$, since $v_1$ is the only occurrence of $x$ in $\gamma_1$, $\mathcal{R}$ being left-free by hypothesis.

$\sigma'_1(\gamma_1) \to \bar{t}$ by stability of $\to$, and thus, taking
$\bar{t} = t[u_1 \to \bar{t}]$, we get $t' \stackrel{*}{\rightleftharpoons} \bar{t}$ and $t'' \to \bar{t}$, by compa-
tibility of $\to$ and $\to$.

b2) $\exists \gamma \notin \mathcal{V} \quad \gamma = \gamma_1 / v \quad \sigma_2(\gamma_2) = \sigma_1(\gamma)$.

Similarly to proposition 9, there exists a critical
pair <t₁, t₂> of E/R and a substitution ρ such that :

$$
\sigma_1(\delta_1) = \rho(t_2) \text{ and } \sigma_1(\gamma_1)[v + \sigma_2(\delta_2)] = \rho(t_1).
$$

By hypothesis, $t_1 \stackrel{\cdot}{\to} t_2$, whence $\rho(t_2) \stackrel{\cdot}{\to} \rho(t_1)$ by stability, and $t' \stackrel{\cdot}{\to} t''$ by compatibility. This concludes case b.

c) $u_2 < u_1$ - Let $v = u_1/u_2$.

Similarly to b, there are two cases :

c1) $v = v_1 \cdot v_2, \gamma_2 / v_1 = x \in \mathcal{V}, \sigma_1(\gamma_1) = \sigma_2(x) / v_2$.

We define substitution $\sigma'_2$ by :

$$
\begin{cases}
\sigma'_2(x) = \sigma_2(x)[v_2 + \sigma_1(\delta_1)] \\
\sigma'_2(y) = \sigma_2(y) \quad \forall y \neq x
\end{cases}
\text{and consider } \bar{t} = \sigma'_2(\delta_2).
$$

We have $\sigma_2(\delta_2) \stackrel{*}{\to} \bar{t}$ by proposition 11, and also
$t'/u_2 = \sigma_2(\gamma_2)[v + \sigma_1(\delta_1)] \stackrel{*}{\to} \sigma'_2(\gamma_2) \stackrel{\cdot}{\to} \bar{t}$, which
shows $t' \stackrel{\cdot}{\to} t''$.

c2) $\exists \gamma \notin \mathcal{V} \quad \gamma = \gamma_2 / v, \sigma_1(\gamma_1) = \sigma_2(\gamma)$.

Again there exists a critical pair <t₁, t₂> of E/R
and a substitution ρ such that :

$$
\sigma_2(\gamma_2)[v + \sigma_1(\delta_1)] = \rho(t_1) \text{ and } \sigma_2(\delta_2) = \sigma_1(t_2).
$$

By hypothesis, $t_1 \stackrel{\cdot}{\to} t_2$, and therefore $t' \stackrel{\cdot}{\to} t''$, which
concludes the proof. $\square$

**Remarks :** The condition $\mathcal{R}$ left-free is essential, and cannot be removed. For instance, with $\mathcal{R} = \{<F(x,x), G(x)>\}$ and $\mathcal{E} = \{A = B\}$, taking $t = F(A,A)$, $t' = G(A)$ and $t'' = F(A,B)$, we do not have $t' \stackrel{\cdot}{\to} t''$. Note that there are no such restrictions for the equations in $\mathcal{E}$.

We have imposed here a condition $v(\delta) \subset v(\gamma)$ for all simplification rules $<\gamma, \delta>$ in $\mathcal{R}$, essentially because it made the definition of $\mathcal{R}$ simpler. If we get rid of this condition, the definition of $\mathcal{R}$ will rely on unification, rather than on the simpler pattern-matching operation of subsumption. But this has some undesirable consequences ; suppose $\mathcal{R}$ contains a rule <A, Fx>. Then, since $\mathcal{R}^+$ is compatible and stable, we must have :

A $\mathcal{R}^+$ F(A) $\mathcal{R}^+$ F(F(A)) $\mathcal{R}^+$ ... which shows that $\mathcal{R}^+$ is not noetherian. Furthermore, since A $\mathcal{R}^+$ F(t) $\forall t \in \mathcal{C}$, $\mathcal{R}^+$ is not locally finite, even if $\mathcal{R}$ is finite. For these reasons, we keep requesting $v(\delta) \subset v(\gamma)$ for all $<\gamma, \delta>$ in $\mathcal{R}$.

For $\mathcal{E}$, the situation is analogous. In the case where $v(\gamma) = v(\delta)$ for all $\gamma = \delta$ in $\mathcal{E}$, we have simply defined the relation $\overline{\mathcal{E}}^+$ as $\overline{\mathcal{E}}^+ \cup \overline{\mathcal{E}}_2$, where $\mathcal{E}_1 = \{<\gamma, \delta>|\gamma=\delta \in \mathcal{E}\}$ and $\mathcal{E}_2 = \{<\delta, \gamma>|\gamma=\delta \in \mathcal{E}\}$. Using the property $\mathcal{D}(\sigma) \subset v(t) \Rightarrow \sigma(t)/t = \sigma$, it is easy to show that $\overline{\mathcal{E}}_2 = \overline{\mathcal{E}}_1^-$, and therefore that $\overline{\mathcal{E}}_1 \cup \overline{\mathcal{E}}_2$ is the smallest compatible stable symmetric relation containing the pairs in $\mathcal{E}$. If on the contrary there exists in $\mathcal{E}$ an equation $\gamma = \delta$ with $v(\gamma) \neq v(\delta)$, then the definition of $\overline{\mathcal{E}}^+$ is more complicated, and has the drawbacks mentioned for $\mathcal{R}$. However here this restriction is more debatable, since we do not use $\overline{\mathcal{E}}^+$ as a computation rule, and therefore do not care about termination or local finiteness. Furthermore, all our results remain true if we remove this condition, using the same definition of critical pairs. In automatic theorem proving terminology, $\overline{\mathcal{E}}^+$ is called paramodulation in non-variable positions. We shall not develop this further in this paper.

We are now able to state our main result. Let us define
the set of *critical pairs* of an *equational theory* <R, E>
as the set of all critical pairs of R and critical pairs
of E/R, as defined above.

**Theorem 3**

Let <R, E> be an equational theory such that R is left-free and +,.- is noetherian, with + = R and ~ = E*. Then <R, E> is confluent iff for all its critical pairs <t₁, t₂> we have t₁ ~ t₂, which may be checked as Œ₁ ~ Œ₂, where Œ is an arbitrary → -normal form of t.

**Proof** Directly from lemmas 6, 8, 12 and 13. □
**Remarks** : The notion of critical pair of <R, E> involves trying all superpositions of equations in E with simplifications in R and conversely and mutual superpositions of simplifications in R. But there is no need to superpose two equations in E.

Remark that for any equational theory $\mathcal{E}$ theorem 3 is trivially applicable with $\mathcal{E} = \mathcal{L}$ and $\mathcal{R} = \emptyset$. This suggests to try to build up $\mathcal{R}$ progressively, removing equations in $\mathcal{E}$ one at a time, checking the termination condition, then generating a set $C$ of critical pairs. All pairs $<t_1, t_2>$ in $C$ that do not verify $t_1 \nvdash t_2$ are then added to $\mathcal{E}$, and the process is iterated. Of course there may be several ways of choosing the candidate simplifications, and the whole process may not terminate. But this kind of algorithm seems a promising way of mechanizing equational theories, compatible with other rules of inference such as resolution. A similar approach is currently being pursued, in particular by Lankford [7], who has already obtained good experimental evidence of its success.

To check the termination condition : $\rightarrow, \sim$ noetherian, the method given in section 2 is still valid, provided the interpretation $\chi$ chosen is such that $\chi(\gamma) = \chi(\delta)$ is identically true for every equation $\gamma = \delta$ in $\mathcal{E}$.

Remark that it is important to get termination criteria as general as possible in lemmas 4, 7 and 8. For instance, the conditions of [15] are too restrictive to be used with Knuth & Bendix's lexicographic ordering [6].

## CONCLUSION

We have presented in this paper general axiomatic properties that are sufficient to prove the confluence of a reduction relation. These results are then applied to term rewriting systems to provide systematic ways of mechanizing an equational theory, favoring simplifications over arbitrary equality replacements. This method, a generalization of early results by Knuth & Bendix, has important applications in formula manipulation systems : program optimization, program validation, automatic theorem proving, operational semantics of programming languages and semantics of parallelism.

## ACKNOWLEDGEMENTS

I wish to thank J.J. Levy and B. Rosen for their helpful remarks.

## REFERENCES

[1] A. Aho, R. Sethi & J. Ullman
Code optimization and finite Church-Rosser systems
Proceedings of Courant Computer Science Symposium
5 Ed. R. Rustin, Prentice Hall 1972.

[2] A. Church & J.B. Rosser
Some properties of conversion
Transactions of AMS Vol 39
(1936) pp 472-482

[3] H.B. Curry & R. Feys
Combinatory Logic, Vol 1
North Holland, 1958.

[4] R. Hindley
An abstract Church-Rosser theorem
part 1 Journal of Symbolic Logic Vol 34 (1969)
pp 545-560
part 2 Journal of Symbolic Logic Vol 39 (1974)
pp 1-21

[5] G. Huet
Résolution d'équations dans des langages d'ordre 1, 2, ... w.
Thèse d'Etat, Université Paris VII, sept. 1976.

[6] D. Knuth & P. Bendix
Simple word problems in universal algebras
Computational problems in abstract algebra
Ed. J. Leech, Pergamon Press 1970, pp 263-297.

[7] D. Lankford
Canonical inference
Report ATP-25, Dec 1975
Departments of mathematics and computer sciences
University of Texas at Austin

[8] M.H.A. Newman
On theories with a combinatorial definition of "equivalence". Annals of Maths, vol 43 (1942)
pp 223-243.

[9] M. Nivat
Congruences parfaites et quasi-parfaites
Séminaire Dubreil, 1971-72, n° 7.
[10] G. Plotkin
Lattice-theoretic properties of subsumption
Memorandum MIP - R - 77
University of Edinburgh, 1970

[11] G. Plotkin
Building-in equational theories
in Machine Intelligence 7, 1972, pp 73-90
American Elsevier

[12] J. Reynolds
Transformational systems and the algebraic structure of atomic formulas
in Machine Intelligence 5, 1970, pp 135-152
American Elsevier

[13] J.A. Robinson
A machine-oriented logic based on the resolution principle
J. ACM Vol 12 (1965) pp 23-41.

[14] B. Rosen
Tree-manipulating systems and Church-Rosser theorems
J. ACM Vol 20 (1973) pp 160-187

[15] R. Sethi
Testing for the Church-Rosser property
J. ACM Vol 21 (1974) pp 671-679
Erratum Vol 22 (1975) p 424.

[16] J. Staples
Church-Rosser theorems for replacement systems
in Algebra and Logic,
Ed. J. Crossley, pp 291-307.
Lecture Notes in Maths n° 450, Springer-Verlag,
1975.

[17] M. O'Donnell
Subtree Replacement Systems: A Unifying Theory
for Recursive Equations, LISP, Lucid and Computational Logic.
Proc. 9th Ann. ACM Symp. on Theory of Computing
(1977), pp 295-305.

[18] M.S. Paterson & M.N. Wegman
Linear unification
Proc. 8th Ann. ACM Symp. on Theory of Computing
(1976), pp 181-186.