|
|
|---|
|
|
|
|---|
Some restrictions on the use of evaluators in meta-level rules
Note: This topic, which explains some subtleties for evaluators, can probably be skipped by most readers.
Rules of class
In a nutshell, we require that a rule's evaluator does not support any meta-extract functions in the rule or any defaxiom events, and we require that the evaluator not be introduced under a non-trivial encapsulate. We also require that no function has an attachment (see defattach) that is both ancestral in the evaluator and also ancestral in the meta or clause-processor functions. We explain these restrictions in detail below, including the notion of one function symbol being “ancestral in”, also expressed as “an ancestor of”, in another function symbol.
An argument given elsewhere (see meta, in particular ``Aside for the
logic-minded'') explains that the correctness argument for applying
metatheoretic simplifiers requires that one be able to ``grow'' an evaluator
(see defevaluator) to handle all functions in the current ACL2 world. Then we may, in essence, functionally instantiate the original
evaluator to the new (``grown'') evaluator, provided that the new evaluator
satisfies all of the axioms of the original. We therefore require that the
evaluator function does not support the formula of any defaxiom event.
This notion of ``support'' (sometimes denoted ``is an ancestor of'') is
defined recursively as follows: a function symbol supports a formula if either
it occurs in that formula, or else it supports the definition or constraint
for some function symbol that occurs in that formula. Moreover, we require
that neither the evaluator function nor its list version support meta-extract functions if they are used in the proposed
These requirements are necessary in order to carry out the functional instantiation argument alluded to above, as follows (where the reader may find it useful to have some familiarity with the paper ``Structured Theory Development for a Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001), pages 161-203). By the usual conservativity argument, we know that the rule follows logically from the axiomatic events for its supporters. This remains true if we functionally instantiate the evaluator with one corresponding to all the functions symbols of the current session, since none of the definitions of supporters of defaxioms or metafunctions are hit by that functional substitution.
Notice though that the argument above depends on knowing that the rule is
not itself an axiom about the evaluator! Therefore, we also restrict
evaluators so that they are not defined in the scope of a superior encapsulate event with non-empty signature, in order to avoid an even more
subtle problem. The aforementioned correctness argument depends on knowing
that the rule is provable from the axioms on the evaluator and metafunction
(and hypothesis metafunction, if any). The additional restriction avoids
unsoundness! The following events, if allowed, produce a proof that
; Introduce our metafunction. (defun my-cancel (term) (case-match term (('f ('g)) *t*) (& term))) ; Introduce our evaluator and prove our meta rule, but in the same ; encapsulate! (encapsulate ((f (x) t)) (local (defun f (x) (declare (ignore x)) t)) (defevaluator evl evl-list ((f x))) (defthm correctness-of-my-cancel (equal (evl x a) (evl (my-cancel x) a)) :rule-classes ((:meta :trigger-fns (f))))) ; Prove that (f x) = t. (encapsulate () (local (defstub c () t)) (local (encapsulate () (local (defun g () (c))) (local (in-theory (disable g (g)))) (local (defthm f-g (equal (f (g)) t) :rule-classes nil)) (defthm f-c (equal (f (c)) t) :hints (("Goal" :use f-g :in-theory (e/d (g) (correctness-of-my-cancel)))) :rule-classes nil))) (defthm f-t (equal (f x) t) :hints (("Goal" :by (:functional-instance f-c (c (lambda () x))))) :rule-classes nil))
To see that the term
; (defun my-cancel (term) ...) as before, then: (defun f (x) (not x)) (defun g () nil) (defevaluator evl evl-list ((f x) (g)))
These events imply the axiomatic events above, because we still have the
definition of
(defthm f-not-t (equal (f t) nil) :rule-classes nil)
It follows that the current session logically yields a contradiction!
Erik Reeber has taken the above example and modified it to prove
(in-package "ACL2") (defun my-cancel (term) (case-match term (('f ('g)) *t*) (('f2 ('g2)) *t*) (& term))) (defun f2 (x) (not x)) (defun g2 () nil) (encapsulate ((f (x) t)) (local (defun f (x) (declare (ignore x)) t)) (defevaluator evl evl-list ((f x) (f2 x) (g2))) (defthm correctness-of-my-cancel (equal (evl x a) (evl (my-cancel x) a)) :rule-classes ((:meta :trigger-fns (f))))) (encapsulate () (local (defstub c () t)) (local (encapsulate () (local (defun g () (c))) (local (in-theory (disable g (g)))) (local (defthm f-g (equal (f (g)) t) :rule-classes nil)) (defthm f-c (equal (f (c)) t) :hints (("Goal" :use f-g :in-theory (e/d (g) (correctness-of-my-cancel)))) :rule-classes nil))) (defthm f-t (equal (f x) t) :hints (("Goal" :by (:functional-instance f-c (c (lambda () x))))) :rule-classes nil)) (defun g () nil) ; Below is the expansion of the following defevaluator, changed slightly as ; indicated by comments. ; (defevaluator evl2 evl2-list ((f x) (f2 x) (g) (g2))) (ENCAPSULATE (((EVL2 * *) => *) ((EVL2-LIST * *) => *)) (SET-INHIBIT-WARNINGS "theory") (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*)) (LOCAL (MUTUAL-RECURSION (DEFUN EVL2 (X A) (DECLARE (XARGS :VERIFY-GUARDS NIL :MEASURE (ACL2-COUNT X) :WELL-FOUNDED-RELATION O< :MODE :LOGIC)) (COND ((SYMBOLP X) (CDR (ASSOC-EQ X A))) ((ATOM X) NIL) ((EQ (CAR X) 'QUOTE) (CAR (CDR X))) ((CONSP (CAR X)) (EVL2 (CAR (CDR (CDR (CAR X)))) (PAIRLIS$ (CAR (CDR (CAR X))) (EVL2-LIST (CDR X) A)))) ((EQUAL (CAR X) 'F) ; changed f to f2 just below (F2 (EVL2 (CAR (CDR X)) A))) ((EQUAL (CAR X) 'F2) (F2 (EVL2 (CAR (CDR X)) A))) ((EQUAL (CAR X) 'G) (G)) ((EQUAL (CAR X) 'G2) (G2)) (T NIL))) (DEFUN EVL2-LIST (X-LST A) (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST) :WELL-FOUNDED-RELATION O<)) (COND ((ENDP X-LST) NIL) (T (CONS (EVL2 (CAR X-LST) A) (EVL2-LIST (CDR X-LST) A))))))) (DEFTHM EVL2-CONSTRAINT-1 (IMPLIES (SYMBOLP X) (EQUAL (EVL2 X A) (CDR (ASSOC-EQ X A))))) (DEFTHM EVL2-CONSTRAINT-2 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'QUOTE)) (EQUAL (EVL2 X A) (CADR X)))) (DEFTHM EVL2-CONSTRAINT-3 (IMPLIES (AND (CONSP X) (CONSP (CAR X))) (EQUAL (EVL2 X A) (EVL2 (CADDAR X) (PAIRLIS$ (CADAR X) (EVL2-LIST (CDR X) A)))))) (DEFTHM EVL2-CONSTRAINT-4 (IMPLIES (NOT (CONSP X-LST)) (EQUAL (EVL2-LIST X-LST A) NIL))) (DEFTHM EVL2-CONSTRAINT-5 (IMPLIES (CONSP X-LST) (EQUAL (EVL2-LIST X-LST A) (CONS (EVL2 (CAR X-LST) A) (EVL2-LIST (CDR X-LST) A))))) (DEFTHM EVL2-CONSTRAINT-6 (IMPLIES (AND (NOT (CONSP X)) (NOT (SYMBOLP X))) (EQUAL (EVL2 X A) NIL))) (DEFTHM EVL2-CONSTRAINT-7 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F)) (EQUAL (EVL2 X A) ; changed f to f2 just below (F2 (EVL2 (CADR X) A))))) (DEFTHM EVL2-CONSTRAINT-8 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F2)) (EQUAL (EVL2 X A) (F2 (EVL2 (CADR X) A))))) (DEFTHM EVL2-CONSTRAINT-9 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G)) (EQUAL (EVL2 X A) (G)))) (DEFTHM EVL2-CONSTRAINT-10 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G2)) (EQUAL (EVL2 X A) (G2))))) (defthm f2-t (equal (f2 x) t) :hints (("Goal" :by (:functional-instance f-t (f f2) (evl evl2) (evl-list evl2-list))))) (defthm bug-implies-nil nil :hints (("Goal" :use ((:instance f2-t (x t))))) :rule-classes nil)
Finally, we also require that no function has an attachment (see defattach) that is both ancestral in the evaluator and also ancestral in the
meta or clause-processor functions. (If you don't use defattach or
apply$ — more specifically, warrants — then you can
ignore this condition.) Without this restriction, the following events prove
(in-package "ACL2") (defstub f () t) (defevaluator evl evl-list ((f))) (defun my-meta-fn (x) (if (equal x '(f)) (list 'quote (f)) x)) (defthm my-meta-fn-correct (equal (evl x a) (evl (my-meta-fn x) a)) :rule-classes ((:meta :trigger-fns (f)))) (defun constant-nil () (declare (xargs :guard t)) nil) (defattach f constant-nil) (defthm f-is-nil ; proved using my-meta-fn-correct (equal (f) nil) :rule-classes nil) (defthm contradiction nil :hints (("Goal" :use ((:functional-instance f-is-nil (f (lambda () t)))))) :rule-classes nil)
Here is an example that doesn't use defattach explicitly, but uses
warrants, which essentially have attachments so that every call of a
warrant evaluates to
(in-package "ACL2") (include-book "projects/apply/top" :dir :system) (defevaluator evl evl-list ((apply$ fn args))) (encapsulate () (local (defun$ f () (declare (xargs :guard t)) t)) (local (defun my-meta-fn (x) (if (and (equal x '(apply$ 'f 'nil)) (apply$-warrant-f)) *t* x))) (local (defthm my-meta-fn-correct (equal (evl x a) (evl (my-meta-fn x) a)) :rule-classes ((:meta :trigger-fns (apply$))))) (defthm unwarranted-fact-about-quote-f (equal (apply$ 'f nil) t) :rule-classes nil)) (defun$ f () nil) (defthm apply$-warrant-f-false (not (apply$-warrant-f)) :hints (("Goal" :use unwarranted-fact-about-quote-f)) :rule-classes nil) ; But apply$-warrant-f is a function with no non-trivial constraint. (defthm contradiction nil :hints (("Goal" :use (:functional-instance apply$-warrant-f-false (apply$-warrant-f (lambda () t)) (apply$-userfn (lambda (fn args) nil)) (badge-userfn (lambda (fn) '(APPLY$-BADGE 0 1 . T)))))) :rule-classes nil)
To see why this restriction is sufficient, see a comment in the ACL2 source code entitled ``; Essay on Correctness of Meta Reasoning.''
One can sometimes work around this restriction; see transparent-functions.