:metarule (a hand-written simplifier)
Major Section: RULE-CLASSES
See rule-classes for a general discussion of rule classes and how they are
used to build rules from formulas. Meta rules extend the ACL2 simplifier
with hand-written code to transform certain terms to equivalent ones. To add
a meta rule, the
corollary formula must establish that the
hand-written ``metafunction'' preserves the meaning of the transformed term.
While our intention is that the set of ACL2 documentation topics is self-contained, readers might find it useful to see the following paper for an introduction to meta reasoning in ACL2.
W. A. Hunt, Jr., R. B. Krug, M. Kaufmann, J S. Moore and E. W. Smith, ``Meta Reasoning in ACL2.'' TPHOLs 2005, ed. J. Hurd and T. F. Melham, LNCS 3603, Springer-Verlag, Berlin, 2005, pp. 163-178.
corollary formulas from which
:meta rules might be
Examples: (equal (evl x a) ; Modify the rewriter to use fn to (evl (fn x) a)) ; transform terms. The :trigger-fns ; of the :meta rule-class specify ; the top-most function symbols of ; those x that are candidates for ; this transformation.A non-
(implies (and (pseudo-termp x) ; As above, but this illustrates (alistp a)) ; that without loss of generality we (equal (evl x a) ; may restrict x to be shaped like a (evl (fn x) a))) ; term and a to be an alist.
(implies (and (pseudo-termp x) ; As above (with or without the (alistp a) ; hypotheses on x and a) with the (evl (hyp-fn x) a)) ; additional restriction that the (equal (evl x a) ; meaning of (hyp-fn x) is true in (evl (fn x) a))) ; the current context. That is, the ; applicability of the transforma- ; tion may be dependent upon some ; computed hypotheses.
nillist of function symbols must be supplied as the value of the
:trigger-fnsfield in a
:metarule class object.
General Forms: (implies (and (pseudo-termp x) ; this hyp is optional (alistp a) ; this hyp is optional (ev (hyp-fn x ...) a)) ; this hyp is optional (equiv (ev x a) (ev (fn x ...) a)))where
equivis a known equivalence relation,
aare distinct variable names, and
evis an evaluator function (see below), and
fnis a function symbol, as is
hyp-fnwhen provided. The arguments to
hyp-fnshould be identical. In the most common case, both take a single argument,
x, which denotes the term to be simplified. If
hyp-fnare guarded, their guards should be (implied by)
pseudo-termp. See pseudo-termp. We say the theorem above is a ``metatheorem'' or ``metalemma'' and
fnis a ``metafunction'', and
hyp-fnis a ``hypothesis metafunction''.
...'' is empty, i.e., the metafunctions take just one argument, we
say they are ``vanilla flavored.'' If ``
...'' is non-empty, we say the
metafunctions are ``extended.'' Extended metafunctions can access
state and context sensitive information to compute their results,
within certain limits. We discuss vanilla metafunctions here and recommend a
thorough understanding of them before proceeding (at which time
Metafunctions and (if supplied) hypothesis metafunctions must be executable.
That is, they cannot be constrained (i.e., introduced in the signature
encapsulate events), nor can they be declared
non-executable. After all, there is no point in installing a
simplifier that cannot be run!
We defer discussion of the case in which there is a hypothesis metafunction and for now address the case in which the other two hypotheses are present.
In the discussion below, we refer to the argument,
hyp-fn as a ``term.'' When these metafunctions are executed by the
simplifier, they will be applied to (the quotations of) terms. But during
the proof of the metatheorem itself,
x may not be the quotation of a
term. If the
pseudo-termp hypothesis is omitted,
x may be any
object. Even with the
x may merely ``look
like a term'' but use non-function symbols or function symbols of incorrect
arity. In any case, the metatheorem is stronger than necessary to allow us
to apply the metafunctions to terms, as we do in the discussion below. We
return later to the question of proving the metatheorem.
Suppose the general form of the metatheorem above is proved with the
alistp hypotheses. Then when the simplifier
encounters a term,
(h t1 ... tn), that begins with a function symbol,
h, listed in
:trigger-fns, it applies the metafunction,
the quotation of the term, i.e., it evaluates
(fn '(h t1 ... tn)) to
obtain some result, which can be written as
'(h t1 ... tn) and
val is a term, then
(h t1 ... tn) is replaced by
val, which is then passed along for
further rewriting. Because the metatheorem establishes the correctness of
fn for all terms (even non-terms!), there is no restriction on which
function symbols are listed in the
:trigger-fns. Generally, of course,
they should be the symbols that head up the terms simplified by the
fn. See term-table for how one obtains some assistance
towards guaranteeing that
val is indeed a term.
The ``evaluator'' function,
ev, is a function that can evaluate a certain
class of expressions, namely, all of those composed of variables, constants,
and applications of a fixed, finite set of function symbols,
gk. Generally speaking, the set of function symbols handled by
chosen to be exactly the function symbols recognized and manipulated by the
metafunctions being introduced. For example, if
expressions in which
binary-append occur as
function symbols, then
ev is generally specified to handle
binary-append. The actual requirements on
ev become clear when
the metatheorem is proved. The standard way to introduce an evaluator is to
use the ACL2 macro
defevaluator, though this is not strictly necessary.
See defevaluator if you want details.
[Aside for the logic-minded.] Why are we justified in using metafunctions
this way? Suppose
(fn 'term1) is
'term2. What justifies replacing
term2? The first step is to assert that
(ev 'term1 a), where
a is an alist that maps
term1. This step is incorrect, because
'term1 may contain function symbols other than the ones,
ev knows how to handle. But we can grow
ev to a
ev*, an evaluator for all of the symbols that occur
term2. We can prove that
ev* satisfies the
ev, provided no
defaxiom events are adding
ev (or callers of
ev, and recursively); ACL2 checks
this additional property. Hence, the metatheorem holds for
ev* in place
ev, by functional instantiation. We can then carry out the proof of
the equivalence of
term2 as follows: Fix
a to be
an alist that maps the quotations of the variables of
to themselves. Then,
term1 = (ev* 'term1 a) ; (1) by construction of ev* and a = (ev* (fn 'term1) a) ; (2) by the metatheorem for ev* = (ev* 'term2 a) ; (3) by evaluation of fn = term2 ; (4) by construction of ev* and aNote that in line (2) above, where we appeal to the (functional instantiation of the) metatheorem, we can relieve its (optional)
alistphypotheses by appealing to the facts that
term1is a term and
ais an alist by construction. [End of Aside for the logic-minded.]
There are subtleties related to the notion of ``growing''
ev to a
``larger'' evaluator, as mentioned in the paragraph just above. For
corresponding restrictions on
:meta rules, see evaluator-restrictions.
Finally, we turn to the second case, in which there is a hypothesis
metafunction. In that case, consider as before what happens when the
simplifier encounters a term,
(h t1 ... tn), where
h is listed in
:trigger-fns. This time, after it applies
'(h t1 ... tn)
to obtain the quotation of some new term,
'val, it then applies the
hyp-fn. That is, it evaluates
(hyp-fn '(h t1 ... tn)) to obtain some result, which can be written as
hyp-val is not in fact a term, the metafunction is not
hyp-val is a term, the simplifier attempts to establish
(by conventional backchaining) that this term is non-
nil in the current
context. If this attempt fails, then the meta rule is not applied.
(h t1...tn) is replaced by
val as in the previous case
(where there was no hypothesis metafunction).
Why is it justified to make this extension to the case of hypothesis metafunctions? First, note that the rule
(implies (and (pseudo-termp x) (alistp a) (ev (hyp-fn x) a)) (equal (ev x a) (ev (fn x) a)))is logically equivalent to the rule
(implies (and (pseudo-termp x) (alistp a)) (equal (ev x a) (ev (new-fn x) a)))where
(new-fn x)is defined to be
(list 'if (hyp-fn x) (fn x) x). (If we're careful, we realize that this argument depends on making an extension of
evto an evaluator
ifand the functions manipulated by
hyp-fn.) If we write
'termfor the quotation of the present term, and if
(fn 'term)are both terms, say
term1, then by the previous argument we know it is sound to rewrite term to
(if hyp1 term1 term). But since we have established in the current context that
nil, we may simplify
(if hyp1 term1 term)to
term1, as desired.
We now discuss the role of the
(Pseudo-termp x) checks that
x has the shape of a term. Roughly
speaking, it ensures that
x is a symbol, a quoted constant, or a true
list consisting of a
lambda expression or symbol followed by some
pseudo-terms. Among the properties of terms not checked by
pseudo-termp are that variable symbols never begin with ampersand,
lambda expressions are closed, and function symbols are applied to the
correct number of arguments. See pseudo-termp.
There are two possible roles for
pseudo-termp in the development of a
metatheorem: it may be used as the guard of the metafunction and/or
hypothesis metafunction and it may be used as a hypothesis of the
metatheorem. Generally speaking, the
pseudo-termp hypothesis is
included in a metatheorem only if it makes it easier to prove. The choice is
yours. (An extreme example of this is when the metatheorem is invalid
without the hypothesis!) We therefore address ourselves the question: should
a metafunction have a
pseudo-termp guard? A
guard for a metafunction, in connection with other considerations
described below, improves the efficiency with which the metafunction is used
by the simplifier.
To make a metafunction maximally efficient you should (a) provide it with a
pseudo-termp guard and exploit the guard when possible in
coding the body of the function (see guards-and-evaluation, especially the
section on efficiency issues), (b) verify the guards of the metafunction
(see verify-guards), and (c) compile the metafunction (see comp). When
these three steps have been taken the simplifier can evaluate
by running the compiled ``primary code'' (see guards-and-evaluation) for
fn directly in Common Lisp. (Note however that explicit compilation may
be suppressed; see compilation.)
Before discussing efficiency issues further, let us review for a moment the
general case in which we wish to evaluate
(fn 'obj) for some
logic function. We must first ask whether the guards of
fn have been verified. If not, we must evaluate
fn by executing its
logic definition. This effectively checks the guards of every
subroutine and so can be slow. If, on the other hand, the guards of
fn have been verified, then we can run the primary code for
'obj satisfies the guard of
fn. So we must next
evaluate the guard of
'obj. If the guard is met,
then we run the primary code for
fn, otherwise we run the logic code.
Now in the case of a metafunction for which the three steps above have been
followed, we know the guard is (implied by)
pseudo-termp and that
it has been verified. Furthermore, we know without checking that the
guard is met (because
term1 is a term and hence
'term1 is a
pseudo-termp). Hence, we can use the compiled primary code directly.
We strongly recommend that you compile your metafunctions, as well as all their subroutines (unless explicit compilation is suppressed; see compilation). Guard verification is also recommended.
Finally, we present a very simple example of the use of
based on one provided by Robert Krug. This example illustrates a trick for
avoiding undesired rewriting after applying a metafunction or any other form
of rewriting. To elaborate: in general, the term
t2 obtained by applying
a metafunction to a term
t1 is then handed immediately to the rewriter,
which descends recursively through the arguments of function calls to rewrite
t2 completely. But if
t2 shares a lot of structure with
it might not be worthwhile to rewrite
t2 immediately. (A rewrite of
t2 will occur anyhow the next time a goal is generated.) The trick
involves avoiding this rewrite by wrapping
t2 inside a call of
hide, which in turn is inside a call of a user-defined ``unhiding''
(defun unhide (x) (declare (xargs :guard t)) x)
(defthm unhide-hide (equal (unhide (hide x)) x) :hints (("Goal" :expand ((hide x)))))
(in-theory (disable unhide))
(defun my-plus (x y) (+ x y))
(in-theory (disable my-plus))
(defevaluator evl evl-list ((my-plus x y) (binary-+ x y) (unhide x) (hide x)))
(defun meta-fn (term) (declare (xargs :guard (pseudo-termp term))) (if (and (consp term) (equal (length term) 3) (equal (car term) 'my-plus)) `(UNHIDE (HIDE (BINARY-+ ,(cadr term) ,(caddr term)))) term))
(defthm my-meta-lemma (equal (evl term a) (evl (meta-fn term) a)) :hints (("Goal" :in-theory (enable my-plus))) :rule-classes ((:meta :trigger-fns (my-plus))))
Notice that in the following (silly) conjectre, ACL2 initially does only does
the simplification directed by the metafunction; a second goal is generated
before the commuativity of addition can be applied. If the above calls of
HIDE had been stripped off, then
Goal' would have been
the term printed in
ACL2 !>(thm (equal (my-plus b a) ccc))
This simplifies, using the :meta rule MY-META-LEMMA and the :rewrite rule UNHIDE-HIDE, to
Goal' (EQUAL (+ B A) CCC).
This simplifies, using the :rewrite rule COMMUTATIVITY-OF-+, to
Goal'' (EQUAL (+ A B) CCC).
The discussion above probably suffices to make good use of this
(UNHIDE (HIDE ...)) trick. However, we invite the reader who wishes to
understand the trick in depth to evaluate the following form before
thm form above.
(trace$ (rewrite :entry (list (take 2 arglist)) :exit (list (car values))) (rewrite-with-lemma :entry (list (take 2 arglist)) :exit (take 2 values)))The following annotated subset of the trace output (which may appear a bit different depending on the underlying Common Lisp implementation) explains how the trick works.
2> (REWRITE ((MY-PLUS B A) NIL))> 3> (REWRITE-WITH-LEMMA ((MY-PLUS B A) (REWRITE-RULE (:META MY-META-LEMMA) 1822 NIL EQUAL META-FN NIL META NIL NIL)))>
We apply the meta rule, then recursively rewrite the result, which is the (UNHIDE (HIDE ...)) term shown just below.
4> (REWRITE ((UNHIDE (HIDE (BINARY-+ B A))) ((A . A) (B . B))))> 5> (REWRITE ((HIDE (BINARY-+ B A)) ((A . A) (B . B))))>
The HIDE protects its argument from being touched by the rewriter.
<5 (REWRITE (HIDE (BINARY-+ B A)))> 5> (REWRITE-WITH-LEMMA ((UNHIDE (HIDE (BINARY-+ B A))) (REWRITE-RULE (:REWRITE UNHIDE-HIDE) 1806 NIL EQUAL (UNHIDE (HIDE X)) X ABBREVIATION NIL NIL)))>
Now we apply UNHIDE-HIDE, then recursively rewrite its right-hand side in an environment where X is bound to (BINARY-+ B A).
6> (REWRITE (X ((X BINARY-+ B A))))>
Notice that at this point X is cached, so REWRITE just returns (BINARY-+ B A).
<6 (REWRITE (BINARY-+ B A))> <5 (REWRITE-WITH-LEMMA T (BINARY-+ B A))> <4 (REWRITE (BINARY-+ B A))> <3 (REWRITE-WITH-LEMMA T (BINARY-+ B A))> <2 (REWRITE (BINARY-+ B A))>