Algebraic Manipulations as a Unification and Matching Strategy for Linear Equations in Signed Binary Trees

ALGEBRAIC MANIPULATIONS AS A UNIFICATION AND MATCHING STRATEGY FOR LINEAR EQUATIONS IN SIGNED BINARY TREES. APPLICATION TO LISP PROGRAM SYNTHESIS AND DERECURSIVATION

C. KIRCHNER, H. KIRCHNER, J.P. JOUANNAUD

CRIN-UNIVERSITE of NANCY I UER de Sciences Mathematiques

Case Off. 140- 54037 NANCY Cedex, FRANCE

An example of application to program derecur­ sivation is shown in section VII.

II ALGEBRAIC FRAME

We recall here some basic notions and results discussed in [13].

A. Signed binary trees

As we are dealing with terms (or trees), we first give some general definitions :

DEFINITION I : given a denumerable set X of variables symbols, a denumerable set A of atoms (or constants symbols i.e. functions with arity 0) and a finite set F of functions symbols (with non-zero arity), the algebra it(X, AUF) is the inductively

defined set :

• ** X ~ Jt(X, AUF)
• ** A ~ .ft(X, AUF)

** ~f€ F, ._t,f:.f.(X,AUF),ISiSarity(f) -i> f( ··· t._ ··· )E. ~(X, AUF).

Elements of Jl: (X,AUF) are called terms. The set of variables of a term tis denoted by V(t), its size by I tl

It is often convenient to consider terms as labelled trees in the following way [4].

DEFINITION 2 : *a term t is a mapping from a set of occurrences denoted D(t) which is a subset of N*, into the set XUAUF such that :

** m € D( t) => any prefix of m belongs to D( t).

• ** mED(t) => m.iED(t) iff ISi~arity (t(m)).

* The number of occurrenc· of x in t is the cardinal of the set {u£D(t) s.t. t(u)·x}.

It is easy to see that these definitions are equivalent. Notice that the empty word £ belongs to D(t) for any t and that t(£) is the top symbol of t. In the following, we generally use the tree-notation f instead off( ·· , t ··· )

t

ABSTRACT

We study the unification and matching problems in the signed binary trees theory. We show that any equation tl·t2 can be transformed into an equivalent one x=t. If x does not occur in t then (x ---> t) is the unique most general unifier in the theory (up to an isomorphism). We apply this technique to find recurrence relations between sets of terms. These relations are used to synthesize LISP pro­ grams from a set of input traces.

KEYWORDS : unification, matching, equation, unifier, substitution, rewrite rule, term, tree, program synthesis.

I INTRODUCTION

Signed binary trees have been introduced in [14] in order to solve equations which have no solu­ tion in binary trees. Such equations appear in program synthesis or transformation processes. This technique enables us to perform such synthesis or transformation processes in various situations. Our goal here is to study how equations may be solved in this theory.

Section II recalls both usual concepts of u­ nification in an equational theory and definitions of signed binary trees considered as terms of an e­ quational theory or as a term rewriting system.

Section III introduces the concept of equiva­ lent equations and sets some basic tools used in the following sections.

Section IV describes and proves an algorithm which transforms an equation into an equivalent one (with less function symbols). Some properties of reduced equations are studied.

Section V is concerned with the resolution of linear equation (an equation is linear if there exists a variable x which has a unique occurrence in the terms of the equivalent reduced equation). We give a constructive caracterisation of the most general solution (up to an isomorphism) of such a linear equation.

The matching problem is then studied in sec­ tion VI.

DEFINITION 3: the set~ =Jt(X,AU{cons}) where cons is a binary function symbol, is called set of binary trees.

It is clear that we have in mind some kind of LISP interpretation of terms in ~ and we thus use capital letters for atoms and small letters for va­ riables.

DEFINITION 4 : the set of signed binary trees on A is the algebra A =jlAX,A U {-,cons}) with the set of axioms

Notice that these axioms look like the axioms of groups theory, In earlier versions [14], the set of axioms was a little more complicated,

It is proved in [13] that this set of axioms is in fact a consequence of the two last axioms A3, A4,

