Defbadge
Issue a badge for a function so apply$ can evaluate with it
It is best to be somewhat familiar with the documentation of apply$ before reading this topic.
Before using defbadge or a utility like defun$ that relies on
it:
(include-book "projects/apply/top" :dir :system)
Badges versus Warrants
It is easy to confuse badges, which are issued by defbadge,
with warrants, which are issued by defwarrant. Badges and
warrants are necessary to ACL2's support of apply$ because ACL2 is
actually first-order, functions cannot be passed around as objects, ordinary
symbols play the role of ``function objects,'' and somehow the logic must
allow the association of a symbol with the function it names. Furthermore,
to insure the consistency of the logic apply$ is not allowed to handle
certain functions such as the russell function illustrated in introduction-to-apply$. But to determine whether a newly defined function
is allowed to be known to apply$, the ACL2 system must be able to
determine, in some sense, all the functions reachable from it. And finally,
to be able to prove theorems about the application of such function names,
the link between the symbols and the functions and the analyzed properties of
the functions must be available to the prover in the form of axioms.
Particularly vexing is the so-called ``local problem'' which raises the
possibility of proving a theorem about the application of a name in the
context of a local definition of the corresponding function and then
exporting that theorem to a context where the name is defined
differently (see Lesson 12 of introduction-to-apply$).
Roughly speaking, badges are about syntax and warrants are about
semantics. The badge for a symbol is a data structure in the ACL2 system
that records information like whether the symbol names a known ACL2 function,
how many arguments that function takes, how many results it returns, which
arguments are treated like function objects to be apply$'d, which are
treated like expressions to be ev$'d, and which are treated like
ordinary ACL2 objects to be car'd, cdr'd, consed, etc. The
warrant for a function is in fact another function (actually a 0-ary
predicate) defined in the logic. That predicate asserts some facts about the
symbol. In particular, it specifies the badge of the symbol and it
constrains the behavior of apply$ on the symbol.
Defbadge analyzes the definition of a function and constructs the
badge if possible. Defbadge does not affect the logic — no
definitions or axioms are added. Defbadge can analyze both
:program mode functions and :logic mode functions.
Defwarrant, on the other hand, can only analyze :logic mode
functions because it must inspect the measure used to justify the termination
of the function and, if it is successful, it adds a :logic mode
definition of the warrant to the logic. This definition links the symbol to
the function via badge and apply$ and if the warrant is a
hypothesis of a conjecture then the prover ``knows'' about the linkage.
Both defbadge and defwarrant affect the top-level
read-eval-print loop because that loop treats :program and :logic
functions differently so that it can (a) allow :program mode terms to be
evaluated to carry out commands such as defun and defthm,
query the world or build and test prototypes, and (b) allow :logic mode
terms to be evaluated while guaranteeing a certain correspondence with what
can be proved. See guarantees-of-the-top-level-loop.
Requirements of Defbadge
General Form:
(defbadge fn)
where fn is a defined function name in either :program
or :logic mode. This command analyzes the body of fn to
determine whether it satisfies certain stringent syntactic conditions
discussed below. If the conditions are not met, defbadge signals an
error. Otherwise, it records a badge for fn. Badges record the
input and output arities of fn and specify which arguments are
``functions'' that may be applied with apply$, which are ``expressions''
that may be evaluated with ev$, and which are neither. The
conditions checked are sufficient to allow apply$ to run the function
safely at the top level of the ACL2 read-eval-print loop. However, in order
to prove anything about a call of apply$ on fn — or even to
evaluate such a call if fn is in :logic mode, as discussed
above — fn will need a warrant as issued by defwarrant. Defbadge does not issue warrants, just badges.
Defwarrant can issue both badges and warrants.
The first condition on fn is that it must be a defined function
symbol. Since fn must be defined it may not be a constrained function
such as one introduced by defchoose or encapsulate. In
addition, fn may not be one of a very few ``blacklisted'' symbols (see
the value of *blacklisted-apply$-fns*) like sys-call (which
requires a trust tag) or an untouchable. (For technical reasons,
untouchables are disallowed even if they are on temp-touchable-fns; see
remove-untouchable.)
The other conditions depend on whether apply$ is reachable from
fn. That is, can a call of fn lead to a call of apply$? If
apply$ is not reachable from fn, then there are no more conditions
on fn. A badge for fn is computed and stored. We are more precise
about ``reachability'' later.
If apply$ is reachable from fn, then there are additional
conditions that must be checked. First, fn must not have been
introduced with mutual-recursion. The current badging machinery is
unable to enforce the syntactic restrictions for mutually-recursive cliques.
Another restriction is that every function mentioned in the body of fn,
except fn itself, must already have a badge. Finally, fn must
respect certain conventions regarding its use of apply$ and other
scions. The basic idea of this last restriction is to make sure that
apply$ is always called on a ``known'' function symbol or lambda
object. This restriction is enforced by checking the following
conditions:
(a) It must be possible for each formal of fn to be assigned
one of three ilks, :FN, :EXPR, or NIL, as described
below. The basic idea is that a formal can be assigned ilk :FN (or ilk
:EXPR) iff it is sometimes passed into a :FN (or :EXPR) slot
in the body of fn and is never passed into any other kind of slot. A
formal can be be assigned ilk NIL iff it is never passed into a slot of
ilk :FN or :EXPR, i.e., if it is used exclusively as an
``ordinary'' object. We are more precise below.
(b) Every :FN and :EXPR slot of every function called in
the body of fn is occupied either by a formal of fn of the same ilk
or, in the case of calls of functions other than fn, a quoted tame function symbol or quoted tame (preferably well-formed) LAMBDA
object. (See well-formed-lambda-objectp.)
This completes the list of restrictions imposed by defbadge.
Discussion and Examples
Note that if apply$ is not reachable from fn, the restrictions
imposed on fn are comparatively generous. Such a fn could be
badged and warranted despite being defined mutually recursively or in terms
of unbadged or even unbadgeable functions. Basically, if fn doesn't
depend on apply$ there is no danger that some argument of fn will
be treated like a function object or an expression.
After a successful defbadge event for fn, the function badge will return the computed badge (when executed in the top-level loop)
and apply$ will be able to accept the fn as a functional
argument. Here is an annotated script. First, carry out these two events,
defining foldr as a :program mode function.
(include-book "projects/apply/top" :dir :system)
(defun foldr (lst fn init)
(declare (xargs :mode :program))
(if (endp lst)
init
(apply$ fn
(list (car lst)
(foldr (cdr lst) fn init)))))
Note the apply$ call in the definition. We see that foldr
treats its middle argument, fn, as a function of arity 2. We can run
foldr, even without assigning a badge to foldr, as long as we
supply a badged function symbol of arity 2 as the middle argument. Since
the ACL2 primitive cons has a badge and has arity 2, we can use it:
ACL2 !>(foldr '(a b c) 'cons '(d e f))
(A B C D E F)
Since foldr has arity 3, we can try to apply it to a list of three
things.
(apply$ 'foldr (list '(a b c) 'cons '(d e f)))
ACL2 Error in TOP-LEVEL: The value of APPLY$-USERFN is not specified
on FOLDR because FOLDR has not been badged.
However, we can use defbadge to compute and store the badge for
foldr. The badge says foldr has input arity 3, output arity 1, and
treats its middle argument as a function. We can recover the badge by
calling the function badge. We can successfully apply foldr.
We can even use it in a lambda expression that we pass as the middle
argument to foldr.
ACL2 !>(defbadge foldr)
FOLDR now has the badge (APPLY$-BADGE 3 1 NIL :FN NIL) but has no warrant.
T
ACL2 !>(badge 'foldr)
(APPLY$-BADGE 3 1 NIL :FN NIL)
ACL2 !>(apply$ 'foldr (list '(a b c) 'cons '(d e f)))
(A B C D E F)
ACL2 !>(foldr '((a b c) (d e) (f g h) (i j k))
(lambda$ (x y)
(foldr x 'cons y))
nil)
(A B C D E F G H I J K)
The ``Reachability'' Test
We now clarify the test that we colloquially described above as whether
apply$ is reachable from fn. The actual test is whether
apply$-userfn is ancestral in fn. That is, does fn call
apply$-userfn, or a function that calls apply$-userfn, or a
function that calls a function that calls apply$-userfn, etc.
Since the only system functions that call apply$-userfn are
apply$, ev$, and warrants, and since it is very unusual for
a user-defined function to call directly apply$-userfn, ev$, or
warrants, we think of this test colloquially as whether apply$ is
ancestral in fn.
The test and the onerous conditions imposed when apply$ is reachable
is crucial to the soundness of the ACL2 proof theory. We discuss this
further in the background material for apply$, including ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore and offer a fully fleshed out metalevel proof that
apply$ and all :logic-mode scions can be modeled in the comment
titled Essay on Admitting a Model for Apply$ and the Functions that Use
It in the ACL2 source file apply-raw.lisp.
But badges are more concerned with syntax (and, for :program mode
functions, evaluation) than the proof theory. Even if we convert foldr
to :logic mode we cannot prove anything interesting about what happens
when it is applied with apply$. We can't even prove that foldr has
a badge or what that badge is!
ACL2 !>(verify-termination foldr)
[Successful. Output deleted.]
FOLDR
ACL2 !>(thm
(equal (apply$ 'foldr (list x 'cons z))
(append x z)))
[Unsuccessful. Output deleted.]
******** FAILED ********
ACL2 !>(thm
(equal (badge 'foldr) '(APPLY$-BADGE 3 1 NIL :FN NIL)))
[Unsuccessful. Output deleted.]
******** FAILED ********
In order to prove anything nontrivial about foldr's badge or behavior
under apply$ we need the warrant for foldr. Warrants are
issued by defwarrant. If we execute (defwarrant foldr) and then
amend the failed thm commands above by adding (warrant foldr) as a
hypothesis, both amended formulas are provable.
How Ilks Are Assigned
If a formal variable (or its slot among the actuals) has an ilk of
:FN then the variable is ``used as a function'' in the sense that it
might eventually reach the first argument of a call of apply$ and is
never passed into an ``ordinary'' slot like those for cons. Similarly,
an ilk of :EXPR means the variable is ``used as an expression'' and may
eventually reach the first argument of ev$. An ilk of NIL means
the variable is never used as a function or an expression. The correctness
of this algorithm is crucial to the safe evaluation of apply$ on
user-defined function symbols. It also is crucial to the termination
argument justifying the consistency of the proof theory created if and when
fn is warranted.
The key to the inductive correctness of the algorithm implicitly described
below is the fact that when the ACL2 logic is being booted up the only
function symbol with a slot of ilk :FN is apply$ and the only
function with a slot of ilk :EXPR is ev$. In both functions it is
the first argument slot that is so distinguished. All other ACL2 primitives
that use apply$ or ev$, e.g., collect$, are defined,
admissible, badged, and warranted under the same conditions user-defined
functions are.
Let v be the i th formal parameter of a defined function
fn. Then the ilk of v is :FN iff the value of v
eventually makes its way into the first argument of apply$, either in
the definition of fn or in some function ancestral to (i.e., eventually
called by) fn. Another way to say this is that there is an occurrence
of v in a slot of ilk :FN. Furthermore, v is never used
any other way: every place v occurs in the body of fn is in a
slot of ilk :FN. And finally, in every recursive call of fn ,
v is passed identically in the i th argument position of the
call. We say such a v is ``used (exclusively) as a function.''
The i th formal variable v has ilk :EXPR under
analogous conditions except that instead of eventually getting into the first
argument of apply$ it eventually gets into the first argument of
ev$. We say such a v is ``used (exclusively) as an
expression.'' Note: ev$ is the natural notion of expression
evaluation in this context: look up the values of variables in the alist
argument to ev$, return quoted constants, and otherwise apply$
function symbols and LAMBDA objects to the recursively obtained list of
values returned by evaluating the actuals. However, ev$ first checks
that the expression is tamep.
The i th formal variable v has ilk NIL if it never
occurs in a :FN slot and never occurs in an :EXPR slot. We say
such a v is ``used (exclusively) as an ordinary object.''
