Synthesis by Completion

1. INTRODUCTION

A (first-order) functional (applicative) program is a set of directed equations, used to compute by replacing instances of left-hand sides with the value of the right­ hand sides. For example, the following is a program for concatenating two lists of elements:

where <= has the declarative meaning "is equal" (nil is the empty list and · denotes the cons function). Given the term

it will compute the result of appending the two ele­ ments a and b in the list a ·b ·nil [with parentheses, that should be a ·( b ·nil)] to the front of the list c ·d ·e ·nil. A logic program [Kowalski-7 4] is a set of Horn clauses used as a pattern-directed program that searches for output terms that satisfy a given goal for given input terms. In this paradigm, the append pro­ gram would be expressed in two statements:

SYNTHESIS BY COMPLETION*

Nachum Dershowitz Department of Computer Science University of Illinois Urbana, 11 61801 U.S.A.

where :- has the declarative meaning "is implied by". Given a goal

this program computes the appended list Z =a ·b ·c ·d ·e ·nil. Throughout this paper we follow the convention of using lower· case for constants and upper case for free (universally quantified) variables.

A rewrite system is a set of directed equations (or equivalences) used as a nondeterministic pattern­ directed program that returns as output a simplified term equal to a given input term. (See [Huet-Oppen-80] for a survey.) For example, the following is a three-rule rewrite system for append:

Rules may be applied in any order to any matching sub­ term until no further applications are possible. Thus, applying the rules to the term

one gets either the rewrite sequence

append (a ·nil ,nil) ""* a ·append (nil ,nil) ""* a ·nil, or (using only the second rule) simply

