Major Section: META
Note: This topic, which explains some subtleties for evaluators, can probably be skipped by most readers.
Rules of class :meta and of class :clause-processor are
stated using so-called ``evaluator'' functions. Here we explain some
restrictions related to evaluators. Below we refer primarily to :meta
rules, but the discussion applies equally to :clause-processor rules.
In a nutshell, we require that a rule's evaluator does not support other functions in the rule, 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.
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 the definition or
constraint for any other function symbol occurring in the proposed :meta
theorem.
We also require that the evaluator does not support the formula of a
:meta rule's metafunction (nor, if there is one, hypothesis metafunction)
or of a :clause-processor rule's clause-processor function. This
requirement, along with with the analogous requirement for defaxiom
events stated above, 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
(f x) equals t even though, as shown below, that does not follow
logically from the axioms introduced.
; 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 (equal (f x) t) does not follow logically from the
axiomatic events above, consider following the above definition of
my-cancel with the following events instead.
; (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
my-cancel, we have a stronger defevaluator event, and
we can now prove correctness-of-my-cancel exactly as it is stated above.
So, the rule f-t is a logical consequence of the chronology of the
current session. However, in the current session we can also prove the
following rule, which contradicts f-t.
(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 nil in
ACL2 Version_3.1, as follows.
(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 (CONSP X) (EQUAL (CAR X) 'F))
(EQUAL (EVL2 X A) ; changed f to f2 just below
(F2 (EVL2 (CADR X) A)))))
(DEFTHM EVL2-CONSTRAINT-7
(IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F2))
(EQUAL (EVL2 X A)
(F2 (EVL2 (CADR X) A)))))
(DEFTHM EVL2-CONSTRAINT-8
(IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G))
(EQUAL (EVL2 X A) (G))))
(DEFTHM EVL2-CONSTRAINT-9
(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 then you can
ignore this condition.) Without this restriction, the following events prove
nil.
(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)
To see why this restriction is sufficient, see a comment in the ACL2 source
code entitled ``; Essay on Correctness of Meta Reasoning.''
