EVALUATOR-RESTRICTIONS

some restrictions on the use of evaluators in meta-level rules
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 appying 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.''