Associative-Commutative Reduction Orderings

Leo Bachmair

MPI–I–91–209 November 1991 Author’s Address

Department of Computer Science, State University of New York at Stony Brook, Stony Brook, New York 11794, U.S.A., leo@sbcs.sunysb.edu

Publication Notes

The present report has been submitted for publication elsewhere and will be copyrighted if accepted.

Acknowledgements

I wish to thank Harald Ganzinger for his comments on a preliminary version of this paper. This research was supported in part by the National Science Foundation under grant CCR-8901322.

Abstract

Rewrite systems are sets of directed equations used to compute by repeatedly replacing subterms in a given expression by equal terms until a simplest form possible (a normal form) is obtained. If a rewrite system is terminating (i.e., allows no infinite sequence of rewrites), then every expression has a normal form. A variety of orderings, called reduction orderings, have been designed for proving termination, but most of them are not applicable to extended rewrite systems, where rewrites take into account inherent properties of given functions such as associativity and commutativity. In this paper we show how an ordering represented as a schematic rewrite system—the lexicographic path ordering— can be systematically modified into an ordering compatible with associativity and commutativity.

Keywords

Termination orderings, rewrite systems, automated deduction.

1 Preliminaries

We consider first-order terms built from given function symbols and variables. With each function symbol f we associate a set α(f) ⊆ N that indicates the number of arguments f may take. A syntactically well-formed term is an expression f(X), where X is a sequence of terms t_{1}, …, t_{n} with n ∈ α(f). The length of a term f(X) is defined by |f(X)| = 1 + ∑_{t∈X} |t|. We say that s is a subterm of t = f(X) if either s = f(Y), for some sequence Y ⊆ X,^{1} or else s is a subterm of some term u ∈ X. If s ≠ t we speak of a proper subterm. For example, if {2, 3} ⊆ α(f), then f(a, c) is a subterm of f(a, b, c).

A rewrite rule is a pair of terms, written s → t. A rewrite system is a set of rewrite rules. A binary relation → on terms is called a rewrite relation if s → t implies f(X, sσ, Y) → f(X, tσ, Y), for all terms s, t, and f(X, s, Y), and substitutions σ. By ← we denote the inverse of → and by →^{+} and →^{∗} the transitive and transitive-reflexive closure of →, respectively. By →_{R} we denote the smallest rewrite relation containing the rewrite system R. We say that t is derivable from s if s →_{R}^{+} t; and write s →_{R}^{!} t if s →_{R}^{∗} t and there exists no term t′ such that t →_{R} t′ (then t is also called a normal form). A rewrite system R is called terminating if there exists no infinite sequence t_{1} →_{R} t_{2} →_{R} t_{3} · · · .

An (rewrite) ordering is an irreflexive and transitive (rewrite) relation. Well-founded rewrite orderings are called reduction orderings.^{2} Evidently, a rewrite system terminates if and only if it is contained in some reduction ordering. A widely used ordering is the lexicographic path ordering, which can be defined as the derivability relation induced by the following recursively defined rewrite system LP O:

f(X) → s  if s ∈ X
f(X) → g(Y) if f ≻ g and f(X) →_{LP O} t, for all
t ∈ Y
f(X, s, Y) → f(X, t, Z) if s →_{LP O} t, |Y | = |Z|, and
f(X, s, Y) →_{LP O} u, for all u ∈ Z

where ≻ is a well-founded ordering on function symbols (called a precedence). Rules of the form f(X) → s are called subterm rules; rules f(X) → g(Y), combination rules; and rules f(X, s, Y) → f(X, t, Z), lexicographic rules.

Rewrite systems are often used to model functions that satisfy certain identities. For instance, the associativity and commutativity of a function symbol f can be described by the rewrite rules

f(s, f(t, u)) → f(f(s, t), u)
f(f(s, t), u) → f(s, f(t, u))
f(s, t) → f(t, s)

which induce a non-terminating rewrite relation and therefore are dealt with in a special way.

The rewrite system R/S consists of all rules u → v such that u →_{S}^{∗} u′ →_{R} v′ →_{S}^{∗} v, for some terms u′ and v′. We consider the problem of proving termination of rewrite systems R/AC, where AC is a set of associativity and commutativity rules. A reduction ordering ≻ is called ACcompatible if s ↔_{AC}^{∗} u ≻ v ↔_{AC}^{∗} t implies s ≻ t, for all terms s, t, u, and v. Since the two relations →_{AC} and ↔_{AC} are identical, a rewrite system R/AC terminates if and only if R is contained in some AC-compatible reduction ordering.

