«Abstract. A method ~sg~ven for dec~dlng formulas in combinations of unquantified first-order theories. Rather than couphng separate decision ...»
Deciding Combinations of Theories
ROBERT E. SHOSTAK
SRI International, Menlo Park, Cahforma
Abstract. A method ~sg~ven for dec~dlng formulas in combinations of unquantified first-order theories.
Rather than couphng separate decision procedures for the contributing theories, the method makes use
of a single, uniform procedure that minimizes the code needed to accommodate each additional theory.
It ~s apphcable to theories whose semantics can be encoded within a certain class of purely equational canonical form theories that ~s closed under combination. Examples are given from the equational theories of integer and real anthmeUc, a subtheory of monadic set theory, the theory of cons, car, and cdr, and others. A discussion of the speed performance of the procedure and a proof of the theorem that underhes ~ts completeness are also g~ven.The procedure has been used extensivelyas the deductive core of a system for program specificaUonand verifcation.
Categories and Subject Descriptors- D.2.4 [Software Engineering]: Program Verificationmcorrectness proofs; verification; F 3 1 [Logics and Meanings of Programs]' Specifyingand Verifyingand Reasoning about Programs--mechamcal verification; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Loglcmmechamcal theorem proving General Terms: Algonthms, Verification AddlUonal Key Words and Phrases: Decision procedures
1. Introduction M u c h attention has been given in the last few years to the problem o f developing decision procedures for applications in program verification and mechanical p r o o f o f theorems in mathematics. It often happens, in these applications, that the formulas to be proved involve diverse semantic constructs. Verification conditions for programs, for example, often mix arithmetic with data structure semantics.
Accordingly, a n u m b e r o f procedures have been developed (such as those o f Jefferson  and the author ) for particular m i x e s o f theories. One o f the m o s t general results along these lines is given by Nelson and O p p e n  in their work on simplification using cooperating decision procedures. Th¢~ central idea, here, is that procedures for diverse unquantified theories in a certain class can be hooked together so as collectively to decide a formula involving constructs f r o m each. T h e coupled procedures c o m m u n i c a t e by passing back and forth information they individually derive a b o u t equality a m o n g terms.
The m e t h o d described in this paper also addresses the p r o b l e m o f deciding c o m b i n a t i o n s o f theories. Rather than connecting separate procedures for the constituent theories, however, it is based on a single, u n i f o r m procedure that This research was supported m part by the National Science Foundation under Grant No. MCS 79and by the Air Force Office of Scientific Research under Contract No. F49620-79-C-0099.
Author's addless" Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025 Permission to~..o~y without fee all or part of th~s material ~s granted provided that the copies are not made or distributed for d~rect commercial advantage, the ACM copyright notice and the title of the pubhcation and its date appear, and notice is given that copying is by permission of the AssoclaUon for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.
© 1984 ACM 0004-5411/84/0100-0001 $00.75 Journal of the Asu~ctaUonfor ComputingMachinery,Vo| 31, No 1,January 1984,pp 1-12 2 ROBERT E. SHOSTAK localizes the mechanism particular to each constituent to a relatively small amount of code. As a result, new semantic constructs can be incorporated quite easily. The method also obviates the explicit computation of entailed equality information required by the distributed approach, and the redundant representation of this information in the separate procedures.
The method is applicable to theories whose semantics can be expressed inside a certain class of purely equational canonical form theories. The class has the property that the canonizing functions of arbitrary members can be combined to obtain a canonizing function for their union. The decision procedure extends the congruence closure methods [1, 5, 6] that have been used for the pure theory of equality. The extension depends upon a notion of semantic signature that generalizes the earlier concept of signature to accommodate the semantics of the canonical form theories.
The method is useful for a surprisingly rich class of constructs. We give examples from integer and real arithmetic, the theory ofrecursive data structures, a subtheory of monadic set theory, and the first-order theory of equality. The procedure has been used intensively in a major verification effort  over the course of several months, and has been found to give good speed performance.
The next two sections characterize the class of theories to which the method is applicable, and prove that it is closed under combination. Section 4 gives the decision procedure and exemplifies its operation. Sections 5 and 6 discuss performance issues and an extension of the method that treats nonconvex theories. The last section gives a proof of the theorem on which the procedure is based.
2. o-Theories a n d Algebraic Solvability The procedure described in this paper operates over a subclass of certain unquantiffed first-order equational theories called o-theories. Such theories have both interpreted and uninterpreted function symbols. Terms whose outermost function symbol is interpreted are themselves said to be interpreted, and all other terms (including variables) are said to be uninterpreted. The distinguishing feature of otheories is that each has an effective canonizer, i.e., a computable function o from terms to terms such that a purely interpreted (i.e., containing no uninterpreted function symbols) equation t = u is valid in the theory iff o(t) --- o(u). The canonizer o must act as an identity on uninterpreted terms, must be idempotent (i.e., o(o(t)) = o(t)), and must have the property that the arguments of each interpreted canonical term must themselves be canonical.
The semantics of o-theories are defined with respect to o-interpretations, i.e., Herbrand interpretations that respect o in the sense that for each interpreted term t = f(t~...., tn), v(t) = o(f(v(tO..... v(tn))), where v(t) is the value of t in the interpretation. Note that these semantics say more than that two terms must be equal in all interpretations if they have identical canonical forms; they also say that certain terms (for example, distinct canonical constants) must be unequal in all interpretations.
A simple example of a o-theory is the equational theory of addition and multiplication by constants over the reals. Each term in this theory can, of course, be reduced to a linear expression of the form a~x~ + a2x2 +... + a,,x, + c (n _0), where each a, is a nonzero real constant, each x, is a variable, and c is a real constant. By specifying some criterion for ordering the xi's (alphabetic ordering, for example), removing unity coefficients, and discarding c if c -- 0, a suitable o can be defined. Note that the theory can trivially be enriched with uninterpreted function symbols.
Deciding Combinations o f Theortes 3 The decision procedure we will describe operates on a-theories with a s~eial property we call algebraic solvabihty Such theories have a solverma computable function that takes a purely interpreted equation (no uninterpreted symbols other than variables) e(say t = u) as input, and returns either true, false, or a conjunction of equations. The returned formula must be equivalent to e and must be either true or false if e has no variables. Moreover, the equations (if any) in the returned formula must all be of the form x, = t,, where the x,'s are distinct variables of t (or u if t has none) that do not occur in any of the t,'s.
Returning to the example of real linear arithmetic, a suitable solver is trivially provided by conventional algebraic manipulation; solving 3x + 2y -- 2x + 4, for example, gives x = - 2 y + 4.
At first glance, one might expect that algebraic solvability is such a strong criterion that there are no nontrivial theories other than, say, theories over fields, that satisfy it. Surprisingly, this is not so. As the following examples suggest, algebraic solvability is characteristic of many constructs one encounters in practice.
Example 1. The convex theory o f cons, car, and cdr.
First consider the theory
of cons, car, and cdr with the following axiomitization:
car(cons(x, y)) -- x, cdr(cons(x, y)) = y, cons(car(x), cdr(x)) -- x.
Using the first two of these axioms as rewrite rules, one can always reduce a term in the theory to a canonical form in which cons is not an argument of either car or cdr.
A solve function for this theory is given by the algorithm shown in Figure 1.
Note that the algorithm introduces new (existentially quantified) variables. The chief function of the main routine solve is to grind the left side of the given equation (represented as an ordered pair) down to a variable; the auxiliary function solvel (which takes two terms and returns a term) takes over from there, and attempts to eliminate that variable from the right side. The routine resolve, called by solve, sees to it that no equations in the returned conjunction have the same left side.
Consider, for example, the action of the algorithm on the equation cons(car(x), cdr(car( y))) = cdr(cons( y, x)).
The two sides are first canonized to obtain cons(car(x), cdr(car( y))) -- x.
This equation is then reduced to the two equations car(x) = car(x), cdr(car( y)) = cdr(x).
The first of these reduces to true and is, in effect, discarded. The second becomes car(y) = cons(a, cdr(x)), where a is a new variable, and then (recursing again) y = cons(cons(a, cdr(x)), d), which is then returned.
It is not difficult to show that the algorithm satisfies the criteria for a solver. The reader might find it amusing to prove that it always terminates.
4 ROBERT E. SHOSTAK
Similarly, A _CB becomes s~ + s5 -- (I,.
It is easy to see that terms in the encoding theory can be canonized simply by ordering the set variables in some way and eliminating redundancies.
A solver for the encoding theory is also easy to construct. One simply replaces each side of an equation with its a-form and cancels variables occurring on both sides. If the two sides thereby become identical, true is returned; otherwise, the conjunction A v, =,I,.
is returned, where the v,'s are the remaining variables.  Example 4. The unquantified first-order theory of equality. This theory has no interpreted function symbols at all. a is therefore just the identity function. The solve function merely returns true if the given equation is an identity, and acts as an identity otherwise.  Until now we have been concerned with solve functions for equations with only purely interpreted terms. In the next section and in the procedure itself it will be necessary to deal with equations that may have uninterpreted terms other than variables. The notion of solver is extended to deal with such equations in the following way.
We will say that a solver for a a-theory T is a computable function that takes an arbitrary equation e(say t --- u) over T as input and returns either true, false, or a conjunction of equations. The returned formula must be equivalent to e and must be one of true or false if e contains no uninterpreted terms. Moreover, the equations (if any) in the returned formula must all be of the form u, = t,, where the ui's are distinct uninterpreted subterms of t(or u if t has none) that do not occur in the t,'s except possibly as proper subterms of uninterpreted terms.
Note that all the solvers we have talked about so far can be trivially extended to satisfy the new definition simply by treating the maximally uninterpreted subterms of a submitted equation as if they were distinct variables. For example, the equation f(x) -- g(x + 2, f(x)) = O, when solved in linear arithmetic, produces f(x) = - l × g(x + 2,f(x)).
6 ROBERT E. SHOSTAK Note that although fix) occurs on the right-hand side of the result, it occurs only as a proper subterm of an uninterpreted term.
3. Combining Theories Algebraically solvable a-theories have the elegant and useful property that they can be combined (provided they are compatible in a certain sense) without giving up algebraic solvability.
One needs to be careful, of course, about what it means to combine theories.
Simply to say that the interpreted symbols of the combined theory are the union of those of the constituents does not suffice. The semantics of mixed terms (terms with symbols from different constituents) must be explicated, and conflicts that may arise when the constituents share interpreted symbols must be resolved.
The most natural resolution (and the one we espouse) of the issue of mixed terms is simply to assume that interpreted symbols from different theories have no semantic interaction in the combined theory; if a function interpreted in T~ but not in T2 is given an argument that is interpreted in T2 but not in TI, the effect is to treat the argument as if it were uninterpreted. For example, in the combination of real linear arithmetic with the theory of cons, car, and cdr, we will have a(car(cons(l + 1, nil)))= 1 + I.
We will consider that + is uninterpreted with respect to cons, car, and cdr, (and vice versa) in the combined theory, and that 1 + 1 is therefore an uninterpreted subterm of car(cons(l + 1, nil)).
It still remains to resolve the question of what happens if the constituent theories share interpreted symbols. Here we will take the conservative stand of requiring that the shared symbols have exactly the same semantics. More precisely, we will say that T~ and T2 are compatible if for each term t in their combination whose function symbol is interpreted in both, a~(t) = a2(t). We will consider only combinations of compatible theories.
Note that as a consequence of the view that uninterpretedness is relative, the purely interpreted terms of the combined theory are exactly the union of those from the constituent theories; the action of the combined a on each such term is the action of the a of the appropriate constituent. It is easy to check that the combined o thus defined satisfies the requirements for a canonizer.