		Search-engine friendly clone of the ACL2 documentation.

Events

Defevaluator

Introduce an evaluator function

Example:
(defevaluator evl evl-list
  ((length x) (member-equal x y)))

See meta.

General Form:
(defevaluator ev ev-list
   ((g1 x1 ... xn_1)
    ...
    (gk x1 ... xn_k))
   :namedp flg)       ; [optional keyword argument]

where ev and ev-list are new function symbols and g1, ..., gk are old function symbols with the indicated number of formals, i.e., each gi has n_i formals. If the :namedp keyword argument is provided, its value should be Boolean. If not provided, the default value for flg is nil.

This function provides a convenient way to constrain ev and ev-list to be mutually-recursive evaluator functions for the symbols g1, ..., gk. Roughly speaking, an evaluator function for a fixed, finite set of function symbols is a restriction of the universal evaluator to terms composed of variables, constants, lambda expressions, and applications of the given functions. However, evaluator functions are constrained rather than defined, so that the proof that a given metafunction is correct vis-a-vis a particular evaluator function can be lifted (by functional instantiation) to a proof that it is correct for any larger evaluator function. See meta for a discussion of metafunctions.

If the :namedp flg is nil (the default) constraints have names of the form ev-CONSTRAINT-i, e.g., EV-CONSTRAINT-0, EV-CONSTRAINT-1, etc. If flg is non-nil, the constraints are named more mnemonically, e.g., EV-OF-VARIABLE, EV-OF-REVAPPEND-CALL, etc. We illustrate the :namedp t names below.

Defevaluator executes an encapsulate after generating the appropriate defun and defthm events. Perhaps the easiest way to understand what defevaluator does is to execute the keyword command

:trans1 (defevaluator evl evl-list ((length x) (member-equal x y)))

and inspect the output. This trick is also useful in the rare case that the event fails because a hint is needed. In that case, the output of :trans1 can be edited by adding hints, then submitted directly.

Formally, ev is said to be an ``evaluator function for g1, ..., gk, with mutually-recursive counterpart ev-list'' iff ev and ev-list are constrained functions satisfying just the constraints discussed below.

Ev and ev-list must satisfy constraints (0)-(7) and (k) below. When :namedp nil is supplied, the i in the generated constraint names are the parenthesized numbers below. When :namedp t is supplied, the mnemonic names are those shown in brackets below.

(0) How to ev an arbitrary function application:
    [EV-OF-FNCALL-ARGS]
    (implies (and (consp x)
                  (syntaxp (not (equal a ''nil)))
                  (not (equal (car x) 'quote)))
             (equal (ev x a)
                    (ev (cons (car x)
                              (kwote-lst (ev-list (cdr x) a)))
                        nil)))

(1) How to ev a variable symbol:
    [EV-OF-VARIABLE]
    (implies (symbolp x)
             (equal (ev x a) (and x (cdr (assoc-equal x a)))))

(2) How to ev a constant:
    [EV-OF-QUOTE]
    (implies (and (consp x)
                  (equal (car x) 'quote))
             (equal (ev x a) (cadr x)))

(3) How to ev a lambda application:
    [EV-OF-LAMBDA]
    (implies (and (consp x)
                  (consp (car x)))
             (equal (ev x a)
                    (ev (caddar x)
                        (pairlis$ (cadar x)
                                  (ev-list (cdr x) a)))))

(4) How to ev an empty argument list:
    [EV-LIST-OF-ATOM]
    (implies (not (consp x-lst))
             (equal (ev-list x-lst a)
                    nil))

(5) How to ev a non-empty argument list:
    [EV-LIST-OF-CONS]
    (implies (consp x-lst)
             (equal (ev-list x-lst a)
                    (cons (ev (car x-lst) a)
                          (ev-list (cdr x-lst) a))))

(6) How to ev a non-symbol atom:
    [EV-OF-NONSYMBOL-ATOM]
    (implies (and (not (consp x))
                  (not (symbolp x)))
             (equal (ev x a)
                    nil))

(7) How to ev a cons whose car is a non-symbol atom:
    [EV-OF-BAD-FNCALL]
    (implies (and (consp x)
                  (not (consp (car x)))
                  (not (symbolp (car x))))
             (equal (ev x a)
                    nil))

(k) For each i from 1 to k, how to ev an application of gi,
    where gi is a function symbol of n arguments:
    [EV-OF-gi-CALL]
    (implies (and (consp x)
                  (equal (car x) 'gi))
             (equal (ev x a)
                    (gi (ev x1 a)
                        ...
                        (ev xn a)))),
    where xi is the (cad...dr x) expression equivalent to (nth i x).

Defevaluator defines suitable witnesses for ev and ev-list, proves the theorems about them, and constrains ev and ev-list appropriately. We expect defevaluator to work without assistance from you, though the proofs do take some time and generate a lot of output. The proofs are done in the context of a fixed theory, namely the value of the constant *defevaluator-form-base-theory*.

(Aside: (3) above may seem surprising, since the bindings of a are not included in the environment that is used to evaluate the lambda body, (caddar x). However, ACL2 lambda expressions are all closed: in (lambda (v1 ... vn) body), the only free variables in body are among the vi. See term.)

Acknowledgment: We thank Sol Swords and Jared Davis for their community book tools/defevaluator-fast.lisp, which provided the model on which the current defevaluator is based. The original defevaluator was very inefficient, e.g., taking thousands of times longer than the current one on an evaluator interpreting 800 function symbols. We refactored their defevaluator-fast (with permission) and made it the new implementation as of ACL2 Version_7.2. Both implementations produce the same constraints modulo the naming option provided by :namedp.

Subtopics

Defevaluator-fast: Formerly a faster alternative to defevaluator, now just an alias.