Ordered Rewriting and Confluence

Ursula Martin^{∗} and Tobias Nipkow^{†}

Department of Computer Science, RHBNC, University of London Egham, Surrey TW20 0EX, UK and University of Cambridge, Computer Laboratory, Pembroke Street, Cambridge CB2 3QG, UK

Abstract

One of the major problems in term rewriting theory is what to do with an equation which cannot be ordered into a rule. Many solutions have been proposed, including the use of special unification algorithms or of unfailing completion procedures.

If an equation cannot be ordered we can still use any instances of it which can be ordered for rewriting. Thus for example x ∗ y = y ∗ x cannot be ordered, but if a, b are constants with b ∗ a > a ∗ b we may rewrite b ∗ a ⟶ a ∗ b. This idea is used in unfailing completion, and also appears in the Boyer-Moore system. In this paper we define and investigate completeness with respect to this notion of rewriting and show that many familiar systems are complete rewriting systems in this sense. This allows us to decide equality without the use of special unification algorithms. We prove completeness by proving termination and local confluence. We describe a confluence test based on recursive properties of the ordering.

1 Introduction

One of the major problems in term rewriting theory is what to do with an equation which cannot be ordered into a rule. Many solutions have been proposed, including the use of special unification algorithms [7] or of unfailing completion procedures [1, 6].

If an equation cannot be ordered we can still use any instances of it which can be ordered for rewriting. Thus for example

x ∗ y = y ∗ x

cannot be ordered, but if a, b are constants with b ∗ a > a ∗ b we may rewrite

b ∗ a ⟶ a ∗ b.

This idea is used in unfailing completion, and also appears in Boyer-Moore [2]. In this paper we define and investigate completeness with respect to this notion of rewriting and show that many familiar systems are complete rewriting systems in this sense. This allows us to decide equality without the use of special unification algorithms. We prove completeness by proving termination and local confluence. We describe a confluence test based on recursive properties of the ordering.

∗The author acknowledges support of the UK SERC under grant GR/E 83634.

†This research was supported in part by NYNEX, NSF grant CCR-8706652, and by the Advanced Research Projects Agency of the DoD, monitored by the ONR under contract N00014-83-K-0125.

1.1 Summary

In this section we summarize our results. Precise definitions are given below. An ordered rewriting system consists of a set of equations E and a monotonic ordering on terms > which is total on ground terms. We say a term s rewrites to a term t, denoted by s ⟶ t, if there is an equation r = l or l = r in E, a substitution σ and a subterm σl of s such that σl > σr and t is s with that subterm replaced by σr. Thus for example if x ∗ y = y ∗ x is in E and a ∗ b > b ∗ a then a ∗ b ⟶ b ∗ a. We observe that the usual notion of a rewriting system can be regarded as a special case of our concepts in the case when the ordering allows all the equations to be ordered into rules.

A ground complete ordered rewriting system is one which is terminating and confluent on ground terms. This means that any ground term can be rewritten to a unique canonical form, and we can decide equality between ground terms, and hence between variable terms by regarding the variables as generalised constants. This process uses only unification in the empty theory. In section 4 we give examples of ground complete ordered rewriting systems including AC, ACI, Boolean rings, Distributivity and Abelian Groups.

Example 1.1 As an example let E be

(x ∗ y) ∗ z = x ∗ (y ∗ z)  (1)
x ∗ y = y ∗ x  (2)
x ∗ (y ∗ z) = y ∗ (x ∗ z)  (3)

and let > be any monotonic ordering on terms which is total on ground terms and satisfies for all ground terms x, y, z

(x ∗ y) ∗ z > x ∗ (y ∗ z)  (4)
x ∗ y > y ∗ x if x > y (5)
x ∗ (y ∗ z) > y ∗ (x ∗ z) if x > y.  (6)

Then (E, >) is an ground complete ordered rewriting system. For example suppose that > is the lexicographic path ordering (see section 3) and a, b, c are constants with c > b > a. Then

b ∗ (c ∗ (b ∗ a)) ⟶ b ∗ (c ∗ (a ∗ b)) ⟶ b ∗ (a ∗ (c ∗ b)) ⟶ a ∗ (b ∗ (c ∗ b)) ⟶ a ∗ (b ∗ (b ∗ c)).

To prove completeness we need as usual to prove termination and confluence. Termination is generally proved by showing that the ordering is well-founded^{1}, and the orderings we need to do this for our examples are discussed in section 3. To prove confluence we need to prove local confluence, and in section 2.1 we prove the necessary version of the critical pairs lemma.

The usual notion of rewriting and confluence allows confluence to be checked automatically by computation of normal forms. Ground confluence, however, is already undecidable for ordinary rewriting systems [8], and thus even more so for ordered rewriting. However we shall explain in section 2.2 how a ground confluence test may indeed be automated in many cases by axiomatising the properties of the orderings and rewritings that we need. This automation works for most of the examples of section 4.

Consider the example above. Computing critical pairs between

(x ∗ y) ∗ z = x ∗ (y ∗ z)
x ∗ y = y ∗ x

