How to test for 0

Below are six commonly used idioms for testing whether `Zip` and `zp` are the preferred termination tests for
recursions down the integers and naturals, respectively.

idiom logical guard primary meaning compiled code* (equal x 0) (equal x 0) t (equal x 0) (eql x 0) (equal x 0) t (eql x 0) (zerop x) (equal x 0) x is a number (= x 0) (= x 0) (equal x 0) x is a number (= x 0) (zip x) (equal (ifix x) 0) x is an integer (= x 0) (zp x) (equal (nfix x) 0) x is a natural (int= x 0) (zpf x) (equal (nfix x) 0) x is a fixnum >= 0 (eql (the-fixnum x) 0)

*See guards-and-evaluation, especially the subsection titled ``Guards and evaluation V: efficiency issues''. Primary code is relevant only if guards are verified. The ``compiled code'' shown is only suggestive.

The first four idioms all have the same logical meaning and differ only
with respect to their executability and efficiency. In the absence of
compiler optimizing,

Note also that

Note that `zip` to
the integers and `zp` to the natural numbers, choosing `zip` and
`zp`. But `zip` reports that `zp` reports that

Note that the last five idioms all have guards that restrict their Common Lisp executability. If these last five are used in situations in which guards are to be verified, then proof obligations are incurred as the price of using them. If guard verification is not involved in your project, then the first five can be thought of as synonymous.

`Zip` and `zp` are not provided by Common Lisp but are
ACL2-specific functions. Why does ACL2 provide these functions? The answer
has to do with the admission of recursively defined functions and efficiency.
`Zp` is provided as the zero-test in situations where the controlling
formal parameter is understood to be a natural number. `Zip` is
analogously provided for the integer case. We illustrate below.

Here is an admissible definition of factorial

(defun fact (n) (if (zp n) 1 (* n (fact (1- n)))))

Observe the classic recursion scheme: a test against `1-`. Note however that the test against `zp` idiom. Note also the absence of a guard making explicit
our intention that

This definition of factorial is readily admitted because when

is false (i.e., `zp` requires its
argument to be a natural number and there is no guard on `logic` definition (which does runtime ``type'' checking) is used
in computation. In summary, this definition of factorial is easily admitted
and easily manipulated by the prover but is not executed as efficiently as it
could be.

Runtime efficiency can be improved by adding a guard to the definition.

(defun fact (n) (declare (xargs :guard (and (integerp n) (>= n 0)))) (if (zp n) 1 (* n (fact (1- n)))))

This guarded definition has the same termination conditions as
before — termination is not sensitive to the guard. But the
guards can be verified. This makes the primary raw lisp definition
accessible during execution. In that definition, the

Now let us consider an alternative definition of factorial in which

(defun fact (n) (if (= n 0) 1 (* n (fact (1- n)))))

This definition does not terminate. For example

(defun fact (n) (declare (xargs :guard (and (integerp n) (>= n 0)))) (if (= n 0) 1 (* n (fact (1- n)))))

But because the termination argument is not sensitive to the guard,
it is still impossible to admit this definition. To influence the termination
argument one must change the conditions tested. Adding a runtime test that

The use of `Zp`
provides the logical equivalent of a runtime test that `=` comparison with

While general rules are made to be broken, it is probably a good idea to
get into the habit of using

We now turn to the analogous function, `zip`. `Zip` is the
preferred `Zip` considers any non-integer to be `zip` is in the definition of
`integer-length`, shown below. (ACL2 can actually accept this
definition, but only after appropriate lemmas have been proved.)

(defun integer-length (i) (declare (xargs :guard (integerp i))) (if (zip i) 0 (if (= i -1) 0 (+ 1 (integer-length (floor i 2))))))

Observe that the function recurs by