Characterization of a Class of Functions Synthesized from Examples by a SUMMERS Like Method Using a "B.M.W." Matching Technique

CHARACTERIZATION OF A CLASS OF FUNCTIONS SYNTHESIZED FROM EXAMPLES BY A SUMMERS LIKE * METHOD USING A "B.M.W." MATCHING TECHNIQUE .

J.P. JOUANNAUD

Centre de Recherche en Informatique de Nancy UER de Mathematiques Universite de NANCY I 54037 NANCY CEDEX

Summary :

This paper describes first a program synthesis from examples method using a SUMMERS like metho­ dology together with a sophisticated pattern matching technique, the BOYER-IIOORE-I.JEGBREIT algo­ rithm. We then characterize the class of functions synthesized from a restricted BMW algorithm. Our methodology is founded on three grounds.The first one is a precise characterization of the list dom3ins fitting the synthesis from examples problem. The second one is. SUMMERS' technique of input-output examples transformation into computational traces. The third one is the descri­ ption by a restricted program scheme of the functions in the cl nss. It seems to us that the proofs methods easily extend to the generalcl ass.

I. INTRODUCTION

The synthesis of functions from a set {x. ~ F(x.)} of input-output examples has been 1 1

extensively studied [ I ,2,4 ,5, 6, 7,8, 9 ,10, 14, 15, 16] our purpose here is to study a powerful! exten­ sion of SUMMER's method [ 161 using a pattern matching technique we shall call the BOYER­ MOORE-1.JEG'BREIT algorithm.

The principles of this technique are discussed in 13,8,9,10,17].

We recall briefly this method which is detailed in I 8, 9, 10] · However we think that it is not enough to describe an algorithm, especially in our field : we must aim at the characterization of the class of functions which can be synthe­ sized. A recent work of SMITH I 15] describes such an investigation for a restricted SUMMER's method. The goal of this paper is to design more adapted tools which allow simpler proofs of our theorems. We are able to characterize the functions synthesized by a restricted BMW algorithm and prove a linear growth property of the functions in this class. We mean that our results shall extend to the general case.

* Partly supported by IRIA-SESORI.

2. _S)'NTHESIS METHODOLOGY

We recall briefly, in an intuitive way, the methodology relative to one variable functions [8,9,10,16]. We are concerned with LISP unary functions defined on lists. Before the synthe­ sis process itself takes place, two transfor­ mations of the input-output values are neces-

sary. The first one transforms .these values in­ to a set of computational traces exprHssed with the set {cons, car, cdr, atom} of primitive functions. The second one transforms the compu­ tational traces into a p~rtial function, defi­ ned on subdomains of F.

In order to make our notations and results clea­ rer, we shall describe the synthesis of an ad'hoc function F described by the following set of examples :

x · (A(B)C) F(x ) · (B) 0 0

x 1 · (A(B(C(D)E))) F(x 1 ) z (C C B) ;

x 2 · (A(B(C(D(E(F)G))))) F(x 2 ) · (C C D C B)

x 3 · (A(B(C(D(E(F(G(H)l))))))) F(x 3 )= (CCCEDCB)

2.1. Notations and definitions

Let L bet the set of LISP lists. A list x of L may be viewed as a cons-tree, each leaf of which is an atom. ~

For instance, X - (A(B)C) or X m ~~il ~nil

o

o

Y. KODRATOFF GR 22 du CNRS Institut de Programmation, T 55-65 Universite Pierre et Marie Curie (Paris VI) 4, place Jussieu 75230 PARIS CEDEX OS

Let I~ be the complexity of the list x, i.e. the number of leafs in the associated cons-tree.

Following KNUTH [II], we shall denute by S(x, y, *) the list obtained by substitution of y to all the *-labelled atoms of x For instance

It is well known that the order associated to the substitution relation is a partial ordering of L.

Definition : A reduction function is a finite composition of car and cdr. Let R be the set of reduction functions. The length lfl of fER is the number of car and cdr in f.

Notice that the triplet < R, composition rule, I >, where I denotes the identity function; is isomorphic to the free monoid constructed on the alphabet {car, cdr}.

Definition : Let A. be the ith occurrence of 1 the atom A in the list x and u the unique reduc­ tion function which verifies u(x) = A .. Then u 1 is said to be the functional name of A. in x. 1 For instance, the name ofF* in a is cadadr.