1In fact, it is sufficient to show well-foundedness within equivalence classes. If all equivalence classes are finite, this follows because any ordering on a finite set is well-founded.

we obtain

z ∗ (x ∗ y) ⟵ (x ∗ y) ∗ z ⟶ x ∗ (y ∗ z),

so we have to prove that z ∗ (x ∗ y) and x ∗ (y ∗ z) are joinable for all ground terms x, y, z. Now since x, y, z are ground terms we may consider the possible relationships between them under >. For example if x > z > y then

x ∗ (y ∗ z) ⟶ y ∗ (x ∗ z) ⟶ y ∗ (z ∗ x) ⟵ z ∗ (y ∗ x) ⟵ z ∗ (x ∗ y)

While our technique allows the computation of canonical forms without a special matching algorithm we note that it is not always as powerful as rewriting with an equational matching algorithm.

Example 1.2 Consider the example above together with the equation f(x ∗ x) = 1. Rewriting with an AC matching algorithm shows that f(a∗(a∗(b∗b))) = 1. However, there is no equivalent ground complete ordered rewriting system as any such system would have to contain infinitely many equations to deal with

f(a ∗ a), f(a ∗ (a ∗ (b ∗ b))), f(a ∗ (a ∗ (a ∗ (a ∗ (b ∗ b)))))

and so on.

On the other hand the advantages of our method are that

• Ground rewriting is possible without E-matching algorithms.

• Ground rewriting is sufficient for theorem proving.

• Completion is possible without E-completion.

It shares these features with unfailing completion, as described for example in [6]. Indeed, it is very similar to unfailing completion in two technical aspects: both sides of an equation may give rise to critical pairs, and complete systems need only be confluent for ground terms. In contrast to [6], our method is specially designed to detect critical pairs all of whose ground instances can be joined. Thus we are able to discard many critical pairs, and to obtain complete systems which their approach fails to verify as complete.

2 Critical Pairs, Confluence, and Completion

We assume that all concepts and definitions are as in [5] or [3]. Let Σ be a set of function symbols and V a set of variables. The set of all terms in Σ ∪ V is denoted by T = T (Σ ∪ V), and the set of all ground terms is the subalgebra T_{G} = T (Σ). The function V returns the set of variables in a term. A term can be represented as subterms in a context by writing C[s_{1}, …, s_{n}]. The context C is a λ-term λx_{1}, …, x_{n}.t, and C[s_{1}, …, s_{n}] denotes application, i.e. the simultaneous the replacement of all x_{i} by s_{i}. In particular we assume that every x_{i} occurs exactly once in t.

An ordering > on a set S is a relation which is irreflexive and transitive, so that it is false that x > x, and if x > y and y > z then x > z. An ordering on T is monotonic if for all function symbols f and terms s_{1}, …, s_{n}, s, t we have f(s_{1}, …, s, … s_{n}) > f(s_{1}, …, t, … s_{n}) if s > t.

An ordered rewriting system is a pair (E, >) where E is a set of equations in T and > is a monotonic ordering on T which is total on ground terms. The notation s≐t ∈ E is short for s=t ∈ E ∨ t=s ∈ E. If for some l≐r ∈ E we have σl > σr for all substitutions σ we write l ⟶ r and call it a rule.

The ordered rewriting system (E, >) induces a relation ⟶ defined as

C[σs] ⟶ C[σt] if s≐t ∈ E ∧ σs > σt

Since > is monotonic, p ⟶ q implies p > q. The restriction of ⟶ to ground terms is denoted by ⟹. We use ⟶^{∗} to denote the reflexive transitive closure of ⟶. Two terms s and t are called joinable, written s ↓ t, iff there is a term u such that s ⟶^{∗} u and t ⟶^{∗} u. They are called ground joinable, written s ⇓ t, iff for any ground substitution σ, σs and σt are joinable. An ordered rewriting system is called ground terminating if there is no sequence of ground terms {a_{i}|i ∈ N} such that a_{i} ⟹ a_{i+1} for all i. An ordered rewriting system is called ground confluent if whenever r, s, t are ground terms with r ⟹^{∗} s and r ⟹^{∗} t then s ↓ t. If the terminating or confluence conditions hold for all terms rather than just ground terms we call (E, >) terminating or confluent respectively. An ordered rewriting system which is terminating and confluent is called complete; one which is ground terminating and ground confluent is called ground complete. It follows from Newman’s lemma that if (E, >) is complete then each term s has a unique normal form, and if (E, >) is ground complete this is true for ground terms. Thus if s, t are terms (ground terms) and (E, >) is complete (ground complete) then s =_{E} t if and only if their normal forms are identical. If s and t are arbitrary terms we may still use a ground complete system to decide equality if we regard the variables occurring in s and t as new constants.

In the sequel let (E, >) denote an ordered rewriting system and let ⟶, ⟹ etc. be the rewrite relations it generates. If there is a second ordering, say ≻, we write ⟶_{≻}, ⇓_{≻} etc. to denote the relations induced by (E, ≻).

2.1 The Critical Pair Lemma

This section deals with the extension of the critical pair lemma to ordered rewriting.