1We write Y ⊆ X to indicate that X is a sequence t_{1}, …, t_{n} and Y a sequence t_{i_{1}}, …, t_{i_{k}}, where 1 ≤ i_{1} < ⋯ < i_{k} ≤ n

2For a detailed discussion of reduction orderings see the survey by N. Dershowitz, J. Symbolic Computation 3(1987):69-116.

Unfortunately, most reduction orderings are not AC-compatible. For example, if f ∈ AC^{3} and a ≻ b, then f(b, a) ↔_{AC} f(a, b) →_{LP O} f(b, a), but of course f(b, a) ↛_{LP O}^{+} f(b, a). We shall design a variant of the lexicographic path ordering in which lexicographic rules are restricted to function symbols f ∉ AC and terms are compared only after they have been converted to a suitable normal form.

2 Transformation

Let AC be a set of associativity and commutativity rules. Henceforth, we shall assume that α(f) = {2, 3, 4, …}, if f ∈ AC, and α(f) is a singleton, otherwise. By F′ we denote the set of all rewrite rules of the form

f(X, f(Y)) → f(X, Y), f ∈ AC, |X| ≥ 1, |Y | ≥ 2;

by ∼ the (symmetric) rewrite relation generated by all rules

f(X, u, Y, v, Z) ↔ f(X, v, Y, u, Z), f ∈ AC;

and by F the rewrite system F′/∼. The rewrite system F is length-decreasing and terminates; its rules are called flattening rules. We also say that s′ is a flattened version of s if s →_{F}^{!} s′. The relation ∼ is called the permutation congruence. Flattened versions of equivalent terms are unique up to permutation:

Lemma 1 If s′ ←_{F}^{!} s ↔_{AC}^{∗} t →_{F}^{!} t′, then s′ ∼ t′.

If L = L′/ ∼ is a rewrite system, we define the relation ≻_{L|_{F}} by: u ≻_{L|_{F}} v if u →_{F}^{!} u′ →_{L/F}^{+} v′ ←_{F}^{!} v. In general, such “transformed relations” ≻_{L|_{F}} are not rewrite relations.

For example, if f ≻ g and f ∈ AC, then f(a, b) →_{LP O} g(a, b), but f(f(a, b), c) →_{F}^{!} f(a, b, c) ↛_{LP O} f(g(a, b), c). Observe that the term f(f(a, b), c), but not its flattened version f(a, b, c), can be rewritten by LP O. To address this problem we shall extend LP O to a rewrite system L with which flattened terms can be rewritten, if necessary.

3 Commutation

We say that a rewrite system S commutes with T if for all terms u, v, and u′ with u′ ←_{T} u →_{S} v, there exists a term v′, such that u′ →_{S/T}^{+} v′ ←_{T}^{∗} v.^{4}

Proposition 1 Let AC be a set of associativity-commutativity rules, F be the corresponding set of flattening rules, and L = L′/ ∼ be a rewrite system. If L/F terminates and L commutes with F, then ≻_{L|_{F}} is an AC-compatible reduction ordering.

3We write f ∈ AC if AC contains the respective rules for f.

4Similar commutation properties have been discussed by L. Bachmair and N. Dershowitz, Proc. Eighth Int. Conf.

on Automated Deduction, Lect. Notes in Computer Science vol. 230, pp. 5–20, Berlin: Springer-Verlag.

Proof. It can easily be seen that ≻_{L|_{F}} is AC-compatible and well-founded. Furthermore, we may use induction on →_{L∪F}^{+} to prove that for all terms u, u′, and v with u′ ←_{F}^{!} u →_{L/F}^{+} v, there exists a term v′, such that u′ →_{L/F}^{+} v′ ←_{F}^{∗} v. (Note that L ∪ F is terminating, as both L/F and F are terminating.) ¿From this one can easily derive that ≻_{L|_{F}} is a rewrite relation. □

For the purpose of extending LP O to a rewrite system L that commutes with F we analyze so-called “critical peaks” between L and F. For instance, a term f(X, f(Y)) can be rewritten in two different ways, which produces the peak

f(X, Y) ←_{F} f(X, f(Y)) →_{LP O} f(X, y)

where f ∈ AC, |X| ≥ 1, |Y | ≥ 2, and y ∈ Y. We include the rule

f(X, Y) → f(X) if f ∈ AC, |X| ≥ 2, and |Y | ≥ 1

in L to ensure that f(X, Y) →_{L} f(X, y). Similarly, the peak

f(X, Y) ←_{F} f(X, f(Y)) →_{LP O} f(X, g(Z)),

where f ∈ AC, f ≻ g, |X| ≥ 1, |Y | ≥ 2, and f(Y) →_{LP O} t, for all t ∈ Z, results in a rule

