A Problem Reduction Approach to Program Synthesis

I Introduction

Program synthesis is the derivation of a computer program from a specification of the problem it is intended to solve. Human programmers often cope with complex problems in the following top-down manner. First an overall program structure is created which fixes certain gross features of the desired program. Some parts of the structure are at first underdetermined but their functional requirements are worked out so that they can be treated as relatively independent subproblems to be solved in a similar manner at a later stage. A formal counterpart to this approach involves the use of program schemas. A schema provides the overall structure of the desired pro­ gram and its uninterpreted operator symbols stand for the underdetermined parts of the structure. To use a schema we require a corresponding design strategy. Given a prob­ lem specification I1 a design strategy derives specifications for subproblems in such a way that solutions for the sub­ problems can be assembled {via the schema) into a solu­ tion for II. A design strategy then is a way of generating an instance of a schema which satisfies a given specification.

Given a collection of such schemas and their associ­ ated design strategies the problem recfu.ction approach to program synthesis can be described by a two phase pro­ cess the top-down decomposition of problem specifications and the bottom-up composition of programs. In practice these phases are interleaved but it helps to understand them separately. We are given an initial specification. In the first phase a design strategy is selected and applied to the initial specification thereby generating some subproblem specifications. Then design strategies are selected and applied to each of the subprob­ lem specifications, and so on. This decomposition process terminates in primitive problem specifications which can be solved directly, without reduction to subproblems. The result is a tree of specifications with the initial

· The work reported herein was supported by the Foundation Research Program of the Naval Postgraduate School with funds provided by the Chief of Naval Research.

TI:x = z such that I:x => O:<x,z> where TI:D-+R

or more compactly, TI = <D,R,I.O>. We ambiguously use the symbol n to denote both the problem and its specification. Here the input and output domains are D and R respectively. The input concii.ti.on I, a relation on D, expresses any properties we can expect of inputs to the desired program. If an input does not satisfy the input condition then we don't care how the program behaves. The output condition 0, a relation on DxR, expresses the properties that an output object should satisfy. Any out­ put object z such that O:<x,z> holds will be called a feasi­ ble output with respect to input x. We say program. F sa.tisfies specifica.l:i.on TI = <D.R.I,O> with dllrived. input condition I' if

is valid in a suitable first-order theory +. If I' is the Boolean constant true then we simply say F satisfies TI. In our synthesis method we attempt to derive a program F and a derived input condition I' from a given specification. In this paper, however, we focus on the derivation of F and for the sake of simplicity omit discussion of the derivation of derived input conditions.

ill A Class of Divide and Conquer Programs

The following schema represents the structure com­ mon to a class of divide and conquer programs:

then Directly_.Eolve:x

else Compose·(FxF)·Decompose:x.

Here f·g. called the composition of f and g. denotes the function resulting from applying f to the result of applying g to its argument. fxg, called the product of f and g, is defined by fxg:<x.y> = <f:x,g:y> where <.:z: 1, ... ,x,.> is ann­ tuple . It is convenient to allow functions to map tuples to tuples. ·

The behavior of an instance of the schema can be described as follows: if q:x holds then F:x evaluates to Directly_.Eolve:x. Otherwise, x is decomposed via Decom­ pose into a 2-tuple which is recursively processed in paral­ lel by FxF. The resulting 2-tuple is composed via Compose thus yielding the value of F:x.

Our design strategy for this schema is based on the following theorem which provides sufficient conditions that an instance of the schema satisfies a given specification. The separability condition (4) provides the most important constraint on the relationship between the output condi­ tion 0 of an instance of the schema and the output condi­ tions of Decompose and Compose. In words it states that if iniM!t z 0 decomposes into subinputs z 1 and z 2 , and z 1 and z2 are feasible outputs with respect to these subinputs respectively, and z 1 and z 2 compose to form z0 , then z 0 is a feasible solution to input z 0· Loosely put: feasible out­ puts compose to form feasible outputs.

