Equational Reasoning using AC Constraints

1 Introduction

Knuth-Bendix completion [Knuth and Bendix, 1970] and its extensions [Bachmair et al., 1989] have been widely used for equational reasoning. One of the main bot­ tlenecks of completion-based inference strategies is the large number of critical pairs generated. This is particu­ larly evident when dealing with equational problems in­ volving associative and commutative functions, i.e. AC equational problems. In this paper, we present a tech­ nique for reducing redundant equational inferences using constraints.

AC equational problems represent an important class of problems in theorem proving. Many mathematical functions of interest are associative and commutative. For example, the union and intersection operations in set theory and the addition operations in ring structures are all associative and commutative. Furthermore, addi­ tion and multiplication in arithmetic are both AC. Some form of AC equational reasoning is necessary if a term rewriting system is used to perform integer arithmetic.

AC equational reasoning is often difficult. One of the most recognized recent successes of automated reason­ ing, perhaps of AI in general, is the solution of the Rob­ bins Problem. The Robbins Problem is in fact formu­ lated as an equational problem with AC functions [Mc­ Cune, 1996] . Most term rewriting systems do inferences by generating rewrite rules using Knuth-Bendix comple­ tion or unfailing completion. Associativity axioms and commutativity axioms often cause an explosion of new rewrite rules in the completion process. When over­ lapped with the AC axioms, an existing rewrite rule can generate an exponential number of AC equivalent rewrite rules. Since commutativity axioms cannot be oriented in any termination ordering, many of these new rewrite rules generated from the AC axioms cannot be simplified.

Special completion procedures are developed to han­ dle AC equational problems [Lankford and Ballantyne, 1977; Peterson and Stickel, 1981]. Most of the ap­ proaches in the literature use flattened terms. For exam­ ple, +(a, +(b, c)) is represented as +(a, b, c) , and terms +(a, c, b) and +(a, b, c) are considered identical. A flat­ tened term represents all terms equivalent up to the AC axioms. Since flattening breaks the original term structure, special unification techniques are needed. AC unification algorithms [Stickel, 1981; Domenjoud, 1991; Boudet et al., 1996] are developed to compute all possible most general unifiers of two terms up to associativity and commutativity axioms. Special AC termination order­ ings are also needed to show termination of AC rewriting systems. Many commonly used orderings, such as recur­ sive path ordering and lexicographic path ordering, are no longer well founded when flattened terms are used. Several AC termination ordering have been devised [Dershowitz et al., 1983; Bachmair and Plaisted, 1985; Kapur et al., 1990] .

We study the problem of AC equational reasoning with a different approach. We propose a procedure called consistent unfailing completion in which only consistent rules and equations are used for critical pair generation and rewriting. A consistent unfailing completion proce­ dure can be regarded as the lifted version of a ground completion procedure. In a standard unfailing comple­ tion procedure, some rewrite rules do not correspond to any rewrite rules in the ground procedure. We call such rules inconsistent. In consistent unfailing completion, inconsistent rules are replaced by its consistent permu­ tations. For example, x * y * x -+ x is inconsistent with respect to the lexicographic ordering. This is because a1 * a1 * a2, an arbitrary instance of x * y * x, is either simplified to a1 * a1 * a2 or a 2 * a 1 * a1 depending on the ordering of a 1 and a2. y * x * x -+ x and x * x * y -+ x are the only two consistent permutations of x * Y* x -+ x . We derive two sufficient conditions for detecting inconsistent rules. Consistency checking based on these conditions greatly reduces the number of critical pairs generated. In the examples that we tested, it shows a factor of 2 to 4 reduction. Our implementation of the algorithm is able to solve all six of equality benchmark problems proposed by [Lusk and Overbeek, 1985].

Consistent unfailing completion does not require the use of flattened terms. AC unification is therefore not needed. Detecting inconsistency takes quadratic time and generating consistent permutations takes single ex­ ponential time. Thus the worse case complexity of an inference rule in consistent unfailing completion is single exponential. The worse case complexity for AC unifi­ cation is double exponential. A special AC termination ordering is not needed either. Consistent unfailing com­ pletion works for most of the commonly used orderings, such as recursive path ordering, lexicographic path or­ dering, etc. In fact, we have a built-in ordering in our implementation, and all of our examples are solved us­ ing the same ordering. The built-in ordering enables us to fully automate the equational reasoning process and incorporate it in a general first-order theorem prover.

