An Algorithm for Reasoning About Equality

I Introduction

A deductive system for program verification must be able to reason proficiently about equality. Equality is often handled in an ad hoc and incomplete way--most usually with a rewrite rule that substi­ tutes equals for equals with some heuristic guid­ ance. We present a simple algorithm for reasoning about equality that is fast, complete, and useful in a variety of theorem-proving situations. We also present a proof of the theorem on which the algorithm is based.

II An Example

The following formula is of the kind one en­ counters in verifying programs involving array indexing:

(I=J II K;:L II A[ I ]=B[K] II J=A[J] II M=B[L])

::J A[M]=B[K]).

Here, A and Bare function symbols while I, .·· M are universally quantified variables.

One might approach such a formula by working backwards from the conclusion, substituting equals for equals until the left-hand-side is transformed into the right-and-side:

A[M]=A[B[L]]=A[B[K]]=A[A[I]]=A[A[J]]=A[J]=A[I]=B[K] One could also work from B[K] rather than from A[M], or from both simultaneously; the links needed in the chain are the same in either case.

While this "backward substitution" method and other methods that transform formulas through a sequence of substitutions are logically sound, they are not well-suited to machine deduction because there is no easy way of selecting the "right" substitution to make at each step.

Intuitively, it would not seem necessary to generate terms beyond a certain depth. However, the critical depth (the smallest depth necessary to consider) cannot be calculated solely as a function of the depths of the terms appearing in the orig­ inal formula; in particular, the critical depth is not simply the maximum of these depths. For example, no backward-substitution proof can be carried out for the above formula without generat­ ing a term of at least depth 3. Even if one could conveniently calculate the critical depth, one would still, in general, generate many more terms

than are necessary.

This difficulty with substitution transforma­ tion methods is not inherent in the problem. The next section presents a more efficient method that considers only the terms appearing in the original formula.

III The Procedure

Our method is a decision procedure for the subclass of predicate calculus with function S)~bols and equality whose formulas have only uni­ versal quantifiers in prenex form. While the decidability of this subclass is well-known, the

AN ALGORITHM FOR REASONING ABOUT EQUALITY

Robert E. Shostak Stanford Re search Institute Menlo Park, California 94025

classical decision procedure for it (W. Ackermann [1]) produces a combinational explosion that makes that method infeasible for non-trivial problems.

The procedure is as follows. The matrix of the formula F is first negated and placed in dis­ junctive normal form. Next, all atomic formulas other than equalities are replaced by equal.i ties as follows. For each n-ary predicate symbol ~ occur­ ring in the formula, a new n,-ary function symbol f~ is introduced. Each atomic formula ~(t 1 , t 2 , ... tn) occurring in the formula is then replaced by the equality f~(tl, t 2 .·· , tn) = c, where cis a constant. The modified d.n.f. is intersatisfiable with the original one, and is satisfiable if and only if one of its disjuncts is satisfiable. Each disjunct, moreover, consists of a conjunction of equalities and negations of equalities. The problem is thus reduced to testing the satisfiability of each such conjunction.

It remains to test each conjunction for satis­ fiability. Let S be the set of equalities and negations of equalities occurring in the conjunction to be tested. Let T be the set of terms and subterms of terms occurring in S , and define the binary relation . as the smallest relation over T X T (where u1, u2 . .. un, tl, t 2 , v 1 , v 2 . .. vn denote terms

and f denotes a function symbol) that :

(1) Contains all pairs <tl,t 2 > for which 't 1 =t2 e S (2) Is reflexive, symmetr1c, and transitive ·

(3) Contains the pair <f(u 1 , u 2 ··· ur), f(v 1 ,v 2 , .. · vr)> whenever it contains the pairs <ui,vi> , 1 $ i $ r, and f(u 1 , u2 ... ur), f(v 1 , v 2 .·. vr) are both in T.

The test for satisfiability of S depends on the following theorem (to be proved later): Theorem. S is unsatisfiable ~ there exist terms t 1 ,

t 2 e T such that 't1 ~ t2 e S and t1 ~ t2 ·

The theorem tells us that to determine the satisfiability of S it suffices to consider the negated equalities of S one at a time. If one is found (say t 1 ~ t 2 ) for which t 1 ~ t2, S is unsatis­ fiable; otherwise S is satisfiable. Note that the definition of~ involves only terms in T.

