A Lemma Driven Automatic Theorem Prover for Recursive Function Theory

1. Choosing an Appropriate Principle

For soundness, all of the induction hypotheses supplied must be instances of the theorem being proved, and, in the Generalized Principle of Induction [10), all the instances assumed must result from instantiating some n-tuple of variables in the conclusion with n-tuples of terms that are smaller (under the conditions governing the induction step) than the variable n­

tuple in some well-founded paritial order. The trick, then, to finding an appropriate induction for a conjecture is to find a well-founded partial order on n-tuples and an n-tuple of variables in t.he conjecture, such that if one were to open up some of the function calls in the conjecture one would find subexpressions occurring that could be obtained by instantiating the conjecture itself with smaller n-tuples chosen from the ordering. Thus, one is lead naturally to the question: "What are some plausible well-founded orderings on n­ tuples of variables that a given recursive function descends through in its recursion?"

To answer this question, our system imposes a basic responsibility upon the user to assume or to prove certain lemmas that we term "measure lemmas". Measure lemmas state that certain t .erms are less than other terms under well­ founded orderings such as LESSP (on the non­ negative integers.) Our induction facility then uses such lemmas at the time a recursive function is defined to determine some induction principles appropriate to that function. Of course, this induction mechanism is capable of examining all subset of arguments to find appropriate principles. It also recognizes lexicographic orderings induced by existing orderings and chains together measure lemmas using transitivity (for example, to derive that (SUB1 (SUB1 x)) is less than x from the fact

that (SUB1 x) is less than x.)

As an example of the use of such "measure lemmas" consider "big number" arithmetic. The problem is to represent and manipulate (in our case, add) integers that are larger than the word size of the host machine. The obvious solution is to represent them as sequences of digits in some chosen base, and to add them with the algorithm we all learned in the third grade. Two examples of the use of that (or similar) algorithms in computing are the "big number" arithmetic of

MACLISP (where the base is 2 36 ) and the binary representation of integers on most machines (where the base is 2).

To state and prove the correctness of a big number addition algorithm one must define the mappings from integers to big numbers and back. Consider the first: To convert an integer i to a big number in base base, if i is less than base, then write down the digit i and stop, otherwise divide i by base, write down the remainder as the least significant digit, and obtain the more significant digits by (recursively) converting the quotient to a big number in base base. This algorithm is embodied in the function POWER.REP (for "power series representation") in Appendix A, where big numbers are represented as lists of integers with least significant digit in the CAR.

Note that the algorithm above recurses on the quotient of i divided by base. What is the measure lemma that justifies this recursion (or, analogously, the induction necessary to unwind it)? It is:

That is, the QUOTIENT of i divided by j is less than i if i is not 0, and j is neither 0 nor 1 (actually, in our untyped language, arithmetic on non-integers is legal and a.ll non­ integers are treated as though they were 1, thus (SUB1 j) ~ 0 is stronger than j ~ 1; it implies that j is neither 1 nor a non-number).

Thus, if one wanted to prove by induction a theorem of the form P((POWER.REP i base)), and one were cognizant of the above lemma, a plausible induction to perform would be:

Note that the induction hypothesis is an instance of the theorem being proved, that the instantiation takes the tuple <i> into the smaller tuple <(QUOTIENT i base)>, according to the above measure lemma, and that the term (POWER.REP (QUOTIENT i base) base) appearing in the hypothesis will reappear when we open up the conclusion. Finally, observe that by employing proved measure lemmas we not only allow the theorem prover to be extended but we insure that it is done soundly. (Our first attempt to state the induction principle for QUOTIENT left out the j 'I 1 case and would have produced unsound inductions had it been either explicitly assumed or wired into the theorem prover program.)

The system has proved the measure lemma above. The proof involves a similar induction by DIFFERENCE (note in Appendix A how QUOTIENT itself recurses) which in turn was justified by a (proved) measure lemma stating that i-j is less than i under certain conditions. Once the QUOTIENT measure lemma has been proved the system, in accepting the definition of POWER.REP, will pre-process it to discover the plausible induction scheme above. That scheme is precisely the one the system uses to prove that the mapping back from big numbers to integers (POWER.EVAL in Appendix A) is the

"inverse" (modulo non-numbers) of POWER.REP:

(EQUAL (POWER.EVAL (POWER.REP i base) base)

(IF (NUMBERP i) i 1)).

The above lemma is crucial to the system's proof that a big number addition algorithm (BIG.PLUS in Appendix A) is correct:

(EQUAL (POWER.EVAL (BIG.PLUS (POWER.REP i base) (POWER.REP j base)

0 base)

consider:

base) (PLUS i j)).

As a second example of a measure lemma,

i < max -> max-(ADD1 i) < max -i

This lemma informs the system that it is sound to induct up by ADD1 to a maximum (e.g., that to prove P(x,y) inductively one may prove it when -ex < y) (base case) and prove it when (x < y) assuming P(x+1,y)). In this ordering, <x+1,y> is less than <x,y>. This induction would be appropriate for a function which counted up.

