`eql`

Major Section: PROGRAMMING

`(remove x l)`

is `l`

if `x`

is not a member of `l`

, else is the
result of removing all occurrences of `x`

from `l`

.

The guard for `(remove x l)`

requires `l`

to be a true list and
moreover, either `x`

is `eqlablep`

or all elements of `l`

are
`eqlablep`

.

`Remove`

is a Common Lisp function. See any Common Lisp
documentation for more information. Note that we do not allow
keyword arguments (such as `test`

) in ACL2 functions, in
particular, in `remove`

.

`eql`

) a list
Major Section: PROGRAMMING

`Remove-duplicates`

returns the result of deleting duplicate
elements from the beginning of the given string or true list, i.e.,
leaving the last element in place. For example,

(remove-duplicates '(1 2 3 2 4))is equal to

`'(1 3 2 4)`

.
The guard for `Remove-duplicates`

requires that its argument is a
string or a true-list of `eqlablep`

objects. It uses the function
`eql`

to test for equality between elements of its argument.

`Remove-duplicates`

is a Common Lisp function. See any Common Lisp
documentation for more information. Note that we do not allow
keyword arguments (such as `test`

) in ACL2 functions, in
particular, in `remove-duplicates`

. But
see remove-duplicates-equal, which is similar but uses the
function `equal`

to test for duplicate elements.

Major Section: PROGRAMMING

`Remove-duplicates-equal`

is the same as `remove-duplicates`

,
except that its argument must be a true list (not a string), and
`equal`

is used to check membership rather than `eql`

.
See remove-duplicates.

The guard for `Remove-duplicates-equal`

requires that its argument
is a true list. Note that unlike `remove-duplicates`

, it does not
allow string arguments.

`cdr`

) of the list
Major Section: PROGRAMMING

In the logic, `rest`

is just a macro for `cdr`

.

`Rest`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(Revappend x y)`

concatenates the reverse of the list `x`

to `y`

,
which is also typically a list.

The following theorem characterizes this English description.

(equal (revappend x y) (append (reverse x) y))Hint: This lemma follows immediately from the definition of

`reverse`

and the following lemma.
(defthm revappend-append (equal (append (revappend x y) z) (revappend x (append y z))))

The guard for `(revappend x y)`

requires that `x`

is a true list.

`Revappend`

is defined in Common Lisp. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(Reverse x)`

is the result of reversing the order of the
elements of the list `x`

.

The guard for `reverse`

requires that its argument is a true list.

`Reverse`

is defined in Common Lisp. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`Rfix`

simply returns any rational number argument unchanged,
returning `0`

on a non-rational argument. Also see nfix,
see ifix, and see fix for analogous functions that coerce
to a natural number, an integer, and a number, respectively.

`Rfix`

has a guard of `t`

.

Major Section: PROGRAMMING

Example Forms: ACL2 !>(round 14 3) 5 ACL2 !>(round -14 3) -5 ACL2 !>(round 14 -3) -5 ACL2 !>(round -14 -3) 5 ACL2 !>(round 13 3) 4 ACL2 !>(round -13 3) -4 ACL2 !>(round 13 -3) -4 ACL2 !>(round -13 -3) 4 ACL2 !>(round -15 -3) 5 ACL2 !>(round 15 -2) -8

`(Round i j)`

is the result of taking the quotient of `i`

and `j`

and rounding off to the nearest integer. When the quotient is
exactly halfway between consecutive integers, it rounds to the even
one.
The guard for `(round i j)`

requires that `i`

and `j`

are
rational numbers and `j`

is non-zero.

`Round`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

See any Common Lisp documentation for details.

Major Section: PROGRAMMING

`(Set-difference l1 l2)`

equals a list whose members
(see member-equal) contains the members of `x`

that are not
members of `y`

. More precisely, the resulting list is the same as
one gets by deleting the members of `y`

from `x`

, leaving the
remaining elements in the same order as they had in `x`

.

The guard for `set-difference-equal`

requires both arguments to be
true lists. Essentially, `set-difference-equal`

has the same
functionality as the Common Lisp function `set-difference`

, except
that it uses the `equal`

function to test membership rather than
`eql`

. However, we do not include the function `set-difference`

in ACL2, because the Common Lisp language does not specify the order
of the elements in the list that it returns.

Major Section: PROGRAMMING

See any Common Lisp documentation for details.

Major Section: PROGRAMMING

`(Signum x)`

is `0`

if `x`

is `0`

, `-1`

if `x`

is negative,
and is `1`

otherwise.

The guard for `signum`

requires its argument to be rational.

