Common Lisp functions are partial; they are not defined for all possible inputs. But ACL2 functions are total. Roughly speaking, the logical function of a given name in ACL2 is a completion of the Common Lisp function of the same name obtained by adding some arbitrary but ``natural'' values on arguments outside the ``intended domain'' of the Common Lisp function.
ACL2 requires that every ACL2 function symbol have a ``guard,''
which may be thought of as a predicate on the formals of the
function describing the intended domain. The guard on the primitive
function car 
, for example, is (or (consp x) (equal x nil)),
which requires the argument to be either an ordered pair or
nil. We will discuss later how to specify a guard for a
defined function; when one is not specified, the guard is t which
is just to say all arguments are allowed.
But guards are entirely extra-logical: they are not involved in the axioms defining functions. If you put a guard on a defined function, the defining axiom added to the logic defines the function on all arguments, not just on the guarded domain.
So what is the purpose of guards?
The key to the utility of guards is that we provide a mechanism,
called ``guard verification,'' for checking that all the guards in a
formula are true. See VERIFY-GUARDS. This mechanism will attempt
to prove that all the guards encountered in the evaluation of a
guarded function are true every time they are encountered.
For a thorough discussion of guards, see the paper [km97] in the
ACL2 bibliography.
