Associative-Commutative Rewriting

1. Introduction

Term-rewrit.ing systems have been widely used in formula-manipulation and theorem-proving systems . As pro­ grams, they have a very simple syntax and semantics based on equalities, and are declarative with no explicit control. In addition , canonical systems, i.e. systems that always rewrite a term to a unique normal form , are used as decision procedures for equational theories. (For a survey of the theory and appli­ cation of rewrite systems, see Huet and Oppen [1980].)

Example: The following rewrite system differentiates an expression (Knuth [1968]):

where u and v are variables of the rewrite system and match any term, z is the symbol with respect to which an expression is differentiated, and a is any atomic symbol other than z .

Unfortunately, associativity and commutativity of func­ tions cannot be handled by including these axioms as rules. Instead, special unification algorithms are used to take associ­ ativity and commutativity into account. Let R be a rewrite system for a set of terms T(FU G), constructed from

·This work was supported in part by NSF Grant MCS 79-08497.

.. on leave rrom University or Illinois.

ASSOCIATIVE-COMMUTATIVE REWRITING*

Nachum Dershowitz Department of Computer Science Vniversity of Illinois Urbana, IL 61801

N. Alan Josephson Department of Computer Science University of Illinois Urbana, IL 61801

Jieh Hsiang Department of Computer Science State University of New York Stonybrook, NY 11794

David A. Plaisted**

Computer Science Laboratory SRI International Menlo Park, CA 94025

assoc iative-commutative function symbols F and regular sym­ bols G. The equational theory A C consists of the axioms

for each symbol JEF. A rule 1-+r in R is applied to a term lET if I matches any subterm ~ of I , under the assumption of assoc iativity and commutativity of sym bois in F, i.e. if there is a term 1 1 that is equal to I in the theory AC, and there is a substitution u for the variables of I, such that u(/)=~ for some suhterm 8 of 1 1 ·

In the next section, we describe two applications of A C­ rewriting in the context of the REVE term rewriting environ­ ment (Lescanne [1 982]}: a refutation ally complete theorem proving strategy based on a canonical rewrite system for Boolean algebra, and a programming paradigm for computing with A C arithmetic operators. In Section 3, we suggest methods for proving termination of rewrite systems contain­ ing A C operators .

2. Applications and Implementations

The Knuth-Bendix [1 970] completion procedure was introduced as a means of deriving canonical term-rewriting systems to serve as decision procedures for given equational theories. The procedure creates new rewrite rules to resolve ambiguities resulting from existing rules that overlap. The REVE environment provides an interactive mechanism for generat.ion of canonical rewriting systems, allowing the user to specify and construct (semi-automatically) any of several different orderings for completion of his system. Using com­ pletion, REVE is able to prove inductive theorems without ex plicitly invoking induction (see, for example, Huet and Hul­ lot [I 980]). An implementation of A C-rcwriting has been incorporated into the REVE term rewriting environment . To extend the system to our purposes, we have added an AC unification algorithm (Stickel [1 981 ]), and a mechanism for efficiently finding basis solutions to the linear Diophantine equations which arise from it (Huet [1978]). In addition, the completion procedure has been modified to handle associative-commutative operators (see Peterson and Stickel [1981]). We plan a series of experiments usi ng this system. In particular, we are interested in using A C unification and a complete rewrite system for Boolean algebra for refutational theorem proving and logic programming .

The following is a canonical rewrite system for Boolean algebra (Hsiang [1982], Watts and Cohen [1980]):

where ~ is 'not', t\ is 'and', V is 'inclusive-or', $ is 'exclusive-or', and ::::) is 'implies'. Both t\ and G) are impli­ citly A C operators. That means, for example, that the rule uAu-+u applied to (pAq)Ap yields pAq. Since these func­ tions are associat.ive, there is no significance to the parent.hesi­ zation, and accordingly terms are "flattened" by removing em beddings of associative functions sym bois, e.g. (pA q )A p is written pA qt\p .

That this system is sound follows from the fact that each rule is a propositional equivalence and A and G) are in fact associative and commutative. Any term that is not a sum of conjunctions is reducible, since it must either contain a symbol other than A , in which case one of the first three rules can reduce it , or else it must contain a conjunction of a sum , in which case it is reducible by the fourth rule . The methods of the following section can be used to prove termi­ nation of the rules. The system is confluent, since all its criti­ cal pairs reduce to the same term. When, as ·in this example, some of the functions on the left-hand sides of I or 1 1 are associative and commutative, then an assocaatave­ commutative unification algorithm (Livesey and Siekmann [1976] , Stickel [1981]) is used to find u such that I [uJ and I' [uj overlap. The definition of "overlap" must include cases in which two rules have overlapping subterms of the same assoc iative-commutative symbol (Lankford and Ballantyne [1977], Peterson and Stickel [1981 ]). To do this, puudo-rule6 I (I ,u 1 )-+I( r ,u') are considered for each rule whose left-hand side I has an associative-commutative outermost symbol J. All such critical pairs must reduce to the same term up to permutation of arguments of the associative-commutative symbols.

