CM-Strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs

1. MOTIVATION

Let us start with an exampie which is nothing more than a presentatlon of our methodology when proving theorems by induction.

The reader is asked to work through thls example with us carefully, because lt will then allow a better understandlog of the theoretlcal explanation whlch follows in next sections.

Let us suppose that we want to prove

Vx (EQL (REV x) (FOO x null)),

noted Vx Q(x), where x is of the type LIST-of-NAT given by the family of constructors (null. unlt, append}. NAT is the type of natural numbers. EQL is the equality on LIST-of-NAT. FOO and REV are functions

FOO: LIST-of-NAT x LIST-of-NAT -> LIST-of-NAT,

REV: LIST-of-NAT -> LIST-of-NAT, defined by following axioms:

A1: (FOO null!) = 1

A2 : (FOO (unit a) l) = (append (unit a) 1)

A3 : (FOO (append (:unit a) l) L) = (FOO l {append (unit a) L))

A4 : {REV null) = null

A5: (REV{unit a)) = {unit a)

A 6 : {REV{append (unit a) l)) = {append (REVl) {unit a)).

Consider the family :of constructors (here (null, unit, appendl). It decomposes the induction proof into cases, each possible valuation of the induction variable x producing a case. Since this valuation is a kind of equality, we shall denote it by EQT.

Our example has three cases:

case(i) (EQT x null), prove Q(x) ;

case(ii) (EQT x(unit a)), prove Q(x);

case(iii) (EQT x (append {lWlit a) 1)), suppose Q(l) and prove Q(x).

Let us note (Valuat x) a chosen valuation of x. Let a., be {x .... (Valuat x)J.

Intuitive description of CM-strategy:

We describe Q(x) by its "pattern" PTQ. As an Ulustration, let us suppose that it is PTQ = (H EXPRl EXPR2) . In the above example, H = EQL, EXPRl = (REV x), EXPR2 = (FOO x null).

Using the valuation of x in each case, (by the evaluation of H with re,gard to EXPRl and with regard to the given valuat!on, and by an application of induction hypotheses, if it is the case) one deduces a valid formula which has the pattern PTQ' = (H EXPRl EXPRl'). In this step, the value of EXPR2 is not t.aken into account.

The next step is the constructive one: We try to find valid transformations of EXPRl' into EXPR2, i.e. we transform EXPRl' into EXPRl", so that EXPR1" = a.,(EXPR2) .

lt may happen that a direct transformation of EXPRl' into EXPR2 is not possible. We then evaluate EXPR2 for the current valuation. This Ieads to EXPR2'. Then, either EXPR1' can be transformed into EXPR2', or the equality EXPRl' = EXPR2' becomes a new theorem, tobe treated as before. The last case may well generate an infinite sequence of theorems to be proven.

Now the example will show how we construct this equality, and how some infinite sequences <tre reduced to a .general­ ized theorem.

case(i):

(EQT x null), a., is I x .... null}. Here,

PTQ' = (EQL {REV x) null) because of A.. We now try to find the axioms th.at can transform EXPRl'(= null) into EXPR2 (= (FOO ... )). The axiom A1 is the only one which can be used, because it may have instances of the form null = (FOO ... ). We obtain the equality (which is an instance of A1): null = (FOO null null), i.e. we have succeeded in obtaining a transformation of EXPRl' (=null) into EXPRl" (= (FOO null null)). Moreover,

EXPRl" = a.,(EXPR2) . This completes the proof of case (i).

case(ii):

(EQT x (unit a)), a., is {x <- (unit a)). Here,

PTQ' = (EQL (REV x) (unit a)). We therefore try to transform EXPRl' = (unit a) into an expression of the form (FOO ... ) . We have no space here to explain why, but only two axioms, which may have instances of the form (unit a) = (FOO ... ), can be used: A1 and A2. Using A1, one tinds th.at EXPRl' ( = (unit a)) can be transformed into EXPRl" (= (FOO null (unit a))). But

EXPRl" 7' a.,(EXPR2), therefore this possibility is rejected. Because (unit a) is (append (unit a) null), using the instance of A2 (i.e . {unit a) = {FOO {unit a) null)), one tinds that EXPRl" is (FOO (unit a) null).

EXPRl" = a~(EXPR2) is satisfied, and this completes the proof of c.ase(ii) .

case(iii):