Definition 2.1 Given two equations C[u] = t, u ∉ V, and v = w with no variables in common and a most general unifier σ of u and v such that σ(C[u]) ≰ σt and σv ≰ σw, then (σt, σ(C[w])) is a critical pair.

The set of all critical pairs of E is the set of all critical pairs between any two equations p≐q, s≐t ∈ E.

Critical pairs in our sense are the extended critical pairs of Bachmair et al. [1]. Note that because of the symmetry of ≐ both sides of an equation can give rise to critical pairs. If > orders every equation in E into a rule our definition of critical pairs reduces to the usual one.

Lemma 2.2 If > is total within equivalence classes of ground terms, both sides of an equation s≐t ∈ E are ground joinable.

The following lemma extends the ordinary critical pair lemma [4] to ground confluence of ordered rewriting systems. It is a corollary to the critical pair lemma in [1].

Lemma 2.3 An ordered rewriting system (E, >) is locally ground confluent iff all critical pairs are ground joinable.

The proof of this lemma relies on the totality of > within equivalence classes of ground terms. The following example shows that this requirement cannot be dropped:

Example 2.4 Let Σ = {∗} ∪ C, where C is a set of constants, E = {x ∗ y = y ∗ x}, and s > t iff the leftmost constant in s is > the leftmost constant in t. Clearly > is not total because a and a ∗ b are incomparable. Assume that a < b. Then the term r = (b ∗ a) ∗ a can be rewritten to s = a ∗ (b ∗ a) and t = (a ∗ b) ∗ a. However, s and t are not joinable because s rewrites only to a ∗ (a ∗ b), which is in normal form, and t is in normal form already.

On the other hand there is only a single critical pair (y ∗ x, y ∗ x) in E which is trivially ground joinable. This shows that for non-total > the consideration of critical pairs does not suffice to determine local ground confluence.

Finally we have:

Corollary 2.5 A terminating ordered rewriting system is ground confluent iff all critical pairs are ground joinable.

2.2 Automating It

In contrast to ordinary rewriting systems, where critical pairs are required to be joinable, we need the weaker criterion of ground joinability. It is not at all clear how a test of the latter property can be automated since it talks about an infinite set of ground instances. In fact we believe that ground joinability is in general undecidable. The purpose of this section is to give some sufficient criteria which are easily implementable and powerful enough to solve some non-obvious examples. On the other hand they are far from complete. Section 4.9 contains an example which is easily proved to be ground joinable but which is not covered by our method.

The principle idea underlying the automation has already been sketched in the introduction: given two terms s and t, we consider all possible relationships between the variables in s and t under > and = and try to join s and t for each of them. Since there are only finitely many relationships, namely all linear orderings, we only have to consider a finite, albeit possibly very large, number of cases. It remains to be explained how rewriting of terms with variables is to proceed if we do not know what the variables stand for, only how they are related to each other with respect to >. As an example take the term y ∗ x with the constraint x < y. It requires some intimate knowledge of > to determine whether this implies that y ∗ x > x ∗ y, i.e. whether commutativity is applicable.

Instead of working with a particular ordering and inferring some of its properties, we assume a small set of properties of the ordering which allow us to order enough terms for proving ground confluence. For the AC case we have seen in the introduction that the implications (4)-(6) are sufficient for joining one of the critical pairs under a particular set of constraints. In section 4.2 we show that the equations (1)-(3) together with any ordering satisfying (4)-(6) are ground confluent.

The advantage of this approach is its generality: ground confluence is proved for any ordering satisfying the properties we have assumed. However, it means that one has to be careful in the choice of properties. For example they must not violate well-foundedness.

We will now describe a test for ground joinability based on the above ideas. Formally, the “properties” of the ordering are given as a closure operator C on T ×T subject to the restriction

(s, t) ∈ C(>) ⇒ (σs, σt) ∈ C(σ(>))  (7)

where σ(>) = {(σu, σv) | u > v}. The intuition is that C takes a relation on terms and returns the set of consequences implied by the properties we assumed of the ordering. The above restriction ensures that C is well behaved with respect to substitutions. This enforces for example that if x ∗ y > y ∗ x follows from x > y, then x′ > y′ must imply x′ ∗ y′ > y′ ∗ x′. We say that an ordering > is compatible with C if C(>) = >. As a consequence of restriction (7) we obtain:

Lemma 2.6 Let E be a set of equations, let > and ≻ be two relations on T , and let σ be a substitution such that σ(≻) ⊆ >. Then u ⟶_{C(≻)} v implies σu ⟶_{C(>)} σv for all terms u, v. Proof From u ⟶_{C(≻)} v it follows that u = C[θl], v = C[θr] and (θl, θr) ∈ C(≻) for some l≐r ∈ E. From (θl, θr) ∈ C(≻) it follows by (7) that (σθl, σθr) ∈ C(σ(≻)). Since C is a closure operator and σ(≻) ⊆ > we also have (σθl, σθr) ∈ C(>). Thus σu = σ(C)[σθl] ⟶_{C(>)} σ(C)[σθr] = σv. □