Such pattern-directed functional programming is avail­ able in SASL [Turner-79], HOPE [Burstall-MacQueen­ Sannella-80], 0BJ2 [Futatsugi,etal.-84], rewrite languages [Hoffmann-O'Donnell-82], and PLANNER-like languages.

In this paper, we describe how the Knuth-Bendix completion procedure [Knuth-Bendix-70] may be used to generate programs from their (equational) specifications. The completion procedure was originally suggested as a means of generating rewrite systems that can be used to decide the validity of identities in equational theories. Given a finite set £ of equations and a monotonic, well­ founded ordering >- on terms, the procedure generates new rules that follow from [ . Each rule 1-r generated by the procedure is a reduction with respect to :>-, i.e. t :>- t 1 whenever t ~t 1 ( t rewrites to t 1 ) by a single appli­ cation of the rule, and each rule is sound for [, i.e. I =r follows from [ by " replacing equals by equals." Imple­ mentations of the complet ion procedure include REVE [Lescanne-83], RRL at GE [Kapur-Sivakumar-83], and FORMEL at lNRIA [Hullot-80].

A rewrite system synthesized by the completion procedure (and not containing nested defined symbols on left-hand sides) can be translated into a terminating functional program in a straightforward manner~with the pattern-directed invocation eliminated, if desired. For example, the above rewrite system for append could translate to

Function definitions can be translated into Horn clauses in the standard manner [by encoding a rule like f(X)-g(h(X)) as a clause f(X)=Z :- h(X)=Y, g(Y)=Z]. Logic programs differ from fun ctional ones in t.hat output variables in a goal are instantiated by unification with the head of a clause. Rewrite rules equating conjunctions correspond to Horn clauses which may be used to solve goals in that way. For example, a rule of the form

corresponds to the two Horn clauses (one for each con­ junct. that appears on on ly one side):

a rule P-true corresponds to the assertion P. In this way , the above logic-program for append follows from the two-rule system:

Note that, in general, a logic program formed from a rewrite system in this way is not guaranteed to ter­ minate when backtracking is employed in the search for solu tions to a given goal.

A rewrite system is complete (as a functional or logic program) if the patterns on the left-hand sides of its rules cover all possible (variable-free) input values. One can determine that a program is complete, and all cases are covered, using methods described in [Thiel-84, Dershowitz-85, Kounalis-Zhang-85] .

Not all rewrite systems correspond to functional or logic programs. Rewrite rules with nested defined sym­ bols on their left-hand side do not have a straightfor­ ward analogue in all functional languages. And equivalences between formulae other than conjunctions do not have Horn clause counterparts. [Dershowitz-85] describes how a restricted form of completion, called "nar rowing, " can be used as an interpreter for logic programs expressed as rewrite rules that are not neces­ sari ly Horn clauses.

2. COMPLETION

Before we present the completion procedure, we need to define the notion of "critical pair." Let L-R and L 1 -R 1 be two (not necessarily different) rules in a system R whose variables have been renamed, if neces­ sary, so that they are distinct. We say that L 1 overlaps L, if the latter has a su bterm that unifies with the former. More formally, L 1 overlaps L if L contains a (nonvariable) subterm S embedded in some context C~to indicate this we write L=C[S]~such that there is a (most general) substitution u for the variables of the two rules for which S u=L 1 u. If L overlaps L 1 , then the overlapped term Lu (L after making the substitu­ tion u) can be rewritten to either Ru or C[R 1 ]u. These two terms, R u and C [R 1 ]u, are called a critical pair of R.

The comp letion procedure takes as input a finite set [ of equations and a program to compute a mono­ tonic well-founded ordering :>-. (By "monotonic" we mean that C[T]u:>-C[T 1 ]u whenever T:>-T 1 , for any con­ text C, substitution u, and terms T and T 1 .) The pro­ cedure then generates new rules, each of which is a sound reduction:

Completion Procedure

Repeat as long as equations are left in [. If none remain, terminate successfully.

[1] Choose an equation M=N (or N=M) from [ such that M;-N. If none ex1sts, backtrack and undo previous choice. If all choices have been ex­ hausted, terminate with fa ilure (abort).

[2] Add the rule M -N to R.

[3] Use M - N (followed by any rules in R) to reduce the right-hand sides of existing rules to their normal forms .

[4] Add to [ all critical pairs formed from R using M-N.

[5] Remove all the old rules from R whose left-hand side contains an instance of M.

1. Use R to reduce both sides of equations in [ to their nor·mal forms. Remove any equation that reduces to identity.

In general, the completion procedure may go on generating an infinite number of new rules. But, some­ times, despite the backtracking in Step [1], a particular choice of (partial) ordering >- forces the whole pro­ cedure to fail with all equations unorientable. On the other hand, as long as the completion procedure does not terminate in failure, for any equation M =N that follows (logically) from the given rules R (considered as equations), the procedure will eventually generate enough rules for M and N to reduce to the identical term. For this to be the case, the procedure must exe­ cute fairly, by which we mean that no orientable equa­ tion remains in t forever.

The completion procedure has been extended [Peterson-Stickel-81, Fages-83) to rewrite systems that contain associative-commutative function symbols (pos­ sibly with identity element) by considering a somewhat extended notion of critical pair and a unification algo­ rithm for associative-commutative symbols. If f is an associative-commutative symbol, then critical pairs are also formed from overlapped terms of the form f (L'u,X u)=Lu, where X is a new variable, and to which two rules L-R and L'-R' (both with associative-commutative outermost symbols) may be applied.

3. SYNTHESIS

Like other theorem-proving methods, completion can be applied to the task of automatic program syn­ thesis from specifications. The completion procedure itself does the "folding" (that is, the introduction of recursive calls) based upon the axiomatization of the problem domain. Other work on the synthesis of recur­ sive programs includes [Burstall-Darlington-77, Manna­ Waldinger-80, Clark-81, Hogger-81). Specifications are expressed as rewrite rules, i.e. as directed equations or equivalences. The importance of using equivalences in specifications, rather than implications has been pointed out in [Kowalski-79, Hogger-81], and others. Heuristic aspects of the synthesis problem are not addressed in this paper.

Assume that we wish to synthesize a program for some function (or predicate) f, and are given an axiomatization t of the problem domain. We can start the completion procedure off with t and run it until a program R is generated that computes f. (In our examples, we will skip the first stage of completion, starting off with already oriented rules for t , and considering critical pairs as necessary.) The monotonic well-founded ordering supplied to the completion pro­ cedure should ensure that terms containing "specification" symbols are greater than corresponding terms containing the defined goal symbol, which in turn should be greater than the constant true. The choice of ordering guides the synthesis and will affect the program derived . Given the "right" ordering, the pro­ cedure will find a program, if it does not abort on account of inability to orient any equation into a rule, and if a program exists that does not require auxiliary definitions. (See [Dershowitz-85] .) When auxiliary pro­ cedures are needed, their definition may be supplied by the user.

As a simple example of the use of completion to "fold" and "unfold," we synthesize an efficient program to reverse a list, given the naive version that uses append ( cf. the same problem in [Burstall-Darlington77)). The naive program is

The synthesis requires a definition of the auxiliary func­ tion rev:

the append system of Section 1:

and the theorem (associativity of append):

Completion proceeds as follows: The left-hand sides of rules (3) and (5) can be unified by letting Z in (3) be nil and V in (5) be reverse (Y). That generates the crit­ ical pair

Since we want reverse to use rev, the ordering supplied to the completion procedure should make anything con­ taining reverse bigger than a term that does not . That way, the above equation is oriented into a rule

The next step is to overlap the naive reverse program with the definition of rev. Unifying the left-hand side of (1) with the subterm reverse(Y) of (3), by letting Y =nil, gives rise to the critical pair

the left side of which reduces, using ( 4), to just Z. There being only one possible way to orient the equa­ tion Z=rev(nil ,Z) into a (terminating) reduction, that pair results in the rule

Overlapping (3) now with the left-hand side of (2), let­ ting Y =A ·X gives the critical pair

append(append(reverse(X),A ·nii) ,Z) = rev(A ·X,Z). Associativity of append (7) comes in here, rewriting the left side to append (reverse (X),append (A ·nil ,Z)), which becomes rev(X,A ·Z) by applying (6), (4), and (3). With an appropriate ordering (one that begins by look­ ing at the first argument of rev, on which the intended program recurs), that gives the rule

The three rules generated by completion, viz. (810), serve as a functional program for reverse, one that does not itself use append:

This program is complete, since Y covers all lists for reverse and (nil ,Z) and (A ·X ,Z) cover all possible pairs of lists for rev . The program is terminating, since completion used a well-founded ordering to the rules.

4. LOGIC PROGRAMS

Suppose that we are given the following definition of multiplication (for natural numbers):

where + and x are associative and commutative (with ident ities 0 and 1, respectively) , and that we wish to synthesize a program for integer division. We will also need the following four facts , expressed as simplification rules:

Positive integers are represented in unary, as sums of ones. (Associativity and commutativity are needed so that U + W, for example, can be matched with 1+1+1+1, with V=V=1+1.)

The completion procedure starts off with the above rules (1-6) and the specification

The procedure is also given a recursive path ordering (see [Dershowitz-82]) in which function symbols are ordered (from "heavier" to "lighter"): 8, =, <, div, + , 1, 0, true. The synthesis proceeds is as follows:

By overlapping (1) Mx0-+0 on the specification (7) (uni­ fying Y + 1 with M and Q with 0), we get

By overlapping the fact (4) V=U-+true on (8) (unifying X, U, and O+R- the unification algorithm takes the identity 0+ R=R into account), and simplifying the resulting left side X sY 8 true to X sY via (3), we get

Next, by overlapping the fact (5) UsU +Z-+true on (9) (unifying U with X andY with X +Z), we obtain

Now, by using (9) to reduce RsY in the specification (7) to div(R,Y+1,0,R), and multiplying out (Y+1)xQ using (2), we get

Overlapping (ll) with (2) Mx(N + 1)-+MxN + M (let­ ting Q =N + 1) yields

Finally, by overlapping the fact (6) U+W=V+W-+U=V on (12) (using associativity and commutativity of + to let W=Y+1, V=YxN+N+R, and X =V + Y + 1), we obtain the critical pair

The left side reduces by (ll) to div(U,Y+1 ,N,R) , yield­ ing the rule

Rules ( 10) and ( 13) together are a complete pro­ gram. Renaming variables and putting into Horn clause form, we have the following:

The second rule is the recursive case (denominator not greater than numerator); the first is the base case (denominator is greater). The program is complete, since, for any nonnegative integer a and positive integer b, the input pair (x,y) matches (X,X+Z+1) when a <b and (X+ Y + 1,Y + 1) when a ?!!b (X is taken to be 0 for a =b). Executing this program as it stands requires associative-commutative unification for + , with 0 as its identity element; getting around that would require additional programs for unary subtraction and companson.

5. FORWARD REASONING

In this section, we synthesize a rewrite system that can be used to search for an integral position P such that th e input value X lies between f(P) and f(P+1) , for monotonically nondecreasing function f. The resul­ tant logic program computes by "forward reasoning" [Kowalski-79], from facts towards the goal.

The following propositional calculus system ( cf. [Hsiang-Dershowitz-83]) can provide additional logical capability for specifications:

where-, is "not," 8 is "and ," Vis "inclusive-or,"= is "equivalence," and :::> is "implies." Both 8 and = are implicitly associative and commutative. That means, for example, that the rule U 8 U -u applied to (p 8 q) 8 p yields p 8 q . Since these two functions are associative, there is no significance to their parenthesi­ zation, and terms are accordingly "flattened" by remov­ ing embeddings of associative functions symbols, e.g. (p 8 q) 8 p is written p 8 q 8 p . The above system simplifies any two equivalent propositional formulae to the same unique irreducible term.

The completion procedure starts off with the out­ put specification

(X lies between P and P+ 1), input specification

(! is monotonically nondecreasing and X lies between A and A+ N), and facts about transitivity of inequal­ ity:

(Any implication of the form U:::>V can be expressed by a rule U 8 V-U.) The synthesis requires the program­ mer to introduce a generalization pos(P,V) of search(P), and to introduce halving of integers, to guide the synthesis to binary search, rather than linear search. (The ordering on symbols has pos between the specification symbols and the goal symbol search.)

The first step is a requisite generalization of (1) on the part of the programmer:

replacing 1 with Y, and meaning that X lies between P and P+ Y. This generates the rule

in place of ( 1), as well as

by overlapping (7) with (3) and (4). Transitivity (5,6), together with (2), generate

.Jn turn , these and (7) generate

Together, rules (8,10,13,14) give a nondeterministic search program:

Note that the left-hand side of a rewrite rule becomes the list of premisses of a clause used for forward­ reasoning.

To derive a binary search program, we introduce the following definition of halving:

This generates

from (13) and (14) . Rules (8,10,16,17) constitute the binary-search program:

Given values for X, A , and N, along with programs for f and +, this program computes P such that search (P) holds. Starting from the axiom pos (A ,N) , it tests in equalities to add new facts of the form pos (P ,Y), until the fact pos(P,1), and its consequence search(P), are generated.

6. AUXILIARY PROCEDURES

The above approach requires that a program be specifi ed equationally. That means that it may be necessary to give recursive definitions of predicates appearing in specifications. (There is a comparable need of definitions for verification purposes in [Boyer­ Moore-79].) For example, the following insertion-sort program

requires the additional rules

along with "more primitive" rules for inequality.

The specification for the above program may be stated as a conjunction of the requirements that the list Z be ordered in nondecreasing order and that it be a permutation of the list X:

ordered(Z) & permuted(X,Z) Given the facts sorted(X,Z).(1)

(an empty list is ordered) and

(any list is a permutation of itself), the desired base case

is generated.

To generate the recursive case, an auxiliary definition is required . To indicate the desire to sort a list by first sorting its tail, the following definition is added:

From this, completion generates the following sequence of rules: Using the definition of ::>

Using the associativity and commutativity of = (mean­ ing equivalence) in overlapping the fact U =U-+ false with (6) , adding =sorted(X,Y) to both sides of the rules, gives

after simplifying the resultant left side with U=false-+U. Overlapping the fact U & U-+U with (7) adds the conjunct sorted(X,Y) to both sides. Then simplifying the resulting critical pair, using proposi­ tional rules, gives

The latter is the desired recursive call.

The next stage is to synthesize the auxiliary pro­ gram. Adding the fact

will generate the two base cases

Generating the recursive case of inserted requires much more information about ordered. The predicate ordered can be defined in terms of smaller:

i.e. a list beginning with an element B is ordered if (and only if) B is smaller than each element in the remainder of the list and the remainder is itself ordered. The predicate smaller can be defined by

In addition, one needs to know that

This fact must either be given as true, or can itself be proved using the completion procedure. (For the use of completion for inductive theorem proving, see, for example, [Huet-Oppen-80].) The result is

7. IMPLEMENTATION

An implementation of these ideas is underway at the University of Illinois. It is being embedded within the rewrite system environments REVE [Lescanne-83] and RRL [Kapur-Sivakumar-83]. In practice, we have not encountered any difficulty in using the well-founded orderings supplied with these systems to successfully guide the synthesis of programs. Pruning futile paths, on the other hand , is a difficult problem.

ACKNOWLEDGEMENT

I thank Alan Josephson for his critical readings and critical implementation work.