`Signum`

is a Common Lisp function. See any Common Lisp
documentation for more information.

From ``Common Lisp the Language'' page 206, we see a definition of
`signum`

in terms of `abs`

. As explained elsewhere
(see abs), the guard for `abs`

requires its argument to be a
rational number; hence, we make the same restriction for
`signum`

.

Major Section: PROGRAMMING

See any Common Lisp documentation for details.

Major Section: PROGRAMMING

`(standard-char-listp x)`

is true if and only if `x`

is a
null-terminated list all of whose members are standard characters.
See standard-char-p.

`Standard-char-listp`

has a guard of `t`

.

Major Section: PROGRAMMING

`(Standard-char-p x)`

is true if and only if `x`

is a ``standard''
character, i.e., a member of the list `*standard-chars*`

. This
list includes `#Newline`

and `#Space`

characters, as well as the usual
punctuation and alphanumeric characters.

`Standard-char-p`

has a guard requiring its argument to be a
character.

`Standard-char-p`

is a Common Lisp function. See any Common Lisp
documentation for more information.

`ld`

prints
Major Section: PROGRAMMING

`Standard-co`

is an `ld`

special (see ld). The accessor is
`(standard-co state)`

and the updater is `(set-standard-co val state)`

.
`Standard-co`

must be an open character output channel. It is to this
channel that `ld`

prints the prompt, the form to be evaluated, and the
results. The event commands such as `defun`

, `defthm`

, etc., which
print extensive commentary do not print to `standard-co`

but rather to
a different channel, `proofs-co`

, so that you may redirect this
commentary while still interacting via `standard-co`

.
See proofs-co.

``Standard-co'' stands for ``standard character output.'' The
initial value of `standard-co`

is the same as the value of
`*standard-co*`

(see *standard-co*).

Major Section: PROGRAMMING

`Standard-oi`

is an `ld`

special (see ld). The accessor is
`(standard-oi state)`

and the updater is `(set-standard-oi val state)`

.
`Standard-oi`

must be an open object input channel, a true list of
objects, or a list of objects whose last `cdr`

is an open object input
channel. It is from this source that `ld`

takes the input forms to
process. When `ld`

is called, if the value specified for `standard-oi`

is a string or a list of objects whose last `cdr`

is a string, then `ld`

treats the string as a file name and opens an object input channel
from that file. The channel opened by `ld`

is closed by `ld`

upon
termination.

``Standard-oi'' stands for ``standard object input.'' The
read-eval-print loop in `ld`

reads the objects in `standard-oi`

and
treats them as forms to be evaluated. The initial value of
`standard-oi`

is the same as the value of `*standard-oi*`

(see *standard-oi*).

Major Section: PROGRAMMING

`(String x)`

coerces `x`

to a string. If `x`

is already a
string, then it is returned unchanged; if `x`

is a symbol, then its
`symbol-name`

is returned; and if `x`

is a character, the
corresponding one-character string is returned.

The guard for `string`

requires its argument to be a string, a
symbol, or a character.

`String`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(String-alistp x)`

is true if and only if `x`

is a list of pairs
of the form `(cons key val)`

where `key`

is a string.

`String-alistp`

has a guard of `t`

.

Major Section: PROGRAMMING

NOTE: It is probably more efficient to use the Common Lisp function
`concatenate`

in place of `string-append`

. That is,

(string-append str1 str2)is equal to

(concatenate 'string str1 str2).

At any rate, `string-append`

takes two arguments, which are both
strings (if the guard is to be met), and returns a string obtained
concatenating together the characters in the first string followed
by those in the second. See concatenate.

Major Section: PROGRAMMING

For a string `x`

, `(string-downcase x)`

is the result of applying
`char-downcase`

to each character in `x`

.

The guard for `string-downcase`

requires its argument to be a string.

`String-downcase`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

For strings `str1`

and `str2`

, `(string-equal str1 str2)`

is true if
and only `str1`

and `str2`

are the same except perhaps for the cases of
their characters.

The guard on `string-equal`

requires that its arguments are strings.

`String-equal`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

The predicate `string-listp`

tests whether its argument is a
`true-listp`

of strings.

Major Section: PROGRAMMING

For a string `x`

, `(string-upcase x)`

is the result of applying
`char-upcase`

to each character in `x`

.

The guard for `string-upcase`

requires its argument to be a string.

`String-upcase`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(String< str1 str2)`

is non-`nil`

if and only if the string
`str1`

precedes the string `str2`

lexicographically, where
character inequalities are tested using `char<`

. When non-`nil`