f(X, Y) → f(X, g(Z)) if f ∈ AC, f ≻ g, |X| ≥ 1, |Y | ≥ 2,
and f(Y) →_{LP O} t, for all t ∈ Z.

We shall see that these two new rules already ensure commutation.

Let L be the rewrite system L′/ ∼, where L′ is the following recursively defined set of rules:

f(X) → s  if s ∈ X
f(X) → g(Y) if f ≻ g and f(X) →_{L′/∼} t, for all
t ∈ Y
f(X, s, Y) → f(X, t, Z) if f ∉ AC, s →_{L′/∼} t, |Y | = |Z|, and
f(X, s, Y) →_{L′/∼} u, for all u ∈ Z
f(X, Y) → f(X)  if f ∈ AC, |X| ≥ 2, and |Y | ≥ 1
f(X, Y) → f(X, g(Z)) if f ∈ AC, f ≻ g, |X| ≥ 1, |Y | ≥ 2,
and f(Y) →_{L′/∼} u, for all u ∈ Z

Rules of the form f(X, Y) → f(X) are called AC-subterm rules; rules f(X, Y) → f(X, g(Z)), AC-combination rules.

Proposition 2 The rewrite system L commutes with F.

Proof. Let s, t, and s′ be terms with s′ ←_{F} s →_{L} t. We use induction on |s| + |t| + |s′| to prove that there exists a term t′, such that s′ →_{L} t′ ←_{F}^{∗} t. There are several cases according to the rule applied in s →_{L} t. We discuss one representative case: application of a combination rule. There are several subcases.

(a) Suppose f(X′) ←_{F} f(X) →_{L} g(Y), where f ≻ g and f(X) →_{L} u, for all u ∈ Y. Since f(X′) ←_{F} f(X) →_{L} u, for all u ∈ Y, we may apply the induction hypothesis to infer that for each u ∈ Y there exists a term u′ with f(X′) →_{L} u′ ←_{F}^{∗} u. Let Y′ be the sequence obtained from Y by replacing each term u by the corresponding term u′. Then f(X′) →_{L} g(Y′) ←_{F}^{∗} g(Y), which proves this subcase.

(b) If the peak is of the form f(X, Z) ←_{F} f(X, f(Z)) →_{L} g(Y), where f ≻ g and f(X, f(Z)) →_{L} u, for all u ∈ Y, then we may again use the induction hypothesis to infer that for each term u ∈ Y there exists a term u′, such that f(X, Z) →_{L} u′ ←_{F}^{∗} u. Thus f(X, Z) →_{L} g(Y′) ←_{F}^{∗} g(Y), where Y′ is obtained from Y by replacing each term u by u′.

(c) For each peak f(X, Z) ←_{F} f(X, f(Z)) →_{L} f(X, g(Y)) we have f(X, Z) →_{L} f(X, g(Y)) by virtue of an AC-combination rule.

The two remaining subcases–application of a combination rule either within the variable part of a flattening rule or at a disjoint subterm–are trivial. Applications of other rules are dealt with in a similar fashion. □

The following lemmas are useful for proving termination of L/F (or L ∪ F).

Lemma 2 If g(X) →_{L∪F} t →_{L∪F}^{n} f(Y) and g ⪰̸ f, then there exist a term u ∈ X and a number k with n ≥ k, such that g(X) →_{L} u →_{L∪F}^{k} f(Y).^{5}

Proof. Use induction on (n, |t|), considering all possible cases of rewrites g(X) →_{L∪F} t. □

Lemma 3 If f ∈ AC, |Z| ≥ 1, and f(X) →_{L∪F} t →_{L∪F}^{n} f(Y), then there exists a term u, such that f(X, Z) →_{L∪F} u →_{L∪F}^{∗} f(Y, Z) and |f(t, Z)| ≥ |u|.

Proof. Similar to the previous lemma, by induction on (n, |t|). □

4 Termination

Suppose L ∪ F is not terminating. We define an infinite sequence of rewrites t_{0} →_{L∪F} t_{1} →_{L∪F} t_{2} ⋯ as follows. Let t_{0} be a shortest term from which there is an infinite sequence of rewrites. Once the term t_{n} has been determined, let t_{n} →_{L∪F} t_{n+1} be any minimal rewrite such that there is an infinite sequence of rewrites from t_{n+1}. Here a rewrite u →_{R} v is considered to be smaller than a rewrite u →_{S} v′ if either |v′| > |v| or else |v| = |v′|, R = L, and S = F. By S we denote the set consisting of all proper subterms of terms t_{i}, i ≥ 0, and terms derivable from them.

