Inducing Function Properties from Computation Traces

1. INTRODUCTION

Inductive reasoning has been a popular task in Artificial Intelligence since the very early beginning. It has been attempted in such doma­ ins as (just to mention a few) series com­ pletion, grammar inference, automatic programm­ ing, and theory formation [5,6,9,10,14,17,19, 20,22].

In deductive sciences, s a peculiar role in development. In fact, inductive reasoning play­ the process of knowledge the correctness of an induction can be confirmed by a rigorous proof, even though only a semi-decision procedure mi­ ght be available, depending on the formal sys­ tem complexity. Moreover, the rejection of an inductive hypothesis may bring forth explan­ ations about the failure which help in refining the hypothesis.

It goes far beyond the scope of this paper to give a complete account of all the work on inductive reasoning in formal systems. We might mention just a few references. Meltzer [1Ql, Michalski [16] , Plotkin [18] and Vere [;n] have tackled various forms of inductive reasoning tasks in the predicate calculus. Brown and Tarn­ lund (4] were concerned with finding a close

form solution to difference equations. In the context of program verification, Boyer and Mo­ ore (2] , Brotz (3], and Aubin (1] generalize theorems which are then proven by a sui table induction principle. The problem domain we have chosen is akin to the latter.

The system we present induces properties of re­ cursive functions. The properties are defined to the system as (boolean valued) recursive functions. The system can observe that a given property holds for given elements of the doma­ ins of the involved functions (called ground property), and examine the corresponding ground property computation. Since the computation is indeed a proof, the evidence the system starts from is that a very trivial theorem holds. The definitions of properties and functions are ava­ ilable and must be taken into account, because no relevant inductive reasoning can be made irrespectively of their nature. Secondly, induc­ tion can depend on the details about the flow of computation. We simply provide the system with the kind of information one might get from any tracing facility, i.e. which function, when and where, was applied during the computation.

Thus, inductive reasoning requires the system to grasp a notion of function definition and computation up to be able to formulate a theo­ rem about functions at an expertise level. We do not claim that a competent system which induces function properties does understand fu­ nctions and computability. The system we prese­ nt here is not at all able to develop a theory of computation, hence it does not compare with systems for scientific discovery, such as Len­ at's AM [12] . Nonetheless, it exhibits some competence in function property induction.

Again, let us stress the advantage we gain from addressing an inductive reasoning task in the framework of a formal system. The aptness of the inductive system can be precisely stated, confirmed by a formal proof, and anyway appreci­ ated on firm grounds (as far as the observer understands the formal function and property definitions). In this prospect, we cared for providing a precise evaluation of our inductive method effectiveness, and we proved that the method is strong enough to induce formulae whi­ ch are actually theorems if the involved functi­ ons and properties belong to a constructively defined class.

2. A FORMAL CALCULUS ENVIRONMENT

We use a simple recursive function formalism, TEL (Term Equation Language) which was introdu­ ced [13] for proving program properties by symbolic computation (e.g. [2] ) and is similar to other independently developed formalisms ~, 7) . For the present application we add types to TEL so that the resulting language is so similar to Aubin's that the formal treatment and all results of his · carry over Typed TEL (later referred to as TTEL). We now briefly overview TTEL, borrowing some nomenclature from

Aubin's.

Every term, application, i.e. every variable and function has a type. Each type is defined by a set of type equations which also define the type constructors. All the types and cons­ tructors occurring in the equation (apart from the type and constructor being defined) must be defined at a lower level. The language is quan­ tifier free, because any variable occurring in an equation is implicitly universally quantifi­ ed over its type. Examples are

(TYPE(TT())=B; TYPE(FF())=B) (TYPE(O())=N; TYPE(S(N))=N) (TYPE(NIL())=L; TYPE(C(N,L))=L) (TYPE(LNIL()·)=LL; TYPE(LC(L,LL))=LL)

