Major Section: PROGRAMMING
Below are six commonly used idioms for testing whether
zp are the preferred termination tests for recursions
down the integers and naturals, respectively.
idiom logical guard primary meaning compiled code**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.
(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)
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,
(= x 0) is probably the most
(equal x 0) is probably the least efficient, and
(eql x 0) is in between. However, an optimizing compiler could
always choose to compile
(equal x 0) as
(eql x 0) and, in
x is known at compile-time to be numeric,
(eql x 0) as
(= x 0). So efficiency considerations must, of
course, be made in the context of the host compiler.
Note also that
(zerop x) and
(= x 0) are indistinguishable.
They have the same meaning and the same guard, and can reasonably be
expected to generate equally efficient code.
(zip x) and
(zp x) do not have the same logical
meanings as the others or each other. They are not simple tests for
0. They each coerce
x into a restricted domain,
zip to the integers and
zp to the natural numbers, choosing
x is outside the domain. Thus,
'abc, for example, are all ``recognized'' as zero by both
zip reports that
-1 is different from
zp reports that
0. More precisely,
(zip -1) is
(zp -1) is
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.
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
0and recursion by
1-. Note however that the test against
0is expressed with the
zpidiom. Note also the absence of a guard making explicit our intention that
nis a natural number.
This definition of factorial is readily admitted because when
is false (i.e.,
n is a natural number other than
0 and so
(1- n) is less than
n. The base case, where
is true, handles all the ``unexpected'' inputs, such as arise with
(fact -1) and
(fact 'abc). When calls of
(zp n) checks
(integerp n) and
(> n 0). Guard
verification is unsuccessful for this definition of
zp requires its argument to be a natural number and there is no
fact, above. Thus the primary raw lisp for
inaccessible and only the
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
(zp n)above is compiled as
(= n 0), because
nwill always be a natural number when the primary code is executed. Thus, by adding a guard and verifying it, the elegant and easily used definition of factorial is also efficiently executed on natural numbers.
Now let us consider an alternative definition of factorial in which
(= n 0) is used in place of
(defun fact (n) (if (= n 0) 1 (* n (fact (1- n)))))This definition does not terminate. For example
(fact -1)gives rise to a call of
(fact -2), etc. Hence, this alternative is inadmissible. A plausible response is the addition of a guard restricting
nto the naturals:
(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
nis a natural number would suffice and allow both admission and guard verification. But such a test would slow down the execution of the compiled function.
The use of
(zp n) as the test avoids this dilemma.
provides the logical equivalent of a runtime test that
n is a
natural number but the execution efficiency of a direct
0, at the expense of a guard conjecture to prove.
In addition, if guard verification and most-efficient execution are
not needed, then the use of
(zp n) allows the admission of the
function without a guard or other extraneous verbiage.
While general rules are made to be broken, it is probably a good
idea to get into the habit of using
(zp n) as your terminating
0 test'' idiom when recursing down the natural numbers. It
provides the logical power of testing that
n is a non-
natural number and allows efficient execution.
We now turn to the analogous function,
Zip is the
0-test idiom when recursing through the integers toward
Zip considers any non-integer to be
0 and otherwise
0. A typical use of
zip is in the definition
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 recurses by
(floor i 2). Hence, calling the function on
25causes calls on
0, while calling it on
-25generates calls on
-1. By making
(zip i)the first test, we terminate the recursion immediately on non-integers. The guard, if present, can be verified and allows the primary raw lisp definition to check
(= i 0)as the first terminating condition (because the primary code is executed only on integers).