Automatic Program Synthesis in Second-Order Logic

Abstract

A resolution-based theorem prover, incorpo­ rating a restricted higher-order unification algo­ rithm, has been applied to the automatic synthesis of SNOBOL-4 programs. The set of premisses in­ cludes second-order assignment and iteration axi­ oms derived from those of Hoare. Two examples are given of the synthesis of programs that compute elementary functions.

Descriptive Terms

Higher-order logic Program generation Program synthesis Resolution Theorem proving Unification algorithms

The automatic synthesis of computer programs, like their automatic verification, requires a set of rules or axioms to account for such typical program features as assignment, iteration and branching, and a program capable of making-appro­ priate deductions on the basis of these rules or axioms. 1 Following current work o~ Luckham and Buchanan and Manna and Vuillemin we h~ve chosen a set of axioms based on those of Hoare , and we are employing a resolution-based theorem prover incorporating a restricted higher-order unifica­ tion algorithm to generate SNOBOL-4 programs from this set.

To aid the formulation of statements about programs, Hoare invented the notation

whose interpretation iea true before initiation of then the assertion R will tion"4. Thus, hie "axiom "If the assertion P is a {j>iece of] program Q, be true on its comple­ of assignment"

says that if P is true before f is assigned to x then P will be 0 true after this assignment, where "x is a variable identifier", "f is an expression" and "P is obtained from P by substituting f for all oc8urrences of x"; and his "rule of iteration"

says that if P is "an assertion which is always true on completion of s, provided that it is also true on initiation", then "P will still be true after any number of iterations of the statement S (even no iterations)". The controlling condition B of the "while loop" may be assumed to be true before execution of s, and will be false upon termination of the loop.

The above notation is, for all its elegance, not the most convenient for use by a predicate calculus theorem prover. Accordingly, we have

Jared L. Darlington

Geeellschaft ftir Mathematik und Datenverarbeitung

Bonn, Germany

written our axioms for assignment and iteration in terms of the variables x 1 , x 2 , etc. ranging over program variables and expressions; s 1 , s 2 , etc. ranging over states, and f 1 , f 2 , etc. ranging over predicates or functions of these objects, depen­ ding on context. Since the variables x and si are taken to be of type "individual", t!e use of the implicitly universally quantified variables f ranging over predicates or functions of these oijects means that our language is second-order. The notation

is used to indicate that the assertion f 1 (x 1 ) is true in the state s 1 , while

means of s usual that f 1 (x 1 ) is true in the state consisting followed oy s 2 (this is the reverse of the practice of reading the order of states from right to left, or "inside out"). In terms of this notation, our assignment axiom

says that if assertion f (x 1 ) is tru.e in state s 1 then assertion f 1 (x 2 ) will oe true in the state resulting from assigning the program variable or expression x 1 to the program variable x 2 , follow­ ing s 1 · DO' may be related to DO by noting that 1 f 1 (x )'corresponds to 'P '· 1 f 1 (x 2 )· to 'P', ·x 1 lo 'f' and ·x 2 · to 'x~. Its meaning may be illustrated by the instance

derived from DO' by instantiating ·x 1 · respectively, by the program variables 'K', and 1 f 1 1 by the lambda-function and 'x '· 'J' an&