Since the Boolean algebra system is sound, terminating, and confluent, it is a canonical system for Boolean algebra and provides a means of deciding the validity of propositional equivalences. Thus, the system may be used to check for both validity and unsatisfiability of propositional terms by reducing . terms to their unique normal form: a term that reduces to true is valid, a term that reduces to false is unsatisfiabl e, w bile a term that reduces to neither is satisfiable but not valid.

In Hsiang and Dershowitz [1983] we have shown how the Boolean algebra system may be used for resolution-like theorem proving in the first-order predicate calculus. For example, adding the rule

(where I is a unary function sym hoi), and applying the A C completion procedure, generates

p(z,fz)Ap(fz,z) --+ p( z ,a )A p(z ,z )A p(z ,z )$true --+ p(z ,a)$true true p( a ,a)$ true true false --+ true, proving that (V y )(Jz )~[p( z ,y )==(V z )~(p(z ,z )A p(z ,z ))] is valid.

Rewrite systems may be used as "logic programs" (Kow Iaski [197 4]), in addition to their straightforward use for computation by rewriting. The programming paradigm described below allows for the advantageous combination of both computing modes. The result is a Prolog-like program­ ming language the main differences being that rewrite rules are equivalences, rather than implications in Horn-clause form , and that the completion procedure acts as the inter­ preter, rather than resolution. Hogger [1981] suggested the use of equivalences to specify Prolog programs.

For example , the following is a program to compute the quotient and remainder of two integers:

where + is associative and commutative. The first rule is the main recursive case; the second is the main base case; the third simplifies sums; the remainder are special cases. For example, to compute the quotient and remainder of the two numbers 7 and 3 with this system (the numerals are just abbreviations for their unary representation as sums of ones), the rule

is added, meaning that q are r are the answer if and only if they are the quotient and remainder, respectively, of 7 and 3. The A C complet ion procedure then generates the rules:

div(4,3,q ,r) div( 1 ,3,q ,r) ana(2,1) --+ ana(q+ I,r) ana(q+ 2,r) --+ true,

where the ana predicate contains the answer values 2 and 1 for q and r, respectively.

3. Termination

The usual methods for proving termination of rewrite systems are frequently difficult to apply in the presence of associat ive and commutative symbols. Since AC completion requires an ordering for associative-commutative terms, it is important that we investigate such orderings. This section presents methods for proving termination of term-rewriting systems containing implicitly A C function symbols.

3.1. Characterization of AC Orderings

The following lemma is straightforward. (It is slightly stronger in the interest ing direct ion than the method 1n Manna and Ness [1970]):

Lemma 1 . A rewrite 8y~tem R over a ut of term~ T terminates, if and only if there exists a well-founded set ( W , >) and a function T mapping term~ from T into W , such that

Let t denote t he fl attened version of a term t , with all nested occurrences of symbols in F stripped , and where t he order of arguments of symbols in F is not significant. Two terms u and v are equal in A C, if and only if tT and IT are the same. Let T'={t:tET}. We assume that R includes pseudo - rules f (I ,x )-+ f ( r , .1 ) . where x is a variable otherwise not occurring in the rule, for each rule 1-+r in R whose left­ hand side I or right-hand side r has outermost associative­ commutative symbol JEF or whose right-hand side is just a variable. For example, the rule x $ 0-+x in the Boolean alge­ bra system implies the two pseudo-rules x $0$ u-+x $ u and (x$0)!\u-+xt\u . (We are including more pseudo-rules than necessary for "compatibility." See Peterson and Stickel [April 1981] .)

Theorem 1. An A C rewrite ~y~tem R terminate~, if and only if there exi~t~ a well-founded ordering > on T' wch that

for rr, ITE 7", and

for each rule and p~eudo-rule 1-+r of R.

3.2. Unsuccessful Extensions

A mu/tiut is a set along with a multiplicity assigned to each element. Any ordering >' on terms can be extended to a mu/tiset ordering on terms >>' in the following way (Dershowitz and Manna [1979]):

Given an ordering > on function symbols, the recur~ive path ordering > rpo on terms containing those sym bois is defined as follows (Plaisted [1978], Dershowitz [1982]): For two terms

The following unsuccessful extensions of the recursive path ordering indicate some of the difficulties in finding useful A C orderings.

Consider two AC operators f and g with f >g . We , certainly have /(a ,b)>rpog(a ,b) . However, we cannot