2. Choosing ~Bight Instances

If one has a well-founded order on n­ tuples then it can trivially be extended to a well­ founded order on n+k-tuples, where the last k elements are simply irrelevant. Thus, once the system has found a plausible well-ordering that accounts for how n of the arguments change in recursion, it is free to throw in the remaining k arguments and let them change arbitrarily. One example of this occurs in the compiler proof. Recall that CODEGEN has two arguments, FORM and INS, and that during recursion it changes FORM by digging out one of its sub-expressions. However, while in one of its recursive calls INS (the instructions thus far laid down) is unchanged, in the other call INS is arbitrarily larger. This is acceptable since the behavior on FORM induces a well-founded order. Thus, the system knows that in a conjecture involving (CODEGEN form ins) an induction on the structure of form leaves it free to choose any instantiation it wants for ins. (For an example of such a choice in a simpler situation see Appendix B.) However, in a conjecture involving (CODEGEN form NIL) (where the INS argument is not a free variable) the system still knows it is sound to induct on form.

We originally tried to avoid such a deep and lemma driven analysis of the well-founded orderings used by functions by using subgoal induction [16], where, provided one assumes a function terminates, one can use the conditional structure of the function plus its recursive calls to define a well-founded order on the n-tuple of all of its arguments. However we found that in many theorems it was crucial to be able to induct on some subset of the arguments (knowing that they alone were sufficient to define an ordering) and that the conditional structure of most functions unnecessarily clutters inductions (which may seem like a mere inconvenience but often sets up too­ restricted subgoals for subsequent inductions).

V REMARKS

We would like to reiterate that this paper reports work in progress (both on the features of our theory and the proof techniques). While the current system is clearly not yet suitable as the theorem prover for practical program analysis, we are encouraged by our success at extending the theory of the our earlier LISP theorem prover without loss of proof-power. We believe we will be able to develop the system into a useful tool.

Appendix A FUNCTION DEFINITIONS

Here we present the definitions of the functions involved in the optimizing compiler proof, the big number discussion, and the proof in Appendix B. Several axiomatically specified primitives are used. (NUMBERP x) is TRUE if x is a number and FALSE otherwise. (LISTP x) is TRUE if x is a CONS and FALSE otherwise. (PUSH x pds) returns a stack with x pushed onto pds. (TOP pds) returns the top-most element of a stack, and (POP pds) returns the popped stack. GETVALUE and APPLY are undefined (but APPLY is axiomatically specified to be numeric - a fact crucial to CORRECTNESS.OF.OPTIMIZE).

(APPEND (LAMBDA (X Y) (IF (LISTP X) (C·)NS (CAR X) (APPEND (CDR X) Y)) Y))) (BIG.PLUS (LAMBDA (X Y I BASE) (IF (LISTP X) (IF (LISTP Y) (CONS (REMAINDER (PLUS I (PLUS (CAR X) (CARY))) BASE) (BIG.PLUS (CDR X) (CDR Y) (QUOTIENT (PLUS I (PLUS (CAR X) (CAR Y))) BASE) BASE)) (BIG.PLUS1 X I BASE)) (BIG.PLUS1 Y I BASE)))) (BIG.PLUS1 (LAMBDA (L I BASE) (IF (LISTP L) (IF (EQUAL I 0) L (CONS (REMAINDER (PLUS (CAR L) I) BASE) (BIG.PLUS1 (CDR L) (CONS I NIL)))) (CODEGEN (QUOTIENT (PLUS (CAR L) I) BASE) BASE))) (LAMBDA (FORM INS) (IF (LISTP FORM) (CONS (CAR FORM) (CODEGEN (CAR (CDR (CDR FORM))) (CODEGEN (CAR (CDR FORM)) INS))) (IF (NUMBERP FORM) (CONS (CONS (QUOTE PUSH!) (CONS FORM NIL)) INS) (CONS (CONS (QUOTE PUSHY) (CONS FORM NIL)) INS)))))

