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.