In the following, 1 is sometimes abbreviated X

in -x and signed binary trees are denoted by letters t,u,v,w.

B. -+ The term rewriting system A

Applying the KNUTH-BENDIX completion algorithm [IS], [9] , axioms are used from left to right only and an infinite set of rules is generated which di­ vides into two parts :

·· rules I and 2 obtained from the two first axioms :

·· 2 meta-rules obtained from the two remai­ ning axioms :

where s denotes a structure and m(s) its opposite mirror,defined as follows :

DEFINITION 5 : the set S of structures and the opposite mirror m(s) of a structure S are inductively defined by

We call type III (respectively type IV) rules the rules obtained from the meta-rule III (respec­ tively IV) by substituting a structure ~o the va­ riable structure s and its opposite mirror to m(s).

PROPOSITION I [ 14] : A is finitely terminating and confluent. The normal form of any term t is compu­ ted in 0(\t\Log\t\) time in the worst case.

C. Unification in A

We first recall some classical definitions and results related to unification in equational theories.

DEFIN!TION 6 : a substitution ~is a mapping from X to A equal to identity except on a finite subset of X called its domain and denoted by D(~). The restriction ~v of ~ to a subset V of X is equal to~ on V and equal to identity on X\V, ThusD(~, )= D(<r) n V. Substitutions are extended to terms by morphism,

In the following, letters cr, e and/"' denote substitutions and r the set of substitutions.

DEFINITION 7 : the equality = - . . 1 A congruence over A conta1n1ng al ~ (d,)) for each axiom g,: · d._ · As t I = t 2 => "icr, crt I = C1 t 2. is the finest pairs (.,.(g;.), a consequence,

A

PROPOSITION 2 [8] : tl ~ t2 iff tl and t2 have the A

same normal form.

We define now a quasi-ordering on terms and extend it to substitutions

DEFINITION 9 : let V be any finite subset of X. cr..,~~ (orG' ~"<t') ifi3f'rs.t, Vx~V,cr'x~\(crx).

<r.., ~ <f~ (or cr,e~f') iff ct~()'' and cr '.Sv cr The classical following proposition, easy to prove, tells us that .$ works well on classes of terms for · congruence

A

DEFINITION 10 : we call unifier of two terms t and t', any substitution 0" such that crt ·4't', Let A U(t,t') be the set of all unifiers. We call equation in A any pair of terms (t,t'). A solution of the equation (t,t') is a unifier oft and t', The equation (t,t') is also denoted t = t'.

A unifier~ of two terms t and t' (a solution of the equation t · t') is said to be minimal iff 't~' such that cr'~O'with V·V(t)UV(t') ·><r'tu(t,t').

We are in fact interested in a basis of the set of solutions of the equation t · t', Such a ba­ sis is called minimal complete set of unifiers and has been defined by HUET [7].

DEFINITION II : a minimal complete set of uni­ fiers of two terms t and t' (a basis of the set of solutions of the equation t · t') denoted UP(t,t') satisfies the three following properties : (I) UP(t,t') E U(t,t')

(2)'t<r~U(t,t') ,3t£UP(t,t') s.t. ~' ~<f,with V· V(t)UV(t') (completenes).

(3)¥<r,tr' E: UP(t,t'), cr;.r· ~~'4 f.(T; (minimality).

REMARK : we do not use the technical condition which appears in [10] , [7], [6]. It is well known that many theories have infinite (sometimes undeci­ dable) minimal complete sets of unifiers. We shall see that it is not the case in A · This problem is solved in the next section by the way of algebraic manipulations allowed by the axioms.

III EQUIVALENT EQUATIONS

In this section, we show how an equation t·t' can be transformed into an equivalent one, in prac­ tice a simpler one. The following results can be proved w~thout difficulty.

DEFINITION 12 : two equations t·t' and u·u' are equivalent iff U(t,t')·U(u,u'), i.e. they have the same set of solutions.

PROPOSITION 4 : if t·u and t'au' then the ttvo equa­ tions t·t' and u=u' ~re equiv~lent.

COROLLARY : let t and t' be two terms of A with t ', t as normal forms, then_t~e equation t·t' is equiva­ lent to the equation t·t'.

Using these general results, we shall now stu­ dy the equations between signed binary trees.

PROPOSITION 5 : '{ t E. A, '# t' ~A, the equations tzt' and -t·-t' are equivalent.

PROPOSITION 6 : V t, t', t"EA, the equations t' at", cons · cons , cons = cons are equivalent. /\I\ 1\1\

PROPOSITION 7: 'tt',t"EA,'#x(V(t')UV(t"),3tEA such that the equation t'·t" is equivalent to the equa­ tion x·t.

The proof is constructive and uses a structu­ ral induction on t'.See [17].

EXAMPLE : Using the proposition 7, the equation cons cons is equivalent to the equations

IV SIMPLIFICATION OF EQUATIONS

A. Reduced equations

Some equations with a great number of nodes labell t·d with cons symbols are equivalent to equations with less cons symbols. For example :

Notice that the simplified form of an equa­ tion is not unique. For example

DEFINITION 13 : considering equations as terms of an algebra, let us define the relation -~ by the three rewrite rules

(0) is the empty equation).