To use the theorem, we must be able to calculate whether a given pair of terms is in the relation ~ · This can be done by building the relation from the definition: (1) is used as a basis, and (2) and (3) are repeatedly applied until no new terms are gener­ ated. Since~ is an equivalence relation, one can conveniently represent it during the construction as a collection of sets of elements of T, each set con­ taining elements known to be in the relation with the other e lements of that set.

For example, for the set S = (I=J, K;:L, A[I]= B[K], J=A[J], M=B[L], AfM]~ B[K]) that arises from the earlier example, ~ is constructed as follows. From the basis (1), one obtains :

((I,J}, (K,L}, (A[I], B[K]), (J,A[J]}, (M,B[LJ}} Using (2):

([I,J,A[J]} [K,L} [A[I], BfK]}, [M,B[L]}}

Using (3) : ((I,J,A[J]} (K,L} (A[ I], B[K]}, (M,B[L]}, (A[ I], A[J]}, (B[K], B[L]}}

Using (2) : ((I,J, A[J], A[I], B[K], B[L], M},(K,L}}

Using (3) : ((I,J,A[J],Ap],B[K],B[L],M}, (K,L,},

{ A[M],A[I]}, {A[M],A[J]J}

Since(3) yields no new pairs, the construction is complete. Since A[M] ~ B[K], S must be unsatis­ fiable.

The rules for building up ~ can be implemented quite efficiently. D. Oppen and G. Nelson* have recently coded a very fast implementation that rep­ resents terms as graphs and use s the Tarjian [4] s e t-union algorithm in the closure step. Oppen and Nelson have ~hown that their implementation requires only order n deterministic time and linear space , where n is the length of the input S.

IV Proof of the Theorem

The main import of the theorem on which the algorithm is based is that it suffices to "consider" only the terms occurring in the formula to be decided. The proof is largely concerned with ex­ tending the mod e l provided by ~ from T to the entire Herbrand Universe.

Proof ~ SupposeS is satisfiable, t 1 ,t 2 e T and t 1 ~ t 2 · Let M be a model for S. Because M satisfies the reflexivity, symmetry, transitivity and substitutivity axioms of equality, t1 ~ t 2 implies that t 1 and t 2 must have the same values in M. Hence, 't1 f. t2' is not inS.

~ Suppose there are no terms t 1 ,t 2 in T such that t 1 ~ t2 and 't 1 f. t 2 ' e S. We will show that S is satisfiable by constructing a Herbrand model M for S.

We first construct the term universe

(X)

Too =i~o Ti of S inductively as follows:

T 0 = T Ti+l = tf(t 1 , ·.· ,tr) iti€ Ti} U T . (where f ranges over all function symbols 1 occurring inS).

Next, pick a representative term from each of the equivalence classes induced by~ on T, and define the function a : T - T that assigns to each term in T the representative of its class.

The model M is now constructed inductively as follows :

Note .·that M is a Herbrand model, i.e., it always assigns values from the Be rbrand Universe. . " ( " The notat1on f(vM t 1 ), ·.· , vM(tr)) is intended to represent the function symbol denoted by f followed by the terms obtained by evaluating vM(ti) for each i.

*Personal communication. A paper describing this work is forthcoming.

It remains to show that

This f ollows straightforwardly by induction on the maximum of the term universe heights of

The author is grateful to Drs . R. E. Boyer , J . Strother Moore, E . Horowitz, and the reviewers for their observations and suggestions.

VI References

1. Ackermann , W., Solvable Cases of the Decision Problem , North-Holland Publishing-cD., Amsterdam (1954), pp. 102-103 .
2. 2 . Mendelson , E . , Introduction to Mathematical Logic, D. Van Nostrand Co . , Inc ., Princeton, New Jersey (1964) .
3. 3 . Robinson, G. , and Wos , L., "Paramodulation and Theorem-Proving in First-order Theories with Equality . " Machine Intelligence IV (1969), ed. by D. Michie and B. Meltzer, pp. 135-150 .
4. Ta rjian, R., "Efficiency of a good but not linear set-union algorithm," J .ACM, V. 22, No . 2, (April 1975), pp. 215-~