,
`(string< str1 str2)`

is the first position (zero-based) at which
the strings differ. Here are some examples.

ACL2 !>(string< "abcd" "abu") 2 ACL2 !>(string< "abcd" "Abu") NIL ACL2 !>(string< "abc" "abcde") 3 ACL2 !>(string< "abcde" "abc") NIL

The guard for `string<`

specifies that its arguments are strings.

`String<`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(String<= str1 str2)`

is non-`nil`

if and only if the string
`str1`

precedes the string `str2`

lexicographically or the strings
are equal. When non-`nil`

, `(string<= str1 str2)`

is the first
position (zero-based) at which the strings differ, if they differ,
and otherwise is their common length. See string<.

The guard for `string<=`

specifies that its arguments are strings.

`String<=`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(String> str1 str2)`

is non-`nil`

if and only if `str2`

precedes
`str1`

lexicographically. When non-`nil`

, `(string> str1 str2)`

is the first position (zero-based) at which the strings differ.
See string<.

`String>`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(String>= str1 str2)`

is non-`nil`

if and only if the string
`str2`

precedes the string `str1`

lexicographically or the strings
are equal. When non-`nil`

, `(string>= str1 str2)`

is the first
position (zero-based) at which the strings differ, if they differ,
and otherwise is their common length. See string>.

The guard for `string>=`

specifies that its arguments are strings.

`String>=`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(stringp x)`

is true if and only if `x`

is a string.

Major Section: PROGRAMMING

`(strip-cars x)`

is the list obtained by walking through the list
`x`

and collecting up all first components (`car`

s).

`(strip-cars x)`

has a guard of `(alistp x)`

.

Major Section: PROGRAMMING

`(strip-cdrs x)`

has a guard of `(alistp x)`

, and returns the list
obtained by walking through the list `x`

and collecting up all
second components (`cdr`

s).

Major Section: PROGRAMMING

`(Sublis alist tree)`

is obtained by replacing every leaf of
`tree`

with the result of looking that leaf up in the association
list `alist`

. However, a leaf is left unchanged if it is not found
as a key in `alist`

.

Leaves are lookup up using the function `assoc`

. The guard for
`(subsetp alist tree)`

requires `(eqlable-alistp alist)`

. This
guard ensures that the guard for `assoc`

will be met for each
lookup generated by `sublis`

.

`Sublis`

is defined in Common Lisp. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

For any natural numbers `start`

and `end`

, where `start`

`<=`

`end`

`<=`

`(length seq)`

, `(subseq start end)`

is the
subsequence of `seq`

from index `start`

up to, but not including,
index `end`

. `End`

may be `nil`

, which which case it is treated
as though it is `(length seq)`

, i.e., we obtain the subsequence of
`seq`

from index `start`

all the way to the end.

The guard for `(subseq seq start end)`

is that `seq`

is a
true list or a string, `start`

and `end`

are integers (except,
`end`

may be `nil`

, in which case it is treated as `(length seq)`

for ther rest of this discussion), and `0`

`<=`

`start`

`<=`

`end`

`<=`

`(length seq)`

.

`Subseq`

is a Common Lisp function. See any Common Lisp
documentation for more information. Note: In Common Lisp the third
argument of `subseq`

is optional, but in ACL2 it is required,
though it may be `nil`

as explained above.

`member`

of one list is a `member`

of the other
Major Section: PROGRAMMING

`(Subsetp x y)`

is true if and only if every member of the list
`x`

is a member of the list `y`

.

Membership is tested using the function `member`

. Thus, the guard
for `subsetp`

requires that its arguments are true lists, and
moreover, at least one satisfies `eqlable-listp`

. This guard
ensures that the guard for `member`

will be met for each call
generated by `subsetp`

.

`Subsetp`

