Evaluating ACL2 expressions

This topic uses examples to expose how ACL2 uses Common Lisp to evaluate expressions. Links are provided to topics that elaborate on aspects of evaluation in ACL2.

At a high level, we can say that ACL2 evaluation takes place using the
underlying host Common Lisp. But consider the form

ACL2 !>(car 3) ACL2 Error in TOP-LEVEL: The guard for the function call (CAR X), which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 3). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>

The message suggests that the function

In fact, every ACL2 function symbol is associated with the following two Common Lisp definitions, as explained below:

- the ``executable-counterpart'' definition, sometimes called the ``*1*'' function (pronounced ``star one star''); and
- the ``submitted'' definition (sometimes called the ``raw Lisp'' function).

We may also speak of the ``executable-counterpart'' and ``submitted'' functions, which are the two functions defined by the ``executable-counterpart'' and ``submitted'' definitions, respectively.

Let us explore these two functions in the case of

The example above does not really explain why the submitted function is
called ``submitted'', so let us consider the more common case of a defined
function, as opposed to a primitive like

(defun f (x) (car x)) (defun g (x) (f x))

ACL2 defines two functions named

ACL2 !>(trace$ f g) ((F) (G)) ACL2 !>(g '(4 5 6)) 1> (ACL2_*1*_ACL2::G (4 5 6)) 2> (ACL2_*1*_ACL2::F (4 5 6)) <2 (ACL2_*1*_ACL2::F 4) <1 (ACL2_*1*_ACL2::G 4) 4 ACL2 !>

It is now perhaps evident why sometimes we call the executable-counterpart
functions the ``*1* functions'': the executable-counterpart is actually
defined in a special ``*1*'' package that corresponds to the package of the
submitted function. The trace above shows that the executable-counterpart of

Such a trace can show us an error caused by applying

ACL2 !>(g 3) 1> (ACL2_*1*_ACL2::G 3) 2> (ACL2_*1*_ACL2::F 3) ACL2 Error in TOP-LEVEL: The guard for the function call (CAR X), which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 3). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>

It is generally more efficient to invoke a submitted functions —
which has as its Common Lisp definition exactly the `defun` form
submitted to ACL2 — than it is to invoke an executable-counterpart,
which is generated by ACL2 to do auxiliary calculations including
guard-checking. So we next modify the example above to show that by
performing a process called ``guard verification'', we can avoid *1* function
calls, so that submitted functions are invoked instead. This time we supply
reasonable guards for

(defun f (x) (declare (xargs :guard (or (consp x) (null x)))) (car x)) (defun g (x) (declare (xargs :guard (consp x))) (f x))

This time, we see that the executable-counterpart of

ACL2 !>(trace$ f g) ((F) (G)) ACL2 !>(g '(4 5 6)) 1> (ACL2_*1*_ACL2::G (4 5 6)) 2> (G (4 5 6)) 3> (F (4 5 6)) <3 (F 4) <2 (G 4) <1 (ACL2_*1*_ACL2::G 4) 4 ACL2 !>

We can also see that because

ACL2 !>(g 3) 1> (ACL2_*1*_ACL2::G 3) ACL2 Error in TOP-LEVEL: The guard for the function call (G X), which is (CONSP X), is violated by the arguments in the call (G 3). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>

See if you can predict the corresponding traces if instead,

(defun f (x) (declare (xargs :guard (or (consp x) (null x)))) (car x)) (defun g (x) (f x))

The corresponding trace is as follows; discussion follows.

ACL2 !>(g '(4 5 6)) 1> (ACL2_*1*_ACL2::G (4 5 6)) 2> (ACL2_*1*_ACL2::F (4 5 6)) 3> (F (4 5 6)) <3 (F 4) <2 (ACL2_*1*_ACL2::F 4) <1 (ACL2_*1*_ACL2::G 4) 4 ACL2 !>(g 3) 1> (ACL2_*1*_ACL2::G 3) 2> (ACL2_*1*_ACL2::F 3) ACL2 Error in TOP-LEVEL: The guard for the function call (F X), which is (OR (CONSP X) (NULL X)), is violated by the arguments in the call (F 3). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>

The traces above show that first, the executable-counterpart of

See also guard and its subtopics, especially, guards-and-evaluation, for a discussion of guards and their connection to
evaluation. Advanced system hackers who want to see the
executable-counterpart definition for

- Guard-checking-inhibited
- Avoiding certain warnings when evaluating ACL2 expressions