(EQT x (append (unit .a) 1)), a., !s {x <- {.append (unit .a) l)J . In this case "We have at our disposal the induction hypothesis:

(EQL (REVl) (FOO 1 null)).

By the evaluation of (REV x) with regard to the given valua­ tion of x, and an immediate application of the induction hypothesis, we obtain

PTQ' = (EQL (REV x) (append (FOO 1 null) (unit a))).

As there are no axioms that have an instance matehing

(append (FOO l nuH) (unit a)) = (FOO . .. ), we must evaluate DCPR2. We obtain EXPR2' = (FOO l (unit a)). We want to prove EXPRl'= EXPR2', i.e .

Q1(l,a): (.append (FOO l null) (unit a)) = (FOO l (unit a)).

This equality becomes a new theorem to be proven:

Vl Va Q1(l,a) .

We skip the application of our methodology to this new i:heorem. It "falls" ag.a!n by leadlog to a new EXPRl' and EXPR2' that..are different, .as before. The new theorem reads: Q:l(l',a,b):

(append (append (FOO l'null) (unit b)) (unit a))

= (FOO l' (append (unit b) (unit a))).

Continuing this way we obtain, that for proving Q2 we need to prove Q3, for proving Q3 we need to prove Q4 , .... After ßeveral steps we try to see, whether it is posstble to find a generalized theorem determined by Q1, Q2. Q3, Q4, ....

The reader can see that the structures of Q1 and Q2 are very similar, being of the form

Q*(l,L): VI VL (EQL (append (FOO 1 null) L) (FOO 1 L)).

Therefore Q· will be this generalized theorem.

In this case, the automation of the common structure of Q1 and Q2 is trivial since Q· is simply the least generalization of Q1 and Q2 (more details can be found in [k31]) .

We have undertaken the proof (still at a conjectural state) that provable theorems can be expressed as a sequence of theorems which can be generalized.

The proof of Q·(l,L) is not difficult, and left to the reader.

Why could we conjecture such a "simple" form of the sequence of constructed theorems? Why can proofs always follow the same scheme (evaluation of an expression, appli­ cation of the induction hypothesis, directed transformation of an:expression into .an other one, ... )? The reasons are sim­ ple:

1) Tlae form of .a given theorem indicates which is the for­ mul.a we have to obtain for a given valuation of the induction variable. This .directs the construction of expressions neces­ sary for a construction of this formula.

2) Functions .and predic.ates are defined recursively, and wi.th '1'egard to a given Jamily of constructors . This facili­ tates a search for links among express!ons, and together with the form of the formula we want to obtain, it indicates missing Iemmas.

3) Moreover, .a good formulation of the structural induction principle points at the elements for which we should expli­ citely express the induction hypothesis, and therefore an application of induction hypotheses no Ionger is (contrary to [b12]) one of the most difficult problems when proving theorems by induct!on.

These arguments are only consequences of next sections.

2.1. PROOFS BY INDUCTION

In pr.actice, when we try to prove by induction a theorem Vx A(x) with x of the typeT we know (or should know) some primitive functions (or constructors) by which we can obta!n elements of the type T by a simple combination of these primitive funct!ons. Functions with a codomain T will be called gene'f'ators of T.

Moreover, we suppose that we know selectors, i.e. functions which for an element x of the type expressed by some primi­ tive function f .as (f y) gives the result y.

Fin.ally, we suppose that we have at our disposal predicates which take the value TRUE only if an element of the type has been.constructed using the given primitive function.

By these predicates p 1 , ... , P~& we can define the equivalence relation - on the type T: for x, y of the type T x~y iff there is p;. such that (p, x) = (p; y) = TRUE.

We can then choose the representative rep; of the dass P,=l x: (p, x) = TRUE J, 1=1, ... ,k. For 1nstance, for T = LIST-of-NAT we have the pred1cates null?, unlt?, append? and the representatlves of the appropriate classes are null, (unit a), (append (unlt a) 1).

So, when we want to prove 'v'x A(x) of the type T it is enough to take all the representatives rep1, ... , rep~r; , and to prove A(rep,) for each 1 = 1, .. . , k.

Now we introduce the notion of the valuat1on of one element x as the choice of one rep, which will be noted (EQT x rep,), and very often we say that x is represe nted by ref!\ . So EQT is in a sense an e9uallty on T. It is not an e9uality throughout the proof but only in the consldered case (for a given representatlve) . When we speak about one possible not­ explicitely determined valuatlon of x, we will wrlte (Valuat x) , l.e . (Valuat x) e lrep 1, ... , rep~r;l .

2.2. THE STRUCTURAL INDUCTION PRINCIPLE- FORMULATION

Let us tlrst introduce some notions and notatlons. Let us denote by FGT the familly of generators of some well-founded type . and by FCT the familly of constructors of the type T, l.e . FCT c FGT. We classify elements of FCT in the following way:

• constants o! the typeT (i.e fJ : ->T)
• basic-T-operators {l.e. fJ: D{ x .. . x D/. 1 ... T, such that there is no m e I 1. ... , n1 I suchthat D/,. ls T) ;
• general-T-Junctions (i.e. fr D{ x ... x D~ 1 ... T, suchthat there ls at least one m e I 1, ... , nJ I suchthat D/,. isT) .

PRINCIPLE OF STRUCTURAL INDUCT1ClN

Let us suppose that we want to prove that A(a) holds for an arbitrary element a of the type T. A(a) holds for all a of the type T provided that the following hold:

• A(J c) holds for every constant J c of FCT,
• A(J 1 (x{, ... , :x/.. )) ca11 be proved for every basic-Tconstructor J 1 of FCT with tne arbltrary arguments x{, ... , ~J ( x/,. is of the type D/,. for m e I 1, ... , n 1 } ) considered, d.uring the proof of A(J1(x{. ... , x~)). as local constants (i.e . they do not change their value during the proof-procedure) ,
• A(!1 (x{, ... , x~ )) can be proved for every general-T­ constructor f J, wit~ x{ , ... , x~ 1 considered during the proof as local constants, and startlag the proof procedure by sup­ posing
• (i) explicit validity of A(x/ ) for each local constant x/ of the typeT (xJ, e l:r{, ... , x~ I) 1
• (ii) implicit validity of A(p.,) for any p 09 < xJ,, where xj 9 is a local constant and p 09 belongs to the well-founded erdering ofT, called DJ, .

Here, impliclt means that during the proof procedure a new parameter Pa, of T can be constructed, and p 81 is smaller than xJ . We can then suppose A(p, ) to be valid. Naturally, I I p., will not occur expllcitely in A(/;(:r{. ... , x~ 1 )), which is the last formula of the deduction.

• (iii) implicit validity of A( 9) for any 9 < f 1 (x{ , ... , x~ ).

As one can easily notice, this principle of structural induc­ tion cuts a proof of 'v'xA(x) into two cases (distinguished by the existence of inductlon hypotheses) .

2.3. STRUCTURAL INDUCTION AND STRUCTURE OF FORMULAE

In this section we explain that the structure of a formula A (when provlng 'v'x A{x)) can Iead to some heuristics when using the structural inductlon princlple dur1ng the proof of the desired theorem.

Remark 2. 3. 1.:

It may happen that we do not want to prove· 'v'x A(x) for all elements of the type T, but only for elements which satisfy some condition P, l.e. we want to prove 'v'x (P(x) :::::> A(x)) . The predic.ate P in our (inductive) approach cannot be arbi­ trary, because we must be able to determine constructors of the type Tp =I x I xeT 11. P(x) holdsl . Then instead of provlng 'v'x (P(x) :::::> A(x)) , we prove the theorem 'v'x A(x) in Tp .

Example 2.3.1.: Let .us suppose that in NATwe want to prove the theorem:

'v'y (odd y) :::::> [(2div y) = (Suc (2div (substr1 y)))] , where 2div is the integer-division-by-two function, the meanlng of odd, Suc and substr1is clear.

The predicate odd determines the type NATort.tJ in which each element is either (Suc 0) or can be written as (Suc (Suc a)) for a e NATort.tJ · It means that we will try to prove

'v'y [(2div y) = (Suc (2div (substr1 y)))] in the domain NAT.ort.tJ ·

Remark 2. 3. 2.:

In A(x) may also occur some functions or predicates which are detlned with the help of a "selective" function df of the typeT (i.e. df: T1 x T ... T, where T1 can be T and for hp e T 1 ( df hp 9) is .an element of T s.ni.aller than 9.)

In a such case, when we want to prove A(x) for x given by some representative of T expressed by a general-T­ constructor, we include in our induction hypotheses also a hypothesis 'v'hp A((df hp x)) . One can see that hp here represents all elements p of T1 for which A((df p x)) is satistled. We call such a hp the help-parameter . A predicate A detlned with the help of a selective function will be called the predicate depending on a help-parameter, which will be written: A depends on hp.

Exa.mple 2.3.2.: Let us suppose that we want to prove 'v'x 3zQ(x,z), where Q(x,z) ls (PERMUT x z) 11. (ORDERED z). The detlnltion of PERMUT, given by (AL23)-(AL27) in -I. con­ tains a "selective" func:tion DELETE. When we have to prove 3z Q((append (unlt a) l),z), we use the induction hypothesis 'v'p 3z' Q((append (unlt a) (DELETE p l)),z')11.(MEMBER p 1) as well .as the more classical one 3z" Q(l,z") . One cannot know in advance which one is tobe used (may be both) . In general one has to use all the possible induction hypotheses induced by the "selectlve" function.

What is gained by using of our structuralinduction principle as a method of provlng theorems? Nothing more than

• the knowledge of the form (or pattern) of the formula which we want to obtain, l.e., A(!1(x{. ... , x~ 1 ))) from given axioms .and formulae A(p. ) A(xJ ) for elements p"v and xJ described in the formul;tion ~f the structural inductio~ principle, .and
• the generatlon of induction hypotheses in the re9uired form.

3. CONSTRUCTIVE MATeHING

The ide.a of constructlve matehing comes from realizing that a given theorem 'v'x A(x), to be proved in a theory F, expresses a form A(x) of a formula B which should be proved from axioms and hypotheses , i.e. we would llke to construct a B, valid in F, such that there is a substitution a such that aA(x) = B.

3.1. DEFINITION AND EXAMPLES

Definition 3.1.1.: Form.ula B matches formula A ltf there ls a substltutlon a suchthat aA is identical toB (l.e . aA=B) .

Exa.mple 3. 1. 1.:

Let B be ((Suc a) = x2*u1 + (Suc «2)).1\ (Suc «2)<x2). let A be (x 1 = x2·z 1 + z2).1\ (-z2<x2)). Then, B matches A with the substitution (x1 <-- (Suc a), z1 <-- «1. z2 <-- (Suc «2)}.

Definition 3.1.2.: If formulae A and B do not match, but from the theocy F and B we can prove B' which mat~hes A, t~en the pr.ocess of fl.nding B' is called Constructtve Matchmg (CM) of A and B.

When proving the theorem YxA(x), using the structural inductlon -principle, we have to prove the validity A( rePt,) for i e (1, ... , k). for all the representatives rep1, .. . , repk Let us note a1 the substitution (x <-- rep.J. Then, in the case (EQT x rep·) we have to obtain the formula a;(A(x)) . One can see tha~ (EQT x rep;) .and A(x) do not match, but, lf YxA(x) ls provable in F, we can prove A(rep;) from theory F (extended by possible induction hypotheses), and (EQT x rep;) .

HOW TO PERFORM THE CONSTRUCTIVE MATCHING

Let Q: T1 x T2 .... :BOOL be a recurslve predicate, detined with respect to representatives of T1· Let rep be a representative glven by .a general-'T1-constructor. Then the part of the detinltion Q with respect to rep c.an be expressed symboli­ cally as follows:

Q(x1,x2) holds

z 1=rep "'Q(srep1.f l(x2)) .1\ PI(! J(rep).f J<x2)) { z 1=rep"' Q(.srep2.ff{x2)) "'P2(j~(rep),JN(x2)) if

z 1=rep"' Q(srep".,fT(z2)) .1\ P".(!'!,'(rep).f~(x2)), where, for j e (l, ... ,m}. the following are satistied: srep; is obtained from rep by some selector, for any y /Hy)<y; P; are already detined predicates, J! are already detined func­ tions, moreover, for any rep and any z 2, the following condi­ tion, called CONDP,

is TRUE.

Let us call the j-th line of the detinition Q for x represented by rep, the formula

Q{srep1 ./ {(z2)).1\P·(/ f( rep).f ~(z~) .

.

On each j-th line z 2 is considered as completely (symboli­ cally) determined by f {(x2) and /i(z2},i.e. there is a "func­ tion" �1 (!{.f~) suchthat G;(/{(m)./Hm))=m for any m.

Let EXPR be an unquantitied expression depending on one variable only, say x, and let Yx Q(x,EXPR) be the theorem to be proved using the structural induction principle.

Q(z1,z2) is detined with regard to z 1· Therefore to prove Yx Q(x,EXPR) means, for an arbitrary x, to prove that EXPR belongs to the dass, say c;, of all x2 for which Q(x,z2) holds.

Let us consider the case, where x is represented by a general-T1-constructor rep. Then we have to consider the above mentioned part of the detinition of Q. Let us note 7'j the substltution (x <-- srep1 }.

If x is represented by rep, the dass c;..p is implicitly deter­ mined by the detinltion of Q: If Q(srep;. ql) .1\ P;(!Hrep),q2) holds for some q1, q2. then we know tliat G;(qi,q2) e Cr.p. i.e. there exists an x 3 from c;..p such that fHxs)=qi and /~(zs)=q2.

Moreover, z 2 e ~ only if there is a j-th line suchthat

('··) · Q(srepi, /{(z2)) "'P;(/f(rep),(!Hz2)) is satistied. This is to say that lf Q(rep,z2) is valid, then there is a j-th line such that ('··) is satistied. Let us call (··) the valid part of Q(rep,x2 ) (correspondig to j-th line). One can see that as soon as the valid part (··) of the formula Q{rep,x2) was obtained, in our consid:eration we can replace (··) by Q{rep,x2) .

In our approach, ftnding out whether or not EXPR e Cr.p , for the given representation of x by rep, is performed by taking an x2 e c;..p, and verifying whether or not x2 is equal to ( or can be transformed into) EXPR, i.e . we "construct" the for­ mula Q(rep,EXPR) in the following way:

We take an x 2 for which Q(rep,x2) is known. Then we vedfy the posslbility of a transformation of x2 into EXPR (for the given representation of x by rep). .

The choice of x2 is not arbitrary. We only choose an x2 which has some links with EXPR. The links between elements of C,..p .and EXPR are expressed in induction hypotheses .

We will show, how these links may be explicited:

Let us suppose, that Q does not depend on hp (see Remark 2.3.2.), i.e. that srep1 does not depend on hp for J = 1. 2, .. _.. m. Then, we have at .our disposal the induction hypothests Q(srep1 , Tj(EXPR)}, where Tj is (x <-- srepil · Because we want EXPR to be from C,..p . for some j must T;(EXPR} be f{(EXPR) . .

Moreover, for the same j, P;(/f<rep), fi!(EXPR}) must be satistied.

Now, if srep; depends on hp for some j, i.e. srep;=(df t1 rep) for some t 1, let us note Pi the replacing of t 1 by hp. Then, we have at our disposal the induction hypothesis

(H/.;,) Yhp P;(Q{srep; , T;(EXPR))) .

7'; is (x <-- srep; }. Therefore T;(EXPR) depends on hp. a~ well. But, if srep1 depends on hp, lt means that 1n .the detinitwn of Q the expression t 1 is determined as g(/S(x2)) for some function g. Therefore instead of taking H/.p we use P;(T;(Q(x,EXPR))withp; = lt1 <-- g(!MEXPR})}. .

Because we want EXPR to be from C,..p, for some J, p ·(T·(EXPR)) must be f{(EXPR) (or, if they are not same, 7'~(E5c?R) must be transfermahle intof{(EXPR)).

Moreover, P;(/Hrep), JMEXPR)) must be satisfied.

Notice, that it may happen that while T;(EXPR} and f{(EXPR) may not be the "same" expressions (for instance (Suc ( + .a b)) .and ( + a (Suc b)) are not the same expres­ sions), T1(EXPR) can be tr.ansformed into f { (EXPR) .

With regard to preceeding remarks , the construction of Q(x,EXPR), for the given representation of x by rep, is as fol­ lows:

Let ~ be a symbol representing elements x2 e C,..P . Let us note (·) the formula Q(x,(). As mentioned above, (*) for x represented by rep holds, only if there is a j-th line suchthat {'**) is satistied.

We therefore take the detinltion of Q on j-th line (j=l, ... ,m). We write

(1j) Q(srep1,f{(Ü) "'P1(!Hrep)./Hü> .

srep1 <rep, therefore we have at our disposal the induction hypothesis Q(.srep;,·;(EXPR)), resp. P;(Q(srep;.T;(EXPR))) if srep1 depends on hp. The induction liypothesis allows us to replace /{ W in (1j) by T;(EXPR) , resp. by P;(·;(EXPR)). So we have constructed

(aj) Q(srep1,T1(EXPR)) 11. P;(J~(r_ep).f~W) . resp. (2j') P;(Q(.srep;.Tj(EXPR))) .1\ P;{J2(rep).J~W) . Now, we verify whether or not

Ps(/fCrep).f~(EXPR))

is satistied. If it is, we verify whether or not

G;( T1(EXPR)./ ~ (EXPR)), resp. �1(pj(Tj(EXPR}}.f~(EXPR)) is equal to (or can be transformea into) EXPR.

If P;(Jf(rep).f~(EXPR)) is not satistied for the j-th line, we call this line a total-failure-line, because there is no sense in looking for some strategy by- which we could succeed in con­ structing Q(x,EXPR) on this line. But if the theorem is prov­ able, then. with respect to the condition CONDP, there must be at least one l!ne 'Wbich is not a total-failure-line, and for which �;(T1 (EXPR)./~(EXPR)) can also be transformed into EXPR.

lt may also happen that G·(T;(EXPR.Jä(EXPR)) cannot be transformed directly into WR. Then, we Iook for a rule (a Iemma) of the form:

Q(rep, 0( T;(EXPR}./HEXPR)) A ... ::::::> Q(rep,EXPR) .

In such a way, if we succeed in constructing a valid part of Q(x,EXPR), for the given representation of x by rep, we can conclude that we have constructed the formula Q(x,EXPR), v.alid for the given representation of x by rep.

Remark: One can argue that we should first verify the condi­ tion P1, rather than jmmediatly apply induction hypotheses. This objection is not valid if theorems Yx 3zQ(x,z) are also treated (see- II}.

In order to link this discussion with our intuitive description of the CM-strategy (section 1), one can notice that H is Q here, EXPRl is x, EXPR2 is EXPR. EXPRl' is �;(T;(EXPR)./~(EXPR)), resp. G;(P;h(EXPR})./HEXPR)).

Let us suppose that P1 (!H,-ep)./~(EXPR)) is satistied. The English commentary produced during the proof is then: By the evaluation of Q with regard to x represented by rep, and with regard to { r.epresenting the class c;..,P we obtain Q(x,G;(/{({).JäW)). Then by the appl!cation of the corresponding induction hypothesis, we obtain the formula

Q(x,G1( r1(EXP~)./ ä{EXPR))) resp. Q(x,G;{p;(r 1 (EXPR))./s(EXPR))), valid for the representation of x by rep.

Finding thc: valid transformation of G;(Tj(EXPR}.fHEXPR)) into EXPR by ... ( axioms and rules !living this transformation are mentloned), the formula Q{x,EXPR), valid for the representation of x by rep, is considered tobe constructed.

Et:ample: Let us suppose that we want to prcrve

Yx (PERMUT x (append (unit (last x)) (DELETE (last x) x)))) the detinit!on of PERMUT, in- I. leads us, for x represented by (append (unit a) 1), to consider the following two l!nes of the detinitlon of PERMUT:

( PERMUT x 1 xi) holds

if / x 1=(append (unit a) l) o'\(PERMUT 1 (CDR x 2)) A(a = (CAR x2)) x 1 =( append ( unit a) 1) "' (PERMUT (DELETE (CAR z 2) (append (unit a) 1)) (CDR x2)) J"~(a ~ (CAR x2))

We have : J{ is CDR, f~ is CAR, Jä is CAR, srep 1 is 1, srep2 is (DELETE (CAR z 2) (append (unit a) 1)). PERMUT is detined with regar.d to the selective function DELETE. For the given EXPR, (CAR EXPR) is (last x).

The corresponding induction hypotheses are therefore (H1) (PERMUT 1 (append (unit (last 1)) (DELETE (last 1) 1)))). r 1 is { x ... [ }.

(H2) ( PERMUT (DELETE (last x) (append (unit a) 1)) (append (unit (last (DELETE (last x) (append (unit a) 1)))) (DELETE (last (DELETE (last x) (append (unit a) 1))) (DELETE (last x) (append (unit a) 1))))) A(MEMBER (last x) (append (unit a) 1)), r 2 = I x .... (DELETE (last x) (append (unit a) l)) }.

We want to construct Q(x,EXPR) for x represented by (.append ( unit a) 1) .

Let us take the 1-st line of the detinition of PERMUT for x represented by (append (unit a) 1). We write (PERMUT x {) holds only if

(11) (PERMUT 1 (CDR Ü) A a=(CAR {) lWe verify whether or not a = (CAR EXPR). ( Le . a=(last x)) is .satisfu:d for the given representation of x.

In our approach, this is performed by checking whether or not a can be transformed into the form (last x) for x represented by (append (unit a) 1). Therefore we Iook at the detinition of the function last, and we sec: that a can be transformed into (last L) for L = (unit a)

or L = (append (unit b) (unit a)) for some b. Both possibili­ ties are rejected, and this failure is registered as a total failure TF1.

Therefore, we take the secend line of the detinition of PER­ MUT for x represented by (append (unit a) 1) . We write

(PERMUT x ü holds only if (12) (PERMUT (DELETE (CAR {) (append (unit a) l)) (CDR Ü) "a ~ {CAR {). By the application of H2 we obtain (22) ( PERMUT (DELETE (last x) (append (unit a) 1)) (append (unit (last (DELETE (last x) (append (unit a) 1)))) (DELETE (last (DELETE (last x) (append (unit a) !))) (DELETE (last x) (append (unit a) 1))))) " a ~ (CAR {). We now ver!fy whether or not a ~ (CAR {) , i.e.

a ~ (CAR (append (unit (last x)) (DELETE (last x) x))) for the given representat!on of x by (append (unit a) 1). (CAR EXPR) is (last x), therefore a ~ ((CAR EXPR) is veritied as (NOT (a = (last x)) . We verify, therefore, whether or not a .can be transformed into (last x) for the given representation r0f x. This is not possible, and we conclude that a ~ (CAR EXPR) is satistl.ed.

Because a ~ (CAR {) is in (2:!) satistied, ~22) is nothing but the valid part of (PERMUT x ~(T2(EXPR)./ 3 (EXPR))).

The last step therefore is to verify whether or not ~(r:;{EXPR).jB(EXPR)) can be transformed into EXPR, i.e. whether or not

(append (unit (last x)) (append (unit (last (DELETE (last x) (append (unit a) !)))) (DELET.E (last (DELETE (last x) (append (unit a) !))) (DELETE (last x) (append (unit a) !)))))) can be transformed into (append (unit (last x)) (append (DELETE (last x) x))). The equality of these two expressions is not possible, there­ fore we are looking for .a rule of the form (PERMUT AB) " ... ::::::> ( PERMUT AC).

We obtain that the rule we look for is the transitivity of PER­ MUT. Then, using the rule

((CAR A)=(CAR B))A(PERMUT (CDR A) (CDR B)) ::::::> (PERMUT AB)

to8ether with H2. completes the proof. For Iack of space, the .detailed description ofthislast part is not given here.

It is very ditiicult to explain such constructions without heing to·o formal. We hope that the examples given in this sectlon, and section 1. as well, help us to be as illustrative as possible.

3.2. SUBPROBLEMS WITH REGARD TO CM-PROCEDURE

During the process of CM we can use only functions and pred!cates detined by axioms. But it may happen that the proof Vx A(x) needs more functions and p,-edicates than those currently awtilable .

This situation is similar to the decomposition of the problern into subproblems (see [s04]), but with a small difference: we do not ask "how to decompose a problern into subproblems", but rather: How to determine that, for a proof of our theorem Vx A(x), we will need some new function or predi­ cate which is not explicitely detined in our system?

The aim of this becomes clear, when one realizes that these new functions will help us to explicit some parts of the representatives ( (see preceeding section and -II).

Definition 3. 2. 1.:

Let M be a predicate {:T1xT2 -+ BOOL) suchthat there exists a function rpy: T1 -+ T2 and three predicates Q1: T,xT2 -+ BOOL, Q 2 : T 1 xT3 -+ BOOL, Q3 : T3xT2 -+ BOOL, suchthat

1. rp11 is the function represented by the Specitication Theorem

Vx (P!(x) => ::Jz Q,(x,z) 1\ (Vy Q2(x,y) => Q3(y,z))), where P 1 characterizes the input domain;

2. M(p,(rpN p)) is true iff Vy Q2(p,y) => Qs(y,(rpy p));

3. Q2 is not a kind of equality;

4. Q3-;. M;

Then, we call M-problem the synthesis of rf!N from the Specitl.cation Theorem. Any M for which we can detl.ne an M­ problem will be said to ha.ve the V-property).

Exa.mple 3.2.1 .: To the predicate LTL detined in -1. we can associate the theorem (LTL-problem):

Vl ((NOT (EQL 1 null)) =>

(3z (MEMBER z 1) 1\ (Vy (MEMBER y 1) => (< z y))))

which defines MIN (minimum) of elements of l. For all u of the type NAT, (LTL u 1) holds only if (< u (MIN 1)).

Definition 3. Z. 2.:

Let C be a unary predicate. We call a formula SDc with the free-variable x, suchthat (C(x) <:=:> SDc(x)) holds for any x, a sema.ntic definition of a condition C(x).

Exa.mple 3.2.2.: Vy (C1(y) => C2(x,y)). where C1, C2 are two known predicates, is a semantic definition of C such that C(x) iti Vy C1(y) => C2(x,y).

Definition 3. 2. 3.:

C is a Trivial Condition if its semantic negation does not con­ tain existential quantifiers . If this is not true, C is called a Non-trivial Condition.

Exa.mple 3.2.3. : (MEMBER a 1) is a Trivial Condition because its semantic negation is Vx (MEMBER x 1) => (-;. x a).

The predicate LTL: NATxLIST-of-NAT-+BOOL the semantic definition of which is (LTL x 1) iff

[Vy ((MEMBER y 1) => (< x y))] is Non-trivial Condition. By analogy, (PRIME x) iff

Vy ((y<x) 1\ (y divides x) => (y = 1)) is a Non-trivial Condi­ tion.

When C is tdvial, it can either be replaced by a simpler con­ dition, or its evaluation is trivial. It can therefore be used as a predicate in the conditional part of a recursive definition. When C is not trivial, since it has the V-property, we shall first try to synthetize a corresponding rf!C· Then, rf!c will help us to simplify the condition C and expllcit, if necessary, some parts of ~ (see -n).

Exa.mple 3.2.4.: Let us suppose that we want to prove Vl 31' (PERMUT 1' 1) 1\ (ORDERED 1'). We can see that ORDERED in -n is detl.ned with the help of LTL, which has the V-property. This is why, hefore starting the proof, we need to synthetise rp correspondig to the theorem

Vl {{NOT (EQL 1 null)) =>

(3z (MEMBER z 1) 1\ (Vy (MEMBER y 1) => (< z y))))). (The application of this can be found in -n.)

One should realize that there is no general strategy for proving theorems of the type Vx ... ::Jy ... Vz .... To see this try proving the weU-known relative-prime-number problern (see in (g02]) :

where RP(p,q) me<~.ns that p and q are relative prime. This is why in our system we have some heuristics in order to solve some simple such problems.

CONCLUSION

We have shown that the CM-procedure is used when we want "constructively" to prove a given theorem. It means that CM is the strategy used to orient our deduction when proving a given theorem from given axioms A1, ... , A.l, .

Beth proposed a solution to the problern of tinding whether or not some formula V is a logical consequence of formulae A 1 , ... , A.l,. His solution is the method of semantic tableaux (b03), formalized by his Completeness Theorem for a system of Natural Deduction F. As Beth bimself pointed out, the practical lnterest of bis method is seriously impaired by complicated splittings of a tableau into subtableaux. By a modltl.catlon of Beth's method of semantic tableaux inspired by the CM-strategy, we have obtained a method for inductive theorem proving.

Our modification consists in

- including the structural induction principle in the set of rules for the construction of tableaux relative to STand

- crienting a development of tableaux (by CM-strategy) tow<~.rds the destred goal.

We do not give here our moditl.cation of Beth's method.

Our approach is currently under implementatlon, but has not been yet completed. Its main ditiiculty is due to the gen­ eralizations which will be left to the user in this first version.

The efficency of our methodology depends on the truth of our conjecture relative to sequence of theorems generated by the recursively gener<~.ted EXPRl' and EXPR2' (see section 1). Jt may be that an elaborate strategy is needed in order to put this sequence in such a form that its generalization appears at once.

ACKNOWLEDGEMENTS

I would ltke to express my warmest thanks to Yves Kodratofi. I also thaak Professor Georg Kreisel for his encouragement. Professor Jean-Luc Remy provided many helpful remarks.

APPENDIX I

We give here only the !ist of axioms explicitly used in the paper.

TYPE NAT- .given by Constructors: 0: -+ NAT and Suc: NAT -+ NAT Selectors: Pred: NAT-+ NAT Predicates: zero?: NAT-+ BOOL and Suc?: NAT .... BOOL.

TYPE LIST-of-NAT- given by

Constructors: null: -+ LIST, unit: NAT .... LIST and append: LIST x LIST --+ LIST

Selectors: CAR: IJST -+NAT and CDR: LIST-+ LIST

Predicates: null?: LIST ... BOOL, unit?: LIST-+ BOOL, append?: LIST-+ BOOL

Relations a.nd Functioas:

EQL : LIST x LIST -+ BOOL

MEMBER: NAT x LIST -+ BOOL

LTI.. : Nl\T x LIST ..... BOOL -defined by (ALB) (LTL x null) (AL9) (LTL X (unit y)) 1\ (= x y) (ALlO) {LTI.. X (unit y)) A. (<X y) (AL11) (LTL X (appenJ. (unit y) 1)) 1\ ( = x y) "' (LTI.. x 1) (AL12) {LTI.. x (append (unit y) !)) 1\ ( < x y) rh (LTI.. x !) ORDERED : LIST ... BOOL (AL13) (ORDERED null) (AL14) (ORDERED (UNIT x)) (AL15) (ORDERED (append (UNIT x) !)) 1\ (LTI.. X 1) 1\ (ORDERED 1) (AL16) {ORDERED (append (UNIT x) (append (UNIT y) !))) 1\ (= x y) 1\ {ORDERED {append {UNITy) !)) (ALl?) {ORDERED {append (UNIT x) (apl'end (UNIT y) !))) 1\ ( < x y) 1\ {ORDERED (append (UNIT y) !)) DELETE: NAT x I.JST ... LIST PERMUT: LIST x I.JST .... BOOL defined by {AL23) (PERMUT null null) (AL24) {PERMUT(unit x) (unit y)),.. (= x y) (AL25) (PERMUT (ap~nd (unit x) (unit y)) (append (unit y) (unit x))) (AL26) (PERMUT (append (unit x) 1) {append (unit y) m)) ,.. ( = x y) 1\ (PERMUT 1 m) (AL27) (PERMUT {append (unit x) 1) (append (unit y) m)) 1\ (-;. x y) 1\ (MEMBER y !) 1\ (PERMUT (DELETE y (append (unit x) !)) m)

APPENDIX II

This appendix is for the automatte programming oriented reader, and is readable only if the section 3. has already been understood.

We try to present, here, the CM-procedure as it appears in our approach to automatic programming.

Let Q, rep be as described in section 3. Let the part of the definition of a predicate R with regard to x represented by rep be as follows:

R( x) holds if

! x=repi\R(srep 1')AP1'(! 1'(rep)) x=repi\R(srep2')AP2'(! 2'(rep)) x=repi\R(srepl: ')1\?1: '(Ii: '(rep)).

Let us suppose, that we want to prove a special theorem of the form YxA(x) which is Yx :=lz Q(x,z) 1\ R(z) .

lf x is represented by rep, then to find z such that Q(x,z) ,..R(z) holds means:

Take an abstract representative ~ of all x2 for which Q(rep,x2)AR(x2) holds . 'rhen with the Information included in axioms, induction hypotheses , rules, .. . , try to explicite this element . How can it be done?

The definition of Q Ieads us to consider m cases for the Q(rep,Ü part of the formula Q(rep, O/\R(~) :

Q(srepJ,f{(O) 1\ PJ(!Hrep).f~W) (j=l, .. .,m) .

Naturally, we have at our d.isposal the induction hyPothesis 3z 1 Q(srep 1 ,z 1 ),..R(z 1 ), resp. Yhp 3z 1 Q(srep 1 ,z 1 )AR(z 1 ),

therefore /{ (Ü can be replaced by z1, and so we have:

Q(rep,G1(zJofsW)) holds

on!y if P1(!Hrep).JHm is satisfied.

Then we Iook at the definition of R and we Iook for a line, say the i-th, where srep1' and f{W are the "same". Because of the lnductlon hypothesis R(srep, ') can be rep1aced by R(z 1 ), and therefore the condition P."(/1'(0) tagether with P 1 (J~(rep)./~W) will help us explicite the f1W part as a function expression depending only on x, or z1. Let z/(x) be this explicitly expressed f~W . Let us note that P 1 (!Hrep),f~(ÜI\P1 ' (!1 'W) cannot be veritied as was the case for the preceeding tyPe of theorems, but it may be reduced to the condition Cj(/Hrep),z{'(x)). Then, naturally, tinding z, for x represented by rep, wil foliow the scheme:

!f 0UHx),z/(x)) holds then z is a1(z1 .z/(x)).

l!beample :

L-et us try to prove Yx ::Jz (PERMUT x z) 1\ (ÖRDERED z) for x represented by (.append (un!t a) 1) (i.e. to find apart of a program SORT when (append? x) is satisfied) .

Then the structur.al induction principle gives the following induction hypotheses: (H1) (PERMUT lv1),.. (ORDERED lv 1) (H2) Yhp 3v9" (PERMUT (delete hp (append (unit a) l)) vQI') "'(ORDERED v9") ,.. (MEMBER hp (append (unit a) 1)). Due to a lack of space, we will only consider the 1-st line of the detinition of PERMUT (see section 3.). Let ~ be a symbol denoting an element for which (PERMUT x Ü 1\ (ORDERED 0 is satisfied. The tirst line of PERMUT indicates, that for the given representation of x, (PERMUT x 0 holds only if (PERMUT 1 (CDR 0) 1\ (a = {CAR Ü) is satisfied. By (H1), (CDR 0 can be replaced by v 1. We obtain: (PERMUT x (.append (CAR ü v 1)) holds only if ( PERMUT lv I) " ( a = ( CAR m is satisfied, i.e. (PERMUT x (.append (CAR Ü v 1)) holds only if (a = (CAR 0) is satisfied. Now we look at the definition of ORDERED, and, with regard to (H1) , we find that (ORDERED (append (CAR 0 v 1)) holds only if (LTL (CAR t) v 1) is satisfied. We obtain, therefore: (PERMUT x ( append ( CAR ü v 1)) 1\ ( ORDERED ( append ( CAR Ü v 1)) holds, only if (.a = (CAR Ü) 1\ (LTL (CAR ~) v 1) is satisfied. The condition (a = (CAR Ü) gives (PERMUT x (.append (CAR Ü v 1)) "'{ORDERED (append (CAR ü v 1)) holds, only !f (LTI.. a v 1) . Now, we can change this condition (see section 3.2.) to (< a {MIN v1)) . Because v 1 is (SORT {CDR x)) we obtain the following part of the program SORT: if (append? x) then 1f (CAR x) < (MIN (SORT (CDR x))) then (appena (CAR x) (SORT (CDR x))).