is defined in Common Lisp. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(Subsetp-equal x y)`

returns `t`

if every member of `x`

is a
member of `y`

, where membership is tested using `member-equal`

.

The guard for `subsetp-equal`

requires both arguments to be true
lists. `Subsetp-equal`

has the same functionality as the Common Lisp
function `subsetp`

, except that it uses the `equal`

function to
test membership rather than `eql`

.

Major Section: PROGRAMMING

`(Subst new old tree)`

is obtained by substituting `new`

for every
occurence of `old`

in the given tree.

Equality to `old`

is determined using the function `eql`

. The
guard for `(subst new old tree)`

requires `(eqlablep old)`

, which
ensures that the guard for `eql`

will be met for each comparison
generated by `subst`

.

`Subst`

is defined in Common Lisp. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`(symbol-< x y)`

is non-`nil`

if and only if either the
`symbol-name`

of the symbol `x`

lexicographially precedes the
`symbol-name`

of the symbol `y`

(in the sense of `string<`

) or
else the `symbol-name`

s are equal and the `symbol-package-name`

of
`x`

lexicographically precedes that of `y`

(in the same sense).
So for example, `(symbol-< 'abcd 'abce)`

and
`(symbol-< 'acl2::abcd 'foo::abce)`

are true.

The guard for `symbol`

specifies that its arguments are symbols.

Major Section: PROGRAMMING

`(Symbol-alistp x)`

is true if and only if `x`

is a list of pairs
of the form `(cons key val)`

where `key`

is a `symbolp`

.

Major Section: PROGRAMMING

The predicate `symbol-listp`

tests whether its argument is a
true list of symbols.

Major Section: PROGRAMMING

Completion Axiom:

(equal (symbol-name x) (if (symbolp x) (symbol-name x) ""))

Guard for `(symbol-name x)`

:

(symbolp x)

Major Section: PROGRAMMING

Completion Axiom:

(equal (symbol-package-name x) (if (symbolp x) (symbol-package-name x) ""))

Guard for `(symbol-package-name x)`

:

(symbolp x)

Major Section: PROGRAMMING

`(symbolp x)`

is true if and only if `x`

is a symbol.

Major Section: PROGRAMMING

For any natural number `n`

not exceeding the length of `l`

,
`(take n l)`

collects the first `n`

elements of the list `l`

.

The following is a theorem (though it takes some effort, including lemmas, to get ACL2 to prove it):

(equal (length (take n l)) (nfix n))If

`n`

is is an integer greater than the length of `l`

, then
`take`

pads the list with the appropriate number of `nil`

elements. Thus, the following is also a theorem.
(implies (and (integerp n) (true-listp l) (<= (length l) n)) (equal (take n l) (append l (make-list (- n (length l))))))For related functions, see nthcdr and see butlast.

The guard for `(take n l)`

is that `n`

is a nonnegative integer
and `l`

is a true list.

Major Section: PROGRAMMING

See any Common Lisp documentation for details.

Major Section: PROGRAMMING

`(The typ val)`

checks that `val`

satisfies the type specification
`typ`

(see type-spec). An error is caused if the check fails,
and otherwise, `val`

is the value of this expression. Here are
some examples.

(the integer 3) ; returns 3 (the (integer 0 6) 3) ; returns 3 (the (integer 0 6) 7) ; causes an errorSee type-spec for a discussion of the legal type specifications.

`The`

is defined in Common Lisp. See any Common Lisp documentation
for more information.

Major Section: PROGRAMMING

See any Common Lisp documentation for details.

Major Section: PROGRAMMING

`True-list-listp`

is the function that checks whether its argument
is a list that ends in, or equals, `nil`

, and furthermore, all of
its elements have that property. Also see true-listp.

Major Section: PROGRAMMING

`True-listp`

is the function that checks whether its argument is a
list that ends in, or equals, `nil`

.

Major Section: PROGRAMMING

Example Forms: ACL2 !>(truncate 14 3) 4 ACL2 !>(truncate -14 3) -4 ACL2 !>(truncate 14 -3) -4 ACL2 !>(truncate -14 -3) 4 ACL2 !>(truncate -15 -3) 5

`(Truncate i j)`

is the result of taking the quotient of `i`

and
`j`

and dropping the fraction. For example, the quotient of `-14`

by
`3`

is `-4 2/3`

, so dropping the fraction `2/3`

, we obtain a result for
`(truncate -14 3)`

of `-4`

.
The guard for `(truncate i j)`

requires that `i`

and `j`

are
rational numbers and `j`

is non-zero.

`Truncate`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

Examples: The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec. Other type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127), (RATIONAL 1 *), CHARACTER, and ATOM.

The type-specs and their meanings (when applied to the variable `x`

as in `(declare (type type-spec x))`

are given below.

type-spec meaning ATOM (ATOM X) BIT (OR (EQUAL X 1) (EQUAL X 0)) CHARACTER (CHARACTERP X) COMPLEX, (AND (COMPLEX-RATIONALP X) (COMPLEX RATIONAL) (RATIONALP (REALPART X)) (RATIONALP (IMAGPART X))) (COMPLEX type) (AND (COMPLEX-RATIONALP X) (p (REALPART X)) (p (IMAGPART X))) where (p x) is the meaning for type-spec type CONS (CONSP X) INTEGER (INTEGERP X) (INTEGER i j) (AND (INTEGERP X) ; See notes below (<= i X) (<= X j)) (MEMBER x1 ... xn) (MEMBER X '(x1 ... xn)) (MOD i) same as (INTEGER 0 i-1) NIL NIL NULL (EQ X NIL) RATIO (AND (RATIONALP X) (NOT (INTEGERP X))) RATIONAL (RATIONALP X) (RATIONAL i j) (AND (RATIONALP X) ; See notes below (<= i X) (<= X j)) (SATISFIES pred) (pred X) SIGNED-BYTE (INTEGERP X) (SIGNED-BYTE i) same as (INTEGER -2**i-1 (2**i-1)-1) STANDARD-CHAR (STANDARD-CHARP X) STRING (STRINGP X) (STRING max) (AND (STRINGP X) (EQUAL (LENGTH X) max)) SYMBOL (SYMBOLP X) T T UNSIGNED-BYTE same as (INTEGER 0 *) (UNSIGNED-BYTE i) same as (INTEGER 0 (2**i)-1)

In general, `(integerp i j)`

means

(AND (INTEGERP X) (<= i X) (<= X j)).But if

`i`

is the symbol `*`

, the first inequality is omitted. If `j`

is the symbol `*`

, the second inequality is omitted. If instead of
being an integer, the second element of the type specification is a
list containing an integer, `(i)`

, then the first inequality is made
strict. An analogous remark holds for the `(j)`

case. The `RATIONAL`

type specifier is similarly generalized.
Major Section: PROGRAMMING

Completion Axiom:

(equal (unary-- x) (if (acl2-numberp x) (unary-- x) 0))

Guard for `(unary-- x)`

:

(acl2-numberp x)Notice that like all arithmetic functions,

`unary--`

treats
non-numeric inputs as `0`

.
Calls of the macro `-`

on one argument expand to calls of
`unary--`

; see -.

Major Section: PROGRAMMING

Completion Axiom:

(equal (unary-/ x) (if (and (acl2-numberp x) (not (equal x 0))) (unary-/ x) 0))

Guard for `(unary-/ x)`

:

(and (acl2-numberp x) (not (equal x 0)))Notice that like all arithmetic functions,

`unary-/`

treats
non-numeric inputs as `0`

.
Calls of the macro `/`

on one argument expand to calls of
`unary-/`

; see /.

Major Section: PROGRAMMING

`(Union-eq x y)`

equals a list whose members
(see member-eq) contains the members of `x`

and the members
of `y`

. More precisely, the resulting list is the same as one
would get by first deleting the members of `y`

from `x`

, and then
concatenating the result to the front of `y`

.

The guard for `union-eq`

requires both arguments to be true lists,
but in fact further requires the first list to contain only symbols,
as the function `member-eq`

is used to test membership (with
`eq`

). See union-equal.

Major Section: PROGRAMMING

`(Union-equal x y)`

equals a list whose members
(see member-equal) contains the members of `x`

and the members
of `y`

. More precisely, the resulting list is the same as one
would get by first deleting the members of `y`

from `x`

, and then
concatenating the result to the front of `y`

.

The guard for `union-equal`

requires both arguments to be true
lists. Essentially, `union-equal`

has the same functionality as
the Common Lisp function `union`

, except that it uses the `equal`

function to test membership rather than `eql`

. However, we do not
include the function `union`

in ACL2, because the Common Lisp
language does not specify the order of the elements in the list that
it returns.

Major Section: PROGRAMMING

`(Update-nth key val l)`

returns a list that is the same as the
list `l`

, except that the value at the `0`

-based position `key`

(a natural number) is `val`

.

If `key`

is an integer at least as large as the length of `l`

, then
`l`

will be padded with the appropriate number of `nil`

elements,
as illustrated by the following example.

ACL2 !>(update-nth 8 'z '(a b c d e)) (A B C D E NIL NIL NIL Z)We have the following theorem.

(implies (and (true-listp l) (integerp key) (<= 0 key)) (equal (length (update-nth key val l)) (if (< key (length l)) (length l) (+ 1 key))))

The guard of `update-nth`

requires that its first (position)
argument is a natural number and its last (list) argument is a true
list.

Major Section: PROGRAMMING

`(Upper-case-p x)`

is true if and only if `x`

is an upper case
character, i.e., a member of the list `#A`

, `#B`

, ..., `#Z`

.

The guard for `upper-case-p`

requires its argument to be a character.

`Upper-case-p`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

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**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 (= 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
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 four idioms all have guards that restrict their Common Lisp executability. If these last four 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 four 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 recurses 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).