The Automatic Synthesis of Systems of Recursive Programs

I. Introduction

In this paper we describe a system that· attempts to construct a program to meet given specifications. The system, called SYNSYS, accepts specifications expressed in a high-level mathematical notation and produces recursive, side-effect-free LISP programs. The basic approach is to find a sequence of transformations which, when applied successively to the output specification, yield a sequence of equivalent descriptions leading to the desired program.

RICHARD WALDINGER Artificial Intelligence Center Stanford Research Institute Menlo Park, Ca.

The SYNSYS system has been partially described in an earlier paper (Manna and Waldinger (1977)). In that discussion we emphasized the mechanisms for introducing conditional expressions and recursion into the program being produced. The exposition in this paper Is self-contained, but our principal concern here will be the formation of systems of recursive programs.

The earlier paper also contained a more complete description of the SYNSYS implementation. The transformation rules of the system are written in QLISP (Wilber (1976)), an extension of INTERLISP with pattern-directed function invocation and backtracking. The two examples we present have been performed automatically by SYNSYS.

In Section II we describe our basic approach. We then (Section III) present the first example, the synthesis of the Euclidean algorithm. Section IV provides a discussion of the method for introducing auxilliary functions, which is then illustrated by the construction of a two-function system for computing Cartesian products (Section Y). A final section outlines some of the system's limitations, and our future research plans.

II. Basic A pproaoh

There are many constructs that are valuable in expressing the specifications of a program, but that are not likely to appear as features in a programming language. For example, in specifying a program to compute the greatest common divisor of two integers x and y, we provide the input specification

