Badge
Syntactic requirements on a function symbol to be used by apply$
``Badge'' is both the name of an ACL2 function and the name of a
concept key to the apply$ machinery. We discuss the function named
badge first. The discussion also mentions the concept of warrants,
which are easily confused with badges. See the discussion of Badges
versus Warrants at the top of defbadge. But roughly put, badges
extend the ACL2 syntax and warrants extend the proof theory. You'll need a
badge for fn to allow the system to syntactically analyze (apply$ 'fn
...). You'll need a both a badge and a warrant for fn if you wish to
reason about that term with ACL2.
General Form:
(badge fn)
The argument, fn, is expected to be a function symbol. If fn is
one of about 800 ACL2 primitives (discussed below) or is a user-defined
function successfully processed by either the event defbadge or the
event defwarrant, the result is an object, called the ``badge'' of
fn, which among other things specifies the ilk of each formal of
fn. Otherwise, an error is caused. We explain below, where we define
the concepts of the ``out arity,'' ``ilks,'' and ``tameness requirements'' of
fn's badge.
A function symbol must have a badge in order to apply$ the symbol and
it is up to you, the user, to invoke an event that will assign a badge to
your user-defined functions, if possible. Defbadge will assign a badge
to a function symbol, if possible, and defwarrant will assign both a
badge (if the function symbol doesn't already have one) and a warrant, if possible. The macro defun$ is just an abbreviation for
a defun followed by a defwarrant. Almost all primitive system
functions already have badges.
The complete list of badged primitives can be seen by evaluating
(append '(BADGE TAMEP TAMEP-FUNCTIONP SUITABLY-TAMEP-LISTP
APPLY$ EV$)
(strip-cars *badge-prim-falist*))
Badge is a defined function in ACL2. You can inspect its definition
with
ACL2 !>:pe badge
and see that after handling the built-in symbols it defers to the
undefined function badge-userfn. In the evaluation theory,
badge-userfn has an attachment that returns the badge computed by
defbadge or defwarrant. But in the proof theory, badge-userfn
is undefined and the warrant for fn specifies the badge of
fn. Thus, in the proof theory, you cannot reason about the application
of a non-primitive function unless there is a warrant for the function
available as a hypothesis.
The rest of this documentation illustrates and explains what badges mean,
starting with a few examples.
ACL2 !>(badge 'cons)
(APPLY$-BADGE 2 1 . T)
ACL2 !>(badge 'apply$)
(APPLY$-BADGE 2 1 :FN NIL)
ACL2 !>(badge 'foldr)
(APPLY$-BADGE 3 1 NIL :FN NIL)
The last example assumes that foldr has been defined with
(defun$ foldr (lst fn init)
(if (endp lst)
init
(apply$ fn
(list (car lst)
(foldr (cdr lst) fn init)))))
In general, badges have the form (APPLY$-BADGE n k . ilks), where
n is the arity of fn, k is the out arity (i.e., the number of
results returned by fn) and ilks is either T or a list of
n tokens. Each token is either :FN, :EXPR, or NIL.
The badge of fn, if any, is computed when the event (defbadge
fn) or (defwarrant fn) completes successfully. See defbadge
for a sketch of the algorithm used to compute badges. Here though we are
just concerned with how badges impact apply$.
The ilks of a function, fn, determines the ``tameness
requirements'' mentioned in the specification of apply$. When the
ilks component of fn's badge is a list, it has as many elements as
there are formals to fn and each successive element is called the
ilk of the corresponding formal. For example, given the definition of
foldr above and the badge shown for it, the first and third formals,
lst and init, each have ilk NIL and the second formal,
fn, has ilk :FN. In the special case that ilks is not a list
it is T and we just say each formal has ilk NIL -- treating
that T as a suitably long list of NILs.
Each non-NIL ilk imposes a tameness requirement on (apply$
fn args). If a formal has ilk :FN the corresponding element of
args must satisfy tamep-functionp. If a formal has ilk :EXPR
the corresponding element of args must satisfy tamep. Ilk NIL
imposes no requirement. (Thus, if the ilks of fn's badge is
T, as it is for cons for example, there is no tameness requirement
at all.) See tame for a discussion of the various notions of
tameness.
Informally, if a formal's ilk is :FN, the corresponding element of
args must be a tame function symbol or well-formed LAMBDA object.
If a formal's ilk is :EXPR, the corresponding element of args must
be a tame expression.
If a formal has ilk :FN then you are allowed to put a lambda$
expression in that slot. Any quoted LAMBDA object you explicitly write
in such a slot must be well-formed (see well-formed-lambda-objectp).
Well-formedness can be hard to achieve in quoted hand-written LAMBDA
objects; we recommend that you use lambda$! But the restrictions on
what can occupy a :FN slot are enforced when user input is translated
into formal terms. It is possible to circumvent these syntactic checks
without endangering soundness: axiomatically apply$ puts no restrictions
on its arguments, it just doesn't behave the way you might expect on
ill-formed LAMBDA objects. See gratuitous-lambda-object-restrictions.
Clarification: The careful reader will note that the formal
requirement on a :FN argument is that it must satisfy
tamep-functionp. Inspection of the definition of tamep-functionp
reveals that the argument must either be badged symbol with ilks T or
else be a tame LAMBDA object. But in the informal description above we
said that it must be a ``tame function symbol or a well-formed
LAMBDA object.'' Well-formedness implies tameness but they are not the
same. What's going on? The reason for this and related discrepancies in the
documentation is that there is a tension between the logical definition of
apply$ and the practical business of executing it. The former involves
the existence of a model, soundness, and the difficulty of proving theorems
about apply$. The latter involves the Common Lisp compiler. We want
the logical foundations to be simple so we -- and you -- can reason about
apply$, but the compiler imposes unavoidable and complicated
restrictions. The upshot is that the logical foundations assign meaning to
LAMBDA objects that cannot be compiled. Applying merely ``tame''
LAMBDAs is slower than applying ``well-formed'' ones. In a sense by
acting like ``tame LAMBDA objects'' and ``well-formed LAMBDA
objects'' are the same thing we're trying to trick you! If you ever have
occasion to formally express the restrictions on apply$ in some theorem,
use tamep-functionp. But when you write concrete LAMBDA constants,
try to keep them well-formed. We try to encourage this by providing
lambda$, which guarantees well-formedness at translate-time, and by
implementing full well-formedness checks -- not just tameness checks -- on
quoted LAMBDA objects in :FN slots. And we give you ways to
circumvent these checks -- see gratuitous-lambda-object-restrictions
-- if you really mean to.