The constructor TYPE is used only to denote type equations. In the following we will omit the argument list of 0-adic constructors. A type is called reflexive if it is defined in terms of itself (e.g. N,L and LL). Analogously, constructors like S and C are reflexive and the argument position where the type they construct occurs is called the reflection argument positi­ on. Non-reflexive constructors will also be cal­ led terminators of the type. Given a term c(tl, ... ,tn) where c is a constructor, tl, .·. ,tn are terms, then ti (lSi~n) is an immediate predecessor of c(tl, .... ,tn) if ti occurs in a reflexion argument position.

Defined functions are introduced by stages. A

function definition is a pair, whose first com­ ponent is a type equation which defines the types of the arguments and the type of the result. For example TYPE(EQN(N,N))=B. The seco­ nd component consists in a set of equations (rewrite equations) , which allows a definition by cases [ 7, 11) . Rewrite equations obey the schema f(al, ... ,an)=(rewriting term) where f is the function being defined, and al, ... , an are terms (formal arguments) which may consist eith­ er in a variable, or in a constructor applied to variables only (recursion arguments). The only variables which may occur in the(rewriting term) are the formal argument variables. If f occurs in the <rewriting term)(recursive equati­ on), its recursion arguments must be immediate predecessors of the formal recursion arguments.

The definition by cases is restricted as fol­ lows. If an argument position is recursive il'l. one equation, then it must be a recursive argum­ ent position for all the equations, and for each constructor of the required type there must be exactly one rewrite equation. If the function simultaneously recurs on two or more argument positions, then exactly one rewrite equation must be given for each tuple of cons­ tructors of the required types (see the example below).

The metalinguistic constraints allow the defi­ nition of total functions only. Nevertheless, all primitive recursive functions over the type of natural numbers N can be defined. This is concrete example.

{EQN(O,O)=TT;

EQN(O,S(y) )=FF;

(ENbl)

(ENb2)

EQN(S(x),O)=FF;

EQN(S(x) ,S(y) )=EQN(x,y)}

(ENb3)

(ENr)

The definition of computation of a TTEL term

follows.

1. Specialize a rewrite equation so that its left-hand side becomes identical to a (sub)term of the evaluating term;
2. ii) Substitute in the evaluating term the specialized equation right-hand side for the (sub)term;
3. iii) Repeat from Step ( i) until no equation left-hand side can be made identical to a (sub)term of the evaluating term.

The interpreter adopts the call-by-need compu­

tation rule.

Let us now extend the TTEL term definition by introducing free typed variables. A free var­ iable can be instantiated to any term of its type, possibly introducing new free variables. A symbolic term is a term in which free variab­ les occur, otherwise the term is ground. We can extend the definition of computation to handle symbolic evaluating terms. Step ( i) only needs to be extended so that the involved test for identity can cause evaluating term free variab­ les to be instantiated. The computation of a symbolic term may be non-deterministic, due to the inherent non-determinism of free variable instantiation. Thus, symbolic computations are (possibly infinite) trees. A concrete example is the following. The term EQN(S(~) ,S(S(l,)) (free variables will be underlined) is reduced to EQN (~,S(l,)) by (ENr) and then either to FF if~ is instantiated to 0 by (ENb2), or to EQN (~.l,) if ~ is instantiated to S(~) by (ENr). From this point on, all EQN equations can be applied.

We might provide the same inference rules avail­ able in Aubin's system. We omit them here since we are not interested in the deductive aspects of the formalism. It is only important. to noti­ ce that ground property computations ~lding TT can be seen as proofs of the property because the interpreter itself implements the tactics Aubin calls simplification.A theorem with unive­ rsally quantified variables is proven by straig­ ht computation if wheryfree variables are substi­ tuted for quantified variables, the obtained symbolic term computation yields TT without in­ stantiating the introduced free variables.

3. ~ INDUCTIVE REASONING TASK IN TTEL

The system accepts TTEL type and function defi n­ itions, and can ask the TTEL interpreter to compute a ground proper ty. The interpreter prov­ ides the system with the resulting value and with a computation trace consisting of a sequen­ ce of pairs (rewritten sub term, applied rewrite equation) . The goal is to induce from this evidence a formula which subsumes the ground property, and hopefully is a theorem itself.

First, the system finds the most general theo­ rem whose proof consists in the given computa­ tion trace. This is a proper generalization and the system is able to check it. Secondly, the system exploits properties of predicates such as equality to further generalize the theorem . The system does not give a proof of the new theorem, but a proof could easily be obtained by simplification and induction.A final general­ ization is obtained on the grounds of few rules which might instead yield non valid results.

4. GENERALIZATION BASED ON PROOF

-------

The first clue the system starts from i s the given computation trace. In fact, the very same computation trace may prove a theorem stronger than the given one. In the first place, if a function application term is never evaluated during the computation, the term can safely be substituted by a universally quantified var i ab­ le and the given computation will still be a proof of the obtained theorem . A typical examp­ le is provided by the following ground property (function definitions are given in Appendi x I )

C(S(O) ,C(O,NIL))), A(C(S(O) ,C(O,NIL)), C(PLUS(S(O),O),NIL))).