1. > rpo on fl attened terms. show that f(a ,b,c )>,po/(g(a ,b) ,c).
2. >rpo on flattened terms , refining operators by their arity. Consider two A C operators f and g with f >g . Although we have /(a ,b)> rpo g( a ,b), we cannot show g(f (a ,b ),c )> rpo g( a ,b ,c ).
3. >rpo on flattened t-erms, eliminating ident ical subterms. Consider one function symbol f with f >a> b > c >d. This ordering however is not well-founded: / ( b ,b ,c )> rpo/ (a ,C)> rpo /(a ,d)> rpo / ( b ,b ,c) .
4. > rpo on flattened terms, looking at powersets or sub-
5. terms . ' Considering the collection of terms that can be obtained from a term f(s 1 , · · · ,sm) by deleting subterins also does not give a valid ordering.
6. Polynomial Interpretations Since addition and mul­ tiplication are themselves associat ive and commutative, poly­ nomi al interpretations, as used , for example, in Lankford [1975], are sometimes helpful. For example, to show termina­ tion of the Boolean algebra example, it is easi ly verified that r(l)>r(r) for each of the rules and pseudo-rules 1-+r , .where T(x) is defined inductively on the structure or x:

and a is any atomic symbol, including 0 and I.

. 3.4. Semantic Path Ordering

Intuitively , the Boolean algebra syst em terminates, since distributivity does, and the other rules only simplify matters. The following ordering attempts to capture that intuition.

Let p( t) be some function mapping terms t into the natural numbers (or any well-founded set) and let > be a well-founded ordering of the function symbols, one of which we denote ®. The umantic path ordering (Kamin and Levy [l 980]) is an extension of the recursive path ordering and is defined recursively as follows:

s=f(s 1 · · · sm)>,pog{t 1 · · · ln)=t if and only if 8 >,potj, j=l, · · · ,n and one the following holds: f >g or [f=g=®!\p(8)>p(t)J or 8;?:.,pot for some i=l, · · · ,m or or (f=g=®!\p(s)=p(t)) and {s 1 · · · sm}>>,po{tl ···In}

Kamin and Levy [l 980] have shown that if

holds for all f, then a semantic recursive ordering (such as the above one) is well-founded and satisfies the monotonicity condition of Theorem l.

The difficulty of using this method lies in picking p( I) and in checking condition ( · ). For the Boolean algebra exam­ ple, let !\ > $ > 1 >O. We can prove the termination of the first four rules (including distributivity) by taking ® to be!\ and p( I 1 /\ · · · !\In) to be n. We can then prove the termina­ tion of the complete system by taking ® to be !\, again, and p( t) to be the length of the longest derivation from I using those first four rules. That requires verifying that ( ·) holds and , for each rule or pseudo-rule 1-+r, we have l>,por.

3.5. Associative Path Ordering

In the recursive path ordering, to show s > rpo I, it is sometimes necessary to show that a given subterm of s is greater than more than one subterm of I, but it is never necessary to show that a given subterm of t is less than more than one subterm of 8. Therefore, if we transform s and I and can make choices in the transformations, it is easy to show that for all choices for s there is a choice for I such that 8 > t. However, it is much harder to show the reverse (for all choices for I there is a choice for s such that s >I). With this motivation, we define the auociative path ordering as fol­ lows: With term t we associate a set M( I) of transforms of I. We say s > apo t in the associative path ordering if VuEM(s) ]vEM(t) u>rpov. Thus, the sets M(t) are ordered by their small elements. M( I) is formed by succes­ sively applying three transforms to the "flattened" version of I. (Note that during flattening, f(u) is replaced by u when f is associative.) The role of M 1 is to transform subterms, of M 2 to transform terms at the top level, and of M 3 to again transform subterms. Composing the three operations, we get M(t) = M 3 (M 2 (M1(T))) . The transforms are given by:

where

if g is not associative or no subterm v; bas function symbol f for which g > f; otherwise,

if v;= f ( s 1 , ··· , s, ), g and f are associative, g > f, where g( ... , ... ) appears as an argument k- 1 times;

if v;=f(s 1 , · ·· , s,), g is associative, f is not associative, and g>f.

For example, F(g(c,d})={c(d),d(c)} if g>c,d and g is asso­ ciative.

Example: Consider the Boolean algebra system. Using the ordering 1 ,a ,b ,c >0>1\ > $ (i.e. constants are big), validates a$ a-+0 since the ordering on function symbols implies x?:. opo 0 for any term x. (Making constants large is, in fact, necessary for > opo to work on this example.) Transforming the left and right hand sides of the distributivity rule yields

Thus a/\ ( b $ c) > opo (a!\ b) $ (a!\ c), and this rule, too, is a reduction. Similarly, for the other rules and pseudo-rules.

Proposition . The ordering > opo is well-founded since it satisfies the conditions for simpl·fication ord­ erings, as defined in Dershowitz {1982].

Note that the condition VuE M( 8) ]vEM( I) u > rpo v depends only on the minimal elements of M( s) and M( t ). Hence we need only compute minimal elements of M( t) at each step (including subterms of I). This can greatly speed up the computations. In fact , if the ordering on operators is total, only one minimum element need be kept. We have implemented the associative recursive path ordering and are making it interactive for A C completion in REVE and are working on comparing terms with variables in > opo.