Ordering the variables in a term with respect to = and > is equivalent to providing a total order on equivalence classes of variables. If ρ is an equivalence on a set of variables, ρ̂ denotes a substitution which maps each variable to some fixed representative of its equivalence class. Testing for ground joinability of two terms s and t by considering all total orders on equivalence classes of variables in s and t leads to the following definition. If ρ̂s ↓_{C(≻)} ρ̂t holds for all equivalences ρ on the variables in s and t and all total orders ≻ on the range of ρ̂, then we write

s ⇓_{C} t.

Restriction (7) ensures that this definition is independent of the particular choice of representatives of ρ-equivalence classes.

The next lemma shows that s ⇓_{C} t does imply ground joinability:

Lemma 2.7 If s ⇓_{C} t then s ⇓_{>} t holds for all orderings > compatible with C. Proof Let > be compatible with C and let σ be some ground substitution with dom(σ) = V(s) ∪ V(t). We have to show that σs ↓_{>} σt.

Let ρ = ker(σ) and define x ≻ y iff σx > σy for x, y in the range of ρ̂. Then ≻ is a total order and s ⇓_{C} t implies ρ̂s ↓_{C(≻)} ρ̂t. Since >, ≻, and σ satisfy the assumptions of lemma 2.6 it follows that σs = σρ̂s ↓_{C(>)} σρ̂t = σt. Since > is compatible with C we have σs ↓_{>} σt. □

From this lemma and the definition of ⇓_{C} it follows directly that

Corollary 2.8 If C(≻) is recursive and well-founded for all recursive and well-founded ≻, then ⇓_{C} is a sufficient recursive criterion for ground joinability with respect to all orderings compatible with C.

This is the first step towards automating the test for ground joinability. The second ingredient is lemma 2.2. Combining all these criteria we obtain the following set of rules:

s ⇓ t ⇐ s = t
s ⇓ t ⇐ s ⇓_{C} t
s ⇓ t ⇐ ∃l≐r ∈ E, σ. σl = s ∧ σr = t
f(s_{1}, …, s_{n}) ⇓ f(t_{1}, …, t_{n}) ⇐ ∀i. s_{i} ⇓ t_{i}

The first clause is obvious, the second and third ones are consequences of lemmas 2.7 and 2.2 respectively, and the last one follows from compatibility of rewriting.

The prototype implementation of this test is written in Prolog and follows exactly the above four Horn clauses. C is just another predicate. In all our examples C consists of the implications (4)-(6) and further clauses specific to the example.

2.3 Completion

The critical pair lemma in the preceding section leads to a completion algorithm in the usual way: critical pairs which are not ground joinable are added as new equations. Formally this can be expressed as an inference rule between sets of equations:

\frac{E}{E ∪ \{s = t\}} if (s, t) is a critical pair of E and not s ⇓ t.

If this process terminates because all critical pairs are ground joinable, we have obtained a ground complete ordered rewriting system. In addition one may want to obtain a reduced rewriting system by simplifying the right or left hand sides of equations by other equations. This can be achieved by the following rule:

\frac{E ∪ \{s≐t\}}{E ∪ \{s = u\}} if t ⟶_{E} u ∧ s≐t ∉ E

Since we are only interested in ground confluence, ground joinable equations can be removed:

\frac{E ∪ \{s≐t\}}{E} if s ⇓ t

The applications of these three rules may be interleaved arbitrarily.

A prototype implementation of this completion procedure has been written in Prolog and was used for all the examples in section 4.

3 Orderings

Our notations and concepts are taken from Dershowitz [3]. An ordering is called well-founded if there is no set {a_{i}|i ∈ N} with a_{i} > a_{i+1} for each i. We have

Lemma 3.1 Let (E, >) be an ordered rewriting system. If > is well-founded then (E, >) is terminating. Proof The monotonicity condition ensures that if s ⟶ t then s > t, so if > is terminating there can be no infinite chain of rewrites. □

The following orderings will be used in the sequel.

Lexicographic Path Ordering

Let s = f(s_{1}, …, s_{m}), t = g(t_{1}, …, t_{n}). Let > be an ordering on function symbols. Then

s > t if and only if

• s_{i} ≥ t for some i = 1, …, m, or

• f > g and s > t_{j} for all j = 1, …, n, or

• f = g (so n = m) and (s_{1}, …, s_{n}) is greater than (t_{1}, …, t_{n}) in the lexicographic ordering from the left on sequences induced by >, and s > t_{i} for i = 1, …, n.

Then we have

Lemma 3.2

1. The lexicographic path ordering is well-founded, and is total on ground terms if the operator precedence is total.

2. If f, g are binary function symbols with f > g and x, y, u, v are any terms and f(x, y) > u, f(x, y) > v then f(x, y) > g(u, v).

Knuth-Bendix Orderings

The essence of the Knuth-Bendix orderings is to compare terms first by weight and then lexicographically by an operator precedence. For details see [9] or [11], where proofs will be found of

Lemma 3.3 The Knuth-Bendix ordering is monotonic and well-founded, and is total on ground terms if the operator precedence is total.

Lexicographic Orderings

