Strategies for Mechanizing Structural Induction

Introduction

In general, proving properties of programs re­ quires an inductive argument of one sort or other. Structural induction is used in this theorem prov­ ing system for automating mildly complex proofs about programs written in a simple programming language without loops or assignments.

Theorem provers using such a me·thod were writ­ ten by Brotz (1974) for number theory and Boyer and Moore (1975) for a theory of lists (see also Moore (1973) and Moore (1975)). The latter was applied to proving properties of programs writ­ ten in a LISP-like language. The present system is an improvement over these previous works by its typed language and it more sophisticated use of induction.

1 Present address: Department of Computer Science, Concordia University, 1455 ouest, boul. de Maisonneuve, Montreal, Quebec, H3C 1M8, Canada.

After an overview of the formal system and the search strategy, the paper explains how induction variables are selected, which includes generali­ zation, and how induction subgoals are generated. Finally, other strategies are presented, includ­ ing simplification. A detailed example and technical remarks constitute the appendices. Aubin (1974) describes the whole system in detail.

Formal System

The formal system can be thought of as a gen­ eralization of number theory, but with implicit outermost universal quantifiers only.

Every term, that is, every variable and func­ tion application, has a type. Types and con­ structor constants are hierarchically introduced. For example,

[true: I false:] + bool [zero: I succ:nat] +nat [nil: I cons:nat,list] +list [atom:nat I consx:sexpr,sexpr] + sexpr [nulltree: I tip:natl node: tree,nat,tree] + tree

Variables are simply declared. Finally, de­ fined function constants are introduced by stages with the help of definitions by cases (Burstall 1969, Hoare 1976). Here are some concrete ex­ amples:

a=>b I bool <= cases a [true <= b I false <= true] a&b I bool <= (a=> (b=>false))=>false m=n I bool <= cases m [zero <= cases n [zero <= true I succ(n) <=false] I succ(m) <=cases n [zero<= false I succ(n <= m=n]]

They introduce the function constants of implica­ tion, conjunction, and equality for terms of type nat. The computer program uses another concrete representation for type and function definitions as can be seen in Appendix 1.

The inference rules are those of (1) truth,(2) specialization,(3) definition by k-recursion,(4) modus ponens, (5) substitutivity of equality,

and (5) induction.

The domain of interpretation is a many-sorted word algebra generated by the empty set. A lexi­ cographic ordering is defined over the domain so that the principle of structural induction holds in it. An interpretation is given for the lang­ uage which leads to a proof of soundness and weak completeness. In particular, the meaning of a function constant defined by cases is a well-de­

fined k-recursive function.

This primitive system is raised by introducing more connectives (or, not, cond) and by deriving some inference rules. Terms are put in normal form by means of rules inspired from Ketonen's dialect of Gentzen's sequent calculus (1955). A thorough description of the formal system can be found in Aubin (1976) .

Search Strategy

Proving theorems can be seen as a game: the formal system sets the rules besides which we have a strategy of play. This strategy must meet three criteria: (1) it must follow the rules of the same (a question of soundness), (2) it must be a winn­ ing strategy (a question of completeness), and (3) it must use a tolerable amount of resources (a question of efficiency).

The search strategy of the present theorem prover works backward, reducing the original goal to subgoals, which are in turn reduced to further subgoals,etc. A solution is found when there is no more subgoals to achieve. A procedure to re­ duce a goal to subgoals is called a tactic (Gordon, Milner, and Wadsworth 1977).

A necessary and sufficient condition of sound­ ness of this strategy is that it never reduces a nonachievable goal to only achievable subgoals. This is fulfilled if the tactics are inverses of valid inference rules, primitive or derived. In particular, the tactic corresponding to the rule of truth reduces the goal true() to no further subgoals. Soundness means that when a solution is found, a proof is indeed found.

A necessary condition of completeness can be seen as the converse of the previous condition: an achievable goal must not be reduced to nonachiev­ able subgoals. This is always fulfilled by tac­ tics corresponding to rules which are actually in­ vertible, either in general or in some context. As for tactics not bound to invertible rules, the theorem prover tries to find counter examples to the subgoals they generate: if it succeeds, the condition is not met and the subgoals, rejected; if it fails, we cannot tell for sure that the con­ dition is satisfied, but we have some ground to believe that it is, and the subgoals are retained.

Finding sufficient conditions for completeness is the main problem of theorem proving and the re­ maining sections of this paper will describe my contribution in this direction.

The preceding points lead to considering the utilization of resources. A source of efficiency in the present prover is the fact that no back­ tracking takes place, that is, at each stage, only one way of reducing a goal is irretrievably taken. So, it is sufficient to keep a simple stack of goals : the original goal is pushed down onto it, each tactic reduces the goal on top, pops up the stack, and pushes down the new subgoals onto it. But above this structure, the choice and use of tactics have a greater bearing on efficiency. This prover uses the following tactics in turn, until the goal stack is empty:

1. Simplification (inverse of a derived rule of substitutivity of equality and rule of definition by k-recursion)
2. Splitting (inverse of a derived rule of conjunction: from t and s, infer t&s)
3. Replacement (inverse of a derived rule of substitutivity) and strengthening (in­ verse of a derived rule of weakenin~: from t, infer s=>t)
4. Contraction (inverse of a derived r.ule of substitutivity)
5. Truth (inverse of the rule of truth)
6. Generalization (inverse of the speciali­ zation rule) , induction (inverse of the induction rule), and strengthening.

The search is aborted if. the current goal can­ not be reduced by any tactic, e.g., the goal false().

Induction Variables and Generalization

The induction tactic has been divided into two distinct parts: (1) the selection of a list of variables to induce upon and (2) the generation of the induction subgoals, given these induction variables. This section treats the first aspect. Actually, I submit that se lection of induction variables and generalization are intrinsically linked together; so, both will be studied in this section.

Boyer and Moore (1975) first put in evidence the fact that only recursion variables were suit­ able candidates as induction variables. I will further constrain their fundamental idea by focusing on certain recursion terms of particular importance. (A recursion term is a term which occurs in the argument position of a case var­ iable.) If we allow ourselves to talk of (sym­ bolic) evaluation regarding the application of k­ recursive definitions, we may as well talk of computation rule. A computation rule tells us which subterm of a term to apply the k-recursion definition rule to. Nothing can be gained from a completeness point of view by introducing this notion, but it can lead to improved efficiency.

The call-by-need computation rule is known to be optimal for recursion equations (Vuillemin 1973) and can usefully be applied to our problem. The starting point is quite simple. What do we need to know about a function application in order to be able to apply the k-recursive definition rule to it? We need to know the values of its recur­ sion terms, if it has any. The interesting point is that if we apply the call-by-need line of reasoning to an induction goal which has already been simplified, the process will be stopped by one or more variables marking argument positions which the call-by-need evaluator must have more information about: I submit that these variable occurrences constitute excellent candidates for doing induction upon. I call them primary var­ iable occurrences.

A simple example can helpfully illustrate this. Take the goal:

(j <>k) <>l=j <> (k<>l).

The infix function constant <> denotes the funct­ ion which appends two lists and is defined thus:

k<>l I list <= cases k [nil <= 1 I cons(n,k) <= cons(n,k<>l)].

we start the chain of reasoning witp the func­ tion constant =; both of its arguments are recur­ sion arguments. So, we need to evaluate both of them before trying to apply the definition of =. We iterate the process: to know about (j <>k) <>l, we must know about j <>k, and to know about j <>k, we must know about j. But we know nothing about j; so, this primary occurrence of j makes a good induction candidate. On the right of the equal­ ity, to evaluate j <> (k<>l), we must know about j again. So, this variable is undoubtedly the in­ duction variable to choose according to this technique. Note its directedness: k and 1 are never considered. And indeed, this theorem is proved automatically in one induction on (j).

The efficiency of this approach is put in evidence if we replace by cons(n,j) as would be done in the generation of an induction conclusion. Primary variable occurrences are the only ones which, once replaced by structures, allow evalua­ tion to be eventually applicable to the whole goal (try with k and 1).

The interesting fact about this approach to in­ duction variable selection is that generalization can be integrated to it in a natural way. Which term occurrences in the goal can we consider as better candidates for induction than the primary variables? The answer is simple: the term occurr­ ences leading to them by the call-by-need evalua­ tion, or in other words, the term occurrences in which the primary variable occurrences appear. I call these primary term occurrences, including the primary variable occurrences.

The strong relation between selection of in­ duction variables and generalization is theoreti­ cally supported by Prawitz's results (1971).

Here is an example with the same flavour as the previous one (the function constant rev denotes

the reverse function on lists) :

(rev(j) <>k) <>l=rev(j) <> (k<>l).

We do as before except that for each term occurr­ ence considered by the call-by-need evaluator, we ask the question: can this occurrence (may be to­ gether with others) be generalized? This is answered negatively or positively according to whether the prover can or cannot find a counter­ example to the generalized subgoal. In this ex­ ample, the answers are negative until we get to rev(j): if we replace both occurrences of it by a variable, the new subgoal is still achievable (it is actually the same as in the previous ex­ ample) . The new variable is chosen to be the induction variable.

The advantage of this purposeful generaliza­ tion is that we can meaningfully generalize only certain occurrences of a term and in particular of a variable. For example, with:

we find that the first and the fourth occurr­ ences of are primary occurrences. We try to generalize them to a new variable which success­ fully yields:

This subgoal can be proved in one induction on (k).

Note two points: (1) a search mechanism for counter-examples is essential to such a generali­ zation method and (2) the approach of Brotz (1974), and Boyer and Moore (1975) to generali­ zation as separated from induction variable selection leads in this example to the nonachiev­ able subgoal k<> j=j<>k.

Some pragmatic aspects must be taken into account in the implementation of this method. In particular, since searching for counter-examples is time-consmning, we limit generalization to the cases which have a better chance of success, i.e., when the term occurrences to generalize appear on both sides of an equality or implica­ tion (Boyer and Moore 1975, Brotz 1974). In addition, the above method may propose several candidates and the system uses some tie-breaking rules to elect a unique one.

Here is an additional example of generaliza­

tion. The original goal is:

subset (k,k).

The function constant subset is defined by cases on its first argument. No generalization is possible, in the goal and induction is done on (k) · we obtain an induction subgoal for which the induction hypothesis cannot be used:

subset(k[l],k[l]) => subset(k[l],cons(n[l],k[l]ll.

The first and third occurrences of k[l] are primary apd can now be generalized to yield the subgoal:

Subset (k[2],[k]l ) =>

Subset (k[2], cons(n[l], k[l])), which is easily proved in one induction on (k[2]).

Induction Subgoal Generation

we now want to find the induction subgoals, given the list of induction variables. In parti­ cular, we need to find heuristically justified instantiations for the induction hypotheses. We may also wish to discard some hypotheses judged useless; it should be clear that this can cut down the complexity of the subgoals considerably.

In order to generate the induction subgoals, Boyer and Moore (1975) use a method which maps the structure of what they call a bomb list into the required terms. The bomb list of a goal contains information about how definitions fail to apply to the goal. In Moore's later version (1975), the corresponding mechanism is directly based on function definitions. I would argue that such techniques whereby induction subgoals are more or less directly constructed from func­ tion definitions do not constitute a sound approach. In particular, the soundness of the Boyer-Moore tactic is not provable, at least for their system.

In my tactic, the heuristic-part is separated from the nonheuristic part. On the one hand, all induction subgoals are generated on the basis of type definitions. For each of them, the con­ clusion and all the hypotheses are considered. Since checking the admissibility of type defini­ tions is straightforward, it is easy to convince oneself of the soundness of this nonheuristic part.

On the other hand, the role of the definitions of the function constants appearing in the in­ duction goal does not so beyond giving informa­ tion about the rejection, or the acceptance and instantiation of tentative induction hypo­ theses, i.e. about the heuristic part. Now, discarding an induction hypothesis from an in­ duction subgoal is sound (by the weakening rule) and preserves the achievability of the in­ duction subgoal. Moreover, instantiating an in­ duction hypothesis is justified by the induction rule.

Induction conclusions and hypotheses are act­ ually represented as substitutions involving the induction variables. By applying these substi­ tutions to the induction goal and bundling up the resulting terms with => and &, we easily ob­ tain the induction subgoals themselves.

The induction tactic first finds the conclus­ ion substitutions. For each variable, the algo­ rithm generates the structures representing all the values that can be assumed by the variable (the system can do induction from any number of bases) . Then, the conclusion substitutions are constructed by successively binding the induc­ tion variables to each of their corresponding structures.

As an example, take the induction goal ack(n,m) >zero; the induction variables (n,m) are select­

ed. The function ack is defined thus:

ack(n,m) I nat <= cases n [zero <= succ(m) succ(n) <= cases m [zero <= ack(n,succ(zero)) I succ(m) <= ack(n,ack(succ(n) ,m))]].

We set as possible substitutions for n, the closed structure zero and the open structure, say, succ(n[l]); similarly, zero and succ(m[l ] ) are associated with m. This means that there are four conclusion substitutions: (1) [zero/n] [zero/m], (2) [zero/n] [succ(m[l]) / m], (3) [succ(n[l])/n] [zero/m], and (4) [ succ(n[l]) / n ] [succ(m[l])/m].

Next, for each conclusion substitution, we have to find zero or more hypothesis substitutions, according to our lexicographic ordering.

consider any conclusion substitution. We simply have to find the immediate predecessors of the list c*(x*) of structures bound to the induction variables, that is, for all i(l<i <n), the list c[l](x[l]*) , ..· , c[i-l](x[i-1]*)-;­ x[i,j], s[i+l], ... , s[n], where x[i,j] in x[i]* has the same type as c[i](x[i]*) and s[j] (i+l~j2nl is any term.

In our examples, we get the following results :

1. No substitutions, since zero has no proper substructures .
2. [zeroj n] [m[l]/m]
3. [n[l]/n] [s[l]/m], where s[l] is any term
4. [n[l]/ n] [s[2]/ m], where s[2] is any term, and [ succ(n[l])/n] [m[l]/ m].

Function definitions come into the picture to serve two purposes: (1) to reject a hypothesis substitution if no use can be foreseen for it, and (2) to find relevant instances for the free variables. Roughly speaking, the strategy applies hypothesis and conclusion substitutions to the induction goal, simplifies the resulting terms (in particular, using function definit­ ions), and then tries to match parts of these terms: a failure counts toward rejection of the hypothesis, while a success both counts toward its retention and provides instances for the free variables.

• In the Ackermann's example, we have that:
• There is already no hypotheses
• The tentative hypothesis is discarded

since the definition of ack is not re­ cursive for this case and matching cannot

even be attempted.

1. By applying the definition of ack to the conclusion and matching, we find the in­ stance succ(zero) for the free variable
2. s[l].
3. There are two recursive calls of ack for this case; we set two matches and retain both hypotheses, letting s[2] be ack(succ(n[l]) ,m[l]l.

So, finally , the four following induction sub­ goals are generated:

1. ack(zero,zero) > zero
2. ack(zero,succ(m[l]ll > zero
3. ack(n[l],succ(zero)) > zero => ack(succ(n[l]),zero) > zero
4. ack(n[l],ack(succ(n[l]),m[l])) > zero & ack(succ(n[l]) ,m[l]) > zero => ack(succ(n[l]) ,succ(m[l])) > zero

This method is not fool proof: it will some­ times retain hypotheses which are in fact useless (as above) , and sometimes discard useful hypothe­ ses. But, in general, it errs on the safe side.

Other Strategies

Other strategies are not so much directly re­

lated to using the induction rule.

Indirect Generalization

In the following definition:

rev2a(l,k) I list <=

cases 1 [nil <= k I

cons(n,l) <= rev2a(l,cons(n,k))],

the nonrecursion argument k does not stay fixed on the right, but becomes cons(n,k). The interest of such definitions lies in the fact that for the class of problems studied, they are literal trans­ lations of iterative programs. Such nonfixed non­ recursion arguments are called accumulators (following Moore (1975)), since they can be con­

sidered ·as holding current values of computations.

Quite often, accumulators have to be general­ ized when they are not variables. For example, we should generalize nil in the goal rev2a(k,nil) =rev(k). Since it will not match cons(n[l],nil) in the simplified conclusion of an induction on (k) . However, we do not have an occurrence on both sides of =. How can we massage our goal so as to make nil recur on the right of the equality? Intuitively, if we know that l <>nil=l, we can re­ write rev(k) as rev(k) <>nil. So, the goal be­ comes rev2a(k,nil)=rev(k)<>nil, and nil occurs on both sides. What if we replace it by a new var­ iable? We get rev2a(k,l)=rev(k) <>l, which is proved easily by inducing on (k) , since 1 can now be replaced by cons(n[l],l) in the induction hy­ pothesis. Similar generalizations can be found automatically for natural numbers and lists by a method using specialization as a means of achiev­ ing generalization.

Replacement and Strengthening

These tactics are responsible for using the induction hypotheses and is an adaptation of a method already experimented with by Brotz (1974) and especially Boyer and Moore (1975) . For those members of the antecedent of a goal which are equalities, it tries to replace the right by the left-hand side, or vice-versa, in one or more members of the consequent. So, grossly speaking, it reduces s=t=>u[t/z] to s=t=>u[s/z], or vice versa. A strengthening tactic is used concurr­ ently. In effect, the antecedent members of an implication which are involved in replacement are discarded from the antecedent, i.e. s=t=>u[s/z] is reduced to u[s/ z]. This is called strenghen­ ing since it is the inverse of the weakening

rule.

These tactics are well justified and preserve achievability when they involve induction hypo­ theses, but replacement with equalities not con­ strained by induction requires a new approach.

Splitting

The prover splits conjunctions, that is, it reduces a goal of the form s&t to the subgoals s and t. This tactic preserves achievability. Brotz (1974) used it, but not Boyer and Moore

(1975).

Contraction

This tactic reduces a goal of the form f(s[l], ... ,s[n]) = f(t[l], ... ,t[n]) to s[i]=t[i], where s[j] is identical to t[j] (l<j <i-1 , i+l~j~n) and s[i] differs from t [I]~ This is actually applied to any consequent member of a term in normal form. The tactic is justified by the substitutivity of equality; however, it does not preserve achievability. A similar strategy can be found in Brotz (1974), but not in Boyer

and Moore (1975).

Simplification

This is the most important tactic besides in­ duction. The simplification problem splits into three subproblems: (1) one of logical equivalence between terms before and after simplification, (2) one of complexity measure for terms, and (3) one of selection,i.e., what to replace by what in the terms to be simplified. This last ques­ tion is perhaps the most interesting.

The method used in this prover is inspired from Vuillemin's call-by-need computation rule (1973) . Applied to simplification, the rule says: select the leftmost-outermost subterm which can be simplified (i.e. call-by-name), but take the maximum advantage of shared subterms. Because all terms have the same internal representation (a three-field record), the tactic can deal with variables and function applications indistinguish­ ably; moreover the program which applies a substi­ tution does not do undue copying. So, once a term t has been fully simplified, the resulting term s, whether it is a variable or not, is copi­ ed into the record of term t, whose boolean field is set to true. Thus any superterm which shared term t now shares its simplified equivalent s.

The second half of the selection question con­ cerns the order in which the various simplifica­ tion rules are applied on a given term. This prover tries successively (1) pure simplification rules, (2) k-recursive definitions, and (3) nor­ malization rules. The rules are further ordered within each category according to other criteria.

The gain in efficiency due especially to the sharing of structures is very important.

Conclusion

The strong points of this theorem proving sys­ tem are (1) its typed language, (2) its mechanism for selecting induction variables and generaliz­ ing, (3) its sound way of generating induction subgoals, and (4) its fast simplification algorithm.

However, its formal system is still too weak: one would like to relax the restrictions on quantification, and on type and function defini­ tions. It is also clear that the pure backward search is too limiting and the discovery of use­ ful lemmas on a reasonably large scale will re­ quire more of the user (interactively or not).

Two recent works have proposed solutions to such problems and others addressed in this paper. Cartwright's system (1976) includes axiomatically defined types constrained to denote the same do­ mains as the type constants described in this paper. Since his language is not typed (despite his claim), his induction rule is more powerful. Moreover, his system accepts all computable func­ tions. His search strategy is crucially depend­

ent on interaction with a user.

Boyer and Moore (1977) have a new and even more powerful system since their types can be de­ fined axiomatically in total freedom. It can accept any total function (then one can only con­ clude that their language is not enumerable:). The additional typing freedom increases the com­ plexity of the proofs found by their automatic search strategy, but they have the facility of specifying any useful lemmas to the prover prior to attempting a proof.

Acknowledgements

I am most grateful to my directors of studies,

Robin Milner and Rod Burstall, and also to Bob Boyer and J Moore. I was supported by the Commonwealth Scholarship Commission and the Conseil national de recherches du Canada.

Appendix 1

Compiling Algorithm for Expressions

In the concrete syntax used by the computer program, type and function definitions are input as POP-2 lists. The following simple compiling algorithm for expressions illustrates the use of such de finitions. Similar algorithms can be found in Burstall (1969); in Milner and Weyrauch (1972) and Cartwright (1976), who obtained a correctness proof interactively by machine; and in Boyer and Moore (1977) who got an automatic proof as I did. Note the presence of vacuously defined type and function constants.

We start by defining the syntax of the source language of expressions by means of type defini­ tions:

(NAME) (OPERA TOll) (EXPRESS (SI MPLE NAME ) (COMPOUND OPERhTOR EXPRESS EX~RESS) )

Written in the form used in the body of this paper, this last type definition, for example, would read: [simple:name I compound:operator,ex­ press,express] + express.

Type definitions are also used for the semant­ ic domains. States are intended to map names to numbers. Our first-order logic forces us to give a function which applies an object of type FUNCTION to two numbers. We assume that the var­ iables F, and M and N have been declared to be of type FUNCTION and NAT respectively:

[FUNCTION) [NAT (ZERO) [ SUCC NAT)) [STATE ) [[[APPLY F M N) NAT) [ ))

The following semantic functions give the meaning of the syntactic constructs; MSE can be said to be an interpreter. NM is a variable of type NAME; ST, of type STATE; OP, of type OPERA­ TOR; and E, El, and E2, of type EXPRESS:

[[[LOOKUP NM ST) NAT) [)) [[[MO OP) FUNCTION) [) ) [([MSE E ST) NAT) (CASES E [[SIMPLE NM) (LOOKUP NM ST)) [[COMPOUND OP El E2 ] [APPLY [MO 0?) [MSE El ST] [MSE E2 ST))]))

Next, "'e turn to the taraet lanauaae. Syn­ tactically, it is a set of programs which are lists of instructions. Postfixed notation is us­ ed. We also give a function to concatenate two target language programs. PR, PRl, and PR2 are variables of type PROGRAM; and IN, of type IN­

STRUCT: [INSTRUCT [OPERATE OPE-"''.TOR] ~FETCH N/.ME )]

[PI<OGRAM (.NULLPR] [ADD INS~' I!UC'f PROGI<AH) ] [[[CONCAT PRl PR2) PROGRAM) [CASES PRl [ [NULLPR] PR2 ) [[ADD IN PRl] [ADD IN (CONCAT PRl PR2] ]) ])

We define the semantic domains for the target language (pushdowns and stores) , together with selecting functions for inspecting their constit­ uents. PO is a variable of type PUSHDOWN; and STR, of type STORE:

[PUSHDOWN [EMPTY) (PUSH NAT PUSHDOWN )) (STORE. (~1KSTORE STATE PUSIJDOWN ) ) (((TOP PO) t;AT)) [CASES PO ((EMPTY) (ZERO ]) ([PUSH N PO] N))) ( [ (POP PO) PUS II DOWN) (CASES PO ((EMPTY) [EMPTY)) [[PUSH N PO) PO))) [((S~'OF' STR) STATE) (CASES STR [[MKSTORE ST PO) ST))) [[[PDOF STR) PUSIIDONN) (CASES STR [[MKSTORE ST PO] PO)))

We have two semantic functions for the target language; they can be said to execute programs:

( [[DO IN STR) STORE) [CASES IN ([FETCH NM) (MKSTORE (STOF STR) (PUSH (J.OOKUP NM [STOF STR)) [PDOF STR)))) ( [ OPERM'E OP) (~1KSTORE [STOF STR) (PUSH (APPLY [MO OP) [TOP fPOP [PnQF ~TR]]J [TOP (POOP f<TR]] J [POP (POP (PDOF STR)]JJJ)) ) (([MT PR STR) STORE) [CASES PR [[NULLPR) STR) [[ADD IN PR) (MT PR (DO IN STR))])J

Finally, the function COMP compiles an express­ ion, that is, it translates it into a program:

[ ( (COMP E) PROGRAM) (CASES E ([SI~WLE NM) [ADD (FETCH NM) (NULLPR))) ([COMPOUND OP El E2) (CONCAT [COM!' El) [CONCAT [CmW E2)

[ADD [OPERATE OP) (NULLPR)))]))) The statement of correctness of this algorithm is: [EQST [MT [COMP E) STR) [MKSTORE [STOF STR)

(PUSH [MSE E [STOF STR)) (PDOF STR))))

In other words, we get the same store if we compile an expression and execute the resulting program, given a storage, as if we interpret the expression with the state of the given store and push the result down onto the stack of the store, leaving its state unchanged.

This statement can be proved automatically by the theorem prover with the help of the lemma:

[EQST [MT [CONCAT <'Rl PR2] S'J'R) [MT PR2 [Wr PRl STRJ))

which can be proved automatically on its own.

Appendix 2

Note on Implementation and Results

The prover is implemented in POP-2. The time taken for finding a proof varies from a few sec­ onds to a few hundred seconds. This is essent­ ially dependent on the extent in which counter-ex­ amples have to be searched for. The proof of the compiling algorithm, which does not involve any generalizations, takes only 25 seconds. This prover could prove most theorems in Brotz (1974) and Boyer and Moore (1975), plus many new ones.

These theorems were proved using only a core of basic lemmas in the subtheory of booleans. How­ ever, the proofs of some of the hardest theorems, (e.g., the compiler correctness) required that equalities of other subtheories be added to the set of simplification rules before they were attempted.