1heorem 1: Let D and R be sets, I a relation on D, 0 a rela­ tion on DxR, ~ a relation on DxDxD, Oc a relation on RxRxR, and >- a well-founded ordering on D. If

1. Decompose satisfies the specification

DECOMPOSE:z 0 = <.:z: 1,z2> such that I:x => I:z 1 /\ I:z 2 /\

x 0 )-z1 /\z0 ')..z2 /\ OD :<zo.x1,x2> where DECOMPOSE:D-+DxD

with derived input condition ~q;

1. Compose satisfies the specification

• where COMPOSE:RxR-+R;
• Directly_.Eolve satisfies the specification

DIREC'ILY_.EOLVE:x = z such that q:x /\ I:x => O:<x,z>

where DIRECTLY_.EOLVE:D-+R.

• ( 4) the following separability concii.tion holds

then the divide and conquer program

then Directly_.Eolve:x else Compose·(FxF)·Decompose:x

satisfies specification TI = <D.R.I,O>.

Proof: A generalized form of this theorem is proved in (Smith, 1982b) .

The key idea in our design strategy for divide and con­ quer algorithms is to use the separability condition like an equation in three unknowns (0, Oc. and OD) : given values for any two we attempt to solve for a value of the third. Initially we are given a specification TI = <D.R.I.O> so we have 0. During synthesis we wish to determine the specifications of the subproblems Decompose and Compose - in essence OD and Oc respectively. One approach is to a) choose a simple known operator D as say, Decompose, b) use the separability condition to "solve for" Oc. then c) form a detailed specitlcation for Compose based on Oc. We turn now to a formal deductive system which enables us to derive output conditions like Oc.

IV 'l'he Precondition Problem

The traditional problem of deduction has been to find a proof of a given formula in some theory. A more general problem, which we call the preconcii.ti.on problem (Smith, 1982a), is most simply stated in the propositional calculus: given a goal A and hypothesis H. find a formula P, called a precondition. such that P/\H => A is a tautology. In other words P provides any additional premises under which A can be shown to follow from H. A more complex definition is required in a first-order theory +. Let Q1z 1 Q~2 .. . Q,z, G be a closed formula not necessarily in prenex form where Q is either 3 or 'v" for i=1,2, ... ,n. A fz~oz2·' · · ,x,.j-preconcii.ti.on of QtZt Qa.:J:2 ... Q,x,. G is a quantifier-free formula P dependent only on variables Z~o%2, ... ,z, such that

is valid in+.

For example, consider the formula

1. "i=O" is a HI-precondition of (1) since

• holds,
• "~j' ' is a !i,jj-precondition of (1) since

holds.

Note that false is a precondition of any formula. In gen­ eral we are interested in preconditions which are as weak as possible yet have a structurally simple form.

Continuing our discussion from the previous section, suppose that we are given a relation 0 on DxR and we have chosen a decomposition operator Decompose with output condition OD · We wish to derive an output condition Oc for the, as yet unknown, operator Compose . To do so we pose the problem of finding a !z0,z 1,z 2j-precondition of

Let Oc be such a precondition, then we have by definition that

holds . That is, any !z 0 ,z 1,z 2j-precondition of (2) enables the separability condition to hold and thus can be used as an output condition for Decompose.

V A Formal System. for Deriving Preconditions

In this section we present a natural deduction-like for­ mal system for deriving preconditions. More extensive sys­ tems are presented in (Smith, 19B2a; Smith, 19B2b).

A. Reduction Rules

A reduction rule generates a precondition for a goal formula by decomposing it into subgoals, then composing the derived preconditions of the subgoals. The following rules are for the most part extensions of typical goal reduction rules (Bledsoe, 1977). Only those rules required by our example are presented. We use the notation Z where H = !h 1 ,h2, ... ,ht! as an abbreviation of the formula

