Zero-test-idioms
How to test for 0
Below are six commonly used idioms for testing whether x is
0. 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, (= x 0) is probably the most efficient, (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 situations where 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.
Note that (zip x) and (zp x) do not have the same logical
meanings as the others or each other. They are not simple tests for equality
to 0. They each coerce x into a restricted domain, zip to
the integers and zp to the natural numbers, choosing 0 for x
when x is outside the domain. Thus, 1/2, #c(1 3), and
'abc, for example, are all ``recognized'' as zero by both zip and
zp. But zip reports that -1 is different from 0
while zp reports that -1 ``is'' 0. More precisely, (zip
-1) is nil while (zp -1) is t.
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 0 and recursion
by 1-. Note however that the test against 0 is expressed with
the zp idiom. Note also the absence of a guard making explicit
our intention that n is a natural number.
This definition of factorial is readily admitted because when (zp
n)
is false (i.e., nil) then n is a natural number other than 0
and so (1- n) is less than n. The base case, where (zp n) is
true, handles all the ``unexpected'' inputs, such as arise with (fact -1)
and (fact 'abc). When calls of fact are evaluated, (zp n)
checks (integerp n) and (> n 0). Guard verification is
unsuccessful for this definition of fact because zp requires its
argument to be a natural number and there is no guard on fact,
above. Thus the primary raw lisp for fact is 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 n will 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 (zp n).
(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 n to 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
n is 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. Zp
provides the logical equivalent of a runtime test that n is a natural
number but the execution efficiency of a direct = comparison with
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-0 natural number and allows efficient
execution.
We now turn to the analogous function, zip. Zip is the
preferred 0-test idiom when recursing through the integers toward 0.
Zip considers any non-integer to be 0 and otherwise just
recognizes 0. A typical use of 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 (floor i 2). Hence, calling the
function on 25 causes calls on 12, 6, 3, 1, and
0, while calling it on -25 generates calls on -13, -7,
-4, -2, and -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).