x ~ 0 and y ~ 0 and (x ,. 0 or y " O) ,

and the output specification

gcd(x y) <· max{z: zlx and zly} .

The output specification requires that we find the greatest integer that divides both x and y. The input specification states that we can expect both arguments to be nonnegative and at least one to be nonzero; if both x and y are zero, the output specification Is not defined. The set constructor {z : ... ) is a valuable aid in expressing the output specification, but it Is not a primitive construct ln most programming languages because it Is not always computable.

Similarly, to specify the program to find the maximum element of a list of numbers, we may supply the input specification

..., empty(x)

(the input list ls not empty) and the output specification maxl(x) <· find z e x and z : z ~ all(x)

(find an element of the given list greater than or equal to all the elements of the list). Here, the constructs "find z : .. ." and "all(x)" are not primitives of any programming language, but are useful components of a specification language.

The goal of a synthesis system is to transform the output specifications into an equivalent description that employs only primitive constructs. The resulting primitive program will then be executable.

Our basic approach is to supply our system with a large set of transformation rules, which transform one description into another, equivalent one. We attempt to find a sequence of these rules which, applied to the output specification, will yield a sequence of equivalent descriptions leading to the desired primitive program. Some of these rules express the semantics of the subject domain (such as facts about lists, sets, numbers and the underlying logic). For example, the rule

represents the fact that every integer divides zero. Other rules express knowledge about the programming language and programming techniques (e.g. the uses of conditional expressions and recursive calls).

A given transformation can only be applied to a description that matches a characteristic pattern. For instance, the above rule can only be applied to descriptions of the form u I v. However, even if the pattern matches the description, a rule may have conditions that prevent it from being applied; the sample rule above can be applied only if the value of the expression that matches v is known to be zero. This logical condition is imposed because the rule could not be applied legitimately it it were violated. Other conditions may be imposed because of strategic considerations; we know that it is unwise to apply the rule when the condition is violated, even though the application would be logically legitimate. For example, the rule

u I v and u IIV ·> u I v and u I rem( IV v)

(the common divisors of v and IV are the same as the common divisors of v and rem(IV v)) has the logical condition

and the strategic condition that we not be able to prove

A It hough the rule could be applied correctly when IV < v, in that case rem( IV v) reduces to w, and the original expression "u I v and u I IV" would reappear.

During · the process of transforming the output specification into a primitive program, we generate a sequence of intermediate descriptions of the desired program. In searching for the next rule to apply, we may find several rules whose patterns match the current description. Most of these rules will be discarded because their conditions will not be satisfied. Of the rules that remain, the system will apply one. If that application fails to lead to a primitive program, backtracking may occur so that the other rules may be attempted instead. The synthesis is complete when a primitive program is generated.

In order to examine the synthesis process in more detail, we present_ the complete construction of a familiar algorithm.

III. Example 1: The Euclidean Algorithm

In this example we illustrate the construction of the classical Euclidean algorithm for computing the greatest common divisor gcd(x y) of two nonnegative integers x and y.

Recall that the specifications for the program are:

input specification: x ;?; 0 and y <: 0 and (x " 0 or y " O)

(the arguments are both nonnegative and at least one of them is nonzero), and

output specification: gcd(x y) <· max{z : z I x and z ly}

(the output is the greatest integer that divides both x and y).

The set constructor {u : ... } is admitted to our specification language but is not a primitive of our programming language. We must find a sequence of transformations to produce an equivalent description of the output that does not use the set constructor or any other nonprimitive construct. This description will be the desired primitive program. In what follows we will exhibit a successful sequence of transformations, but we will not always indicate hqw the next transformation at a given stage was found, or which sequences were attempted and discarded before the successful sequence was found.

Among the transformations we may apply, let us assume we have the following rules which express properties of division useful in developing the desired program:

For any integers u, v, and w

• (I) u I v ·> true if v · 0 (any integer divides zero)
• u I v and ul w ·> ul v and u I rem(ru v) if v " 0 (the common divisors of v and w are the same as those of v and rem(w v)), and
• max{u : ulv} ·> v ifv > 0 (any positive integer is its own greatest divisor).

In applying these transformations, we will produce a sequence of goals; the first will be derived directly from the output specification, and the last will be the desired program itself.

Goal 1: Compute max{z : z I x and z ly}.

for any x and y satisfying the input specification. The transformation (2) above,

u I v and u I w ·> u I v and u I rem(w v) if v " 0 ,

applies directly to Goal I, yielding

Goal 2: Compute max{z : z I x and z I rem(y x)} and prove x " 0 .

Note that the condition v " 0 attached to the transformation rule produced a condition x .. 0 to be proved in the resulting goal. We cannot prove or disprove this condition --it may be true for some inputs and false for others -- so we will consider separately the case in which it is false. This case analysis will yield a test on the condition x · 0 in the final program.

Case: x · 0

We cannot achieve Goal 2 here, so we examine alternate transformations to apply to Goal 1. The rule (1),

and the basic logical transformation

yield

Here, the transformation rule (3) applies, producing

It is straightforward to prove y > 0, because y 2: 0 and (x " 0 or y " 0), by the input specification, but x · 0 by our case assumption. Consequently, we have reduced the problem in this case to the task of computing y, which involves no nonprimitive constructs. The desired program may simply output

We have thus completed one branch of our case analysis; the corresponding branch of the program is

We now turn to the alternate possibility.

The case analysis was introduced in attempting to satisfy the condition x " 0 of Goal 2. This condition is satisfied In this case, and Goal 2 is reduced to

Goal 5: Compute max{z : z I x and z I rem(y x)}.

Goal 5 is an instance of our output specification (i.e. Goal I), with x and y replaced by x and rem(y x). This suggests achieving Goal 5 by a recursive call to gcd(x rem(y x)), because the gcd program is intended to satisfy all instances of its output specification. However, the program is only guaranteed to work if its input specification is satisfied. To insure that the recursive call gcd(x rem(y x)) will compute the desired result, we must prove that the input specification is satisfied by the arguments of the recursive call, i.e.

We will call Goal 6 the input condition for the recursive call gcd(x rem(y x)).

Furthermore, in introducing a recursive call we must be concerned with the termination of the final program. In other words, we must ensure that an infinite sequence of recursive calls cannot occur- in any computation of the program. To prove termination we employ the concept of the well-founded set, one whose elements are ordered in such a way that no infinite decreasing sequence can exist. (The nonnegative integers, for ex ample, constitute a well-founded set under the usual greater­ than ordering. The integers, on the other hand, do not.)

To prove the termination of a program j(x) with one recursive call j(t), we must find a well-founded set W 1 with ordering > f such that

If a infinite sequence of recursive calls were to occur, the corresponding arguments would constitute an infinitely decreasing sequence of elements of W 1 , contradicting the well­ foundedness of W,.

Thus, to show the termination of the recursive call gcd(x rem(y x)) in the program gcd(x y), we must achieve the following termination condition:

Goal 7: . Find a well-founded set W ,cd with ordering > t<d such that (x y) E W t<d and (x rem(y x)) E W red and (x y) > ,rJ (x rem(y x)) .

We cannot satisfy Goal 7; in fact, in the case that y < x, rem(y x) · y, and there is no well-founded ordering > such that (x y) > (x y). Because we cannot show the termination of the recursive call gcd(x rem(y x)) that was introduced in an attempt to achieve Goal 5, we look for an alternate approach to achieve this goal.

The logical transformation

applied to Goal 5 yields

Goal 8: Compute max{z: z I rem(y x) and z I x).

Goal 8 is again an instance of our output specification, Goal I, and we therefore attempt to achieve it by the recursive call gcd(rem(y x) x). Actually, the SYNSYS system reaches this goal in a slightly different manner to be discussed below. The input condition for this recursive call is

and the termination condition is

Goal 10: Find a well-founded set W t<d and ordering > grd such that (x y) E W crJ and (rem(y x) x) E W ,,J and (x y) >red (rem(y x) x) .

Goal 9 is satisfied immediately: in this case x is positive and rem(y x) is always nonnegative. To achieve Goal 10, we take W ,rd to be the set of all pairs of nonnegative integers ordered by the usual > ordering applied to the first component; this suffices because x > rem(y x). The proposed recursive call is therefore successful in achieving Goal 8 and the program can output

gcd(rem(y x) x)

We have succeeded in transforming all the goals into primitive program segments. The final program, formed directly from the outlined program segments is ·

This is a recursive version of the algorithm Euclid provided for computing the greatest common divisor.

Recall that when we fail to achieve Goal 5,

Compute max{z : zjx and zlrem(y x)}

by a recursive call, we applied a logical transformation

to the goal and then successfully introduced a recursion. Actually, the SYNSYS system does not represent the commutativity of "and" by a transformation; that property is built into the underlying QLISP system. Normally, in QLISP, a function f applied to several arguments u1, u2, ... , un is represented internally as f<u 1 u2 ... un>, where <u1 u2 ... Un> is an ordered tuple. An expression such as

however, is represented internally as

where {u 1 u2 ... unJ is an unordered set, because the order and multiplicity of the arguments does not influence the value of the expression. In attempting to introduce a recursive call, the system tried to match the subexpression and{x rem(y x)} of Goal 5 against the subexpression and{x y} of Goal I. The Q..LISP pattern matcher discovered two distinct matches, pairing x and y with x and rem(y x) or pairing x and y with rem(y x) and x. When the first match failed to lead to a satisfactory recursion, the second match was attempted automatically.

The m~chanisms employed to construct the gcd program are examined more closely in our earlier paper (Manna and Waldinger [1977]). A similar mechanism to ours for introducing conditional tests into synthesized programs has been implemented by Warren [1976]. A facility for initiating a case analysis in a mathematical proof is included in the theorem proving system of Bledsoe and Tyson [1977]. Our recursion­ introduction device is the same as the "folding" rule of Burstall and Darlington [ 1975]; their system is interactive, however, and they require that the user be responsible for establishing the input and termination conditions.

IV. Introducing Auxillia.ry Functions

In the preceding example we introduced a .recursive call when we discovered that a subgoal was an instance of our output specification, the top-level goal. In other words, we found that the subgoal is of form

Compute cx(t(x)) ,

where the top-level goal is of form where

If the input specification is P(x), then a recursive call j(t(x)) could be introduced to achieve the subgoal "Compute cx(t(x))", provided we could prove the input condition

P(t(x))

and the termination condition

Find a well-founded set W 1 with ordering > 1 such that x € W 1 and t(x) € W 1 and X >I t(x) .

Actually, in attempting to introduce recursion we compare the subgoal not only with the top-level goal, but also with each of the intermediate subgoals. If we discover that our subgoal is of form

Compute !i(t(x))

Compute ,:J(x)

is an intermediate subgoal, then we introduce a new auxilliary function g whose output specification is

The subgoal "Compute il(t(x))" might then be achieved by a recursive call g(t(x)).

Of course to introduce a recursive call to an auxilliary function, we must establish the appropriate input and termination conditions. The input specification for the auxilliary program is not the same as the input specification P(x) for the entire program f. For, suppose that in developing the subgoal "Compute ,:J(x)," we have made several case assumptions "Case R 1 (x)," ... , "Case R,.(x)". Then the conditions R1(x), ... , R,.(x) will be the tests of conditional expressions in the final program f, and must be true if control is to reach the call to g(x). Thus, we may expect that the conjunction Q.(x) of all these tests with the original input specification, i.e.

will be true of the input to g. Moreover, the .correctness of g may depend on the truth of the above conjunction Q.(x),which we therefore take as the input specification for g. The input condition for a recursive call g(t(x))) is then Q.{t(x)), i.e.

In the simple case that the auxilliary function g does not call the main function f, the termination condition for a recursive call g(t(x)) is analogous to the termination condition for a recursive call to f, i.e. we must

Find a well-founded set W 1 with ordering > 1 such that x € W 1 and t(x) € W 1 and x > 1 t(x) .

The general case, in which g may also call f, is more complicated and will not be considered here.

In the next section we illustrate the formation of auxilliary functions in a concrete example.

V, Example 2: The Cartesian Product

A problem that requires the formation of a simple system of recursive programs is the computation of the Cartesian product cart(X Y) of two (finite) sets X and Y. This is set of all pairs (x y) such that x e X andy e Y. The output specification is therefore

There is no input specification, because the program is intended to appl.Y to any two sets. Again, the set constructor {z : ... ) is regarded as a nonprimitive component of our specificaton language. We include in our programming language the fotlowing primitive operations:

u {t,, 12, ... , t.} { } empty(U) head(U) ~aii(U) (u v) set union the finite set of elements t 1, 12, ... , t. the empty set the test for emptiness a specific element of a nonempty set U the set of elements of U other than head(U) the pair with elements u and v

and if-then-else and recursion. Let us assume that the transformations we can use in transforming the goat include

• (I) Membership expansion u e U ·> if empty(U) then false else u = head(U) or u e taii(U) ;
• Empty-set introduction

{u :false} ·> {};

1. Union introduction

{u : P(u) or Q.(u)} => {u : P(u)} u {u : Q.(u)} ; and

1. Equality elimination

where u and t are expressions with no variables in

• {u : u · I} ·> I, common.

Applying membership expansion rule (I) to the subexpression x e X of Goal 1. yields

Goal 2: Compute {(x y) : [if empty(x) then false else x · head(X) or x e taii(X)) andy e Y} .

Applying the logical if-then-else distribution rule

yields

We next apply the logical transformation

to the then-clause, and the and-or dimibution rule to the else-clause, to obtain

Goal 4: Compute if empty(X) then {(x y) :false} else {(x y) : (x · head(X) and y e Y) or (x e taii(X) and y e Y)} .

The empty-set introduction rule (2) applies to the then-clause of Goal 4 and the union-introduction rule (3) applies to, the else­ clause, to produce

Goal 5: Compute if empty(X) then {} else {(x y) : x = head(X) and y e Y) u {(x y) : x e laii(X) andy e Y) .

The subexpression {(x y) : x e taii(X) andy e Y} is an instance of our output specification,

this suggests replacing this subexpression by a recursive call

There is no input condition for the proposed recursive call because the desired program has no input specification. The termination condition,

Goal 6: Find a well-founded set w,.,, and ordering > ,.,, such that (x y) e W ,.,, and (taii(X) Y) e W '"" and (X Y) >,.,, (taii(X) Y).

is solved by taking W '"'' to be the set of all pairs of finite sets, ordered by the usual proper containment relation on the first component. This ordering is sufficient because X property contains taii(X).

Goal 5 is therfore reduced to

Goal 7: Compute if empty(X) then {} else {(x y) : x · head(X) and y e Y} u cart(taii(X) Y) .

We still have to remove the remaining set-constructor from the else-clause. To simplify the exposition we will reduce this subexpression In a separate series of starred subgoals

Applying the member expansion rule (1) to the subexpression y e Y yields

Applying the if-then-else distribution rule and the union­ introduction rule (3) produces

Goal 9*: Compute if empty(Y) then {(x y) : x · head(X) and false} else {(x y) : x = head(X) and y · head(Y)J u {(x y) : x = head(X) andy e taii(Y)} .

The then-clause of Goal 9* is transformed by the logical rule

and the empty-set introduction rule (2). The first component of the else-clause is transformed by the equality-elimination rule (4). The resulting goal is

Goal 10*: Compute if empty(Y) then {} else {(/zead(X) head(Y))} u {(x y) : x = head(X) andy E taii(Y)} .

Now the subexpression

is an instance of Goal 7*. This sugg·ests that we introduce an auxilliary function cart2(X Y) to achieve Goal 7*, and replace the above subexpression by the recursive call cart2(X taii(Y)). To establish that this proposed recursive call is legitimate, we must prove its input and termination conditions.

Even though the main program cart(X Y) had no input specification, the auxilliary function cart2(X Y) is applied in the else-branch of the program, for which it is known that X is not empty. This condition -, empty(X) is therefore the input specification for cart2(X Y). Thus, the input condition for the recursive call cart2(X taii(Y)) is simply

This condition is satisfied immediately, because it is identical to the input specification for cart2(X Y).

The termination condition for the recursive call cart2(X tall(Y)) is

Goal 12*: Find a well-founded set Ww, 2 with ordering > ,.,, 2 such that (X Y) E W w<2 and (X taii(Y)) E W '"" 2 and (X Y) >w, 2 (X taii(Y)) .

Goal 12* can be achieved by taking Ww, 2 to be the set of all pairs of finite sets, with the usual proper containment ordering applied to its second component.

Having established both the input and termination conditions, we are justified in introducing the recursive call cart2(X taii(Y)) into Goal 10*, yielding

Because Goal 13* is composed entirely of primitive constructs, we have succeeded in constructing the auxilliary function

cart2(X Y) <· if empty(Y) then {} else (head(X) head(Y)) u cart2(X tall(Y))

This program computes the Cartesian product of {head(X)) with Y.

The auxilliary function cart2(X Y) is intended to satisfy Goal 7*, a subexpression of Goal 7. We can therefore replace that subexpression by a call to the new function, yielding

Goal 14: Compute if empty(X) then {} else cart2(X Y) u cart(tail(X) Y) .

Now Goal 14 contains no nonprimitives and we have succeeded in constructing the desired program

VI. Limitations and Future Research

The preceding example illustrates construction of the simplest form of auxilliary function, which does not call the main function . The general case is more difficult, and is beyond the capabilities of our current system because of the complexity of the termination condition.

We introduce a recursive call only when a subgoal is an instance of a higher-level subgoal. For some problems it may be necessary to generalize the higher-level subgoal to force the match to occur. This situation is analogous to proving a mathematical theorem by mathematical induction: it is often necessary to generalize the theorem to be proved, so that the induction hypothesis will be strong enough for the induction step to be proved. Some such generalizations have been performed automatically by the theorem-proving system of Boyer and Moore [I 975), and the program synthesis system of Darlington [1975).

Our current SYNSYS only constructs pure LISP programs, which produce an output value bllt do not have any side-effects. Systems by Warren [1974) and Waldinger [1977) can produce programs with side-effects, but they cannot introduce recursive or iterative loops into these programs. We intend to integrate both abilities into a single system.

VII. References

• Bledsoe, W. W., and M. Tyson [1977), Typing and proof by cases in program verification, in Machine Intelligence 8: Machine Representations of Knowledge, (E. W. Elcock and D. Michie, editors), John Wiley & Sons, New York, N.Y. (to appear).
• Boyer, R. S., and J S. Moore [Jan. 1975], Proving theorems about LISP junctions, JACM, Vol. 22, No. I, pp. 129-144.
• Burstall, R. M. and J. Darlington [April 1975], Some transformations for developing recursive programs, Proceedings of the International Conference on Reliable Software, Los Angeles, Ca., pp. 465-472.

• Darlington, J. [July 1975], Applications of program transformation to program synthesis, Colloques IRIA on Proving and Improving Programs, Arc-et-Senans, France, pp. I 33- I H .
• Manna, Z. and R. Waldinger [August 1977], The automatic synthesis of recursive programs, Proceedings of the SIGART-SIGPLAN Symposium on Artificial Intelligence and Prog·ramming Languages, Rochester, N.Y.
• Waldinger, R. J. [1977], Achieving several goals simultaneously, in Machine Intelligence 8: Machine Representations of Knowledge, (E. W. Elcock and D. Michie, editors), john Wiley & Sons, New York, N.Y. (to appear).
• Warren, D. H. D. [June 1974], WARPLAN: A system for generating plans, Technical Note, Dept. of Computational Logic, University of Edinburgh, Edingurgh, Scotland.
• Warren, D. H. D. [July 1976], Generating conditional plans and programs, Proceedings of Conference on Artificial Intelligence and Simulation on Behaviour, Edinburgh, Scotland, pp. 311-351.
• Wilber, B. M. [Mar. 1976], A QLISP reference manual, Technical note, Stanford Reserch Institute, Menlo Park, Ca.