Meta
Make a :meta rule (a hand-written simplifier)
See rule-classes for a general discussion of rule classes,
including how they are used to build rules from formulas and a discussion of
the various keywords in a rule class description.
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.
Examples:
(defthm fn-correct-1 ; Modify the rewriter to use fn to
(equal (evl x a) ; transform terms that are calls of
(evl (fn x) a)) ; nth or of foo.
:rule-classes ((:meta :trigger-fns (nth foo))))
(defthm fn-correct-2 ; As above, but this illustrates
(implies (and (pseudo-termp x) ; that without loss of generality we
(alistp a)) ; may restrict x to be shaped like a
(equal (evl x a) ; term and a to be an alist.
(evl (fn x) a)))
:rule-classes ((:meta :trigger-fns (nth foo))))
(defthm fn-correct-3 ; As above (with or without the
(implies (and (pseudo-termp x) ; hypotheses on x and a), with the
(alistp a) ; additional restriction that the
(evl (hyp-fn x) a)) ; meaning of (hyp-fn x) is true in
(equal (evl x a) ; the current context. That is, the
(evl (fn x) a))) ; applicability of the transformation
:rule-classes ; may be dependent upon some computed
((:meta :trigger-fns (nth foo)))) ; hypotheses.
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.
A non-nil list of function symbols must be supplied as the value of
the :trigger-fns field in a :meta rule class object (except that a
macro alias can stand in for a function symbol; see add-macro-alias).
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
; meta-extract hyps may also be included (see below)
)
(equiv (ev x a)
(ev (fn x ...) a)))
where equiv is a known equivalence relation, x and a
are distinct variable names, and ev is an evaluator function (see below),
and fn is a function symbol, as is hyp-fn when provided. The
arguments to fn and hyp-fn should be identical. In the most common
case, both take a single argument, x, which denotes the term to be
simplified. If fn and/or hyp-fn are guarded, their guards should be trivially implied by pseudo-termp. We say the
theorem above is a ``metatheorem'' or ``metalemma'' and fn is a
``metafunction'', and hyp-fn is a ``hypothesis metafunction''.
If ``...'' 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 see extended-metafunctions).
If a metafunction application to a term, u, evaluates to a result of
the form (if TEST NEW-TERM u), then TEST is treated as an ``implicit
hypothesis''. For discussion of this relatively advanced feature, see meta-implicit-hypothesis.
Additional hypotheses are supported, called ``meta-extract hypotheses''.
These allow metafunctions to depend on the validity of certain terms extracted
from the context or the logical world. These hypotheses provide a
relatively advanced form of metatheorem so we explain them elsewhere; see
meta-extract.
One might think that metafunctions and (if supplied) hypothesis
metafunctions must be executable: that is, not constrained (i.e., introduced
in the signature of encapsulate events), and not declared :non-executable. After all, there is no point in
installing a simplifier that cannot be run! However, such a restriction is
not enforced, because one could introduce a metafunction using encapsulate and then use defattach to attach it to an executable
function; see defattach.
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, x, of fn and
hyp-fn as a ``(translated) term,'' i.e., an object satisfying the ACL2
built-in predicate termp. 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 pseudo-termp hypothesis, 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 pseudo-termp and 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, fn, to
the quotation of the term, i.e., it evaluates (fn '(h t1 ... tn)) to
obtain some result, which can be written as 'val. If 'val is
different from '(h t1 ... tn) and val is a well-formed term (see the
next paragraph), 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 metafunction fn.
Note that the result of applying a metafunction (or a hypothesis
metafunction) must be a term, i.e., must satisfy the predicate termp
in the current logical world. If not, then an error occurs. See term-table for how one obtains some assistance towards testing that val
is indeed a term. ACL2 actually enforces a stronger requirement, disallowing
calls of certain ``forbidden'' function symbols as described in set-skip-meta-termp-checks. Both of these runtime checks can be avoided by
proving that the metafunction (and the corresponding hypothesis metafunction,
if any) always produces an acceptable term. See well-formedness-guarantee. Alternatively, with an active trust tag (see
defttag) you can tell ACL2 to skip these tests; see set-skip-meta-termp-checks.
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,
g1, ..., gk. Generally speaking, the set of function symbols
handled by ev is chosen to be exactly the function symbols recognized and
manipulated by the metafunctions being introduced. For example, if fn
manipulates expressions in which 'equal and 'binary-append occur as function symbols, then ev is generally specified
to handle equal and 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
term1 by term2? The first step is to assert that term1 is
(ev 'term1 a), where a is an alist that maps 'var to var,
for each variable var in term1. This step is incorrect, because
'term1 may contain function symbols other than the ones, g1, ...,
gk, that ev knows how to handle. But we can grow ev to a
``larger'' evaluator, ev*, an evaluator for all of the symbols that occur
in term1 or term2. We can prove that ev* satisfies the constraints on ev, provided no defaxiom events are adding
constraints to ev (or callers of ev, and recursively); ACL2 checks
this additional property. Hence, the metatheorem holds for ev* in place
of ev, by functional instantiation. We can then carry out the proof of
the equivalence of term1 and term2 as follows: Fix a to
be an alist that maps the quotations of the variables of term1 and
term2 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 a
Note that in line (2) above, where we appeal to the (functional
instantiation of the) metatheorem, we can relieve its (optional) pseudo-termp and alistp hypotheses by appealing to the facts that
term1 is a term and a is 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 fn to '(h t1 ... tn)
to obtain the quotation of some new term, 'val, it then applies the
hypothesis metafunction, hyp-fn. That is, it evaluates (hyp-fn '(h t1
... tn)) to obtain some result, which can be written as 'hyp-val. If
hyp-val is not in fact a term, the metafunction is not used. Provided
hyp-val is a term, the simplifier attempts to establish (by conventional
backchaining) that this term is non-nil in the current context. Note
that this backchaining is done just as it is done for hypotheses of rewrite (and linear) rules, namely, by rewriting with special
attention to calls of certain functions including force, case-split, syntaxp, and bind-free. If this attempt to
establish this term fails, then the meta rule is not applied. Otherwise,
(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 ev to an evaluator ev* that handles if and the
functions manipulated by hyp-fn.) If we write 'term for the
quotation of the present term, and if (hyp-fn 'term) and (fn 'term)
are both terms, say hyp1 and 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 hyp1 is non-nil, we may
simplify (if hyp1 term1 term) to term1, as desired.
We now discuss the role of the pseudo-termp hypothesis.
(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 pseudo-termp
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 (fn 'term1) 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 fn, provided 'obj
satisfies the guard of fn. So we must next evaluate the guard of fn on '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 :meta rules,
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 t1,
then 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'' function,
unhide.
(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) conjecture, ACL2 initially does only
does the simplification directed by the metafunction; a second goal is
generated before the commutativity of addition can be applied. If the above
calls of UNHIDE and HIDE had been stripped off, then Goal'
would have been the term printed in Goal'' below.
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 submitting the 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))>Subtopics
- Force
- Identity function used to force a hypothesis
- Syntaxp
- Attach a heuristic filter on a rule
- Extended-metafunctions
- State and context sensitive metafunctions
- Meta-extract
- Meta reasoning using valid terms extracted from context or world
- Backchain-limit
- Limiting the effort expended on relieving hypotheses
- Magic-ev-fncall
- Call the named function on the given arguments and return the value.
- Evaluator-restrictions
- Some restrictions on the use of evaluators in meta-level rules
- Meta-implicit-hypothesis
- A potentially more efficient way of coding a hypothesis metafunction
- Transparent-functions
- Working around restrictions on the use of evaluators in meta-level rules
- Set-skip-meta-termp-checks
- Skip output checks for meta functions and clause-processors
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Term-table
- A table used to validate meta rules
- Magic-ev
- Evaluate a term under a ground substitution using magic-ev-fncall.
- Meta-lemmas
- A book of general purpose meta lemmas.
- Set-skip-meta-termp-checks!
- Skip output checks non-locally for meta functions and
clause-processors