The rest of the paper is organized as follows. We pro­ vide some background in the next section. We then present the consistent unfailing completion algorithm and show its completeness. We then show how the al­ gorithm can be refined and implemented. We give some test results in the end.

2 Background

In this section, we define some relevant concepts. For surveys on equational reasoning, see [Plaisted, 1993; Dershowitz and Jouannaud, 1990; Klop, 1992]. For in­ troductions to the area of theorem proving, see [Chang and Lee, 1973; Loveland, 1978; Wos et al., 1984]. We follow the conventions of [Plaisted, 1993] in this paper.

We use the standard definitions of term, substitution, instance, the most general unifier etc. Readers may con­ sult the aforementioned references for more details. We use/, g, h, ... as function symbols, a, b, c, ... as constant symbols, and x , y, z , . .. as variables.

An equation is an expression of the form s = t where s and t are terms. An equational system is a set of equations. Assume E is an equational system, we use E f= s = t to represent that s = t is a logical conse­ quence of E . The problem of equational reasoning can be reduced to the problem of first-order theorem prov­ ing. Ef=s=tiff{EUAE}h s=t,where AEisthe set of equality axioms and L is any sound and complete first-order strategy. In practice, term rewriting based approaches are often much more efficient.

A rewrite rule is written as r -+ s, where r and s are terms. A rule r -+ s indicates that an instance of r can be replaced by an instance of s, but not vice versa. r H s if r -+ s or s -+ r . ·Sometimes r -+ s is also rewritten as s t- r. A term rewriting system R is a set of rewrite rules. We use -+ R to represent the rewrite relation. For example, a term rewriting system R is {f(x) -+ b,g(b) -+ a}. Then g(f(x)) -+R g(b) . We define -+'R as the reflexive transitive closure of -+R· Thus g(f(x)) -+'R a. We define H'R as the reflexive transitive closure of HR. Suppose R is a term rewriting system { r1 -+ s1 , . . . , r n -+ Sn} , R= is defined as the associated equational system { r1 = s1, ... , rn = Sn} . By Birkhoff's theorem [Birkhoff, 1935], R= f= r = s iff r H 'R s. This essentially shows the soundness and com­ pleteness of equational reasoning based on term rewrit­ ing. However, the rewriting system is not yet satisfactory for theorem proving purposes: to show r H'R s, rewrit­ ing has to be done in both directions, and it is highly non-deterministic and inefficient .

A term r is reducible if there is a term s such that r -+ s, otherwise r is irreducible. If r -+* s and s is irreducible then we call s a normal form of r . We write r + s if there is a term u such that r -+* u and s -+* u. We write r t s if there is a term u such that u -+* r and u -+* s. We say a rewriting system R is confluent if for all terms r and s, r t s implies r + s . It can be shown that if R is confluent and r H'R s then r + s. A rewriting system R is terminating if it has no infinite rewriting sequence. If there exists a termination ordering > such that for all rules l -+ r in R, l > r , then R is terminating. If R is confluent and terminating, r H'R s can be decided by rewriting r and s to normal forms and compare the normal forms.

Definition 2.1 Suppose that 11 -+ r1 and l2 -+ r2 are two rewrite rules with no common variables. Suppose u is a non-variable subterm of 11 , {if 11 is a variable, u may be a variable). Suppose u and 12 are unifiable and () is the most general unifier. We call the pair (ll[u t­ r2]B, r 1B) a critical pair for rules h -+ r 1 and l2 -+ r 2 . ll[u t- r 2] denotes the term obtained by replacing a specified occurrence of the sub term u in 11 with r2.

Theorem 2.2 Suppose a term rewriting system R is terminating. R is confluent iff for all critical pairs ( s , t) in R, s + t.

If a rewriting system is not confluent , an equiva­ lent rewriting system might be obtained by adding new rewriting rules. Theorem 2.2 can be used to generate such new rules. The idea is to add rule s -+ t or s t- t to R while preserving termination for all critical pairs (s , t) in R. The algorithm was initially proposed in [Knuth and Bendix, 1970], and is often called Knuth­ Bendix completion, or simply, completion. Sometimes, it is not possible to orient an equation, i.e. f(x , y) =