Let Σ = {f, a_{1}, …, a_{k}} where f is binary and a_{1}, … a_{n} are constants. Assume a_{1} < a_{2} … < a_{k}. Define >_{t} for t = 1, 2 by

a_{i} >_{t} a_{j}  if and only if  i ≥ j
f(x, y) >_{t} f(z, u) if and only if  x > z or x = z and y > u
f(a_{i}, x) >_{1} a_{j} if and only if i ≥ j
a_{j} >_{1} f(a_{i}, x) if and only if  j > i
f(a_{i}, x) >_{2} a_{j}  for all i, j = 1, …, k

where x, y, z, u are arbitrary ground terms. Then

Lemma 3.4 For each of the orderings >_{1}, >_{2}

1. >_{t} is a monotonic ordering and total on ground terms

2. f(f(x, y), z) >_{t} f(x, f(y, z)) and if x >_{t} y then f(x, y) > f(y, x) for all ground terms x, y, z.

3. >_{t} is not well-founded.

Proof The proof is straightforward. For (3) notice that we have

f(a_{2}, a_{1}) >_{t} f(a_{1}, f(a_{2}, a_{1})) >_{t} f(a_{1}, f(a_{1}, f(a_{2}, a_{1}))) >_{t} ….
□

Notice that >_{1} is described by Boyer and Moore [2], where it is expressed in terms of projecting onto strings by

s(a_{i}) = a_{i}, s(f(x, y)) = fs(x)s(y)

where f denotes function application, and ordering the strings lexicographically.

To enable us to use the automatic confluence test described in section 2.2 we need to identify orderings with certain properties.

Definition 3.5 An ordering is called AC compatible for the binary operator f if it is monotonic, well-founded and total on ground terms, and satisfies for all ground terms x, y, z

f(f(x, y), z) > f(x, f(y, z))
f(x, y) > f(y, x)  if x > y
f(x, f(y, z)) > f(y, f(x, z)) if x > y

Lemma 3.6 Let > be the Knuth-Bendix ordering or the lexicographic path ordering and f any binary function symbol. Then > is AC-compatible for f.

4 Examples

We present here examples of ground complete ordered rewriting systems. 4.1-4.9 are standard algebraic systems. In 4.10 we investigate combination of rewriting systems. In 4.11 we investigate an alternative ordering for which AC has a ground complete system containing two rules only, and in we give a ground complete ordered rewriting system for abelian groups.

Examples 4.2-4.9 are all ground complete for any ordering > which

1. is AC-compatible for all AC operators in the system, and

2. satisfies s > t for all rules s ⟶ t.

For examples 4.1-4.6 the Knuth-Bendix orderings and the lexicographic path orderings have the required properties. These examples were all proved ground complete using the method of section 2.2. The closure operator C was induced by 1 and 2 above.

Intuitively one reason why all the examples involving AC work is that we are doing is using a sorting algorithm. Any ground term is equal to a product of irreducibles and the AC rules (1)- (3) are sorting these irreducibles into increasing order using bubble sort. The two rule version is merely using a different sorting algorithm.

4.1 Commutativity

Let E be {x∗y = y ∗x} and > any monotonic ordering total within equivalence classes of ground terms. Then (E, >) is a ground complete ordered rewriting system. It is confluent because there are no (non-trivial) critical pairs. It is terminating since each equivalence class is finite, and so any infinite chain of rewrites would contain a loop, which would imply that > was not irreflexive.

4.2 Associativity and Commutativity

This example has been discussed in the introduction. Let E be

(x ∗ y) ∗ z ⟶ x ∗ (y ∗ z)
x ∗ y = y ∗ x
x ∗ (y ∗ z) = y ∗ (x ∗ z)

(E, >) is also ground complete if > is either of the lexicographic orderings >_{i}.

4.3 Associativity and Commutativity — Another Version

In the introduction we observed that one of the critical pairs generated by 4.2 was (z ∗ (x ∗ y), x ∗ (y ∗ z)). We may use this to obtain another three rule ground complete ordered rewriting system for AC. Let E be

(x ∗ y) ∗ z ⟶ x ∗ (y ∗ z)
x ∗ y = y ∗ x
z ∗ (x ∗ y) = x ∗ (y ∗ z)

and > any ordering which satisfies (5) and z ∗ (x ∗ y) > x ∗ (y ∗ z) if z > x. The lexicographic path ordering and the Knuth-Bendix ordering have this property.

4.4 Associativity, Commutativity, and Idempotence

Let E be

(x ∗ y) ∗ z ⟶ x ∗ (y ∗ z)
x ∗ y = y ∗ x
x ∗ (y ∗ z) = y ∗ (x ∗ z)
x ∗ x ⟶ x
x ∗ (x ∗ y) ⟶ x ∗ y.

4.5 Groups of Exponent Two

Let E be

(x ∗ y) ∗ z ⟶ x ∗ (y ∗ z)
x ∗ y = y ∗ x
x ∗ (y ∗ z) = y ∗ (x ∗ z)
x ∗ x ⟶ 1
x ∗ (x ∗ y) ⟶ y
x ∗ 1 ⟶ x
1 ∗ x ⟶ x