where IDENT is a primitive SNOBOL function that tests whether two objects of any data type have the same value. The statement says that if IDENT(J,'STRING') is positive in s 1 then IDENT(K, 1 STRING') will be positive if J is as­ signed to K in the state following s 1 ·

In applying DO' to program synthesis, we have found it necessary to supplement it with axioms expressing properties of IDENT, namely

In practice it is simpler to use two corollaries of DO' , namely

derived by resolving

(obtained from DO' by change of variable) with ID1 to yield CL1, under the substitutions

and with ID2 to yield CL2, under the substitutions

followed by restandardising the variables of the resolvents.

The iteration axiom used by our program is related to Hoare's D3, but is based more directly on the inductive principle for natural numbers. We start with the formula

where 1 f 1 (x 1 )· corresvonde to 'P' in D3, 1 f 2 (x 2 )· to ,,B' and ·s 2 · to ·tsJ·. We then replace 'x ' in D3' by a program variable 'J', which in facl serves as a counter taking only integer values, replace 'x ' by a program variable 'N', and par­ tially Sko~emise the result, in the process re­ placing ·s 3 · by a constant 1 s 0 1 , thereby obtaining

Resolving on the underscored literal with the fol­ lowing instance of DO'

yields

thereby introducing the operation of incrementing J into the while loop. The iteration axiom used in our program,

is derived from D3''' by adding a subscript 'n' to 'J', adding the literal 'IN(IDENT{Jn,o), s 1 )· and then replacing 'J ' in the erstwhile firet literal by ·o·, there~y setting the counter Jn to 0 in the entering e.tate s 1 , and finally replacing the "while" notation by t:tie corresponding SNOBOL terminology of rule names and go-to's. The sub­ script 'n', in the contexts 'Jn'· 'RUL~n' and 'EXIT '· is instantiated by an integer, the serial numbs~ of the clause generated, whenever CL3 en­ ters into a resolution.

The use of axioms like Cl1 - Cl3 in a resolu­ tion-based theorem prover requires a unification procedure capable of handling functional varia­ bles. Pietrzykowski and Jensen5 have formulated an algorithm that generates all unifie~s for any two strings inw-order logic, and Huet has anal­ gorithm that generates all the unifiers required by hie deductively complete ~-order system of "constrained resolution", but since (as previously indicated) we are dealing with a second-order lan­ guage it is sufficient for our purposes to use an algorithm devised primarily for first- and second­ order logic. The unification algorithm that we employ is based on that for first-order logic7, but it introduces the higher-order operations of lambda-abstraction, in unifying for example P{a,b) and f (x 1 ) under the substitutions x 1 · a, f · Au 1 .P~u 1 ,b), and lambda-normalisation, in unffying for example Au 1 .P{u 1 ,b).a and P{x 1 ,x 2 ) under the substitutions x 1 · a, x 2 · b. In describing the algorithm, we borrow from Pietrzykowski and Jensen the notion of a "progress triple"

where A and B are two strings to be unified and where ~is the set of unifying substitutions, if any, so far generated. In our usage, A and B need not be single well-formed-formulae but may be strings of wffs, so any progress triple <A, B, cr-> may be written as

where a 1 and b 1 are respectively the leftmost wffs in A and B and where a 2 and b 2 are respectively the remaining strings of wffs in A and B. The par,~thesisation of A and B follows that of Robin­ son according to which, for example,

is written as

though, in contrast to the system described in his paper, we retain the lambda-notation. As a pro­ gramming convenience we may disregard any previ­ ously unified substrings of A and B, so that at any given stage in the unification A and B repre­ sent the not-yet-unified remainders of the origi­ nal A and B. The object of unification is to re­ duce A and B simultaneously to the null string,

)

(

under a set of unifying substitutions ~. In the first-order case there will be at most one way of doing this, represented by the terminal progress triple ( _, _,a), while in the higher-order case there will normally be several, and sometimes in­ finitely many (as in the case where A · f 1 (F(a)), B · F(f (a)), a is of type "individual" and f 1 and Fare ot type "individual-+ individual"), success­ ful unifications

The basic way of unifying two subobjeots a 1 and b 1 is to set b 1 equal to a 1 where al is a varlable {or vice versa if b 1 is a variab e), provided that aj and b 1 agree in type. In our system the vari­ aoles xi agree in type with other xi and with ex­ pressions denoting program variables or integers; the si agree with other si and with expressions denoting states, and the ri agree with other fi and with lambda-functions. The actual algoritnm is given below; it is the current version of what we haTe called "f-matohing" in earlier publica­ tions.

To unify two strings A and B, define S as the string of progress triples so far generated, and set

where c- is null. GOTO START.

• START: Read in a progress triple T -(·A, B, ct-) from S. SUCCEED: GOTO S1. FAIL: GOTO EXIT.
• 811 If A and B are null, T represents a suc­ cessful unification. SUCCEED: GOTO START. FAIL: GOTO S2.
• 821 If A and B are headed by opposing con­ stants, T represents an unsuccessful unification. SUCCEED: GOTO START. FAIL: GOTO S3.
• T ·(a a 2 , b b 2 ,cr)where a and b 1 are respeo~ively ~he leftmost wfts in A and B and a 2 and b 2 are _respeotively the (pos­ sibly null) remaining strings of wffs in A and B. If a 1 · b 1 , or if a 1 · x or b 1 · xu where xu is a dummy variab~e, set

SUCCEED: GOTO S1. FAIL: GOTO S4.

• If T ·(fi a 21 a 22 , itu:I.B b 2 , cr-) form the string or progress triples

where c 1 ··· c are the distinct occur­ rences of wffsn(other than variables bound byA) in Band where B(uj/ci) results from B by replacing oi by u~. A~d T' to S. Switch a 1 with b 1 and K 2 with b 2 and re­ exeoute S4. GOTO S5.

• If a 1 is a variable, if a 1 and b 1 agree in type, and if a 1 does not occur in b 1 , substitute b 1 for a 1 in a 2 and b 2 , using

lambda-normalisation where possible, and set

SUCCEED: GOTO S1. FAIL: GOTO S6.

• Switch a 1 with b 1 and a 2 with b 2 and re­ exeoute 85. SUCCEED: GOTO S1. FAIL: GOTO S7.
• If T · ((aj1 a12) a2, b1 b2' if) where the nead of a11 is fi, form the string of progress triples

where n is the largest subscript on a 'u' occurring in b 1 , o 1 ··· en are the dis­ tinct occurrences of wffs (other than var­ iables bound by~) in b 1 , and b 1 {un+/ci) results from b 1 by replacing c. by un 1 · Add T' to s. Switch a 1 lwith b 1 and a 2 with b 2 and re-execute S7. GOTO sa.

If not, T represents an unsuccessful unification. SUCCEED: GOTO S1. FAIL: GOTO START.

It may be noted that this algorithm is, except for S4 and S7, equivalent to the usual first-order unification algorithm.

To give an example, applying the algorithm to

yields the intermediate progress triples

and finally the unifiers

By way of comparison with Pietrzykowski and Jen­ sen, these are the same unifiers that are gener­ ated by their "imitation" and "projection" rules, which operate directly on the disagreeing objects to reduce the area of disagreement, but our algo­ rithm has no equivalent of their "elimination" and "iteration" rules, which operate on variables outside the area of disagreement. Thus, it will not handle the triple

since elimination is required to produce the unifier In the application of second-order logic to pro­ gram synthesis we have so far found no need for an equivalent of the elimination rule, nor do we need an iteration rule since by definition this applies only to languages of order higher than two (see Pietrzykowski and Jensen8 fot the formal defini­ tions of these rules). Huet~ also di~penses with these latter two rules, but in a way that pre­ serves deductive completeness. Our algorithm is actually an incomplete one for w -order, rather than just second-order, logic, the essential re­ striction being that, since the unification of f 1 (x 1 ,x 2 , ··· ,x ) and B proceeds by trying to match tne x. with we~l-formed pieces of B, B must ac­ tuall} contain well-formed pieces of the same type as the xi. Our program has in fact proved some theorems of order higher than two, such as the example in section 5 of Pietrzykowski's and Jen­ sen 1 s paper 1 ·

The generation of resolvents, like the uni­ fication algorithm, is based on the first-order procedure, in that the substitutions generated in the course of unifying two literals are applied to. the disjunctively connected "remainders" (that is, literals not being resolved on) of the two clauses being resolved, the one important difference being that lambda-normalisation is applied during the substitution process in order to eliminate lambda­ functions from the resolvent wherever possible. The order of generating resolvents is based on the "S-L resolution" method for first-order logic of Kowalski and Kuehner11, and is essentially a "depth-first" search strategy with resolution only on first literals of clauses, but with the aid of a set of reductive rules that perform algebraic simplifications or transformations on the clauses generated, Among the problems solved by our pro­ gram are the construction of SNOBOL programs for computing the factorial function and for iterative division; the computer printouts are given fol­ lowing the text. By way of explanation, axioms CL1 - CL3 are equivalent to those given in the text, but with the order of literals changed and with some implications expressed in terms of con­ junction and negation, for more effective appli­ cation of "first-literal resolution" and for en­ suring that the resulting proofs will be linear. CL4 in each of the examples formulates the prob­ lem; M and N are input variables, and Jn and K are output variables. In example 1, CL4 says that if there is a state s 1 in which K has the same value as J ! where J has the same value as N (in other wordi, if K hai the same value as N!), then s 1 is an answer. In example 2, CL4 says that if K has the same value as M - (Jn.N) where the value of K is less than that of N (in order words, if M · Jn.N + K, K<N) in s 1 , then s 1 is an answer. Both of t~~se examples were taken from Manna and Waldinger Of the reductive rules exhibited by the examples, Rule 2 transforms (x+1)! into (x!).(x+1); Rule 3 transforms x- ((y+1).z) into (x - y.z) - z; Rule 0 4 reduces O.x, x.O or Ox to 0; Rule 5 reduces x or 0! to 1; Rule 6 reduces O+x, x+O or x-0 to x, and Rule 8 is a "frame" rule that reduces IN(IDENT(x 1 ,x 2 ), s (s 2 )) to IN(IDENT(x 1 ,x 2 ), s 1 ), provided lhat s 2 "does not affect" x 1 or x 2 · Most of these rules are purely ad hoc and are chosen with the particular examples rn-view; for serious program synthesis one would need a more systematically organised algebraic simplifier. Finally, there is a routine· called "ANSPRINT" that polishes up the answer and prints it out in the correct SNOBOL line-by-line format, though it may be noted that the sample programs are not as "simple" as they could be. Running times for examples of this general type are three to five minutes on the IBM 360/50 at the GMD in Bonn. The theorem-proving program, like the pro­ grams generated, is coded in SNOBOL-4. Apart from line divisions, the output is an exact transcrip­ tion of the computer printouts.