f(y, x), in either direction while maintaining termina­ tion. Thus Knuth- Bendix completion is extended to unfailing completion[Bachmair et al., 1989]. In unfailing completion, if a critical pair (s, t) can not be oriented then it is added as an equation s = t . Equation s = t may participate in further critical pair generation. It is regarded as containing rules s-+ t and t-+ s. However , the use of equation in rewriting is restricted : sB can be replaced by tB only if sB > tB, where> is the termination ordering.

We give names to a set of inference rules. We fol­ low the convention used in [Plaisted, 1993]. The rule U C P(-+,-+) is the operation of generating critical pairs between two rewrite rules. If a critical pair can be ori­ ented, a new rewrite rule is added to the rewrite system; otherwise, an equation is added. UCP stands for Un­ failing Critical Pair generation. Similarly, U C P( = , -+) generates critical pairs between a rewrite rule and an equation; UCP(=, =) generates critical pairs between two equations. Inference rule Sf M P RULE is the oper­ ation of simplifying a rewrite rule or an equation with other existing rewrite rules or equations. For example, if a rewriting system R contains {!(x) -+ x, f(b) -+/(a)}, the second rewrite rule can be simplified to b -+ a, and thus R contains {!(x) -+ x, b -+ a} after rule SIMPRULE is applied. E f= s =tiff EU {s' =/= t'} is unsatisfiable, where s' and t' are skolemized terms of s and t, respectively. Thus we may include { s' =/= t'} as an inequation in a rewriting system R and show a contradiction can be derived from R. Sf M PGOAL is the operation of simplifying an inequation using existing rewrite rules or equations. The rule CONTRA derives FALSE when the inequation s =/= s is derived. In ap­ plying these inference rules, the concept of fairness is needed. Fairness means that every henceforth possible inference will eventually be performed.

Theorem 2.3 Fair unfailing completion starting from a set of R of rules, equations and ground inequation and using the inference rule {UCP(-t, -+), UCP(=, -+) , UCP(=,=), SIMPRULE, SIMPGOAL, CONTRA} will eventually generate FALSE if R= is unsatisfiable.

Theorem 2.3 show the completeness of an equational reasoning strategy based on unfailing completion. We will also use the fact that Sf M P RULE is inessential to the completeness of the strategy.

In this paper, we are concerned with equational sys­ tems that involve associative and commutative func­ tions, or AC functions . An AC function f satisfies the following axioms {f(J(x , y), z) = f(x , f(y , z)),f(x, y) = f(y, x)}.

3 AC-Consistent Completion

In this section, we introduce the concept of consistency for AC equational problems. We present a new com­ pletion algorithm in which only consistent rules can be used for critical pair generation and simplification. We call the new algorithm consistent unfailing completion.

We show the correspondence between a consistent un­ failing completion and a ground completion procedure. The correspondence helps us in deriving the consistency constraints and establishing the completeness proof of the consistent unfailing completion algorithm.

Definition 3.1 Suppose that > is a termination order­ ing and > is total on ground terms. A ground term s is an A C minimal term if s is the minimal term of its A C-equivalence class with respect to the ordering >. A rewrite rule s -+ t is consistent if there exists an in­ stance sB -+ tB such that both sB and t(} are A C minimal terms, and that (} assigns distinct ground terms to dis­ tinct variables in s and t. The consistency of an equation (a critical pair) is similarly defined.

