Metafunctions in Nqthm and Acl2 Bob Boyer (boyer@cli.com) Matt Kaufmann (kaufmann@cli.com) J Moore (moore@cli.com) Meta-level reasoning was added to the Boyer-Moore theorem prover by 1979. We have recently re-implemented and, we think, slightly improved our approach to meta-theoretic reasoning in the Acl2 theorem prover. However, there is lots of room for much more substantial improvement. Our talk will consist of 3 parts: review, recent results, and general remarks. A. We will present briefly the approach to metafunctions in Nqthm by way of a small example. Here is a brief description of such an example. Imagine a function cancel-equal-plus that takes one argument, which is intended to be a formal term, and returns a formal term that is obtained as follows. If the input term is an equation between two terms such that at least one of them is a PLUS term, then the output term is the result of cancelling the common summands on both sides of the equation. Otherwise, the output term is the same as input term. Now our meta lemma has the following form, where we think of x as a formal term and env as an environment associating values to variables. eval(x,env) = eval(cancel-equal-plus(x),env) Once this is proved, we can store it as a meta lemma that will "fire" on every equation, by applying the meta function to it. B. We will discuss recent improvements that we have made to our approach. These include a simpler notion of "evaluator" and conditional metalemmas. The Nqthm evaluator is actually rather complicated, because it is allowed to "learn" about new functions when they are defined, and hence it has a sort of evolving definition. In Acl2 there is a simpler notion of an "evaluator" that can be defined by the user. We'll outline how a second-order instantiation principle makes it possible for this notion of evaluator to suffice. In Acl2 and some other systems, functions may have preconditions. Because of this, it seems useful to have a notion of "hypothesis metafunction" in a metatheorem that generates appropriate hypotheses in order for the actual metafunction to apply. For example, in Acl2 the example meta theorem stated above might take the rough form eval(numeric-leaves-hypothesis(x),env) ==> eval(x,env) = eval(cancel-equal-plus(x),env) where for a formal equation x, numeric-leaves-hypothesis(x) is a term saying that all leaves of the plus-tree on each side of the equation x are numbers. C. We will make some general remarks that could be of interest for future work, including our own and others'. Such remarks will probably include the following. 1. It is useful to view meta-level reasoning as merely an application of program verification. Simply put, one is verifying the correctness of certain programs (the metafunctions), which happen then to be installed in the prover's code. 2. For efficient meta reasoning, it seems crucial to focus upon a very fast method (one machine instruction or so) for quoting and dequoting terms. Boyer and Moore believed this to be so important that they recoded Nqthm to be able do it. This issue is both subtle and tedious. 3. Although Nqthm's meta reasoning capability has received a good bit of use by very experienced users, it still suffers from the small number of places in the overall structure of the prover where it can be applied. Figuring out how to attach a meta-theoretic capability in more places, soundly of course, would be a good idea. 4. Both Nqthm and Acl2 use an approach based on evaluators (roughly, functions that provide an operational semantics for the term language). This approach is probably not as useful an approach as a full-fledged proof-theory style approach, which would, for example, permit one to prove and add meta theorems such as generalization.