• Rl. Reduction of Cant.ncf:i:ve Goals - if the goal formula has the form B ~ then generate subgoals Z and ;;. It p and Q are derived preconditions of Z and k respec­ tively, then return P/\Q as derived precondition of B/\C n·
• R2. Substitution of Equal Terms - if the goal is Z where G contains an occurrence of a term r , and r ' = s' is an

axiom in -J1 or hypothesis in H, and, unifies !r.r '! then generate the subgoal �[s'~/r] (G with s', replacing an occurrence of r) . It P is a derived precondition of G[ s'J/ r] then return P as derived precondition of ;;.

B. Primitive Rules

We also use two rules , called primitive rules, which can directly generate a precondition for a goal.

• P l. If the goal is Z and substitution, unifies G with either an axiom of -{1 or an hypothesis in H, then generate the precondition true .
• P2. If the goal is Z and we seek a !.:t: 1, ... ,.:t:n!·precondition and G and H' depend only on the variables .:t:t , .... .:I:n where H' has the form ;~t~ and !~!;= t .m !: H, then generate the precondition H'=>G.

C. 'lb.e Deduction Process

The derivation of a precondition of goal statement Z can be described by a two stage process. In the first phase reduction rules are repeatedly applied to goals reducing them to subgoals. Primitive rules P1 and P2 are applied whenever possible. The result of this reduction process can be represented by a goal tree in which 1) nodes represent goals/subgoals, 2) arcs represent reduction rule applications, and 3) leaf nodes represent goals to which a primitive rule has been applied. The second phase involves the bottom-up composition of preconditions. Initially each application of a primitive rule to a goal yields a precondi­ tion. Subsequently whenever a Jrecondition has been found for each subgoal of a goal H then a precondition is composed for Z according to the reduction rule employed. In a working system we have developed a single precondi­ tion is selected from amongst the alternative derived preconditions of a goal by maximizing t>ver a heuristic measure of weakness and structural simplicity. A detailed presentation of the derivation of a precondition is provided in the following section.

VI Synthesis of a llergesort Algorithm

Consider again the specification

SORT:x = z such that Bag:x = Bag:z /\ Ordered:z where SORT:LIST(N) .... LIST(N) .

As indicated above , we shall proceed with the synthesis of a divide and conquer algorithm by trying to establish the conditions of Theorem 1. The main task before us is to find operators Compose and Decompose whose output condi­ tions satisfy the separability condition. One way to proceed is to select some simple known operator for either Decompose or Compose. Suppose we concentrate on Decompose. We know it is to map LIST(N) to LIST(N)xLIST(N) . An appropriately structured Data Struc­ ture Knowledge Base should allow us to retrieve all known operators which perform such a mapping. Suppose we have avallable the operator Split which decomposes its input list into two halves of roughly equal length. Split can be specified as follows:

Split:z 0 = <x1,z2> such that Length:z 1 = Length:z 0 div 2 /\ Length:.:t:2 = (1+Length:z 0) div2 /\ .:t: 0 = Append:<x 1,z2> where Split:LIST(N) .... LIST(N)xLIST(N) .

By x div k we mean integer division by k. In order to verify that Split can be used as the Decompose operator we instantiate the specification of Decompose (condition (1) of Theorem 1) as follows :

i . replace the input conditions I:x 0 , I:x 1, and I:x2 with true (the input condition of SORT);

ii. replace x 0 )-x 1 and x 0 ?-x2 with Length:x0>Length:x 1 and Length:x0>Length:x2. See (Smith, 19B2b} for details of selecting a suitable well-founded ordering on the input domain;

iii. replace On with the output conditions of Split;

1. replace the input and output domains of Decompose with the input and output domains of Split respectively.

It is easy to prove that Split satisfies the resulting specification with derived input condition Length:x0> 1. Intuitively, the meaning of the cierived input condition is that only inputs of length greater than 1 are decomposed by Split into strictly smaller sublists.