Example 3.2 In this example, we use the lexicographic ordering as the termination ordering. We assume f is an AC function and g is not an AC function. f(a, f(b, c)) is an AC minimal term. f(J(a , b), c) is not an AC minimal term, because f(J(a , b), c) > f(a , f(b, c)) and they are AC equivalent. We sometimes say f(a , f(b , c)) is the AC minimal term of f(J(a , b) , c). The rewrite rule g(J(x, f(y, z))) -+ a is consistent, g(J(a, f(b, c)) -+ a is a consistent instance of the rule. Rewrite rule g(J( x, y)) -+ f(y, x) is not consistent, neither are f(g( x), g(y)) = f(y , x) and critical pair (J(x, a), f(a, x)) .

Definition 3.3 Inference rule CUCP(-+,-+) is the op­ eration that generates critical pairs between two consis­ tent rewrite rules. The critical pairs generated are ori­ ented as rewrite rules or added as equations. CUCP(-+ , -+) is the same as U C P(-+, -+) except that only con­ sistent rewrite rules are used for critical pair generation in CUCP. CUCP(=, -+) and CUCP(=, =) are simi­ larly defined. We say the extended set of AC axioms is the set {f(J(x , y), z) = f(x, f(y, z)), f(x, y) = f(y, x), f(x, f(y, z)) = f(y , f(x, z))} for all AC functions f In­ f erence rule U C PAC is the operation that generates crit­ ical pairs between a rule or an equation and an equation from the extended set of A C axioms.

Theorem 3.4 Fair consistent unfailing completion starting from a set of R of rules, equations and ground inequation and using the inference rule { C U C P (-+, -+), CUCP(=, -+), CUCP(=, =), UCPAc, SIM PGOAL, CONTRA} will eventually generate FALSE if R= is unsatisfiable.

Theorem 3.4 outlines the consistent unfailing comple­ tion procedure. The soundness of the procedure is ob­ vious, as each inference rule generates only logical con­ sequences. We show that consistent unfailing comple­ tion can be regarded as a lifted version of the ground completion procedure outlined in Theorem 3.6, and thus establish its completeness proof.

Definition 3.5 Inference rule IN ST is the operation of generating an instance of a rewrite rule or an equation and orienting it as a new rewrite rule. Inference rule GC P(-+ , -+) is the ope ration of generating critical pairs between two ground rewrite rules and orienting them as new rewrite rules. GSf M PAc is the operation of re­ placing a ground rewrite rule s -+ t by a new rewrite rule s' -+ t', where s' and t' are A C minimal terms of s and t, respectively.

Theorem 3.6 Fair instance-based completion starting from a set of R of rules, equations and ground inequa­ tion and using the inference rule {INST, GCP(-t,-+), GSIMPAc, SfMPGOAL, CONTRA} will eventually generate FALSE if R= is unsatisfiable.

PROOF: If R= is unsatisfiable, by Herbrand's theo­ rem, there is a finite unsatisfiable set of instances R[ of n=. By the fairness assumption, all instances in the set R[ will be generated by IN ST. As a consequence of Theorem 2.3, {GCP(-t, -t), GSIM PAc, SfM PGOAL, CONTRA} will eventually generate FALSE from the set R[.

Remark 3. 7 The consistent unfailing completion pro­ cedure in Theorem 3.4 is a lifted version of the instance­ based completion procedure in Theorem 3.6.

We now give an example to show the effect of the consistency constraints.

Example 3.8 Consider a rewriting system with the fol­ lowing rules, {(x * y) * z -+ x * (y * z), x * y = y * x }. We use an ordering in which the associativity axiom can be oriented 1 . We refer to the associativity axiom as R1, and the commutativity axiom as R2 .

Applying UC P( -+, =) on R1 and R 2 , equations (Y*X)* z = (x * y) u and Z* (x * y) = (x * y) u will be generated. Applying rule Sf M P RULE, they are simplified to R3 y * (x * z) = x * (y * z) and R4 z * (x * y) = x * (y * z). Applying UCP(=, =) and Sf M PRU LE on R1 and R3, equation R5 x * (y * (z * w)) = y * (x * (z * w)) will be generated.

Now let's consider the permutations of the variables on each side of the equation R5 . In unfailing completion, all such permutations, e.g. X*(Y*(Z*w)) = Y*(x*(wu)), will eventually be generated from R1 and R 2 . There are 24 such permutations up to the renaming of variables. Since none of the permutations except x * (y * (z * w)) = x*(Y*(z*w)) can be simplified, 23 equations will be added to the rewriting system. However, none of the permuted equations are consistent, and x * (y * ( z * w)) = x * (y * ( Z* w)) is an instance of x = x and can be deleted. Thus in consistent unfailing completion, no permutations of the equation R5 will be added to the rewriting system.

4 Refinements

In this section, we present some refinements of Theo­ rem 3.4. Theorem 4.2 outlines the refined consistent un­ failing completion algorithm. We then show how the algorithm can be efficiently implemented.

Definition 4.1 Inference rule PERM is the operation that generates all consistent A C equivalent rewrite rules

1 one such ordering is defined in Definition 4.3.

(equations) of an existing rewrite rule (equation). Infer­ ence rule CUCPA is the operation that generates critical pairs between a consistent rule or equation and the asso­ ciativity axioms {f(f(x, y), z) = f(x, f(y , z))}.

The inference rule PERM and CUCPA combined are equivalent to the rule UCPAc in Theorem 3.4, and they are more efficient. Sf M P RULE often greatly reduces the number of rewrite rules and equations in a rewriting system. Sf M P RULE can be added to the consistent unfailing completion procedure in Theorem 3.4 without affecting its completeness. The proof ir-volves extend­ ing the instance-based completion procedure as in The­ orem 3.6 with a restricted version of Sf M P RULE and then lifting it to the nonground case.

Theorem 4.2 Fair consistent unfailing completion starting from a set of R of rules, equations and ground inequation and using the inference rule { CUC P( -t ,-+), CUCP(=,-+), CUCP(=,=), PERM, CUCPA, SfMPRULE, SIMPGOAL, CONTRA} will eventu­ ally generate FALSE if R= is unsatisfiable.

We now define an ordering that's used in our imple­ mentation.

Definition 4.3 We define size lexicographic path or­ dering >.tpo on ground terms as follows. Suppose s and t are ground terms, s = f,(a 1, ... , am) and t = ft ( b1, . .. , bn), and >1 is the lexicographic ordering. S >8 tpo t iff

1} size(s) > size(t), or