Then (E, >) is a ground complete ordered rewriting system for groups of exponent two.

4.6 Groups of Exponent Two in Disguise

We want to prove that the two laws

(x ∗ x) ∗ y = y
(x ∗ y) ∗ z = (y ∗ z) ∗ x  (8)

axiomatize groups of exponent two. Starting from this system, the completion procedure generated the following list of critical pairs, ordering some of them into rules:

(x ∗ y) ∗ x ⟶ y
(x ∗ y) ∗ y ⟶ x
x ∗ x = y ∗ y  (9)
x ∗ x ⟶ 1  (10)
1 ∗ x ⟶ x
x ∗ 1 ⟶ x
x ∗ (x ∗ y) ⟶ y
x ∗ y = y ∗ x
(x ∗ y) ∗ z ⟶ x ∗ (y ∗ z)
x ∗ (y ∗ z) = y ∗ (x ∗ z)

Notice that (10) is the result of “dividing” (9), i.e. introducing the new constant 1. The final set of equations (all the ones below and including (10)) is the same as in section 4.5. All the other equations are now joinable.

In [10] the same problem is attacked with the help of the term rewriting system Reve. Because (8) cannot be oriented into a rule, Reve cannot deal with it directly. Martin obtained the result by working with consequences of (8) that can be ordered.

4.7 Distributivity

Let E be

(x ∗ y) ∗ z ⟶ x ∗ (y ∗ z)
x ∗ y = y ∗ x
x ∗ (y ∗ z) = y ∗ (x ∗ z)
x ∗ (y + z) ⟶ x ∗ y + x ∗ z
(x + y) ∗ z ⟶ x ∗ z + y ∗ z

and let > be any ordering which is AC-compatible for both + and ∗. For example the lexicographic path ordering fits the bill. Then (E, >) is a ground complete ordered rewriting system.

4.8 Boolean Rings

The following is a ground complete set of ordered rewrite rules for Boolean rings.

\begin{matrix}x + y & = & y + x & x ∗ y & = & y ∗ x \\ x + (y + z) & = & y + (x + z) & x ∗ (y ∗ z) & = & y ∗ (x ∗ z) \\ x + x & ⟶ & 0 & x + 0 & ⟶ & x \\ 0 + x & ⟶ & x & x ∗ x & ⟶ & x \\ 1 ∗ x & ⟶ & x & x ∗ 1 & ⟶ & x \\ x ∗ 0 & ⟶ & 0 & 0 ∗ x & ⟶ & 0 \\ (x ∗ y) ∗ z & ⟶ & x ∗ (y ∗ z) & (x + y) + z & ⟶ & x + (y + z) \\ x ∗ (y + z) & ⟶ & x ∗ y + x ∗ z & (x + y) ∗ z & ⟶ & x ∗ z + y ∗ z \\ x ∗ (x ∗ y) & ⟶ & x ∗ y & x + (x + y) & ⟶ & y \end{matrix}

The ordering must be AC-compatible for both + and ∗. The lexicographic path ordering has these properties. Ground confluence can be checked by the technique of section 2.2.

4.9 Another System

Herewe present two similar small examples; for one our method works and for the other it does not.

Consider the equation

(x ∗ y) ∗ z = z ∗ (x ∗ y),  (11)

and any ordering > in which x ∗ y > z implies (x ∗ y) ∗ z > z ∗ (x ∗ y). The criteria of section 2.2 fail to prove ground confluence, although there is a very simple proof. The two critical pairs are

(z ∗ (x ∗ y)) ∗ u = u ∗ ((x ∗ y) ∗ z)  (12)
((x ∗ y) ∗ z) ∗ u = u ∗ (z ∗ (x ∗ y)).

Let us just consider the first one. If (x ∗ y) = z, (12) is an instance of (11). If (x ∗ y) > z or (x∗y) < z, (12) can be rewritten to (z∗(x∗y))∗u = u∗(z∗(x∗y)) or ((x∗y)∗z)∗u = u∗((x∗y)∗z), both of which are instances of (11). Again lemma 2.2 implies ground joinability. The proof for the second critical pair is practically identical.

The tests in section 2.2 cannot cope with these critical pairs because the proof of ground joinability is based on a case distinction which compares not just variables but whole subterms, namely x ∗ y and z.

On the other hand the equation

(x ∗ x) ∗ y = y ∗ (x ∗ x)  (13)

is an example of a system that our method proves ground confluent for any ordering total and well-founded on ground terms. The reason is that the only nontrivial critical pair

y ∗ ((x ∗ x) ∗ (x ∗ x)) = ((x ∗ x) ∗ (x ∗ x)) ∗ y

is an instance of (13). By lemma 2.2 this implies ground joinability.

4.10 Combination of Systems

In this section we discuss how a ground complete ordered rewriting system may be combined with a ground complete rewriting system in the usual sense.

Lemma 4.1 Suppose that

1. R is a ground complete rewriting system in the usual sense over a set of function symbols Σ and R′ = {l = r | l ⟶ r ∈ R},