Since the terms PLUS(S(O),O) are never evaluat­ ed, they can be sustitut.ed by a universally quantified variable, yielding the theorem EQLN(A(C(x,NIL),C(S(O),C(O,NIL)),

A(C(S(O),C(O,NIL)),C(x,NIL))).

The same generalization can be done on those data terms (i.e. terms built on constructors only) whose structure is irrelevant to the com­ putation. The system can distinguish the relev­ ant part of the occuring data terms by resort­ ing to the function rewrite equations, whose formal argument terms describe exac tly the most general data term the rewrite equation can be applied to. The required generalization is ob­ tained by firstly substituting free variables for the maximal data terms in the theorem. Then the resulting symbolic term is evaluated by forcing the computation to exactly follow the given computation trace. The original free vari­ ables will turn out to be instantiated only as far as needed to obtain the given computation. Let us work out the above example to clarify the matter.

Suppose the maximal data terms are replaced as EQLN(A(vl,v2) ,A(v2,vl)). (2)

Since the computation trace reports that the recursive A equation was applied to the A terms, the variables ~ and v2 need to be instantiated to C(~,vl2) and C(v21,v22) re­ spec tively. Analogously, vl2 is subsequently in­ stantiated to NIL and v22 to C(v23,NIL). Colle­ cting all instantiations, and substituting the still remaining free variables by universally quantified variables, we obtain the theorem EQLN(A(C(vll,NIL),C(v21,C(v23,NIL))),

A(C(v21,C(v23,NIL)),C(vll,NIL))). However, if the starting term isEQL(A(vl,~), A(~.~)) the forced computation is not able to reconstruct the identities of vl to v4, and of v2 to v3. Consequently, the substitution of free variables for input data terms must be done carefully.

The heuristic rule for free variable introduc­ tion adopted by the system is based on the following observation. In order to have inter­ esting theorems, the variables occurring in one actual argument term of functions such as EQLN (called balanced functions) should occur in the other argument term as well. The system is able to recognize balanced functions from their defi­ nitions (basically because they recur simultane­ ously on both argument positions). Moreover, the user is allowed to tag functions as being balanced (e.g. the boolean functions AND and IMPLIES may conveniently be handled as balanced functions). Thus, the system substitutes identi~ cal data terms with different free variables in one argument term, and if the involved function is balanced, carries the introduced variables over the other argument term. For example, if the ground property is

EQLN(A(C(O,NIL),C(O,NIL)),A(C(O,NIL),C(O,NIL))) then free variables are introduced as follows EQLN(A(~,v2),A(v2,~))

and forced computation yields the theorem EQLN(A(C(vll,NIL),C(v21,NIL)),

A(C(v21,NIL),C(vll,NIL))).

Actually, ~ and ~ in the second A term could also be introduced the other way around, thus yielding a trivial theorem. The system produces all possible free variables introductions. Some of them are proven by a triviality checker, others are discarded by subsumption.

The limitation of the proof based generaliza­ tion method stems from its strong dependence on the involved functions. For example, consider the following ground property.

EQL(A(C(O,NIL),A(C(O,NIL),R(NIL))), (3) A(A(C(O,NIL),C(O,NIL)),R(NIL))).

No free variable introduction helps, because the forced computation will anyway yield back the ground property. In fact, EQL is a much more demanding equivalence relation than EQLN, because EQL accurately checks the list elements by means of EQN.

The generalization method presented in the next Section exploits the presence of equivalence predicates in the theorem, and it is a first start on generalizing the proof.

5. GENERALIZATION ~ ON EQUIVALENCE

Let us describe the role of equivalence by means of example ( 3). The forced computation starts with the following term (called symbolic input term).

EQL(A(~,A(~,R(v3))),A(A(vl,~),R(v3))).

The computation trace forces the instantiation of vl to let the outermost A terms produce (through the recursive A equation) two C terms. Thus the symbolic term is rewritten as follows EQL(C(vll,A(~,A(~,R(~)))

C(~,A(A(~,~),R(v3)))).

The EQL recursive equation is applied yielding AND(EQN(~.~),EQL(A(~,A(v2,R(~))), A(A(vl2,v2),R(v3)))).

This is the first place where the notion of equivalence can help generalizing. The system notices the occurrence of the term EQN(~.~) whose corresponding evaluation in the computa­ tion trace yields TT. Since EQN is an equivalen­ ce relation, the reflexivity lemma EQN(x,x) can easily be proven, and used to rewrite EQN(~.~) to TT.The part of the computation trace describing the evaluation of EQN can be by-passed thus leaving the variable ~ free.

More precisely, whenever an equivalence predi­ cate application e(tl,t2) is found during the forced computation, the system attempts to use the reflexivity lemma e(x,x). If tl and t2 are identical, and are sub-terms of the symbolic input term, a new free variable is introduced for both tl and t2.

In the given example, the computation proceeds with the evaluation of the EQL term, and by

instantiation of ~ to NIL yields EQL(A(v2,R(~)),A(v2,R(~})).

The reflexivity lemma is not applied because the second A term is not part of the symbolic input term but it comes from the computation of the term A(vl,~). On the contrary, after a few steps the variable ~ ripples out and the evalu­ ating term becomes EQL(R(~),R(v3)).

Both R(v3) terms satisfy the conditions above, and the system generalize them. Finally, colle­ cting all instantiations, the induced theorem is the following

EQL(A(C(vll,NIL),A(C(v21,NIL),v4)), (4)

A(A(C(vll,NIL),C(v2l,NIL)),v4)).

The given computation trace is no more a proof of the induced theorem. Yet, a proof could easi­ ly be obtained by a simplification inference rule, and by use of reflexivity lemmas. Hence,

the induced formula is actually a theorem.

Since the system exploits only the reflexivity property of the equivalence relations, any re­ flexive predicate can be handled this way. We did not attempt to let the system discover reflexivity by itself from the predicate defini­ tions. However, the system is able to induce such a property.

Although the formula induced at this point is valid, it is a poor generalization, because the structure of the given data terms may still over-specialize the theorem. We would like for example the C terms in (4) to be generalized,

thus obtaining the associativity theorem for A.

6. GENERALIZATION BASED ON ESTIMATED FUNCTION BEHAVIOUR

The data structures still present in the theor­ em mirror (part of) the structure of the given data terms. A further (and possibly bold) gener­ alization is now required. The first problem is to select data terms as candidates for generali­ zation. The second problem is to check that candidate modifications do not change the compu­ tation structure.

The system looks for those data terms which are so general that they appear as "skeletons" for their type. A skeleton of type T is a data term such that: i) All constructors of type T occur in it; ii)In the argument positions of type T'IT a variable of type T' occurs .