Lemma 4 There is no infinite sequence of rewrites from any term in S.

Proof. Evidently, there is no infinite sequence of rewrites from any proper subterm of t_{0}. Suppose there is an infinite sequence of rewrites from some proper subterm t of t_{i+1}, but from no term that is (derivable from) a proper subterm of t_{i}. We consider several cases, depending on which rule is applied in the rewrite t_{i} →_{L∪F} t_{i+1}.

If t_{i} ∼ f(X, f(Y)) →_{F} f(X, Y) ∼ t_{i+1}, then t ∼ f(X′, Y′), where X′ ⊆ X, Y′ ⊆ Y, and |X′| ≥ 1. If X′ ≠ X, then

f(X′, f(Y)) →_{L} f(X′, Y) →_{L} f(X′, Y′)

and hence t is derivable from a proper subterm of t_{i}, which is a contradiction. Suppose X′ = X. If Y′ ≠ Y and |Y′| ≥ 2, then f(X, f(Y)) →_{L} f(X, f(Y′)) is a smaller rewrite than f(X, f(Y)) →_{F} f(X, Y) (because |f(X, Y)| ≥ |f(X, f(Y′)|), which together with f(X, f(Y′)) →_{L} f(X, Y′) yields a contradiction. Finally, if |Y′| = 1, then t can be derived from t_{i} in one step (because f(X, f(Y)) →_{L} f(X, u), for all u ∈ Y), which is a contradiction.

5We write s →^{n} t to denote a sequence of n rewrites.

Similar arguments can be applied in other cases. □

The lemma shows that the restriction ≻_{S} of the rewrite relation →_{L∪F}^{+} to terms in S is wellfounded. The lemma also indicates that no term t_{i+1} is a proper subterm of t_{i}. Thus, if t_{i} is written as f_{i}(Y_{i}), then f_{i} ⪰ f_{i+1}, for all i ≥ 0. Since the precedence ≻ is well-founded, we may infer that f_{j} = f_{j+1} = f_{j+2} = ⋯, for some j ≥ 0. Let s_{i} denote the term t_{j+i} and suppose s_{i} is of the form f(X_{i}), for all i ≥ 0.

The sequence s_{0} →_{L∪F} s_{1} →_{L∪F} s_{2} →_{L∪F} ⋯ contains infinitely many rewrites where a rule in L ∪ F is applied at the top. If f ∉ AC, then only lexicographic rules can be applied at the top. and the sequence X_{0}, X_{1}, … is lexicographically decreasing with respect to ≻_{S}, which is a contradiction. If f ∈ AC, then only flattening and AC-combination rules can be applied at the top. (There have to be infinitely many applications of flattening, as AC-combination rules strictly decrease the number of top-level subterms.)

Now let us assign a status to the elements of X_{k}, for all k ≥ 0. All terms in X_{0} are free, and corresponding terms in X_{k} and X_{k+1} have the same status. Furthermore, if X_{k+1} = (X_{k} \{f(Y)})∪ Y, then all terms in Y are free (application of a flattening rule at the top introduces free terms); if X_{k+1} = (X_{k} \ Y) ∪ {g(Z)}, where |Y | ≥ 2, then g(Z) is bound (application of an AC-combination rule at the top introduces a bound term); and if X_{j+k+1} = (X_{j+k} \ {u}) ∪ {v}, then v has the same status as u. Observe that bound terms can only be introduced by AC-combination rules.

We claim that whenever there is a rewrite

s_{k} ∼ f(X, f(Y)) →_{F} f(X, Y) ∼ s_{k+1},

then f(Y) is free. For if f(Y) is bound, it must have been derived from some term g(Z′) that had previously been introduced in a rewrite

s_{l−1} ∼ f(X′, Z) →_{L} f(X′, g(Z′)) ∼ s_{l},

where k > l, |Z| ≥ 2, f ≻ g, f(Z) →_{L} u, for all u ∈ Z′, and f(X′, Y) →_{L∪F}^{∗} f(X, Y). Using Lemmas 2 and 3 we may infer that f(Z) →_{L} u →_{L∪F}^{∗} f(Y), for some u ∈ Z′, and f(X′, Z) →_{L∪F} u′ →_{L∪F}^{∗} f(X′, Y), for some term u′ with |f(X′, g(Z′))| > |f(X′, u)| ≥ u′, which contradicts the minimality of the rewrite s_{l−1} →_{L} s_{l}.

Finally, for each term s_{k} we define a finitely-branching (labeled) tree T_{k} as follows. The tree T_{0} consists of a root labeled with the symbol ⊤ and |X_{0}| successor nodes labeled by the elements of X_{0}. The tree T_{k+1} is obtained from T_{k} as follows: if X_{k+1} = (X_{k} \ {f(Y)}) ∪ Y, then new nodes labeled with the terms in Y are added as successors to the leaf f(Y); if X_{k+1} = (X_{k} \ Z) ∪ {g(Y)}, where |Z| ≥ 2, then a single successor node labeled with the symbol ⊥ is added to each leaf representing a term in Z; if X_{k+1} = (X_{k} \ {u}) ∪ {v}, where u is free, then v is added as a successor to u. Note that each free term in X_{k} is represented by some leaf in the tree T_{k}. Furthermore, T_{k} ≠ T_{k+1} whenever the rewrite s_{k} →_{L∪F} s_{k+1} is by application of a rule at the top. Thus, T_{∞} = ⋃_{i} T_{i} is an infinite tree and, by König’s Lemma, contains an infinite branch. On the other hand, if v is the label of a successor of a node labeled by u, then u ≻_{S} v (assuming ⊤ and ⊥ represent maximum and minimum elements, respectively). The existence of an infinite branch therefore contradicts the well-foundedness of ≻_{S}.

In summary, we have proved:

Proposition 3 The rewrite system L ∪ F is terminating.

As a corollary to Propositions 1, 2, and 3 we obtain:

Theorem 1 The relation ≻_{L|_{F}} is an AC-compatible reduction ordering.

It can easily be proved that the ordering also satisfies the subterm property (i.e., t[s] ≻_{L|_{F}} s, for all terms t and proper subterms s of t) and hence is a simplification ordering. We have thus also established that the lexicographic path ordering is a simplification ordering (this being the special case where AC = ∅.)

We conclude this section with an example. Let R be the rewrite system

x + 0 → x
x + y′ → (x + y)′
x ∗ 0 → 0
x ∗ y′ → x + (x ∗ y)
(x + y) ∗ z → (x ∗ z) + (y ∗ z)

and ≻ be a precedence in which ∗ ≻ + ≻ ′ ≻ 0. Then R is contained in ≻_{L|_{F}} and hence R/AC is terminating.

5 Summary

We have illustrated by way of the lexicographic path ordering how to systematically modify a reduction ordering so as to obtain an ordering compatible with associativity and commutativity. The modification is guided by the requirement of establishing certain commutation and termination properties and employs standard techniques of term rewriting, such as an analysis of critical peaks. The specific ordering we have obtained essentially corresponds to an ordering introduced by Kapur, Sivakumar, and Zhang.^{6} (The main difference is in the presentation: we describe an ordering via a schematic rewrite system, while Kapur et al. present an algorithm for computing the corresponding rewrite relation. The various operations used in their algorithm—“partitioning,” “pseudo-copying,” “elevating,” etc.—correspond to sequences of rewrites by L/F.)

We believe that the above approach to designing reduction orderings can be applied in other contexts as well, e.g., to rewrite systems R/AC1 where AC1 is a set associativity, commutativity, and identity axioms. The associative path ordering^{7} can also be formulated in this framework. This ordering differs from the above ordering in that commutation of the peak

f(X, Y) ←_{F} f(X, f(Y)) →_{LP O} f(X, g(Z))

6Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science, 1990.

7L. Bachmair and D. Plaisted, J. Symbolic Computation 1(1985):329-349.

is achieved, not by introducing AC-combination rules, but by enriching F with “distributivity rules”

f(X, g(Z)) → g(f(X, t_{1}), …, f(X, t_{n})),

where f ≻ g and Z = t_{1}, …, t_{n}. Certain restrictions on the precedence ensure that the corresponding ordering ≻_{AP O} is indeed a reduction ordering. (The main difficulty consists in establishing a suitable commutation property, while termination is straightforward.) The ordering ≻_{L|_{F}} imposes no such restrictions, but has the disadvantage that certain terms can not be compared, e.g., f(a, c) and f(b, b), where f ∈ AC and a ≻ b ≻ c. The associative path ordering, on the other hand, allows for more flexible comparisons of arguments of associative-commutative function symbols, so that f(a, c) ≻_{AP O} f(b, b). Similar extensions of the rewrite system L that would allow for such comparisons result in non-terminating rewrite systems. It is an open question whether there exist any precedence-based AC-compatible reduction orderings so that two ground terms are either equivalent with respect to AC or else are comparable.^{8}

8There are orderings with these properties, but they are not precedence-based, see P. Narendran and M. Rusinowitch, Proc. Fourth Int. Conf. on Rewrite Techniques and Applications, Lect. Notes in Comp. Scie. vol. 480, pp. 423–434, Berlin: Springer-Verlag.