2. (E, >) is a ground complete ordered rewriting system over a set of function symbols Γ,

3. there is a well-founded monotonic total ordering ≻ on T (Σ ∪ Γ) such that ≻ ⊇ > and σl ≻ σr for each rule l ⟶ r ∈ R and ground substitution σ, and

4. there are no critical pairs in the sense of definition 2.1 between E and R′ w.r.t. ≻.

Then (E ∪ R′, ≻) is a ground complete ordered rewriting system. Proof Condition 3 ensure that (E ∪ R′, ≻) is terminating. Due to condition 4 the only critical pairs of (E ∪ R′, ≻) are those of E or of R and hence are ground joinable. Thus (E ∪ R′, ≻) is ground complete. □

As a corollary we see immediately that the combination of any of the theories we have considered above with new free function symbols (so R is empty) gives a ground complete ordered rewriting system.

If R and E are both proved terminating using the lexicographic path ordering or Knuth-Bendix ordering, and assuming that the operator precedences are consistent on Σ ∩ Γ, we may obtain a total ordering ≻ by constructing a total operator precedence on Σ ∪ Γ which subsumes the two partial precedences. Thus we may combine any of the examples above with any such R.

4.11 AC with Two Rules

In this section we show how with a suitable choice of ordering two rules suffice for a ground complete AC rewriting system. Let E be

(x ∗ y) ∗ z ⟶ x ∗ (y ∗ z)
x ∗ y = y ∗ x

and > any monotonic ordering which is total on ground terms and satisfies for all ground terms x, y, z and all constants a, b

(x ∗ y) ∗ z > x ∗ (y ∗ z)
x ∗ y > y ∗ x  if x > y
a > b ∗ x  if a > b.

We show that (E, >) is ground complete. Notice that the ordering >_{2} of the previous section has the required properties. (In fact it is not hard to see that any ordering with these properties is not well-founded).

We must first prove termination. Suppose that s_{1} ⟹ s_{2} ⟹ ⋯ is an infinite chain of rewrites. Since each equivalence class is finite it must contain a loop s_{i} ⟹ s_{i+1} ⟹ ⋯ ⟹ s_{i+k} ⟹ s_{i}. But since s ⟹ t implies s > t we have s_{i} > s_{i+1} > ⋯ > s_{i}, which contradicts the definition of >. Thus (E, >) is terminating.

To prove ground confluence we first observe

Lemma 4.2 Let g and h be ground terms and let S_{w} be the multiset of all constants occurring in the term w. If g =_{E} h then S_{g} = S_{h}. Proof S_{g} is invariant when applying the equations of E. □

Then we can prove

Theorem 4.3 Let (E, >) be as above. Then

1. If w ∈ T_{G} then

w ⟹^{∗} a_{1} ∗ (a_{2} ∗ ⋯ ∗ (a_{n−1} ∗ a_{n}) …)

where S_{w} = {a_{1}, …, a_{n}} and a_{1} ≤ a_{2} ≤ ⋯ ≤ a_{n}, and this expression is irreducible.

2. (E, >) is a ground complete ordered rewriting system.

Proof

1. The proof is by induction on n = |S_{w}|. If n ≤ 2 the result is clear. Now by applying associativity we may assume w ⟹^{∗} a ∗ v where S_{v} = S_{w} − {a}. By induction we may assume that v has the required form, so that in particular v = b ∗ u, where b ≤ c for each c ∈ S_{u} = S_{v} − {b}. Now if a ≤ b we are done, so assume that a > b. Then

w ⟹^{∗} a ∗ (b ∗ u) ⟹^{∗} (b ∗ u) ∗ a ⟹^{∗} b ∗ (u ∗ a).

Now by induction u ∗ a rewrites to the required form, a_{2} ∗ (a_{3} ⋯ ∗ a_{n}), and since b < a and b ≤ c for each c ∈ S_{u} we have b ≤ a_{i} for each i = 2, …, n. So

w ⟹^{∗} a_{1} ∗ (a_{2} ∗ (⋯ ∗ a_{n})),

where a_{1} = b. It is clear that this expression is irreducible.

2. Suppose that v, w are ground and v =_{E} w. Then S_{v} = S_{w}, so by part 1

v ⟹^{∗} a_{1} ∗ (a_{2} ∗ (⋯ ∗ a_{n}))

and

w ⟹^{∗} a_{1} ∗ (a_{2} ∗ (⋯ ∗ a_{n}))

where S_{v} = {a_{1}, …, a_{n}} and a_{1} ≤ ⋯ a_{n}. Thus v and w are joinable. Hence (E, >) is ground confluent, and as it is terminating it is ground complete.

□

4.12 Abelian Groups

Let E be

x ∗ y = y ∗ x
x ∗ (y ∗ z) = y ∗ (x ∗ z)
(x ∗ y) ∗ z = x ∗ (y ∗ z)
x ∗ i(x) = 1
1 ∗ x = x
x ∗ 1 = x
x ∗ (i(x) ∗ y) = y
i(x ∗ y) = i(x) ∗ i(y)
i(i(x)) = x
i(1) = 1