Examples of skeletons are C(vl,C(v2,NIL)) and S(O), while the following data termsdo not classify as skeletons: TT, because it does not contain the constructor FF, and C(S(O), C(vl,NIL)), because S(O) is not a variable.

Focussing on skeletons embodies a peculiar noti­ on of computation. First of all, the "stru­ cture" of data terms and the "structure" of computations are considered to be strongly in­ terrelated, so that the forced computation is believed to be able to reconstruct the details of data terms which are necessary and suffici­ ent to determine the computation flow. Second­ ly, the skeleton definition requires all constr­ uctors for the type to occur in a skeleton, in the assumption that if a constructor would not occur, the given computation trace would not be a representative of all the possible computati­ on traces. Finally, the hierarchical definition of types is believed to induce a corresponding nesting in the computation, and therefore will require hierarchical generalizations, as we wil­

l see later.

Still, two different skeletons may be related to each other in such a way that their general­ ization to two different variables would not be valid. The system adopts just a naive notiorfof

relationship, i.e. two skeletons are related iff they share a universally quantified varia­ ble.

Good candidates for generalization are defined to be the maximal unrelated skeletons. However, the given theorem may hold only if the actual data terms obey exactly the structure described by the corresponding skeletons. A classical ex­ ample is the following

EQN(PLUS(S(O),S(S(O))),TIMES(S(O),S(S(S(O))))). Hence, the system must test whether candidate skeleton modifications appear to bring about computation structure modifications.