(COMPILE (LAMBDA (FORM) (REVERSE (CODEGEN (OPTIMIZE FORM) NIL)))) (DIFFERENCE (EXEC (LAMBDA (I J) (IF (EQUAL I 0) 0 (IF (EQUAL J 0) (IF (NUMBERP I) I 1) (DIFFERENCE (SUB1 I) (SUB1 J)))))) (LAMBDA (PC PDS ENVRN) (IF (LISTP PC) (IF (LISTP (CAR PC)) (IF (EQUAL (CAR (CAR PC)) (QUOTE PUSH!)) (EXEC (CDR PC) (PUSH (CAR (CDR (CAR PC))) PDS) ENVRN) (EXEC (CDR PC) (PUSH (GETVALUE (CAR (CDR (CAR PC))) ENVRN) PDS) ENVRN)) (EXEC (CDR PC) (PUSH (APPLY (CAR PC) (TOP (POP PDS)) (TOP PDS)) (POP (POP PDS))) ENVRN)) PDS))) (EVAL (LAMBDA (FORM ENVRN) (IF (LISTP FORM) (APPLY (CAR FORM) (EVAL (CAR (CDR FORM)) ENVRN) (EVAL (CAR (CDR (CDR FORM))) ENVRN)) (IF (NUMBERP FORM) FORM (GETVALUE FORM ENVRN))))) (FLATTEN (LAMBDA (X) (FORMP (IF (LISTP X) (APPEND (FLATTEN (CAR X)) (FLATTEN (CDR X))) (CONS X NIL)))) (LAMBDA (X) (IF (LISTP X) (IF (LISTP (CAR X)) FALSE (IF (LISTP (CDR X)) TRUE))) (IF (LISTP (CDR (CDR X))) (IF (FORMP (CAR (CDR X))) · (FORMP (CAR (CDR (CDR X)))) FALSE) FALSE) FALSE)) (LESSP (LAMBDA (X Y) (IF (EQUAL X 0) (LESSP (SUB1 X) (SUB1 Y)))))) (MC.FLATTEN (LAMBDA (X Y) (IF (LISTP X) (MC.FLATTEN (CAR X) (MC.FLATTEN (CDR X) Y)) (CONS X Y)))) (OPTIMIZE (LAMBDA (FORM) (IF (LISTP FORM) (IF (NUMBERP (OPTIMIZE (CAR (CDR FORM)))) (IF (NUMBERP (OPTIMIZE (CAR (CDR (CDR FORM))))) (APPLY (CAR FORM) (OPTIMIZE (CAR (CDR FORM))) (OPTIMIZE (CAR (CDR (CDR FORM))))) (CONS (CAR FORM) (CONS (OPTIMIZE (CAR (CDR FORM))) (CONS (OPTIMIZE (CAR (CDR (CDR FORM)))) NIL)))) (CONS (CAR FORM) (CONS (OPTIMIZE (CAR (CDR FORM))) (CONS (OPTIMIZE (CAR (CDR (CDR FORM)))) NIL)))) FORM))) (PLUS (LAMBDA (I J) (IF (EQUAL 1 0) (IF (NUMBERP J) J 1) (ADD1 (PLUS (SUB1 I) J))))) (POWER.EVAL (LAMBDA (L BASE) (IF (LISTP L) (PLUS (CAR L) (TIMES BASE 0))) (POWER.REP (LAMBDA (I BASE) (IF (EQUAL I 0) NIL (IF (EQUAL BASE 0) (CONS I NIL) (IF (NUMBERP BASE) (IF (EQUAL BASE 1) (CONS I NIL) (POWER.EVAL (CDR L) BASE))) (CONS (REMAINDER I BASE) (POWER.REP (QUOTIENT I BASE) BASE))) (CONS I NIL)))))) (QUOTIENT (LAMBDA (I J) (IF (EQUAL J 0) 0 (IF (EQUAL Y 0) (IF (EQUAL Y 0) FALSE FALSE TRUE) (IF (LESSP I J) 0 (ADD1 (QUOTIENT (DIFFERENCE I J) J)))))) Theorem Proving-1: Boyer

(REMAINDER (LAMBDA (I J) (IF (EQUAL J 0) (IF (NUMBERP I) I 1) (IF (LESSP I J) (IF (NUMBERP I) I 1) (REMAINDER (DIFFERENCE I J) J))))) (REVERSE (LAMBDA (X) (IF (LISTP X) (APPEND (REVERSE (CDR X)) (CONS (CAR X) NIL)) NIL))) (TIMES (LAMBDA (I J) (IF (EQUAL I 0) 0 (PLUS J (TIMES (SUB1 I) J))))) Appendix B THE FLATTEN.MC.FLATTEN THEOREM This Appendix contains the machine's output during its proof of a relationship between two different tree flattening functions, FLATTEN and MC.FLATTEN (see Appendix A). The purpose is two­ fold: To illustrate in 2 pages the theorem prover performing an induction similar to that done for CORRECTNESS.OF.CODEGEN (which takes 11 pages), and to exhibit the theorem prover's output. PROOF OF THE "FLATTEN.MC.FLATTEN" LEMMA The conjecture to be proved is: (EQUAL (MC.FLATTEN X Y) (APPEND (FLATTEN X) Y)) Simplification produces: *i. (EQUAL (MC.FLATTEN X Y) (APPEND (FLATTEN X) Y)). Give this the name ·1. We'll try to prove it by induction. There are 2 plausible inductions. These merge into one likely candidate induction. Induct on X (instantiating Y). This induction is justified by the CAR.LESSP and CDR.LESSP inequalities. We must now prove the following 2 goals: *1.i. (IMPLIES (NOT (LISTP X)) (EQUAL (MC.FLATTEN X Y) (APPEND (FLATTEN X) Y))) and (EQUAL (MC.FLATTEN (CDR X) Y) (APPEND (FLATTEN (CDR X)) Y)) (EQUAL (MC.FLATTEN (CAR X) (MC.FLATTEN (CDR X) Y)) (APPEND (FLATTEN (CAR X)) (MC.FLATTEN (CDR X) Y)))) (EQUAL (MC.FLATTEN X Y) (APPEND (FLATTEN X) Y))). Simplification produces: *1.iii. (IMPLIES (AND (LISTP X) (EQUAL (MC.FLATTEN (CDR X) Y) (APPEND (FLATTEN (CDR X)) Y)) (EQUAL (MC.FLATTEN (CAR X) (MC.FLATTEN (CDR X) Y)) (APPEND (FLATTEN (CAR X)) (MC.FLATTEN (CDR X) Y)))) (EQUAL (MC.FLATTEN (CAr X) (MC.FLATTEN (CDR X) Y)) (APPEND (APPEND (FLATTEN (CAR X)) (FLATTEN (CDR X))) Y))). Apply the lemma ASSOCIATIVITY.OF.APPEND to *1.iii. This produces: *1.iv. (IMPLIES (AND (LISTP X) (EQUAL (MC.FLATTEN (CDR X) Y) (APPEND (FLATTEN (CDR X)) Y)) (EQUAL (EQUAL (MC.FLATTEN (CAR X) (MC.FLATTEN (CDR X) Y)) (APPEND (FLATTEN (CAR X)) (MC.FLATTEN (CDR X) Y)))) (MC.FLATTEN (CAR X) (MC.FLATTEN (CDR X) Y)) (APPEND (FLATTEN (CAR X)) (APPEND (FLATTEN (CDR X)) Y)))) Cross fertilize (MC.FLATTEN (CDR X) Y) for (APPEND (FLATTEN (CDR X)) Y) in *1.iv, and throw away the equality. This produces: TRUE. That finishes the proof of *1. Q.E.D. Load average during proof: .4605102 Elapsed time: 5.377 seconds CPU time: 4.159 seconds CONSes consumed: 4926 *1.ii. (IMPLIES (AND (LISTP X)

All of the commentary in the above proof was mechanically produced by the theorem prover in response to the user command to prove (EQUAL (MC.FLATTEN X Y) (APPEND (FLATTEN X) Y)). Several additional comments are in order.

The base case of the induction argument is formula *1.i and the induction step is *1.ii. Note that in both cases the conclusions are the same (namely the theorem to be proved) and that in *1.ii the two induction hypotheses are instances of the theorem to be proved. One sends the tuple <X,Y> into <(CDR X),Y> and the other sends <X,Y> into <(CAR X),(MC.FLATTEN (CDR X) Y)>, both of which are smaller than <X,Y> according to the measure that compares only the first elements and uses the traditional ordering on list structures. The instantiation picked for Y in the second hypothesis was chosen because such a term would reappear when the conclusion was opened up.

Formula *1.i simplifies to TRUE and is thus proved. Formula *1.ii simplifies to *1.iii, which is proved by re-associating one of the APPEND terms (to produce *i.iv) and then doing a "cross­ fertilization." (The result of "cross-fertilizing y for x in (IMPLIES (EQUAL x y) Q)" is Q with some occurrences of x replaced by y.)

If the associativity of APPEND had not been previously proved, the theorem prover would have automatically produced it (from *1.iv, by two cross-fertilizations, a generalization, and an elimination of an irrelevant hypothesis) and then proved it by induction.