and > any AC compatible ordering which orders the last seven equations from left to right for all ground terms x, y, and has

a_{1} < i(a_{1}) < a_{2} < i(a_{2}) < ⋯ < a_{n} < i(a_{n})

where the constants are a_{1}, …, a_{n}. The lexicographic path ordering with precedence ∗ < i < a_{1} < … < a_{n} will do this. We shall show that (E, >) is ground complete.

Unfortunately our automated ground confluence checking procedure fails in this case as it has to reduce arbitrary terms of the form x ∗ (y_{1} ∗ (y_{2} ∗ (⋯ (y_{n} ∗ (i(x) ∗ z) …). But we may prove ground completeness using the technique of the previous example.

If a is a constant and t is a term we define the polarity of a in t as p(a, ) : T_{G} ⟶ Z inductively as

p(a, a) = 1
p(a, b) = 0
p(a, i(x)) = −p(a, x))
p(a, s ∗ t) = p(a, s) + p(a, t)

where s and t are terms and b is any constant distinct from a. Thus for example p(a, i(i(a) ∗ (t ∗ a))) = −p(a, t).

Lemma 4.4 If g and h are ground terms with g =_{E} h then for each i p(a_{i}, g) = p(a_{i}, h).

Now we have

Theorem 4.5 Let (E, >) be as above. Then

1. If w ∈ T_{G} and w ≠_{E} 1 then

w ⟹^{∗} e_{1}^{p_{1}} ∗ e_{2}^{p_{2}} ⋯ ∗ e_{n}^{p_{n}},

(assumed associated to the right) where for each i we have p_{i} = |p(a_{i}, w)|, and e_{i} = a_{i} if p(a_{i}, w) ≥ 0, e_{i} = i(a_{i}) if p(a_{i}, w) < 0. Furthermore each such expression is irreducible.

2. (E, >) is a ground complete ordered rewriting system.

Proof

1. If w ∈ T_{G} then by applications of the last seven equations it is easy to see that

w ⟹^{∗} e_{1} ∗ (e_{2} ∗ ⋯ ∗ e_{n}) …)

where each e_{i} ∈ {a_{j}, i(a_{j}) | j = 1, …, n}. Now as a_{1} < i(a_{1}) < a_{2} < i(a_{2}) ⋯ < a_{n} < i(a_{n}) an argument similar to the previous theorem shows that we may assume e_{1} ≤ e_{2} < ⋯ < e_{n}. Now applying (7) we see that each expression of the form u ∗ (a_{i} ∗ (i(a_{i}) ∗ z)) reduces to u ∗ v, and thus

w ⟹^{∗} e_{1}^{p_{1}} ∗ e_{2}p_{2} ∗ ⋯ ∗ e_{n}^{p_{n}},

where each a_{j} is a_{j} or i(a_{j}). Now by the lemma each p_{i} = |p(a_{i}, w)|. It is clear that this expression is irreducible.

2. Since the ordering is well-founded, (E, >) is terminating.

To prove confluence suppose that u =_{E} v with u, v ground. We have by the lemma that p(a_{j}, u) = p(a_{j}, v) for each j. But then by the first part u and v are joinable. Thus (E, >) is ground confluent. □

Acknowledgements

This paper was written while the second author was at the Laboratory for Computer Science at MIT and the first author was visiting there. We would both like to acknowledge the generous hospitality of John Guttag.

References

[1] L. Bachmair, N. Dershowitz, D. Plaisted: Completion Without Failure, Proc. Coll. on Resolution of Equations in Algebraic Structures (1987).

[2] R.S. Boyer, J.S. Moore: A Computational Logic Handbook, Academic Press (1988).

[3] N. Dershowitz: Termination of Rewriting, Journal of Symbolic Computation (1987) 3, 69-116.

[4] G. Huet: Confluent Reductions: Abstract properties and Applications to Term Rewriting Systems, Journal ACM 27, 4 (1980), 797-821.

[5] G. Huet, D.C. Oppen: Equations and Rewrite Rules - A Survey, in: Formal Languages: Perspectives and Open Problems, R. Book (ed.), Academic Press (1982).

[6] J. Hsiang, M. Rusinowitch: On Word Problems in Equational Theories, Proc. ICALP’87, LNCS 267 (1987), 54-71.

[7] J.-P. Jouannaud, H. Kirchner: Completion of a Set of Rules Modulo a Set of Equations, SIAM Journal of Computing 15 (1986), 1155-1194.

[8] D. Kapur, P. Narendran, F. Otto: On Ground-Confluence of Term Rewriting Systems, to appear in Information and Computation.

[9] D.E. Knuth, P.B. Bendix: Simple Word Problems in Universal Algebras, in: Computational Problems in Abstract Algebra, ed J. Leech, Pergamon 1970, 263-297

[10] U. Martin: Doing Algebra with Reve, Report UMCS-86-10-4, Dept. of Comp. Sci., University of Manchester (1986).

[11] U. Martin: How to Choose the Weights in the Knuth Bendix Ordering, in: Rewriting Techniques and Applications, LNCS 256, 1987, 42-53.