We say that e' immediately simplifies e iff e --> e'.

The last example shows that irreducible equa­ tions (for -->) are equivalent to reducible ones. We shall first design an algorithm able to compute the reducible equation e' equivalent to the equa­ tion e, when it exists.In our example, let d deno­ te the duplicated term cons

z A

We see that d belongs to the left side of the first equation, while the second occurrence of d is split into 3 parts, -z and -A in the left-hand side and x in the right one. We thus can use the proposition 6 and 4 to build the second occurrence of d in the right side and then delete it. At each step, the part of d which goes from left to right across the · symbol is smaller than d. If such a full d exists at the beginning on the left-hand side of the equation, it remains at its place un­ til the second d appears in the right-hand side.

DEFINITION 14 : we define now the relation I··> by the rewrite rules : cons · cons l·a> vi =

Let us denote by I·~ the symetric closure of 1=·> and by <·=I the inverse of I·=>. Notice that we use the term cons which is in normal form if wt;w2, instead of the term cons

, which is

not in normal form, according to the lemma proved in [13] : -t- m(t). A

DEFINITION 15 : let E be the set of equations tl · t2 where tl and t2 are terms of A. Terms of E are called equational terms. We define the opposite mirror m(tl·t2) of the equational term tl = t2 as the equational term m(t2)·m(tl).

LEMMA 2: tl·t2 I·=> tl'=t2'<=-t tl"=t2" =s> ( t I "·t2") = ( t I =t2) or ( t I "=t2") 1==1 m( t I ·t2) ·

LEMMA 3: tl=t2 1-'21 tl'=t2' ·> m(tl·t2) 1-!!1 m(tl'·t2')

