On Syntax-Directed, Semantics-Supported Program Synthesis

ON SYNTAX-DIRECTED, SEMANTICS-SUPPORTED PROGRAM SYNTHESIS

Wolfgang Bibel Institut fur Angewandte Informatik und Formale Beschreibungsverfahren Universitat Karlsruhe on leave from Institut fur Informatik Technische Universitat Munchen

A number of strategies for the synthesis of algorithms from a given input-output specification of a problem are presented which are centered around a few basic principles. It has been veri­ fied tor more than ten different algorithms that their uniform application in all cases results in a successful deductive synthesis. They include a spanning-tree algorithm, a graph-circuits algorithm., a finding-the-ith-smallest-element algorithm, and a linear (string) pattern-matching algorithm. Two of them are presented here.

INTRODUCTION

This paper is based on the view that (human or mechanical) programming is a deductive process which starts with a more or less detailed spe­ cification of the given problem in some repre­ sentati on language and after some search guided by several strategies eventually ends up with a deduction of the program which consists in the application of rules taken from logic, the un­ derlying theory and from a knowledge base for programming skill. It also adopts the view that predicate logic (in a wider sense) sofar still i s the most suitable r epresentation language for studying this process, because of its concise­ ness, naturalness, flexibility, extendibility - both descriptive probl em specification and ma­ chine programs can be r epresented in logic - and in particular because of the well-understood

deductive mechanisms for it.

Specifically, the topic of this paper is the search for such a deduction from a logical des­ cription of a problem t o some equivalent funational form (be it in logic or in an Algol­ like language). It is no secret that the search­ t r ee for such a deduction is tremendous even f or rather simple problems. Yet, it is a common observation that people a r e able t o move in a rather direct way towards a solution even for problems that require knowledge not experienced be f ore. There must be general guideline s or

str a tegies, then.

Unfortunately, . (no, fortunately!) our human thinking is not organized such that these stra­ tegi es could be easily bootstrapped from our behaviour. Therefore the only way to detect gene­ ral strategies seems to be by a detailed compa­ rative study of different deductions of diffe­ rent problems in order to detect common mecha­ nisms. This has been done by the author for the usual maximum problem and for Hoare's FIND prob­ lem resulting in a few principles in the form of strategies [6,9]. The surprising experience after this study was that these strategies proved successful for a number of different other problems. They include such interesting algorithms like a linear (string) pattern­ matching algorithm [16], a spanning tree algo­ rithm [1], and a graph-circuits algorithm [20].

The strategies center around f our basic ideas how to deal with a predicate logic formula des­ cribing a given problem: an 3-quantifier to­ gether with a non-functional specification re­ quires some kind of guessing (see GUESS); two (or more) consecutive 3-quantifiers require the evaluation of the dependency of the respective variables inherent in the specification (see GET-RNV,-SOC,DEPEND); for both requirements the cardinality of oertain problem inherent domains and other semantic knowledge provide helpful strategic informati on (see DOMAIN and CHVAR); the rewriting process can be strongly goal­ oriented with several intermediate goals (see GET-G) . This uniform and concentrated strategic concept seems to distinguish this approach from other work done in this field like [11-15,19, etc.]. Specifically, no other approach offers both, a uniform scheme based on a few basic principles, and a guidance of the synthesis to

such an extent that there is some reason for the claim that the automatic synthesis of programs like those in this paper seems to become fea~ sible. Of course, the second claim could only be fully verified by a running system (which at present does not exist) . But the text has been formulated with such a system in mind and se­ veral details have been included in order to support that claim.

In the following the basic strategies are in­ troduced and explained by application to the usual maximum problelli. Exactly the same sequen­ ce of strategies mechanically produces the de­ duction· of a linear pattern matching algorithm which for reasons of space is presented in a very packed form (see [7] for more details).

BASIC STRATEGIES