The system test is based on those functions,

such as EQN, which simultaneously recur on their arguments. Simultaneously recurring functions (srf's) implicitly define a measure on the argu­ ment values (i.e. the number of recursive appli­ cations which are needed to completely "peel down" an argument value). The difference betwe­ en the argument measures determines which srf base equation is applied to terminate the compu­ tation. If the actual argument measures depend at different degree on the measure of the candi­ date skeleton, a skeleton modificationmay cause a different base equation to be used to termi­ nate the (modified) computation. To be on the safe side, the system discards the candidate.

The measure of a data term cannot be computed a priori since it is defined by the rewrite equa­ tions of the functions which recur on it.

In the current implementation a drastic simpli­ fication is made, and only data structures whi­ ch are reflexive on one argument position are tested. Mo'reover, the actual argument terms of a srf will in general be function application terms (just like in the example) . Hence, the system must be able to estimate how functions transform data term measures.

For each function, the system computes an ari­ thmetical expression (called norm) which, rou­ ghly speaking, expresses the measure of the function value in terms of the measure of its arguments. Function composition in the argument terms of the srf can be accounted for by introd­ ucing two suitable auxiliary functions (defined by composition) such that the srf argument term­ s can be rewritten as applications of the auxi­ liary functions to data terms only. The auxilia­ ry function norms tell the system how the measu­ res of the the outermost predicate argument values depend on the measures of the skeletons. Since we want to capture the effect of the modi f i cation of a specific skeleton, the parti­ a l derivatives of the auxiliary function norms w.r.t. the argument position under generaliza­ t ion are computed. The generalization is accept­ ed i ff the derivatives can be simplified to the same expression. Note that such a test brings together the function definitions, the form of

the theorem, and the computation structure.

For i nstance, let S(O ) in the example pl+p2 (see below), us consider the candidate above . The norm of PLUS is and the norm of TIMES is pl *p2 (the variable symbol pi occurring in norm expressions stands for the measure of the i-th argument term). The partial derivatives of pl+p2 and pl *p2 w. r. t. pl are 1 and p2, thus S(O) is not generalized.

Since constructors may occur in function defin­ itions, norms for constructors must be given (which, by the way, define the measures of data terms). The norm of a constructor is defined to be 0 if the constructor is not reflexive, other­ wise l+pi if the constructor is ,reflexive in the argument position i. The norm of a function is computed from the function definition and from the norms of the occurring functions. Basi­ cally, the norm of the function used in the base equation is combined with the norm of the function used to perform recursion where the operators are substituted by higher rank opera­ tors. The algorithm for computing the norm [~ is rather intricate because many heuristics ha­ ve been designed to cope with the complexity of function definitions. The computed norm is actu­ ally satisfactory for a wide class of functions (examples are reported in Appendix II). Howev­ er, the estimate of decreasing functions, and of functions with more than one recursive or

base equations are far from being adequate.

We can now describe the stepwise generalization method based on estimated function behaviour. Candidate skeletons are recognized in the given theorem, and each candidate is tested as follow­ s. The computation trace is analyzed to pick out those srf application terms in which the candidate occurs. If no such term is found, the candidate skeleton is generalized. If for each srf application term the partial derivatives of the arguments w .r. t. the candidate are the sa­ me, then the candidate is generalized, otherwi­ se it is discarded. Candidate generalization may introduce new candidate skeletons which are in turn tested and generalized as above.

7. A COMPLETE EXAMPLE

Let us consider the following ground property EQS(LR(LA(LC(C(PLUS(S(O),O),C(S(O),NIL)), (El)

LNIL),

LC(C(PLUS(S(O),O),C(S(O),NIL)), LNIL))),

LA(LR(LC(C(PLUS(S(O),O),C(S(O),NIL)),

LNIL)),

LR(LC(C(PLUS(S(O),O),C(S(O),NIL)),

LNIL)))).

The term PLUS(S(O),O) is never evaluated. A free variable ~ is substituted for it,and free variables ~ and nlly are introduced to force computation yielding the symbolic terms

The forced computation of (E2) gives EQS(LR(LA(LC(C(~,C(nx2,NIL)),LNIL), (E4)

The type LL terms are due to the applications of LA equations, while the type L terms come from the applications of EQLN equations. Th~ variables appear because EQLN checks for L length equality only. The forced computation of (E4) gives

The generalization method based on equivalence is applied to (E4). The reflexive predicate EQLN application term

EQLN(C(nl!,C(~,NIL)),C(nl!,C(~,NIL)))

was reduced to TT (note the role of LR). Since the argument terms are identical and do occur in (E4), they are generalized to~· Analogous­ ly,.the data term C(nxl,C(nx2,NIL)) is generaliz­ ed to nlx. The following theorem is thus induced EQS(LR(LA(LC(nlx,LNIL),LC(~,LNIL))), (E6)

LA(LR(LC(~,LNIL)),LR(LC(nlx,LNIL)))).

11/hen the method is applied to (E5) ,the following EQLN term is found

EQLN(C(nl!,C(~,NIL)),C(~,C(nx2,NIL)))(E5.1) Since the argument terms are not identical, (E5) is correctly no more generalized.

Finally, the generalization method based on est­ imated function behaviour is applied to (E6). The skeletons are LC(nlx,LNIL) and LC(~, LNIL), and EQS is the only srf which applies to terms containing them. Since the partial deriva­ tives of LR(LA(pl,p2))and LA(LR(pl),LR(p2)) w.

r.t. pl are bothl, the skeleton LC(nlx,LNIL) is generalized to nllx. LC(~,LNIL) is analog­ ously generalized to nlly, and the system indu­ ces the following theorem

EQS(LR(LA(nllx,nlly)),LA(LR(nlly),LR(nllx))). 11/hen (E5) is considered, the skeletons C(nxl, C (~,NIL)) and C(nl!,C,(~,NIL)) are not gen­ eralized. In fact, the srf EQLN is directly applied to them (see(E5.1)), i.e. we have a term of the form EQLN(pl,p2). The partial deriv­ atives of pl and p2 w.r.t. p1're 1 and 0, thus the skeleton C(nl!,C(~,NIL)) is not generali­ zed. The same happens for C(nxl,C(nx2,NIL )). A­ gain (E5) is correctly no more generalized.

8. COMPARISON IIliTH RELATED WORK

---- ----

The inductive method we have presented has been influenced in many respects by previous resear­ ch in induction. First of all, the generali za­ tion based on proof can be classified as a successive refinement method. We do not need to iterate the process of guessing and refi ning , because the formal calculus environment provi de­ s for a powerful technique (forced symboli c computation) to exactly adjust the initial gues­ sing. The use of the given computation trace to strengthen the theorem, relates to Brown ' and Tarnlund's temporal me thod based on proofs (4) .

Secondly, we have had the advantage of being able to draw on the ideas of Boyer and Moor e (2] and of Aubin (1] , who tackle the problem of generalizing the theorem to be proven by induc­ tion. One basic problem is that of dist i n­ guishing different occurrences of a variable. Boyer and Moore generalize terms which the i nvo­ lved functions recur on, thus relating generali­ zation to function definition . In their

footsteps, Aubin points out the c lose relation­ ship among generalization, proof by induct i on and symbolic computation. His method general ­ izes those variables which an interpreter would first instantiate during symbolic computation. Thus, only the first and fourth occurrences of x are generalized in the theorem

EQL(A(x,A(x,x)),A(A(x,x),x ) ). We br i ng the who­ le computation structure to bear on the prob­ lem, and we can capture rather complex relation­ ships, as shown in the example in Se.-, t i on 7. Because of the peculiar role played by the LR function, Aubin's method would incorrectly gene­ ralize the first and third occurrence of x in the theorem EQS(LR(LA(x,x)),LA(LR(x),LR(x) ) ) .

9. PROPERTY INDUCTION, THEOREM PROVING AND PROG­ RAM VERIFICATION

Just as one can prove whether a specifi c i nduce­ d property does hold, one can prove t hat t he inductive method· itself is guaranteed to induce valid properties only. We have been able to prove this result, with a few limitations [8).

First of all, the induced theorem must have the form b( tl, t2), where b is a boolean function defined according to the schema

b(T,T')=BCONSTl b(c(x,y),T')=BCONST2

b(T,c'(z,w))=BCONST3

b(c(x,y),c'(z,w))=bl(b2(x,z),b(y,w))

bl(BCONST4,y)=BCONST5 bl(BCONST6,y)=y

where BCONSTi are boolean constants (note that BCONST4~BCONST6) , T, T 1 , c, c' type constructors, and b2 a boolean function belonging to the class .

The following definition schemata characterize the class of functions occurring in tl and t2.

n(T,y)=u(y) n(C(x,y),z)=C 1 (p(x),n(y,z))

r(T,y)=w(y} n' (T' ,y)=v(y) r ( C ( x, y) , z) =n' ( r ( y, z) , C' ( x, T 1 ) ) n 1 (C 1 (x,y) 1 z)=C"(x,n 1 (y,z))

s(x,y)=f(g(x,y),h(x,y))

where u,v,w,p and f,g,h either are constructors or belong to the class (note that n' is a res­ tricted n-function).

The limitations on the form of the property and of the boolean functions are introduced to avoi­ d theorems whose proofs need case analysis. The form of the involved functions is constrained so that the structure of their computation grad­ ually changes · when the structure of the data terms is gradually changed. Significant functio­ ns, predicates and theorems fall into the clas­ s. It is certainly not possible to express significance by a figure, but it may be interes­ ting that about 35% of the theorems listed in [lJ and involving single reflexive data types are induced by our system and belong to the

above class. Classical examples are

EQL(A(x,A(y,z)},A(A(x,y),z)), EQL(R(R(x)),x), and EQL(R(A(x,y)) ,A(R(y) ,R(x))). The reflexiv­ ity theorems for EQN, EQL, EQLN, and EQS fall into the class and are induced by the system.

At the present, the application of such induc­ tive method to theorem proving has one advanta­ ge but suffers from a few limitations. The advantage is that no combinatorial explosion arises in the proof. Free variable introduction is indeed a non-deterministic process, but no nesting of non-deterministic choices is invol­ ved. On the other hand, the major limitation of the proposed method is that it is not proven complete. Thus, it can be used only as an auxi­ liary tool, which may fail, but at least requir­ ing a bounded amount of resources. Moreover, the method can prove only function properties whose restrictions have been described above. These are heavy limitations for a general purpo­ se theorem prover.

In the framework of program verification, where the goal is in general that of proving proper­ ties of functions, it is more likely that the inductive method can help, provided that the theorem to be proven (or a subgoal generated during the proof) is within its reach.

The present inductive method has been implement­ ed into an experimental system mainly by modify­ ing existing TTEL symbolic interpreters. No ca­ re has been taken to obtain an effic~ent system.

APPENDIX I

(TYPE(EQLN(L,L))=B; {EQLN(NIL,NIL)=TT;

EQLN(C(x,y),NIL)=FF; EQLN(NIL,C(z,w))=FF;

EQLN(C(x,y),C(z,w))=EQLN(y,w)})

(TYPE(EQL(L,L))=B; { EQL(NIL,NIL)=TT;

EQL(C(x,y),NIL)=FF; EQL(NIL,C(z,w))=FF;

EQL(C(x,y) ,C( z, w) )=AND(EQN(x, z) ,EQL(y, w) )} ) (TYPE(EQS(LL,LL) )=B; { EQS(LNIL,LNIL)=TT; EQS(LC(x,y),LNIL)=FF; EQS(LNIL,LC(z,w))=FF; EQS(LC(x,y),LC(z,w))=AND(EQLN(x,z),EQS(y,w))}) (TYPE(AND(B,B))=B; lAND(TT,TT)=TT; AND(TT,FF)=FF; AND(FF,FF)=FF; AND(FF,TT)=FF}) (TYPE(PLUS(N,N))=N; {PLUS(O,y)=y; PLUS(S(x) ,y)=S(PLUS(x,y) >J) (TYPE(HANOI(N) )=N; l HANOI(O)=O; HANOI(S(x))=S(TIMES(S(S(O)),HANOI(x))}) (TYPE(TIMES(N,N) )=N; { TIMES(O,y)=O; TIMES(s(x),y)=PLUS(TIMES(x,y),y)}) (TYPE(A(L,L))=L; {A(NIL,z)=z; A(C(x,y) ,z)=C(x,A(y,z) l}) (TYPE(R(L))=L; {R(NIL)=NIL; R(C(x,y) )=A(R(y) ,C(x,NIL) )} )

(TYPE(LA(LL,LL))=LL;

{LA(LNIL,z)=z; LA(LC(x,y),z)=LC(x,LA(y,z))})

(TYPE(LR(LL) )=LL; { LR(LNIL)=LNIL;

LR(LC(x,y))=LA(LR(y),LC(x,LNIL))})

APPENDIX II

We report here the norm computation for some functions given in Appendix I. We look at funct­ ion definitions in terms of the schema f(T,y)=g(y) f(c(x,y),z)=h(x,f(y,z)), If Norm(h) has the form a+pl, then Norm(f)=Norm(g)+a*pl. For example, since Norm(S)=l+pl and Norm(C)=l+pl, then Norm(PLUS)=Norm(y)+1*p1=p2+pl, and Norm(R)= =Norm(NIL)+Norm(C(x,NIL)*pl=O+l*pl=pl. If Norm(h)=a+b*pl, then Norm(f)=a*(btpl)/(b-1)+ +Norm(g)*bt pl.For example,Norm(HANOI)=1*(2tpl­ -1 )/(2-1)+0*21 p1=21p1-1, since Norm(g)=O, a=1, b=2.