Definition : lf v E R is a right factor of u E R, then u v-1 denotes the function of R such that u = (u v-l)v. Let u modulo v be the func­ tion u v-k provided vk' is a right factor of u iff Q .;;;; k I .;;;; k,

-I Example : u = caadadr, v ·= cadr, u v = caadr, u modulo v car.

Definition Given a set of terminal functions (Generally R U {nil}) a cons-expression is a cons-tree, each leaf of which is a terminal function or nil. //---.

Example : f = car I~ cddr

Notice that nil may be viewed either as an atom or as a function.

Let 1u be the undefined atom, D(f) the domain of the function f, i.e . the set {xlx E L, f(x)~w

Definition : The adapted structure [ 15] ad(f) of a function fER is the smallest x E D(f).

For example, ad(caddar)= A~nil Notice that the atoms of ad(f) do not have any importance at all, i.e. ad(f) is in fact a list structure.

Definition : The adapted set F · {f.}, f. E R Vi, x E D(F) · 1 0 D(!.). 1 1 For example, ad {caddar, structure ad(F) of a is the smallest cddr} = ~il

In the following, we shall suppose that no atoms of ad(F) bear the same name.

2.2. Computational traces

A main step in SUMMER's method is to transform the sequence {x. ~ F(x.)} of input-output exam1 1 ples in a sequence {p.(x) ~ f.(x)} of computational traces. 1 1

2.2.1. Ascending linear domains.

The further step of synthesis requires the existence of recurrence relations between the predicates p .. It is thus natural to study the input domain~ that possess this property.

Definition : Given x E L, a E L, a owning a 0 single *-labelled atom, the set {x , x. 1 = 0 1+ S(a, x., *)}is called ascending linear domain Jt (x 0 , 1 a).

In fact, we change the names of the atoms in order to avoid several occurrences of the same atom in x .· 1

~(x ,a) is the set 0

{(A(B)C),(A(B(C(D)E))),(A(B(C(D(E(F)G))))), ... } Notice that the partial ordering on L is total on h(x , a). 0

We now have to exhibit a sequence pi of predi­ cates which verify

p.(x.) = T, p.(x.) 1 1 - 1 J j < i, 1~here T and true and false. = F iff j > i,p.(x.) · W iff - 1 J F denote the logical values

Let us call b the function name of the *-label­ led atom in a and suppose that we know a reduc­ tion TI such that atom. TI(x ) = T. 0 - It is obvious that b(x. 1 ) · x. and it follows 1+ 1 that the sequence pi · atom.n.bi verifies pi(xi) · T. We still need to find the "good" function n, i.e. the function such that p. veri­ fies the two remaining conditions p.(x.) ~ F 1 J iff j > i and p.(x.) = w iff j < i.

Definition : An atom in a list x is said to be 1n the d1rection of f E R P {I} iff its functio­ nal name has the form f' . f \vhere f' is a pro­ per right factor of f, i.e : f. f".f'. f" r I.

For instance, nil* in x · ~

the direction of cadr cdadr · cdr.cadr.. i ts functional name is

The intuitive meaning of this concept is the following : if we compute cadr(x ) we obtain /"-...... 0 B ni4which is not yet an atom. We cannot com­ pute cadr.cadr(x ) which is not defined, but we

0

start the computation and keep computing as long as we do not reach an atom : cdr.cadr(x ) · nil is an atom ; we therefore stop the cog-* h' . putat1on at t 1s po1nt.

Property of the ascending linear domains gi­ ven an ascending linear domain 1t (x , a) and the name b of the ·-labelled atom 8f a, let n be the functional name of the atom of x which is in the direction of b. Then {p. = at8m.n.b 1 } 1

is a sequence of predicates for the domain.

Notice that the sequence of predicates verify­ ing these previous conditions is not unique in the sense that n is not unique in some particu­ lar cases.

Example : Let us consider the previous set ilit(x , a). \~e obtain b · cadadr and n = cdadr.

0 Thus p 0 = atom.cdadr, p 1 = atom.cdadadadr, p 2 = atom.cdadadadadadr. The match of pi aod pi+! succeeds and we obtain :

i More generally, pi = atom.n.h and pi+! p .. b 1

2.2.2. Fragments

The output F(x.) is taken in its cons-tree form. Each atom, exc~pt nil, of this cons-tree is re­ placed by its functional name in x .. The pro­ cess is unambiguous iff there are fiot several atoms (except nil) bearing the same name in any xi. Each obtained cons-expression f(xi) is then turned into a partial function f . (x) by the su­ bstitution of x to each x. of f(~.) . The func­ tion f. is called the ith 1 fragmen! of F. Notice 1 that f . is defined for any x ~ x. and equal to f (x.) Qhen x = x. . 1 l l

i.2.3. Approximations

The input-output sequence {x. ~ f(x.)} has been changed into a sequence of ptedicat~s and frag­ ments {p.(x) ~ f.(x)} which is embedded into an if ··. th~n .·. el~e .·. function in order to ob­ tain the following n-approximation of F :

Notice that the names of the atoms are now lost we therefore cannot synthesize functions depen­ ding on these names, like the function which is true iff all the names of the atoms are diffe­ rent.

Our problem now is to get a finite expression of the oo-approximation.

2.3. The synthesis technique

The principle of the method consists in detec­ ting a repetitive computation on the successive traces.

Fragments :We attempt to match f.(x) and f. 1 (x) using the BMW algorithm. When 1 it succee~;, we use its substitutions to write recurrence relations proved to be equivalent to programs by SUMMER's main synthesis theorem [ 16] or its ex tens ions [ 9] ·

The classical pattern matching techniques [ 13] do not succed to match the preceeding sequence of fragments. In this case, a first order pat­ tern matching attemps to use generalization te­ chniques together with matches between subtrees, i.e. the BMW algorithm. ·rt works as follows A first generalization leads to replace the nil atom by a variable z in each fragment :

titutions

Since the variable x receives two different substitutions, a new generalization is necessa­ ry : the variable x becomes x' if it undergoes the first substitution and x" if it undergoes the second substitution, and the fragment f.(x) 1. becomes f ~ (x' , x", z) : 1.

The matching between two consecutive fragments now succeeds and we find the following recurren­ ce relations

Notice that {h.} and {g.} are two sequences of 1. 1. fragments associated to the sequence of predica­ tes pi+ I. In the present case, hi and gi are

The matching is now possible Each fragment is matchea with the first subtree of the successi­ ve fragment, provided the following set of subs-

~------------------------------------------------- constant cons-expressions.sometimes h. and g. are not constant. I.Jhen it is the case! we usi repetitively the same algorithm until we get

constant h and g.

In the following, we shall restrict ourself to a one step BMW algorithm (the above example be­ haves in this way).

Since we use matches between subtrees, the suc­ ceeding match is generally not unique. One should not worry about this : we shall prove that all the matches lead to equivalent programs.

From the relations {I) and (2) a program is de­ rived using the following extension [9) of SUMMER's Synthesis Theorem (MST) :

Theorem : If the infinite sequences {p.} and l {f.} verify the recurrence relations : l

h and g are constant cons-expressions then the ~approximation associated to the computational traces sequence {p.(x)..,. f.(x)} is equivalent to the program : 1 1

The xx variable, defined as the domain variable, iS introduced to take into account the recur­ sion on p.(x). One realizes its importance when l

we look back to the previous example : neither x' nor x" have the same relation as xx :

F(x) +- F' (x,4,x,nil) F' (x' , x", xx, z) +- If a tom(cdadr xx) then (cons(caadr x")z)- h(x' ,x" ,xx,F' (x', (cadr x"), (cadadr xx),g(x',x",xx,z))). h(x' ,x",y) +- (cons(caadadr x')y) g(x' ,x",z) +- (cons(caadr x")z)

In the following, the symbol F used as an example will always denote the above function.

Remark : Given a function, the recurrence rela­ ~are supposed to begin with the first exam­ ple of the function. For the sake of readabili­ ty, we shall rule out the trivial cases where the first examples of the function's behaviour (i.e. a finite number of them) have particular properties.

3. THE SYNTHESIS ALGORITHM AND THE RESTRICTED PROGRAM SCHIDffi ·

Let us recall that we are only concerned with unary LISP functions given by a sequence {x . ..,. F(x.)} of examples, the set {x.} of inputs l l l belonging to an ascending linear domain i?f'(x 0 ,a).

Synthesis algorithm

1. Compute the functional name b of the uni­
2. que * - labelled atom of a.
3. Compute the functional name rr of the unique atom in x which is in the direction of b. 0
4. Compute the fragments fi.
5. Look for recurrence relations between conse­ cutive fragments using the BMW algorithm restricted to one step.
6. If recurrence relations are found then use the MST. Our present aim is to precise which functions can be synthesized and how many examples are needed.

Let us call ~~ the set of functions which can be synthesized. If F E'S;k, obviously F veri­ fies the program scheme used in the MST . Our purpose is to prove the reciprocal. Following SMITH [IS), we shall first introduce some very natural restrictions on the program scheme which come from the fragment computation techni­ que.

Program scheme 0 :

F is a cons-tree whose terminal functions g . belong to R U {nil} 1

Restriction: Y g 1 ,g 2 ,g 1 · v.g 2 ~ v · I.

Notice that this restriction comes very natural­ ly : It means that g 1 and g 2 are terminal func­ tions of fragments (Since F is constant, f . · F, Y.) and thus g 1 (x.) and g 2 (x . ) are both atAms. l 1 l

It follows that v.g 2 (xi) is defined iff v · I.

Program scheme I : F(x) +-F'(x,x,nil) F'(x,xx,z) +-If p (xx) then f'(x,z) - 0 -- 0 else h[x,F'(c(X),h(xx},g(x,z)))

In fact x,c and z in the F' definition should be vectors as shown by the example. l~e do not use vectors in order to lighten the notations but this simplification implies no loss of gene­ rality.

We shall call~ j the set of functions which can be computed b~ an instance of this restric­ ted schema.

Restrictions :

• 3/ f' is a cons-tree whose terminal functions 0 f' . belong to R-{I} U {nil} when applied to 0,1 x and equal I when applied to z.
• 4/ h is a cons-tree whose terminal functions h. belong to R-{I} U {nil} when applied to 1 x and equal I when applied to F'.
• 5/ g is a cons-tree whose terminal functions g. belong to {R} - {I} U {nil} when ap1 plied to x and equal I when applied to z.
• 6/ Let X be the set of functions defined below which 0 lead to a computation on x starting from a computation F(xk).: 0

• 7/ Letc{ be the set of functions defined below which lead to a computation on a starting from a computation F(xk)

'If E c{ · f 1 I and Yf, g€ c1 , f ~ v. g =* v · I.

These two last restrictions mean that functions of X and cl come from fragments. It follows that 0 if g belongs to X , then g(x ) is an atom. Thus v.g(x ) is define8 iff v ~ I~

. -k k uy {gi.cJ.b lo <j <k,b is a right 1 · factor of g .. cJ}

l

U U {h .. c .b lo < j < k,b is a right

i . 1 factor of h .· cJ} 1

c{ a {b} U U {f' .. cj modulo blo j, r 1 q}, i o, l

where r and q are defined in restriction

Example : In the above example (section 2) c was a two-dimensional vector (c 1 ,c 2 ). Its first component, c 1 , is associated with the terminal functions which compute on x 1 and c 2 is associa­ ted with the terminal functions which computP.

j -k

k

• b = cadadr ; U{f' .. cj modulo b)={caadr,cad; . i o, l · U {g .· cJ modulo b} = {caadr,car} ; ~h .· cJ i 1 l 1 modulo b} · {car} ;.

Thus~ .. {car,caadr,cadadrL

Let us call T~ the set of functions be computed by a program whictLis an ~f th~f.estricted scheme and~J the J'jo UJ" I' which can instance set

Theorem : 'Jjt= 'r!.

Before proving this theorem, ·.·e shall first ex­ press the fragment fk in terms of the functions f 1 h and g which appear in the program schema I.

This lemma is easy to prove by induction on k. As a consequenoe, the set of t~rminal functions of fk is {h .. cJ, f 1 .. ck,g .. cJ jj < k}. 1 0,1 1

First part of the proof : j:Jt <;;; 1' $

Two cases may occur : the computed fragments are constant or not. If they are constant, the program scheme o is used and the restriction holds, else scheme I is used and we have to prove the restrictions I to 7.

Lemma 2 : Restriction I holds.

Proof : The matching of the fragments provides a function c E R such that Vi> o,j < i, cJ(x.) 1 u.> This implies that either c · I and lemma 1 2 is proved with e = b, q = I and r · o, or c;r and c and b "compute in the same direction".

It follows that blcl= clbl. As b and c belong to the free monoid construc­ ted on the alphabet {car,cdr} they are powers of the same e E R. Thus b = eq and c = er. Moreover if q < r, then for k large enough

Restriction 2 holds becauseJt(x ,a) is an ascending linear domain. 0

Restriction 3,4,5 come from the working techni­ que of the BMW algorithm.

Restriction 6 follows easily.

Restriction 7 follows then easily and the first part of the theorem is proved.

Seaond part of the proof :'1'1c'S*. Three steps are needed.

Firat step.

We have to exhibit an ascending linear domain tx ,a). This domain should ve the "smallest" doo

main on which the synthesis of the known func­ tion F is possible. Given F E3':f, we naturally take as x 0 and a

This has a meaning, because

Lemma 5 : X and o[ are finite sets. 0

The proof is simple.

Example : for the example F we have X 0

It follows that : x 0 = A~nil

{car ,caadr, cdadr}, <i = {car ,caadr ,cadadr},

rr---- B nil

Notice that the new x is simpler than the preo vious one which contained useless information. To define ~(x ,a), we need a *-labelled atom in a, the func~ional name of which is b : it is thus the atom C.

Seaond step.

Given the set {x.} ble to compute tHe of inputs, it is now possi­ set {x. ~ F(x.)} of examples 1. 1. and the set {p'.' 4 f'.'} of computational traces. 1. l We shall now prove that the sets {p. ~f.} and l l · {p'.' ~ f'.'} l l are identical, where p. · atom.n. b 1 l and f. is defined in lemma I. l

Lemma 6 : Given a set G of reduction functions and x · ad(G), if atom.f(x) .. F then there exists g E G such that g .. v.f~ v E R-{I}.

Third step.

We now may match the consecutive fragments. We know recurrence relations between these frag­ ments : they derive from the given program F. Nevertheless, several matches may succeed and lead to different programs with program scheme o or I . \~e thus have to prove that all these different matches lead to equivalent programs, although a finite number of examples are used to compute the fragments and the recurrence rela­ tions.

Notice that there is no problem if F is given by a program which is an instance of the program scheme o. In this case, F will be synthesized with the same program. Difficulties appear when F is given by a program which is an instance of the program scheme I .

Before solving this problem, we shall prove a property of the class~!.

Lemma 10 : If F is an instance of the program scheme I and F" an instance of the program sche­ me o which take the same values in x 0 and x 1 ,

then F and F" are equivalent . The synthesis pro­ cess of F needs two examples : x 0 ~ F(x 0 ) and x 1 ~F(x 1 ).

Lemma II : If F and F" are two instances of the program scheme I, which take the same values in x , x 1 and x 2 , then F and F" are equivalent. TRe synthesis process of F needs three examples x 0 ~ F(x 0 ), x 1 ~ F(x 1 ) and x 2 ~ F(x 2 ) .

Proof : A detailed proof is rather techni cal and can be found in [ 7 bis] . Its principle is characterize the links between the two sets { n,b,c,f' ,h,g} and { n, b , c",f",h,g}(whi ch defi - o 0

ne F and F") when F and F" have the same values on x 0 ,x 1 and x 2 . These links enable us to prove

easily that the sequences of fragments {f~ } and {fk} are identical.

\~e have thus proved that any function in~~ i s synthesized from 2 examples and in~·~'ffrom 0 3 e-x mples. '1>

4 . CONCLUSION

We have obtained a characterization of the class of functions synthesized from examples, when a restricted BMW algorithm is used. More­ over, we have proved an important property of the functions in this class : the existence of a deep relation between the number of exampl es needed for their synthesis and their growth speed. These above results, obtained for the classes tJ'j and 3' ~I may be extended to the class~~ d~fined by the use of an n-step BMW n algorithm. A key step for this proof is the obtention of an equivalence result between an instance of the program scheme n and an instan­ ce of the program scheme m ~ n wich take the sa­ me values for the inputs x 0 ,x 1 , ··. ,xn+l ·

A further interesting problem should be to ob­ ~1r an intuitive characterization of the class 'J'.J · U ~S. We mean that there is a strong anan n logy between the properties of the polynomials and those of 'J' J.

The BMW algorithm has been implemented in LISP by E. PAPON (unpublished "stage de D.E.A." Univ. Paris-Sud).