Logically, a programming problem has the form Vi :lo (IC (i) -+ OC (i ,o)), i, o, IC ,OC abbreviating in­ put, £Utput, input-£ondition, £Utput-£Ondition, resp. For example, the usual maximum problem in this format reads

1.1. IIS~m(5·�I·m€5A5~"'), shortly V53m MAX(5) ·m, where S~m: .. ··Vx(x£s~x~m).

Neither mE S nor S i m (nor both) provide a way how to determine m for given S, not even par­ tially. Therefore, in view of an algorithmic solution some trial-and-error method cannot be avoided. In this simple example we only can try for a hopefully correct m. Apparently it is wise to restrict such attempts somehow, specifically by requiring a subset of the conditions listed in the output-condition. The subset has to be proper since otherwise no reduction of the problem would be possible. Formally, this idea in the case of our example reads

1.2.v5vm'3m(m' €5 ·(5·+ ··m€5A5~m" (m' ·mvm' ·m))), or

1.3.v5vm'3m(5~m· + (5· ... m€ 5A5~m" (m' ·mvm' ·m)))

The underlying general strategy which is of a purely syntactic nature is the following (with v denoting exclusive disjunction) .

GUESS: Transform a problem of the form Vi3y(IC(i) -+OC(i,y)) to ViVy'3y(ds-+ (IC(i) -+OC(i,y) A (y*y'Vy=y'))) where domain-specification (ds) is a con­ junction of a proper subset of the con­ juncts in OC(i,y')

~li thout any additional support the synthesis would now have to consider in our example two (in general as many as there are proper subsets of clauses in OC(i,y')) different cases, (1.2) and (1.3) possibly leading to different algo­ rithms. In order to reduce the search space, a semantical argument in favour of one of those cases would be desirable. In our example such an argument can easily be seen, favouring (1.2)

rather than (1.3) for the case of usual assump­ tions on the domain of S and its representation. Namely, if we keep in mind that m' has to be chosen to satisfy the domain-specification then apparently this choice can be performed immedi­ ately for m' E S while it would require a number of steps for S i m' . Moreover, if S is finite then in the first case the guess also is more likely to be correct than in the second one since lsl<l{m'ls~m'}l= ~.These considerations can be generalized in the following strategy which requires semantic knowledge for its application.

For a problem as described in GUESS consider the set P of subsets of those conjuncts in OC(i,y) which specify y. By conjuncting the el=ments of each of these subsets P becomes a set P of for­ mulas . . For each cEP let q (i) :=I {ylc holds} I, and s (i) be the number or steps required to de­ termi~e an arbitrary y ' such that C holds. Then for a given weight-fa~tor k and for C, DE P let C< D iff q ·S <k·q ·S Aq ·S ~k·q ·S. With thfs priorify-Felatign BhicR c~pture~ t~e con­ siderations illustrated above in a general form, the strategy reads as follows.

DOMAIN: For domain-specification in GUESS choose a minimal C E P w. r. t. < k (which has not been considered sofar) .

Apparently, all the information necessary to apply DOMAIN has to be provided to the system from outside (interactively or via a knowledge base). Of course, application of DOMAIN to (1.1) yields m' E S as domain-specification, thus ex­ cluding (1.3) in a first attempt to synthesize MAX.

In the following we will see that (1.2) impli­ citly already contains an algorithmic solution for MAX which only has to be unfolded by re­ writing the formula in a rather constrained goal­ oriented way. The general strategic scheme and three of its instances are the following ones.

GET-G (.2_oal-oriented ~quivalence !_ransformation with goal G): Rewrite a given formula ac­ cording to domain and goal dependent equi­ valence transformation rules until goal G is achieved.

GET-DNF: the soal is that the resulting formula is in ~isjunctive normal form (alternative cases).

GET-REC: the goal is to find some kind of recur­ sion; if necessary, generalize the problem

GET-EP: the goal is that £redicates become evaluable, at least recursively.

In a program we need alternative cases. There­ fore GET-DNF will be applied to the conclusion in (1.2) which yields

(o :'t.en we drop the quantifiers and some paren­ theses if they are understood, where A binds more than~. both more than~, etc.)

Next we look for some kind of recursion for the first alternative (in the second one the result is already determined) . The formula talks on two objects m,m 1 and on a set S . . Imaqine a recursion generator which from a knowledge base produces the different possible recursive forms of prob­ lem reduction for these kinds of objects. It is just reduction of cardinality in the present case of a set (but even in general there are only a few known possibilities). A rule gene­ rator (knowledge base and/or theorem prover) tries to · merge the newly derived information (m * m 1 in 1.4) by rewriting the conjunction of these clau­ ses on the basis of the input-condition and the underlying theory (a search limited by a func­ tion in the number of given clauses even in the exhaustiVe mode). Here this might start with the application of the rule m 1 * S ~

(mESAm*m 1 -<-·mES-m 1 Am*m 1 ). Whenever in the result there is a match with one of the alter­ native recursive forms (mE s-m 1 in this case), this suggests a substitution possibly leading to a recursive problem reduction. It is explored for the whole problem under the guidance of a theorem pover. Because of

m' £ 5+ (S~mAm·m·-s ... m' ~mAm' ~mAm·m'++S .... m' ~mAm'<m), this process yields

1. 5. m' E s ... (S, m' · ' V s · { m' } -· m E S'm' "' s,m' ~ r.1 A m' < m) V MAX (S) =m' 1. 6. . , m' E S -+(S .... m' · ·-+ mE S""' AS,I'l' ~m Am'< m) A 5 · (m' )vHAX(S)·m' 1. 7. m' £ S + tll'.X(S,m') ·"' Am'~ mAS · (m')VMAX(S)sm'

completing the efforts of GET - REC in this case.

There is still the unpleasant clause m 1 < m which cannot be executed, not even recursively. This causes GET- EP to rewrite (1.7) which gives the equivalent formula

1 · 8 . m 1 £ S + MAX ( S, m' ) · m A m' < MAX ( S ,m' ) A S · ( m' ) v M"'X ( S) ·m'

All these 8 formulas are logically equivalent. The last one can easily (and automatically) be compiled into efficient algorithmic code (see [7] for some more details). Note that the de­ duction also serves as a correctness proof for the resulting algorithm.

A CHALLENGING PROBLEM

For the general case a few additional strategies are required. But even with these basi c ones quite a few non-trivial algorithms can be syn­ thesized by mechanical application of the basic and standard sequence GUESS, DOI~IN, GET-DNF,

-REC, -EP. Linear string-pattern-matching is among these algorithms, for the development of which several outstanding r esearchers in compu­ ter science have been a\o.·arded with honour.

We denote by lN n the natura.l numbers k with m ~ n. A string is a f:nction c :1Nisl~<characters>. Further assume fct as a 5uil~-in test for func­ tionality, dom as the function which denotes the domain of a function. Then the definition of the pattern-matching problem can be stated as:

shortly vc 5 vcp3k(PM(c 5 ,cp) · k) GUESS, DOMAIN, GET-DNF, -REC yield 2.2.

GET-EP recognizes a subproblem determined by 3j which has to be solved prior to the solution of the whole problem. This subproblem can betreatad in isolation since there is no clause containing both output-variables k and j; a solution - the well-known quadratic algorithm - is easily and mechanically obtained with the standard tech­ nique of this paper (see [8]).

The linear solution can be obtained only if this treatment in isolation is abandoned or, more precisely, if the range of the 3j-quantifier, which determines the subproblem, does include also the remaining clauses in the second alter­ native in (2.2) (causing a search in general which again is limited by a function in the num­ ber of clauses) . In this case our subproblem, denoted by DIFF, has the following output-condi­ tion (abbreviated by A(lN~))

GUESS adds a ( j * j 1 v j = j 1 ) -clause where DOMAIN ~ho~ses j 1 from lN 7. The only clauses with which j * j 1 in the first alternative can be mergP.d are those containing j with the following obvious result.

But this time the GET-REC can be moresuccessfull if it keeps merging the added conjunct with the clauses in the original part,specifically with c (j) = c (j+k); since in the first alternative

f~r C ( j r * C ( j I ) We haVe: c (j+k) =c (§') *c (j 1 ) =c (k 1 +j 1 ) =c (j+k 1 +j 1 -j), s p p s p i.e. k * k 1 +j 1 -j in this case for any appropriate k 1 ,j 1 ,j. Similarly,inthe second alternative for c (j) =c (j 1 ) and j*j 1 we have: cp(j 1 +k 1 J*c (j 1 ) =c (j) =c (k+j) =c (j 1 +k+j-j 1 ) s p p s s i.e. k * k 1 +3 1 -j also in this case for any appro­

priate k 1 , j 1 ,j. We obtain the following recursive solution for DIFF in which PK,PJ denote the sets of £OSsible k- and j-values.

2. 5. o 1 :·(k' +)' -jEPK I k 'EPKA)' (pjl\jElN ~"cp I j) ·cp (j') l" D 2 :·(k'+)'-jt?Kik'€PKA)'€Pjl\j(lN~ACp(j)·cp(j')Aj·J')A 3' (pj + ·DIFF (pj ,PK)·DIFF (Pj<l', PK,D 1 ) 1\Cp (j') ·cs (k' +3') v DIFF(Pj,PJ<)·PK,D 2

which has an obvious algorithmic interpretation.

With that solution (~.2) now reads 2. 6. k' EPK+ (IC+OCAk·k') v ( IC+OCAkEI;liFF ( lN ~, PKh k')

Comparison with (2.1) gives

1. 7. k' EPK + PM(c 5 ,cp, PK) · k' v PM(c 5 ,cp,PK) · PM(c 5 ,cp,DIFF(lN~,PK),k')

In algorithmic (loop) form this reads:

1. 8. proc pm (c 5 ,cp) ·kJn+ I dom c 5 I 1m+ I dom cp I :PK + lN g-m:
2. loop I PK l1 chooee k' !.!!.£!! that k'EPK:PK+diff (lN~ ,PI<): !! PK·falee then~ k';PK+PJ<,k': if PK·tll then return fahe1 end1

FURTHER STRATEGIES AND ALGORITHMS

For more general cases the following additional strategies are necessary: In order to structure complex problems output-conditions have to be separated into (partly) independent parts (GET-SOC); if possible, output-variables have to be expressed by others in the presence of more than one 3-quantifier (GET-RNV), otherwise, a hierarchical order between the different 3's has to be determined (CHVAR).

These and the basic strategies applied mechani­ cally (hand-simulation) in the standard sequence y~elded a detailed synthesis - as that for the maximum and the pattern-matching algorithm - of the following algorithms: maximum algorithms in different semantic context; binary search in lists; searching for duplicates in lists; testing equality of two lists; partitioning a set w.r.t. a given element; finding the i-th smallest ele­ ment in a set; determining circuits in a graph; determining a minimum-cost spanning tree in a graph. Othe~s have been synthesized in detail such as determining the moves of a roboter, etc. This remarkable list suggests that there is something fundamental in our strategies. For

further details and all references see

1. Bibel, w., Syntax-directed, Semantics-suppor­ ted Program Synthesis, Proceedings 4th Work­ shop on Automated Decution (W.H.Joyner,jr., ed.,IBM, Yorktown Heights, N.Y.), Austin, Tex., 140-147 (1979).

Improved version available as Report no. 78, University of Karlsruhe (submitted to Arti­

ficial Intelligence).

This work has been partially supported by the

Deutsche Forschungsgemeinschaft (DFG) . Typescript: G. Weiher