2} size(s) = size(t) and f, >t ft , or

3} size(s) = size(t), f.=ft, ak=bk \lk from 1 to i- 1, and a; > ·lpo b;.

size(s) is defined as the length of s written as a charac­ ter string( excluding commas and parentheses). The size lexicographic path ordering is extended to nonground terms as follows, s >·lpo t iff \10 sO >.tpo tO. It can be difficult to order two nonground terms with respect to >.tpo· In practice, we use sufficient conditions based on special cases such as g(x) >.tpo x and f(x, x) >.tpo g(x). It can be showed that size lexicographic path ordering is a termination ordering.

Definition 4.4 Suppose that f is an AC function, we call f(s1 , s2, ... , sn) the flattened term of f(s1 , f(s2 , .. .f(sn-1, sn), ... )), where s; does not contain f as a top level function symbol. Suppose that s and t are subterms of an expression e, we says AC-precedes t in e, or s < <t, if the flattened term of e contains a sub­ term of the form f( ... , s, .. . , t, .. . ), where f is an AC function.

We now describe two sufficient conditions for detecting the inconsistency of rewrite rules( or equations).

Theorem 4.5 Suppose a size lexicographic path order­ ing <.Lpo is used as the termination ordering. A rewrite rule s -+ t is inconsistent if

1) u1 <·lpo u2 and u2 < < u1

or 2) u 1 << u2 and u 2 << u 1, where u 1 and u2 are subterms of s and t, respectively.

PROOF: For case 1): Equation s = t contains a subterm f( ... , u2, ... , Ut, ... ). Since u1 <.tpo u2, /( ... ,u2, . .. ,ul, . .. )O >.tpo /( . . . ,ul, ... ,u2, ... )B, for all 0. That is, no instances off( . . . , u2 , ·. . , u1, · .. ) can be an AC minimal term. s -+ t is thus inconsistent . The proof for case 2) is similar.

The inference rule PERM generates all consistent AC-equivalent rewrite rules or equations of an existing rewrite rule or equation. It essentially involves solving a constraint satisfaction problems. The simplest solution is to enumerate and check. Namely, for each rewrite rule s -+ t, all AC equivalent rules of s -+ t are enumerated, and then Theorem 4.5 is used to filter out the incon­ sistent rules. More specifically, to apply PERM on a rewrite rule s-+ t , we flatten s -+ t, collect new rewrite rules by permuting the arguments of AC functions in s -+ t, delete all inconsistent rules, and finally unflatten the remaining rewrite rules in the collection. For a term f( a1 , ... , an) where f is an AC function, unflattening the term generates f(a1 ,/( . .. ,f(an_1 ,an))). To unflatten a term or an expression, unflattening is done recursively for all its subterms. For example, g(f(a, h(b), x)) -+cis unflattened to g(f(a, f(h(b), x)))-+ c, assuming that f is the only AC function. Note that flattened terms are only used as an intermediate representation for detecting inconsistent rules, and they are not used in the rewrite rules and equations of the rewriting system.