We next attempt to create a specification for Compose which has the form given in condition (2) of Theorem 1. To do so, we need to derive an output condition Oc. In order to find an output condition Oc we set up the following precondition problem (as discussed in Section IV) : Find a (z0 ,z 1,z2!-precondition of

'v' <z0,z1,z2>eLIST(N)xLIST(N)xLIST(N)

'v' <x0,x 1,x2>eLIST(N)xLIST(N)xi.JST(N)

[Length:x0> Length:x 1 A Length: xo> Length:x 2 A

Length:x 1 = Length:x0 div 2 A

Length:x2 = (1+Length:x0) div 2 A Append:zo = <x 1.x2> A

Bag:x 1 = Bag:z 1 A Ordered:z 1 A

Bag:x2 = Bag:z2 A Ordered:z2

:::::;. Bag:x0 = Bag:zo A Ordered:zo].

This precondition problem has been created from (2) by replacing

i . 0 with the output condition of SORT,

1. D and R with the input and output type (LIST(N)) of SORT, and .

iii. 0J with the output conditions of Split.

The derived precondition gives us an output condition for Compose which satisfies the separability condition of Theorem 1. A derivo.tion of the precondition

is presented in Figure 1 and described below. For concise­ ness we list the hypotheses separately at the top of the derivation. To the left of each goal node in this tree and in brackets is given the derived precondition of the goal. The arcs of the goal tree are annotated with the name of the rule and axiom or hypothesis used. The primitive rule used on each leaf node is also noted. In this example the given goal Bag:x0 = Bag:z 0 A Ordered:z 0 is reduced by application of the rule R1 (reduction of a conjunction}. The primitive rule P2 is applied to the subgoal Ordered:z0 yielding precondition

The subgoal Bag:x0 = Bag:z 0 is reduced by application of rule R2 and hypothesis h1 to and then further reduced via axiom

to

Applying rule R2 with hypotheses h6 and hB the subgoal (4) finally reduces to

This formula is expressed in terms of the desired variables zo, z 1, and z2 only so primitive rule P2 can be applied yielding the pre~ondition

In the composition phase of the derivation the precondi­ tions generated by the primitive rules are passed up the goal tree and composed. Each newly composed precondi­ tion is then run through a simplification process. We record only the simplified form of a composed precondi­ tion. Finally (3) is formed by simplifying the conjunction of (4) and (6).

A specification for Compose is created by instantiating condition (2) of Theorem 1 as follows:

i . replace Oc by (6):

ii. replaceD and R by LIST(N) .

The resulting specification describes the problem of merg­ ing two sorted lists into a single sorted list:

Merge:<z 1,z2> = z 0 such that Ordered:z 1 A Ordered:z 2

:::::;. Union:<Bag:z 1,Bag:z 2> = Bag:z 0 A Ordered:z 0

In (Smith, 19B2b) we derive a divide and conquer algorithm which satisfies this specification.

It remains to synthesize a program for Directly....Solve. From the verification of Split we obtain Length:x>l as ~q: x, thus we take Length:~1 as q:x. Instantiating the specification in condition (3} of Theorem 1 we obtain

DIRECTLY....SOLVE:x = z such that Length:xsl:::::;.

where DIRECTLY ....SOLVE :LIST(N} .... LIST(N)

It is easily shown that the identity function satisfies this specification.

Finally the operators constructed above are assem­ bled into the following mergesort program:

Msort:x = if Length:~1

thenx

else Merge·(MsortxMsort)·Split:x

According to Theorem 1 this program satisfies specification SORT. In other words, Msort terminates with a feasible output on all input lists.

Hypotheses: hl. Append:<x1,x2> = Xo

h2. Length:x1 = Length:x0 div 2

h3. Length:x2 = {1+Length:x0) div 2

h4. Length:x0 > Length:x 1

h5. Length:x0 > Length:x2

h6. Bag:x1 = Bag:z 1

h7. Ordered:z 1

hB. Bag:x 2 = Bag:z2

h9. Ordered:z 2

where Q1 is Ordered:z 1 /\ Ordered:z 2 ~ Union:<Bag:z 1,Bag:z 2> = Bag:zo.

Q2 is Ordered:z 1 /\ Ordered:z2 ~ Ordered:z0 , and

Q3 is Ordered:z 1 /\ Ordered:z2 ~

Union:<Bag:z 1,Bag:z2> = Bag:z0 /\ Ordered:z0

Figure 1: Derivation of output conditions for Merge.

vn Concluding Remarks

Several of the choices made during the derivation of mergesort were arbitrary in the sense that alternatives were available which lead to other sort algorithms. If we had chosen to select a simple Compose operator, say Append, we would derive a Quicksort algorithm. With a slight variation on the divide and conquer program schema analogous derivations lead to insertion and selection sorts. Each of these four sort algorithms are derived in detail in (Smith, 1982b). See (Green and Barstow 1978; Clark and Darlington, 1980) for related derivations of these sorting algorithms.

Our problem reduction approach is most closely related to theorem proving approaches to program syn­ thesis (e.g. Bibel, 1980; Manna and Waldinger, 1980). which. given a specification il=<D,R,I,O>. extract a pro­ gram F from a constructive proof of the theorem

In contrast, the problem reduction approach extracts a program F from a constructive derivation of an !x!­ precondition of {7). The resulting precondition is the derived input condition of F. Since the synthesis process itself can generate some or all of the input conditions, the task of creating specifications is made easier for the user. Also, the design strategies can be viewed as complex infer­ ence rules applied in a backwards-chaining manner result­ ing in the decomposition of complex problems into simpler subproblems. With this approach we hope to make the synthesis process more manageable, to cope with more complex problems, and to produce larger well-structured programs.

The formalization of top-down programming · has also been explored in (Dershowitz and Manna, 1975) where several strategies for designing program sequences, if­ then-else statements, and loops are presented.

In this paper we have introduced a problem reduction approach to program synthesis. If we hope to automate the synthesis of programs for solving complex problems then we must have formal methods for breaking problems into simpler subproblems. The problem reduction approach is based on decomposing problems with respect to the structure of program schemas representing various classes of algorithms. The schemas and their design stra­ tegies capture much of our .knowledge about program­ ming. In order to obtain powerful synthesis performance we need to discover those algorithm schernas which cover the important applications in some domain and devise design strategies for them. We have taken a first step in that direction with design methods for divide and conquer algorithms and a few others. A prototype system has been constructed which can perform the derivations in this and our earlier papers.

1. Bibel, W., "Syntax-directed, Semantics-Supported Pro­ gram Synthesis." ArtificiaL Intelligence 14:3 {1980) 243-262.
2. Bledsoe, W., "Nonresolution Theorem Proving ." ArtificiaL JnteUigence 9:1 (1977) 1-35.
3. Clark, K.L., and Darlington, J., "Algorithm Classification through Synthesis." The CaTnputer Jou:r­ nal23:1 (1980) 61-65.
4. [ 4] Dershowitz, N., and Manna, Z., "On Automating Struc­ tured Programming", in Proc. Collaques !RIA an Prov­ ing a.nd !TnprO'IJ'ing Pragra.TTLS, Arc-et-Senans, France, July 1975.
5. [5) Green, C. C., and Barstow, D.R., "On Program Synthesis Knowledge." ArtificiaL Intelligence 10:3 (1978) 241279.
6. Manna, Z., and Waldinger, R.J., "A Deductive Approach to Program Synthesis." ACM TOPLAS 2:1 (1980) 9D-121.
7. Smith, D.R., "Derived Preconditions and Their Use in Program Synthesis", in Si:zth Conference an Au.tama.tecl Deduction, Ed. D.W. Loveland, Lecture Notes in Computer Science 138, Springer-Verlag, New York, 1982, 172-193.
8. [8) Smith, D.R., Top-Down Synthesis of Simple Divide and Conquer Algorithms, Technical Report NPS 52-82-011, Naval Postgraduate School, Monterey, California, November 1982.