Proof : by induction on n. See [17] for details. From now up, we consider the only equational term.!!. t l·t2 such that t I and t2 are in nor~al form for A. Let us denote by R the set of equat1onal terms tl·t2 reducible for --> (and such that tl and t2 are normal forms of 't) .

Terms of R are thus instances of the two follo­ wing terms :

where x,u and v are variables which can be instan­ ciated by irreducible terms of A.

Notice that m(e) t R iff e ( R.

We are now able to prove the following impor­ tant result.

PROPOSITION 8 : if tl=t2 1="=1 e E.R, where tl and t2 are irreducible t erms of Awith Itt! > lt2l , then there exists a sequence of equational terms : (tt=t2)=(t~=t2 > I==> t1=t~ 1==> ··· I==> t'i'=tr' 1-z> tf=t~ with tr·t~f.R andVO~ i!: p-t,jtttl> ltil and (trmtf)=e or m(e) in normal form. Proof : the proof is long, technical, and not easy. It uses an induction on the length n of ~ · See [17]. 0

We are now ready to design and prove the sim­ plification algorithm.

B. Simplification algorithm

DEFINITION 16 : given e·(tl=t2) € E, with tl and t2 in normal form for ~ let C(e) denote the set of equations equivalent to e modulo the equiva­ lence generated

LEMMA 4: if tl·tl' A and t2=t2' then C(tl=t2) · A

C(tl'=t2'). * * * * * Proof : we prove that (tl·t2) (--> .<--. !-·>,<·~ ) (tJ 1 zt2 1 ), 0

PROPOSITION 9 : given any equation e=(tl=t2) with [ttl ~ Jt2J , tl and t2 in normal form for?\, the following algorithm REDUIRE computes a minimal ele­ ment of C(e), i.e. which is not equivalent (for~) to a reducible one (for _. ) REDUIRE (tl=t2)

• CASE (0) tl is an atom (a variable or a constant) AND tl·t2 THEN 0.
• (I) e=(cons · cons) OR (cons · cons) I\/\ /\1\ X U I X u2 U I X u2 X

THEN REDUIRE (ul·u2).

1. e·(cons = x) OR (cons = x)

\

I

\

cons u2

u2 cons

I

\

x ul ul x THEN IF ul > u2 THEN REDUIRE (ul-m(u2)) ELSE REDUIRE (m(u2)·ul).

1. lttl S Jt21 THEN (tl=t2) is the result.
2. tl· cons AND (vi >Jwl THEN REDUillli(v,cons) I \ ' I \ v w t2 m(w)
3. ELSE REDUIRE (w= cons) I \ m(v) t2

ENDCASE END REDUIRE.

REMARK : the aim of case (2) is to express the fact that in proposition 8, the equational term

tlr=t2r may verify Jttrl<lt2rJ .It is possible to avoid this case (2) but cases (I) and (4) become much more complicated,

Proof : REDUIRE terminates obviously, because the size of the left term of the equation argument of REDUIRE is strictly decreasing at each recursive

call.

The proof of correctness uses proposition 8, see [I 7].

This algorithm is very performant : it is easy to convince oneself that it stops after a few calls when the equation e is not reducible and we have proved that its complexity is linear in the worst case [ 17].

C. Properties of reduced equations

Before studying how equivalent reduced equa­ tions are related, we first prove :

PROPOSITION 9 : -->/ 1!-1 is confluent, Proof : -->/ 1-~ is locally confluent and finitely terminating. 0

COROLLARY 2 : if e1and e2 are irreducible elements of C(e), then V(e I) ·V(e2) and\' x, O(x,e I )·O(x,e2), where O(x,e) denotes the number of occurrences of x in e.

Proof : it follows from proposition 9 that el =· e2.

V LINEAR EQUATIONS

In this section, we show that for linear equa­ tions, the minimal complete set of unifiers has on­ ly one element, which is easy to compute.

A. Definitions

DEFINITION 17 : we say that a term t in normal form is linear in a variable x iff O(x,t)·l,

We say that an equation e is linear in x iff O(x,e)=t.

We can remark first that a non-linear equation can be equivalent to a reduced linear one, as in the example of section IV.

Secondly, for two equations e and e' deduced one from the other by some manipulations of section III, their reduced equivalent e~uations e and e' ar e linear or non-linear at the same time : it is an obvious consequence of the corollary 2,

So the property of linearity can be extended to the whole set C(e).

We shall say that C(e) is linear in x iff e is linear in x. So we suppose from now on that we are dealing with reduced equations.

We use in what follows the classical notion of linear contexts.

DEFINITION 18 : let t a term in A, oc an ele­ ment of D(t) and s the subterm of t at the occuren­ ce oc ; then Ct oc[ ! denotes the context such that c4: « [s1=t, that is the term obtained by substitu­ ti~g [ 1 to s at occurrence oc in t and c~ 1 [ 1 the context such that c-1 [t1 = s. ,oc t,oc A

With this notation, proposition if x is a variable at the occurrence if tl=t2 is an equation linear in x, equivalent to the equation x=c-tll ' oc 7 becomes : oc in tl and then tl·t2 is [ t21.

B. Minimal complete set of unifiers for a linear equation

PROPOSITION II : let tl·t2 be an equation li­ near in x and x=c- 1 1 [t21 the equivalent equation. t ,oc -1 . . . Then {cr }, where <r·(x-t=C 1 [t21), lS a m1mmal . . t oc complete set of un1f1ers of t! and t2.

Proof : · IS' is clearly an unifier of x and t since x does not belong to V(t),

· if<Tbelongs to U(x,t), thena'crxcr'because <r'cr (x)A cr'(t)A <f(x) and for y</<x, cr'cr(y)A cr'(y).

· The third condition of definition II is clearly true. 0

REMARK!: when tl·t2 is also linear in y#x, yEV(tl) for example, let oc,.. and oc') the respective occurrence of x and y in_ t I · -I

Then CJI=(x-c 1 [t21) and 2=(y-ctl t ,oc,. ,oc')o [t2]) verify <rl:;vef2(V·V(ti)O V(t2)).

{~I} and{~2} are two distinct minimal complete sets of unifiers of tl and t2.

REMARK2: the most general unifier in A is not neces­ sarily a minimal unifier in A : for example the equation cons

has <r =f(y -B) (z -cons >) as I \ X A most general unifier

in A, and 0:= {(y -cons

cons cons

I

J \

\

I \

as minimal unifier in 11:. & <T · ~, but there is no~ such that ~o · ~ , because ~~(y) · ~(B)·B and i(y)</<B.

B z -A -x

>)

A. Definition and examples

DEFINITION 19 : in A, matching a term tl to a term t2 is defined as looking for a substitutioncr such that~t1At2. When such a substitution exists, let us call match from tl to t2 the substitution <Tv where V·V( t I). .

Contrary to the first order theory without axioms, the following example shows that when a match exists, it is generally not unique, For t I = cons and t2 · cpns ·

are two solutions to the matching problem, REMARK : a strategy to find a match from t 1 to t 2 when t 1 is linear (for example in x) consists in using the results about unification :

a) renaming all the variables of t 2 with a one to one mapping ~such that V(tl)n 'f (V(t2)) · 0, is always possible.

b) Since t 1 is linear in x, t 1 and f ( t2) have a minimal unifier<f'·(x ~t) such that lft(A <T( :J (t2)· t<t2) because D(O')O '/ (! (t2)) · 0.

Thus, r-lcrt 1;;;t 2 and t- 1 ~r is a match from t 1 to t2. But it is in general not minimal : for example, let t 1 = cons and P ·(x- c,ons )

is the match found with the above method and it is easy to verify that \ is not smaller than

II" · (x -7> cons ) (y- cons ) which cannot be obI

tained by the same technique, This remark justifies the following results.

From now on, F(tl, t2) denotes the set of all matches from tl to t2, and we define a minimal com­ plete set of matches.

DEFINITION 20 : a set of substitutions FP(tl, t2) is a minimal complete set of matches from tl to t2 iff :

I) FP(tl ,t2) «;; F(tl ,t2),

2) oli<T£F(tl,t2), 3rHP(tl,t2) such that~"< <rvwith V=V(tl). ,

3) .Vcr,II''E.FP(tl,t2) tr#tr' => t:., J,crv.

B. Manipulations on equations and matching

We should like to know what happens to the matchings when the former manipulations are applied to the terms, The following lemmas attempt to ans­ wer this question.

LEMMA 5 : let <r be a substitution and t any term verifying <rt=t ,<Tis a match from tl to t2 if and only if cr is a match from cons / ~I to cons I ~2 Proof : <$' t I At2 <-> rn' A ;on\ A r\ G" t .rt 1 crt t2 t t2 Obviously we get the same result with cons and cons I \ I \ t I t t2 t LEMMA 6 : <ris a match from tl to t2 if and only if cr is a match from -tl to -t2. Proof c:rt1At2 <-> - IJ' tiA-t2<-> c:r(-ti)A-t2 . C

LEMMA 7: let tl,t2,tl ',t2' be terms such that tl=t2 ~tl'·t2 1 and cr a substitution such that D(cr)C\V(t2) · D(<I")OV(t2') · 0; then <I" is a match from t I to t2 if and only if cr is a match from t I' to t2'.

Proof : obvious, since ~is a unifier of both tl, t 2 and t I ' , t 2'

REMARK : it follows that some matches are lost du­ ring the manipulations, precisely these which con­ tradict the hypothesis of lemma 7.

In the particular case of a term tl linear in x, x do not occur in a subterm u of tl removed from the left during the sequence of manipulations of propo­ sition 7, Thus lenuna 6 applies and <T= (x-+c-1 tl ,ocx

[t2]) is a match from tl to t2. But some matches can exist from tl to t2 which do not verify for any sub term u of t I , <T u A u ·

When t J is linear in x and x tV( t2) we are in the case of lemma 7 with tl'·x and t2'=c-tl [t2] I 1,ocx and so cr-(x ->c[ t2]) is the only match from tl to t2. Here a~!igcx linearity hypothesis leads to stronger results, and we are going to study these cases.

C. Linear terms

Under some restrictive conditions, we can pro­ ve the existence of a minimal complete set of mat­ ches reduced to only one element.

PROPOSITION 12 : if tl is linear in x and V(tl)l\ V(t2) ~ {x} then {<S} where G"=(x -t=C1 [t2]is a minimal complete set of matches fromt1,ocx tl to t2.

Proof : I) erE. F ( t I , t2) see lemma 5 and the remark above.

C ftl·ocx~xlAt2 then~x·Cf~l,ocx [t2l. Let V·V(tl) andf"=~V\~ 1 )' When y(Vdx} :ry=ry ·>

c,t 1 ocx [ ): c.,.~, oc 1 [) · A~ (~\{xl) 0 Vtt2~-~ by hypothesis, ~(t2)=t2 and on the other hand ( ( t) E r ( t). So let us show that 't z E. v. r.- .. ZA('Z.

*When zi'Jc, f"'II'Z ·rz= fZ

-1

· When z·x, ru = rt and ~xAC tl

[fH2J= r{Ctl,ocx[t 2)]A rt·

-I

\

,ocx

-1

[t2]=C

f'tl,ocx

Thus ~. ~ ~., 2) The condition 3 of definition 22 is obvious .O

PROPOS!TION 13 : if tl and t2 are li~ear if t·C 1 [t2], then {cr ·(x-»t)} 1s a t ,ocx complete set of matches from tl to t2. in x and minimal Proof : similar to propos1t1on 12 except for 2) : ~eE.F(tl,t2), let us find a substitutionrverifying '41~V(ti)=V :~crz~p i.e.

· When zfx : t' zA t z

· When z·x : \" tA (X

Since tl and t2 are linear in x, ~x occurs only one time in t~t. Let x'·~x. The equation t'!j ex is li:- near in x' and has a solution (x'-->C t [px]) t' · ocx \

VII APPLICATION TO PROGRAM SYNTHESIS AND PROGRAM DERECURSIVATION

We use a derecursivation technique which is detailed in [16] : from a given recursive defini­ tion, a set of "computational traces" is computed first, Then recurrence relations are found by mat­ ching together the successive terms of the set of computational traces. Finally, the recurrence rela­ tions are transformed into tail-recursive programs using a synthesis theorem [16]. The derecursivation process is thus based on a synthesis technique.

In what follows, we detail an example where the generalized matching techniques used in [16], [2ol do not work : the use of signed binary trees will erase this difficulty.

Let us consider the following LISP program where F' has a recursive definition.

H' [xx,x ,z ]-g atom (cddr(xx)) then cdr( cdr(z))

else H[ cdr(xx) ,x, cons ]

/'\

car z

!

Let tp· be .the functional which defines F'

and ~H the functional which defines H. We are in­ terested in the chain of approximations of F (also called computational traces of F), i.e. in the chain t}. [n.] (x, x, nil), where .n. is the function undefined everywhere.

For instance Let us now call predicates the terms occurring before the then keyword and fragments the terms oc­ curring after-the then keyword.

Predicates and fragments are terms of an abstract data type, the so called set of"S-expres­ sion", considered here as a term rewriting system by using the axioms from left to right only : car (cons(x,y)) ->x cdr(cons(x,y)) ~y

We now use the term rewriting system to com­ pute the normal forms of the predicates and the fragments :

We now use our classical technique [II), [12) to infer a program from a sequence of traces, by matching the terms of the sequence. If we take the usual way to match terms, it is clearly impossible to get z starting from cons(car{x),z). But it is possible if we use the frame of the signed trees :

The substitution is now constant. We thus use the theorem 2 of [ 1 t,J , and get the following tail recursive program :

FF'(xx,x,z)~If atom (cdr(xx)) then cons(car(x),z) else FF'(cdr(xx),x,GG(xx,x,z)

GG(xx,x,z) ~ If atom (cddr(xx)) then cons(-car(x),z) else GG(cdr(xx) ,x,cons(ca.r(x) ,z)).

Notice that the theorem used says that the function FF' is the least upper bound of the chain of functions obtained by replacing inti [nJ (xx, x,z) the predicates and the fragments Fby their normal forms, provided that the recurrence rela­ tions found by matching the first five fragments are valid for all fragments. So, to prove that F' and FF' are equivalent programs, i.e. compute the same function, one only has to prove that the frag­ ments of F' and those of FF' are equivalent, We know that it is true for the first five ones, but we have to prove that it is always true. It is clear that such a proof is not so hard and could be done by an automatic system.

Moreover the proof of equivalence of F' and FF' could be perfnrmed by an automatic system such as [1), [2) and [5). There is in fact a stron­ ger argument for the equivalence of F' and FF' : F' has a kind of polynomial behaviour and we belie­ ve in a not yet proved conjecture that polynomial functions on trees are characterized by a finite number of examples (or computational traces) and that they may be obtained from these computational traces by using a "differentiation" algorithm such as ours.

We thus have synthesized a non monotonic func­ tion (in the sense that the size of the fragments is a non monotonic function) using an auxiliary function : the - function. A good way to deal with this extra function would be to build the term re­ writing system described in section III.2 in the LISP interpreter itself in order to compute in a systematic way the normal forms of signed S-expres­ sions. We use in fact a classical LISP and we thus have to process the outputs of functions using the - function.

VIII CONCLUSION

Our goal was both the description of a synthe­ sis system and the design of a mathematical theory which allows us to extend the concept of unifica­ tion. Our first motivation was synthesis and dere­ cursivation, and we are now still working to find a general algorithm to synthesize non monotonic "tree-polynomial";but we also think that our theory could have other applications and perhaps allow to design new unification algorithms. To reach such a goal, we first have to generalize signed binary trees, which is rather easy :

• For any ternary symbol f, we generalise axioms 3 and 4 :

A axiom 2- like is introduced for any function symbol.

These axioms and the deduced rewriting rules system enable us to solve other interesting exam­ ples, as the following one.

As in [16], in order to synthesize the LISP program, defined on lists, which maps (A) to (A), (A(B)) to ((A),B), (A(B(C))) to (((A)B)C) and so on we first build the sequence of fragments :

To make the matching successful!, we have to generalize the constant nil in a variable z. Moreo­ ver, we have to distinguish occurrences of x which are substitued with different values. We thus obtain the following new set of fragments :

We get now the following tail recursive pro­ gram :

F(x)4'-o G(x,x,nil)

�(xl,x 2 ,z)~lf atom (cdr xz) ~ cons(car(xJ),z) else G( car (cons (car (x 1 ). , z)) , cadr (xz) , cons ( caadr (xz, -- nil)).

where car is some inverse function of car. It is easy to verify that this function F leads·to correct computations, provided we have a LISP interpretor which performs th~ reductions defined by the term rewriting system~.

• A second point is the problem of non linear equations. Solutions of non linear equations on si­ gned binary trees are infinite signed binary trees. But it is not easy to deal with both infinite trees and equations. Moreover results of (3] do not apply easily and must be adapted to our problems.

We finally want to outline the idea of using meta-rules in order to avoid loopings in the KNUTH­ BENDIX algo·rithm : it seems to be a rather general feature which applies successfully in many cases, for instance in group theory, with the rule

• It would thus be interesting to study the looping cases and the corresponding meta-rules.

ACKNOWLEDGEMENTS

We thank the CNRS for financial support.