Theorem 4.5 provides only sufficient conditions for in­ consistency, and thus some inconsistent rules can also be generated. More deliberate approaches based on con­ straint satisfaction might be able to compute the exact set of consistent rules, and thus further reduce the num­ ber of critical pairs and rewrite rules generated in the completion procedure.

5 Test Examples

It is fairly straightforward to implement the consistent unfailing completion algorithm. We implemented the algorithm with several hundred lines of Prolog code. We tested a number of pure equality problems. The results are listed in Table 1.

E1-E6 is a set of benchmark problems for equality proposed by [Lusk and Overbeek, 1985]. E3 and E6 in­ volve AC functions. wos21(equality version), RNG015-6, RNG023-6 and RNG024-6 are problems from ring the­ ory, all four of them involve AC functions. For non-AC problems, the procedure is same as unfailing completion. For AC problems, we study the effect of consistency checking by comparing the result from unfailing com­ pletion and consistent unfailing completion. Note that consistency checking significantly reduces the number of critical pairs generated, the number of rules kept and the time needed to obtain a proof. Our implementation serves the purpose of demonstrating the effect of consis­ tency checking. A state of the art equality prover can solve most of the listed problems in tens of seconds[Mc­ Cune, 1990]. Efficient data structures can be used to improve our current implementation.

It is particularly encouraging that we are able to prove E6, which says a ring with x 3 = x is commutative. The problem has a long history. Wos had the follow­ ing remarks on the problem, "if one succeeds in having a reasoning program prove this theorem, and it can be shown that the success is the result of a new technique, then one has solid evidence of the potential value of the new idea" [Wos, 1988]. Veroff obtained a proof of the problem using AURA [Veroff, 1981] . However, the input contained many additional clauses that facilitated the proof. Stickel was the first to prove the problem with a natural set of input equations [Stickel, 1984]. The proof took over 14 hours. Zhang and Kapur could find a proof in a few minutes using RRL [Zhang and Kapur, 1990]. Both [Stickel, 1984] and [Zhang and Kapur, 1990] used approaches based on AC unifications. The use of the cancellation law for additional group was important for them to get the proof efficiently.

6 Discussion

In term rewriting systems with AC functions, a term can have an exponential number of AC equivalent terms, and a rewrite rule can generate an exponential number of new rules when combined with AC axioms for critical pairs generation. A common approach for avoiding the combinatorial explosion is to represent all AC equiva­ lence terms as a single term. Flattened terms are used to represent terms equivalent up to associativity, and terms with arguments permuted are considered identi­ cal. AC unification algorithm is used to unify two flat­ tened terms. Flattening breaks the well-foundedness of most termination orderings. Special AC termination or­ derings are needed to handle flattened terms.

On the other hand, the combinatorial explosion oc­ curs only because all AC equivalent terms of a term are kept in a rewriting system. If they are simplified to a single normal form, the explosion will not occur. This is exactly the case for ground completion procedures: all ground AC equivalent terms can be rewritten to a normal form using AC axioms when a total termination ordering on ground terms is used. Our approach is based on the observation that a nonground completion proce­ dure can be constructed by lifting a ground completion procedure, and thus avoid much of the redundancy in representing AC equivalent terms. Our approach does not need a special AC unification. It does not need a special AC termination ordering either. The latter fa­ cilitates the complete automation of the equational rea­ soning process. We used a single termination ordering for all of our test examples. We were also able to use the equational prover as a component in a general first order theorem prover.

There are some previous works on reducing unneces­ sary equational inferences, both for AC equational prob­ lems and equational problems in general[Zhang and Ka­ pur, 1990; Bachmair et al., 1992] . Most of them are fun­ damentally different from our approach. They reduce the number of critical pairs generated by blocking out certain positions for overlapping two rewrite rules. Some of these works might be combined with our approach. It would also be interesting to study the applicability of our approach to other equational theories.