Apply$
Apply a badged function or tame lambda to arguments
We recommend that you read the paper ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore for both motivation and foundational details. You might
also read introduction-to-apply$!
This documentation starts with a glossary of terms. Then we
provide some examples and present the specification of
apply$. Next, we deal with issues related to apply$ in
definitions, stating and proving theorems, guards and guard
verification, and top-level evaluation. Finally we exhibit the
formal definitions apply$ and some related concepts. We have
sprinkled in a little tutorial material for readability but have not provided
much motivation for some design decisions.
Glossary
Here is a brief glossary of terms used in the semantics of apply$.
While we provide links to the documentation of the concepts, we urge you not
to follow those links until you've understood the big picture!
- apply$ — the ACL2 function that takes two arguments, one
representing a function and the other listing actuals to be fed to that
function. Under certain conditions, apply$ applies the function to
the arguments and returns the result. Apply$ is mutually recursive
with apply$-lambda, ev$, and ev$-list.
Apply$'s ``badge'' (see below) is (APPLY$-BADGE 2 1 :FN NIL)
its arity is 2, its ``out arity'' is 1 (i.e., it returns 1 result), its
first argument has ``ilk'' :FN and is thus treated as a
``function;'' its second argument has ilk NIL and is thus treated as
an ordinary object.
- badge — an object associated with some function symbols
indicating that apply$ can ``handle'' them and under what
conditions. The badge of a function symbol specifies its arity, its
``out arity,'' (i.e., the number of results the function returns), and
the ilk of each argument position telling apply$ how each
argument is treated. The ilks are :FN, :EXPR and NIL.
The association between a non-primitive function symbol and its badge is
managed by warrants. In proofs, apply$ must have a warrant
for every non-primitive function symbol to be applied. Those warrants
are provided as hypotheses to the theorem being proved. Symbols without
badges cannot be apply$d. Badges are generated, when possible, by
defwarrant. (Badges can be generated for :program mode
functions by defbadge, allowing apply$ to handle such
functions in top level evaluation not in proofs.) Not every function
symbol can have a badge.
- compiled LAMBDA cache (or simply cache in this context) — a
cache in the raw Lisp under ACL2 that supports the application of
apply$ on well-formed, guard verified LAMBDA objects. Later in
this Glossary we define ``lambda expression,'' ``LAMBDA object,''
and ``lambda$ expression'' — three similar looking phrases with very
different meanings. See print-cl-cache for some details of the
cache.
- evaluation theory — the logical theory in which expressions
submitted at the top level of the ACL2 read-eval-print loop are
evaluated. The evaluation theory is a consistent extension of the proof
theory, the latter being the logical theory in which the ACL2 theorem
prover operates. The evaluation theory was introduced in ACL2 when
defattach was added, but it was changed with the introduction of
apply$. All warrants introduced by defwarrant are
assumed true in the evaluation theory but not in the proof theory. This
means ACL2 can execute calls of apply$ that arise in the evaluation
of top-level input, but ACL2 cannot evaluate all calls of apply$
that arise in proofs unless the appropriate warrants are available as
hypotheses. See guarantees-of-the-top-level-loop for some details
of the evaluation theory and how it differs from the proof theory
supported by the ACL2 theorem prover.
- lambda expression — an integral part of ACL2's formal term syntax,
lambda expressions are the way let expressions and other
variable-binding idioms are translated into formal terms. Lambda
expressions have nothing to do with apply$! See lambda for a
discussion of three confusingly similar but different concepts: lambda
expressions, LAMBDA objects, and lambda$ expressions. Read
carefully anytime you see the word ``lambda!''
- LAMBDA object — an ACL2 list constant, typically of the form
(LAMBDA vars body) or (LAMBDA vars dcl body) that may be used
as a ``function'' by apply$. Apply$ treats any consp
object in its first argument position as though it were a LAMBDA
object. But it only gives sensible meanings to tame LAMBDA
objects. And only well-formed LAMBDA objects are executed
efficiently. But well-formed LAMBDA objects are hard to type by
hand — there are many constraints to keep in mind to guarantee
well-formedness. See well-formed-lambda-objectp if you really
want to see all the rules. But that is generally unnecessary. We
strongly recommend not entering LAMBDA objects as quoted
constants, e.g., '(LAMBDA (X) (+ 1 X)) — which is actually
ill-formed! Instead, use lambda$, as in (lambda$ (x) (+ 1
x)). See also lambda for some clarifications.
- lambda$ expression — an ACL2 macro that allows you to enter
quoted well-formed LAMBDA objects into your terms by typing
untranslated expressions that resemble lambda expressions. The
lambda$ expression (lambda$ (x) (+ 1 x)) essentially translates
into the quoted LAMBDA object '(LAMBDA (X) (BINARY-+ '1 X)).
We say ``essentially'' because lambda$ always inserts a
(DECLARE (IGNORABLE v1 ... vn)) listing every formal and tags the
body with a return-last form that indicates it came from a
translated lambda$. See also lambda for some
clarifications.
- scion — a function that is ancestrally dependent on apply$.
In the early days of apply$ we called scions ``mapping functions''
but in the Lisp community that implies iteration over a list and scions
are more general. Of course, a function that iterates over a list
apply$ing a ``function'' to each element and collecting the results
is an example of a scion. But so is function that takes a ``function''
and applies it in one special situation, e.g., as a test or base case.
Any function ancestrally dependent on apply$ is a scion whether or
not it takes a ``function'' as an argument or maps over a domain.
- tame — the class of functions that apply$ knows about; we
actually talk about ``tame functions,'' ``tame LAMBDA objects,'' and
``tame expressions.'' The last are expressions that are evaluable by an
interpreter named ev$ that is mutually-recursive with apply$.
Apply$ cannot handle all definable functions: ACL2 is first order
and if apply$ were able to ``handle'' certain functions the logic
would be inconsistent.
- warrant — a 0-ary predicate associated with some user-defined
function symbols that must be a hypothesis of any theorem whose proof
involves ``expanding'' apply$ on such symbols; the warrant gives
apply$ ``permission'' to expand if the arguments to which the
function is applied are appropriately tame. The warrant for a
function specifies the function's badge and how apply$
behaves on the function symbol. Warrants (and badges) are computed and
introduced by the defwarrant event. Not all function symbols can
be warranted.
You will get a much better understanding of these concepts if you read the
paper cited above.
Examples
To illustrate apply$ and some related concepts we need some
user-defined functions. We therefore imagine that the following events
have been successfully admitted.
We strongly recommend that you include the following book in any
session in which you intend to use or reason about apply$.
(include-book "projects/apply/top" :dir :system)
(defun$ sq (x) (* x x))
(defun$ collect$ (fn lst)
(if (endp lst)
nil
(cons (apply$ fn (list (car lst)))
(collect$ fn (cdr lst)))))
(defun$ foldr (lst fn init)
(if (endp lst)
init
(apply$ fn
(list (car lst)
(foldr (cdr lst) fn init)))))
(defun$ russell (fn x)
(not (apply$ fn (list x x))))
Note: Collect$ is pre-defined in ACL2 because it is part of the
support for the loop$ statement.
Collect$ and foldr might informally be called ``mapping
functions'' because they map a given function over some domain and accumulate
the answers somehow. They are useful examples of what we call scions
of apply$ or simply scions: functions in which apply$ is
ancestral, i.e., functions that call apply$ or call functions that call
apply$, etc. Russell is also a scion. See scion for
more.
Here are some evaluations carried out at the top-level of the ACL2 loop
after the events above. Top-level evaluations take place in ACL2's
evaluation theory (see the discussion of the semantics of defattach),
which is an extension of the theory in which proofs are conducted. Put more
bluntly, the following evaluations won't be carried out in proofs unless you
have the right hypotheses!
ACL2 !>(apply$ 'sq '(5))
25
ACL2 !>(collect$ 'sq '(1 2 3 4 5))
(1 4 9 16 25)
ACL2 !>(collect$ (lambda$ (x) (* x x)) '(1 2 3 4 5))
(1 4 9 16 25)
ACL2 !>(foldr '(1 2 3) 'cons '(4 5 6))
(1 2 3 4 5 6)
ACL2 !>(foldr '(1 2 3 4 5)
(lambda$ (x y)
(cons (sq x) y))
nil)
(1 4 9 16 25)
ACL2 !>(foldr '(1 2 3 4)
(lambda$ (x y) (foldr y 'cons (list x)))
nil)
(4 3 2 1)
ACL2 !>(russell 'natp 3)
NIL
ACL2 !>(russell 'consp 3)
T
Apply$ doesn't always work the way you might want!
ACL2 !>(let ((x 'russell))(russell x x))
ACL2 Error in TOP-LEVEL: The value of APPLY$-USERFN is not specified when
the first argument, fn, is RUSSELL, and the second argument, args,
is (RUSSELL RUSSELL). Fn has badge (APPLY$-BADGE 2 1 :FN NIL) and
args is not known to satisfy the tameness requirement of that badge.
Apply$-userfn is the undefined function called by apply$
when it is asked to apply a user-defined function symbol instead of a builtin
function symbol. The warrant for russell actually specifies the
value of (apply$-userfn 'russell ...) under the tameness
requirements, and those requirements are violated above. This is necessary
to preserve the consistency of the logic. Otherwise:
(russell 'russell 'russell)
= {by defun of russell}
(not (apply$ 'russell (list 'russell 'russell)))
= {by the naive expectation that apply$ always ``works''}
(not (russell 'russell 'russell))
Contradiction!
Top-level evaluation of apply$ expressions raises problems not seen
anywhere else in ACL2's execution model: While executing syntactically legal
terms the evaluator can encounter undefined functions or weirdly ill-formed
terms not caught by the usual ACL2 translation mechanism. The ACL2
translation mechanism checks the well-formedness of lambda$
expressions (and user-typed quoted LAMBDA objects) that occur in
positions of ilk :FN and are therefore destined for apply$. But
the translation checks can be defeated. The LAMBDA object below
contains a call of the undefined function foo but the error is not
caught at translation time; it is caught only when the form executed.
ACL2 !>(apply$ `(lambda (x) (foo x)) '(5))
ACL2 Error in TOP-LEVEL: The value of BADGE-USERFN is not specified
on FOO because FOO is not a known function symbol.
Note the backquote on the LAMBDA object. This defeats the
check of well-formedness because the LAMBDA object is not quoted.
We could have equally written
ACL2 !>(apply$ (list 'lambda '(x) (cons 'foo '(x))) '(5))
with the same result. There is nothing unsound about this. Apply$
can take any objects as arguments. But it won't always ``behave'' as you
might expect. One way to explore the edge cases of apply$ is to execute
it on ill-formed input. In addition, some theorems may require consing up a
LAMBDA object in terms of objects used elsewhere in the theorem. See
example theorem [3] below.
A peculiar aspect of LAMBDA objects is that they can be written as
legal ACL2 constants before they are well-formed LAMBDA objects,
e.g., by referring to undefined functions, :program mode functions,
unbadged functions, etc. They are, after all, just arbitrary quoted objects
and any value in ACL2 can be quoted. But an ill-formed object can
become well-formed if the world is appropriately extended, e.g., the
appropriate defuns, defbadges, and defwarrants are made.
Perhaps worse, they can be well-formed and then become ill-formed by
an undo. So at runtime apply$ has to check that the function symbol or
LAMBDA object is appropriate. There is a sophisticated cache behind the
execution machinery for LAMBDA objects in the evaluation theory. See
print-cl-cache.
Here are some theorems that can be proved about these concepts. The last
of the theorems shown below requires two lemmas, named
weird-little-lemma1 and weird-little-lemma2, shown in
books/projects/apply/report.lisp.
For a summary of how the rewriter handles apply$, ev$, and
loop$ scions, see rewriting-calls-of-apply$-ev$-and-loop$-scions.
; [1] SQ squares, if you have the warrant for sq! Imagine for a moment that
; we could prove (equal (apply$ 'SQ (list i)) (* i i)) without the warrant
; hypothesis shown below. And imagine that we did so in an encapsulated
; environment in which sq was locally defined to be (* x x). Then imagine we
; exported the simpler theorem out of that encapsulate and defined sq to be
; (+ 1 (* x x)). Then ACL2 would be unsound. Exporting a theorem requires
; that the theorem be ancestrally independent of every locally defined
; function and the simpler hypothetical theorem is, because the symbol 'SQ is
; not ancestrally dependent on sq. But ACL2 cannot prove the simpler
; theorem! It cannot ``open'' apply$ on 'SQ without the warrant for sq and
; the warrant for sq is ancestrally dependent on sq. So the theorem below
; cannot be exported from an environment in which sq is locally defined.
; Thus warrants solve the so-called ``LOCAL problem.''
(thm (implies (warrant sq)
(equal (apply$ 'SQ (list i))
(* i i))))
; [2] Collect$ distributes over append for any fn.
(thm (equal (collect$ fn (append a b))
(append (collect$ fn a)
(collect$ fn b))))
; [3] Foldr can be used to collect$, but the collection must
; be with an ``ok'' function (a tame function of one
; argument). Note the backquote on the LAMBDA. This is
; a theorem that requires us to cons up a LAMBDA object.
(thm (implies (ok-fnp fn)
(equal (foldr lst
`(LAMBDA (X Y) (CONS (,fn X) Y))
nil)
(collect$ fn lst))))
Specification of APPLY$
We strongly recommend that you include the following book in any
session in which you intend to use or reason about apply$.
(include-book "projects/apply/top" :dir :system)
General Form:
(apply$ fn args)
where fn is some function symbol or LAMBDA object and args
is a true list. Informally, apply$ applies the function named by the
first argument to the appropriate number of elements taken from the second
argument. We might express this as:
Naive Specification (for a single-valued function):
(apply$ 'fn args) = (fn (nth 0 args) ... (nth (- n 1) args))
Naive Specification (for a multi-valued function):
(apply$ 'fn args) = (mv-list k (fn (nth 0 args) ... (nth (- n 1) args)))
where fn is of arity n and k is the ``out arity'' of
fn (the number of returned values). However, these naive
specifications are guaranteed only if either (i) fn is a function symbol
that has a badge and args satisfies the tameness
requirements of the badge, or (ii) fn is a well-formed LAMBDA
object that returns 1 result. The tameness requirement is that if an element
of args is in an argument position of fn with ilk :FN then the
element must satisfy tamep-functionp and if the element is in an
argument position of ilk :EXPR it must satisfy tamep. See badge for further discussion of condition (i). As for (ii), rather than
explain ``well-formed LAMBDA object'' here we encourage you to write
lambda$ expressions when you want to apply$ a LAMBDA
object.
The ilks of apply$ are :FN and NIL respectively,
telling us that apply$ treats its first argument as a ``function'' and
its second as an ordinary object (never as a function). Initially
apply$ and several functions used in the translation of loop$
statements are the only symbols in ACL2 with an ilk of :FN. However as
defwarrant is used successfully on scions — functions that
somehow call apply$ — user-defined symbols can have ilk :FN
too.
Apply$ has a guard, namely (apply$-guard fn args). This is an
exceptionally weak guard, requiring only that args be a true-list and,
if fn is a cons — which is automatically treated as a LAMBDA
object — the length of args be the length of the second element of
fn. We discuss guards and guard verification in a subsequent
section.
Note for Experts: Technically, apply$ treats any consp
object as a LAMBDA object. But the results are as you'd naively expect
only if the object is a tame LAMBDA object. However, we
frequently write as though the object must be well-formed, which is
different from but implies tameness. 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 to
make it easier to 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 synonymous 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 encourage this by
providing lambda$ and by enforcing full blown well-formedness checks
— not just tameness checks — in translate on every quoted LAMBDA
object entered in a :FN slot. And we give you ways to circumvent these
checks — see gratuitous-lambda-object-restrictions — if you really
mean to supply ill-formed LAMBDA objects to :FN slots.
Badges are assigned by defwarrant, and also by defbadge.
See badge for documentation about how to find out whether a function
has a badge and how to interpret a badge. The terms ``out arity'' and
``tameness requirements,'' used above, are explained there too.
Intuitively, the badge of fn tells apply$ how each formal of
fn is used in the definition of fn and there are only three
``ilks'' of use. Ilk :FN means the formal is used exclusively as a
function, meaning the formal can be passed into :FN slots of other
functions and eventually reaches apply$, but it is never touched by
other ACL2 functions. Ilk :EXPR means the formal is used exclusively as
an expression, meaning the formal may be passed into :EXPR slots of
other functions and eventually reaches ev$, but is never otherwise
touched. Finally, ilk NIL means the formal is treated as an ordinary
ACL2 object and, in particular, never used as either a function or an
expression. The ``tameness requirement'' on each actual is determined by the
ilk of the corresponding formal: actuals in :FN slots must satisfy
tamep-functionp, actuals in :EXPR slots must satisfy tamep,
and there are no requirements on actuals in ilk NIL slots. For
discussions of tamep-functionp and tamep see the topic tame.
Generally speaking, if you want to be able to apply$ a function you
should introduce it with defun and then call defwarrant on
the function name, or use defun$, which is a convenient abbreviation
for the above sequence of events. But defun$ only works for :logic
mode functions because defwarrant enforces that restriction. If you
want to apply$ a :program mode function you should define it with
defun and then call defbadge on its name.
We summarize the specification of apply$ with an example.
Consider
(apply$ 'foldr
'((1 2 3) ; actual 1
cons ; actual 2
(4 5 6))) ; actual 3
The badge of foldr, computed by (badge 'foldr), is
(APPLY$-BADGE 3 1 NIL :FN NIL). The arity is 3, the out arity is
1 (foldr is single-valued) and the ilks list is (NIL :FN NIL).
Thus the first and third formals have ilk NIL and are treated as
ordinary objects; the second formal has ilk :FN and is treated as a
function. Thus, the tameness requirement is that the second actual to a call
of foldr must satisfy tamep-functionp. Referring to the
specification above, we see that the apply$ term has the ``naive
specification'' since foldr has a badge, its out arity is 1, and its
second actual, cons, satisfies tamep-functionp. That is,
(apply$ 'foldr
'((1 2 3) ; actual 1
cons ; actual 2
(4 5 6))) ; actual 3
=
(foldr '(1 2 3) 'cons '(4 5 6))
=
'(1 2 3 4 5 6)
The first equation above is just the naive specification of apply$
and the second equation is just the definition of foldr.
Formals are classified by defwarrant when it tries to compute the
badge of a function. What are the rules that lead to a formal being assigned
ilk :FN, for example? What does ilk :FN actually signify?
Let v be the i th formal parameter of a badged function
fn. If the badge says that v has ilk :FN then we know
that v is ``used as a function'' in the definition of fn ,
i.e., the value of v eventually makes its way into the first argument
of apply$. Furthermore, v is never used any other way: every
place v occurs in the body it is treated as a function. And finally,
in every recursive call of fn v is passed identically in the i
th argument position of every recursive call.
If the badge says that formal variable v has ilk :EXPR then
it signifies 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 formals are ``used as expressions.''
Ev$ is the natural notion of 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.
If the badge says a formal v has ilk NIL in the definition of
fn then v is never used as a function or as an
expression in the definition.
It is the job of defwarrant to analyze a definition and assign
ilks, if possible. But it may not be possible! For example,
(defun foo (x) (apply$ x (list x)))
is such a definition. The formal x is used as a function in its first
occurrence but is not used as a function in its second. Thus
(defwarrant foo)
will fail.
When successful, defwarrant also defines the warrant
function for the function it analyzed. Warrants are crucial to stating and
proving theorems about function symbols being applied with apply$. We
illustrated warrants in the ``Examples'' section above and discuss them
further in the section on ``Theorems Involving Apply$'' below. See also
warrant.
Apply$ is a defined function in the ACL2 source code. We exhibit its
definition at the end of this documentation but you may also see its
definition by doing
ACL2 !>:pe apply$
The definition is mutually recursive with
- apply$-lambda: used by apply$ to handle the case when
the first argument to apply$ is a LAMBDA object.
- ev$: used by apply$-lambda to evaluate the body of a
LAMBDA object in an environment binding the object's formal variables to
the actuals.
- ev$-list: used by ev$ to evaluate a list of expressions in
an environment binding formals to actuals.
Apply$ calls three undefined functions:
- apply$-userfn: used by apply$ when it is asked to apply
anything other than a LAMBDA object or a built-in function symbol. In
the evaluation theory, we attach a function to apply$-userfn that
explicitly enforces the tameness requirements for each user-defined
:logic mode function symbol that has had a badge computed by defwarrant and, if those requirements are met, applies the corresponding
function. Magically, that attachment to apply$-userfn can also evaluate
:program mode functions with badges created by defbadge. We say
``magically'' because there are no axioms that explain this behavior, just as
there are no axioms that explain how you can evaluate ordinary calls of
:program mode functions in the evaluation theory. But in the proof
theory apply$-userfn remains undefined. The value of (apply$-userfn
'fn ...), and thus of (apply$ 'fn ...), is specified by a special
hypothesis, called the ``warrant for fn.'' You can't prove anything
interesting about the behavior of apply$ on a user-defined function
symbol fn unless the warrant for fn is a governing hypothesis. We
discuss warrants in warrant. See also defwarrant.
- untame-apply$: used by apply$ when it is asked to deal with a
situation in which tameness is violated.
- untame-ev$: used by ev$ when it is asked to deal with a
situation in which tameness is violated.
Definitions Involving on Apply$
In one sense, apply$ is just an ordinary ACL2 function that takes two
arguments and returns one result. Like all ACL2 functions, apply$ is
untyped. You can supply any two objects as arguments and the axioms tell you
what the result is — though sometimes the result is delivered by an
undefined function.
But in a deeper sense, if you want apply$ to ``behave,'' and in
particular if you want functions that use apply$ to ``behave,'' you have
to follow certain rules. For example, ACL2 must be able to determine whether
a formal parameter is ``used as a function'' in a given definition.
Basically, you will want every :logic mode function that you define to
be processed by defwarrant so that it gets a badge and warrant if at all
possible and at least has a chance of being applied as expected by
apply$.
The macro defun$ is just an abbreviation for a defun followed by
a defwarrant and it is easy to imagine the other ACL2 definitional
idioms introduced in the ACL2 Community Books eventually being extended to
include a subsequent defwarrant.
So the question becomes ``What rules must a defun obey in order to be
processed successfully by defwarrant?'' The full answer is given in the
documentation for defwarrant. But here are some guidelines to
follow:
- use :logic mode,
- use a measure that either returns a natural number or a
lexicographic combination of natural numbers as defined by the llist
function in the Community Books at books/ordinals/,
- make sure every function used in the definition has a badge,
- ensure that every :FN slot in the body is occupied either by
a formal parameter or a quoted, badged function symbol or lambda$
expression, and
- ensure that no parameter occupying a :FN slot is ever used in a
slot of any other ilk, and
- ensure that every parameter passed into a :FN slot is passed into
the same argument position in any recursive calls of the function being
defined.
You can certainly violate some of these rules and still get an admissible
definition. For example (defun rus (x) (not (apply$ x (list x)))) is
admissible and you can run it on some arguments, e.g., (rus 'consp)
evaluates to T. You can even prove (equal (rus 'consp) t). But
(defwarrant rus) fails because rus violates the rules. So you will
not be able to apply$ 'rus.
Note for Experts: One may wonder why it is possible to warrant a
function, fn, that calls badged but unwarranted functions. Naively one
might expect the semantics of (apply$ 'fn args would involve the
ev$ of the body of fn and therefore require the successful
application (via apply$) of subfunctions in the body. But that
expectation is incorrect. The semantics of (apply$ 'fn args) as
formalized by the warrant for fn says that (under restrictions on the
tameness of the arguments) (apply$ 'fn args) is (fn (car args) (cadr
args) ...).
Theorems Involving Apply$
Because apply$ is undefined on user-defined function symbols and
warrant hypotheses specify the tameness requirements and value of apply$
on such symbols, you can't prove much about the application of particular
user-defined symbols unless you provide the corresponding warrants as
hypotheses.
To emphasize this point, suppose sq has been introduced with
defun$ as shown above, then the following top-level evaluation is
possible:
ACL2 !>(apply$ 'sq '(5))
25
You might expect to be able to prove the obvious little theorem
(thm (equal (apply$ 'sq '(5)) 25))
However, you would be wrong! While ACL2's evaluation theory assumes all
warrants, the proof theory does not. (If it did we could suffer the
LOCAL problem mentioned in example theorem [1] above and in introduction-to-apply$.) Logically, there is no connection between the
symbol 'SQ and the user-defined function sq. That connection is
established by warrant. All the necessary warrants must be explicitly
provided as hypotheses by the user.
The warranted version of the little theorem above is easily proved.
(thm (implies (warrant sq) (equal (apply$ 'sq '(5)) 25)))
Here (warrant sq) is just an abbreviation for a call of the 0-ary
function symbol apply$-warrant-sq which is the name of the warrant for
sq. Apply$-warrant-sq is introduced when (defwarrant sq)
completes successfully. In particular, the following is a theorem:
(warrant sq)
<-->
(force (apply$-warrant-sq))
<-->
(((badge 'SQ) = '(APPLY$-BADGE 1 1 . T))
&
((apply$ 'SQ args) = (sq (car args))))
Note that the warrant macro forces the warrants for the
functions listed. But logically force is just the identity.
Thus, the warrant for sq specifies the value of (badge 'sq) and
of (apply$ 'sq ...). Operationally, by forcing the warrant it means the
absence of a warrant among the hypotheses of a conjecture which is otherwise
provable just results in a forcing round that highlights the need for the
warrant.
If you try to prove the unwarranted version of the little theorem about
'sq it fails in a forcing round with
[1]Goal
(APPLY$-WARRANT-SQ)
This is a clear indication that you forgot to provide the warrant.
You might worry that theorems burdened by warrants are vacuously valid
because it might be impossible to satisfy all the warrant hypotheses. You
needn't worry about this. There is a model of apply$ and all of its
scions that makes every warrant issued by defwarrant valid. The
proof of this is sketched in ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore and fully fleshed out 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.
So there are four lessons here:
Lesson 1: When stating theorems involving apply$ or scions on
concrete user-defined functions, provide as additional hypotheses the
warrants for all user-defined functions that apply$ will encounter
during the proof. This generally means you should add the hypothesis
(warrant fn1 fn2 ... fnk) typically listing every
function symbol that appears inside a quoted constant destined for
apply$ or ev$ in your conjecture. In particular, you should
include every quoted function symbol appearing in a :FN slot of
apply$ or any scion, including every function symbol appearing in the
body of any LAMBDA object or lambda$ term or any until,
when, or body expressions of loop$s. (Macro expansion in
lambda$s and loop$s may introduce function symbols not evident in
the untranslated forms. See :translam and :trans.)
Lesson 2: You need not worry that adding warrant hypotheses makes
your theorems vacuously valid! There is a model of apply$ and all your
scions in which all warrants are valid.
Lesson 3: If a proof involving apply$ or a scion fails in a
forcing round with a checkpoint whose conclusion is the warrant for some
function, you should remember Lesson 1 and include the warrant for that
function symbol in the hypotheses of your conjecture! That is, if you forget
to supply a warrant but your conjecture is otherwise provable, ACL2's
checkpoints will often remind you. (It is possible, in the absence of an
explicit warrant hypothesis, for a proof to fail before the prover detects
that only the warrant is missing.)
Lesson 4: If a proof involving apply$ or a scion fails here
are some things to think about. The basic question is whether something is
``wrong'' with one or more function symbols supposedly handled by
apply$. You have to identify which quoted function symbols are not
being simplified or expanded. Typically you'll see a checkpoint with a term
like (apply$ 'fn ...) or (ev$ '(fn ...) ...) that you expect would
be expanded into an actual call of fn. In that case, fn is of
interest. You should realize that problems of these sorts can drastically
slow down a proof attempt. We have seen example proofs where failure to
simplify an apply$ term slowed the proof-attempt down by several orders
of magnitude. Here are some questions you should ask yourself about
fn.
- Is fn defined and in :logic mode? If fn is in
:program mode it is treated by the prover as an undefined symbol. You
should try to convert it :logic mode with verify-termination.
- Is fn warranted? If not, see defwarrant. If fn is
warranted then it is possible fn is not the problem. Maybe the warrant
for fn was not provided as a hypothesis? Normally, missing warrant
hypotheses are forced, but the proof might have failed for other reasons
before the warrant for fn was forced. But you should ask whether
forcing is disabled; see force.
- If you see (apply$ 'fn ...) then perhaps the rewrite rule
APPLY$-fn is disabled. That rule is the one that forces the warrant for
fn and it was proved when fn was warranted.
- Consider how the rewriter handles apply$ terms, by reading
rewriting-calls-of-apply$-ev$-and-loop$-scions and inspecting
the enabled/disabled status of the runes mentioned there.
These issues are discussed further in the documentation for warrant.
An unfortunate implication of the need for warrants is highlighted during
the proofs of measure conjectures while admitting new definitions.
Consider
(defun$ my-cdr (x) (cdr x))
(defun$ my-len (x)
(if (endp x)
0
(+ 1 (my-len (apply$ 'my-cdr (list x))))))
The definition of my-len fails! The reason is that without the
warrant for my-cdr we cannot prove that the measure decreases in the
recursion above. Unfortunately, there is no way to provide a warrant in a
definition. At the moment we advise users to avoid the use of apply$ —
and functions that use apply$ — in ``termination-critical'' roles. By
that we mean do not use apply$ if its properties are important to proofs
of your measure conjectures. This is easy advice to implement in the case of
my-len, i.e., replace the recursive call above by (my-len (my-cdr
x)). However, in more sophisticated definitions, e.g., where a loop$ is being used in recursive calls and the loop$ calls user-defined
functions in its body, following this advice means replacing that loop$s
by a recursive function. That is unfortunate since the whole point of
loop$ is to avoid the introduction of such functions! We hope to
address this limitation in the future, e.g., by making the definition of
my-len above be conditional on the warrant for my-cdr.
Guards and Guard Verification
As noted, apply$ has a guard of (apply$-guard fn args) and is
itself guard verified. The guard is weak, basically requiring that fn
either be a symbol or a LAMBDA object, that args be a true-list,
and, when fn is a LAMBDA object, the length of the list of formals
is equal to the length of args. To verify the guards of a scion you
must make sure these properties hold of every application of anything in a
:FN slot. Mainly you must make sure that every time a function object
is apply$d, it is applied to a list of the right length.
Note also that mixed-mode-functions, i.e., :logic mode
functions that use :program mode functions in slots of ilk
:FN or :EXPR, cannot be guard verified.
But guards arise in another way in connection with apply$. How does
(apply$ fn args) behave when fn has guards? The short answer is:
logically speaking, apply$ completely ignores guards. Guards in ACL2 are
``extra-logical.''
Let's define and warrant a well-guarded version of ``square'',
(defun$ squ (n) (declare (xargs :guard (natp n))) (* n n))
Squ is guard verified. Now let's consider the little conjecture:
(thm (implies (warrant squ) (equal (apply$ 'SQU (list x)) (* x x))))
Do we need need to require (natp x)? We would if the logical
definition of apply$ checked the guard of fn before interpreting
it. But it does not check. It just behaves as specified above. So,
regardless of whether the guard is satisfied or not, (apply$ 'squ (list
x)) naively expands (under the warrant) to (squ x), from which the
rest of the proof follows.
However, now let's do a top-level evaluation of this apply$ term:
ACL2 !>(apply$ 'SQU (list 'NAN))
ACL2 Error in TOP-LEVEL: The guard for the function call
(SQU N), which is (NATP N), is violated by the arguments
in the call (SQU 'NAN).
(Remember that ACL2's evaluation theory effectively assumes all warrants.)
What happened? Apply$ expanded to (SQU 'NAN) and that caused the
usual guard violation, given the default configuration of set-guard-checking.
A similar guard violation error is signaled if a guarded LAMBDA
object is apply$ed to something violating its guard.
But now consider
(defun$ strange (x)
(declare (xargs :guard t))
(apply$ 'SQU (list x)))
This succeeds and strange is now a guard verified, warranted
function, with a guard of T. This might be surprising since (a) the
guard of strange tells us nothing about x, (b) SQU is applied
to x, and (c) we know the guard of SQU requires its argument to be
a natp. Guard verification ignores the guards of a quoted function
symbol being applied by a scion. This may be particularly offensive to one's
intuitions when the scion is apply$ itself, since the appropriate
information is available. But consider a call of an arbitrary user-defined
scion, e.g., (my-scion 'SQU x). To what arguments will my-scion
apply$ SQU? And how can the definition of my-scion even
specify what functional objects are acceptable in its first argument? This
is a limitation suffered by ACL2 that a logic with a suitably expressive type
system would not suffer. Our way of coping with it is to ignore the guard
here and make sure that when apply$ applies the function symbol executes
it checks the guard of the symbol.
Guard verification does not ignore guards of a quoted lambda object being
apply$ed. Thus, for example, while strange can be guard
verified,
(defun$ stranger (x)
(declare (xargs :guard t))
(apply$ (lambda$ (e) (SQU e)) (list x)))
cannot be guard verified, because guard verification tries to verify the
guards of every lambda object in a :FN slot so that the lambda
object can be marked as guard verified in the compiled lambda cache
(see print-cl-cache). But guards of lambda objects must be
verified independently of the context in which they are used. To be specific,
even
(defun$ stranger (x)
(declare (xargs :guard (natp x)))
(apply$ (lambda$ (e) (SQU e)) (list x)))
cannot be guard verified because the lambda object's guards are
verified independently of the context. The lambda object must carry
its own guard, as in
(defun$ stranger (x)
(declare (xargs :guard (natp x)))
(apply$ (lambda$ (e)
(declare (xargs :guard (natp e)))
(SQU e))
(list x)))
The last definition of stranger can be guard verified, the lambda
object is so marked in the cache and compiled, and if that lambda object
is used in any other context it is recognized as being guard verified. The
guard for that lambda is checked when the object is apply$ed but if
the check approves then the body of the lambda is executed as compiled
code without further guard checking.
While apply$ is not evident in a loop$ statement like
(loop$ for e in lst collect (SQU e))
similar treatment is given. In particular, the loop$ above cannot
be guard verified but
(loop$ for e in lst collect :guard (natp e) (SQU e))
can be and is compiled into a Common Lisp loop. Recall also from
the loop$ documentation that the formal semantics of the above
statement is essentially
(collect$ (lambda$ (e)
(declare (xargs :guard (natp e)))
(SQU e))
lst)
so guard verification of the loop$ also compiles and marks that
lambda expression as guard verified.
So now let's return to consideration of
(defun$ strange (x)
(declare (xargs :guard t))
(apply$ 'SQU (list x)))
which we've seen is guard verified despite the fact that SQU expects
a natural number and will not necessarily be given one. What happens when we
call strange on a non-natural?
ACL2 !>(strange 'NAN)
ACL2 Error in TOP-LEVEL: The guard for the function call (SQU N),
which is (NATP N), is violated by the arguments in the call (SQU 'NAN).
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
? (strange 'nan)
ACL2 Error in ACL2-INTERFACE: The guard for the function call (SQU N),
which is (NATP N), is violated by the arguments in the call (SQU 'NAN).
We see that we can provoke a guard violation with strange
even though it is guard verified with a guard of T. Furthermore,
we get the error both in the ACL2 read-eval-print loop and in the raw
Lisp under ACL2. (Be careful though about exiting the ACL2 loop; see q.)
This might at first violate your understanding of the link between ACL2
and Common Lisp. Naively, a guard verified ACL2 function with a guard of
T never causes a runtime error in Common Lisp. But that's not quite
what the guarantee is. Such a function will never cause a hard Lisp error,
other than possibly resource errors like running out of memory or stack
space. Neither of the errors above were signaled by Common Lisp. They were
``soft'' ACL2 errors. In particular, when apply$ calls squ above,
even when running in raw Lisp, it actually calls the executable counterpart
of squ, which checks guards at runtime and executes properly under the
ACL2 axioms.
ACL2 !>(set-guard-checking :none)
Turning off guard checking entirely.
ACL2 >(strange 'nan)
0
The last evaluation can be explained by the fact that ACL2 multiplication
defaults non-numbers to 0.
We discuss the evaluation of ground apply$ terms in the evaluation
theory further below.
When the guard conjectures of a function are proved all necessary warrants
are assumed. This is unlike what happens when the measure conjectures are
proved. The reason we can assume warrants during guard verification is that
guard verification is relevant in the evaluation theory, where attachments
are allowed and all warrants have true attachments.
Top-Level Evaluation of Apply$
As noted, ACL2's evaluation theory implicitly assumes all warrants
produced by defwarrant. See guarantees-of-the-top-level-loop. Since top-level evaluation in ACL2 is
conducted in the evaluation theory, ground calls of apply$ —
whether literally in top-level input to the ACL2 read-eval-print loop or
hidden inside scions called from the top-level — can be evaluated on
quoted warranted function symbols and lambda$ expressions —
provided the tameness restrictions are met. This is in contrast to
opportunities for evaluation of ground apply$ expressions arising in
proofs, where warrant hypotheses must be explicit.
In this section we focus on calls of apply$ arising in the evaluation
theory. We start with a discussion of the use of apply$ with warranted
:logic mode functions. We then describe how apply$ handles badged
:program mode functions. Note that a mere badge is not
sufficient for evaluation when using apply$ on a :logic mode
function that is not warranted; see defbadge and guarantees-of-the-top-level-loop for discussion of this case. In short:
evaluation involving :logic mode functions is expected to respect the
evaluation theory, and while defwarrant extends the evaluation theory
appropriately, defbadge does not.
Evaluation of apply$ terms in the evaluation theory respects guards
on quoted function symbols and lambda$ expressions (which is to say,
on the quoted well-formed LAMBDA objects that lambda$ produces).
So consider a call of apply$ on fn and args in the evaluation
theory, where fn is a warranted function symbol or a well-formed (and
thus tame) LAMBDA object. Here's what happens. Except where noted, the
description below applies both to warranted :logic and badged
:program mode functions.
Apply$ determines whether fn's tameness restrictions are met by
args. Tameness is a syntactic property and so can be checked. If the
function's tameness restrictions are not met, an error is caused.
If the tameness restrictions are met, apply$ determines whether
fn has been guard verified. In the case of function symbols this is a
simple lookup on the property list of fn. (Of course, this check fails
for :program mode functions.) In the case of LAMBDA objects it is
a cache query (see print-cl-cache) and if the query reveals that we
have not yet tried to verify the guards of this LAMBDA object,
apply$ uses tau reasoning alone (see introduction-to-the-tau-system) to try to verify the guard conjectures.
Note:An important distinction between the runtime handling of
function symbols versus LAMBDA objects by apply$ is that function
symbols can only be guard verified by prior events, e.g., the introductory
defun or a subsequent verify-guards, but apply$ tries to
verify the guards of LAMBDA objects on the fly! The reason for
this distinction is that we anticipate that many LAMBDA objects will not
be associated with any event. For example, an ACL2 macro might generate a
call of a scion on a never-before-seen LAMBDA object and that
LAMBDA object may only be seen by the top-level evaluator. We discuss
this further in verify-guards
If fn is guard verified, apply$ next checks whether fn's
guard holds of the actuals in args. This is done by evaluation of the
compiled code for the guard on args.
If the guard check of args succeeds, a compiled version of fn is
applied to args. If the check fails, a guard violation is signaled or
else the application of fn to args is interpreted under the
definitional axioms of apply$ and ev$, depending on how set-guard-checking has been configured.
Finally, if fn is not guard verified, the application of fn to args
is interpreted under the definitional axioms of apply$ and ev$.
We discuss the cache that supports LAMBDA application in print-cl-cache. See also the discussion of guard verification in lambda$. It should be noted that a LAMBDA object can also be guard
verified using the verify-guards event. This brings the full power
of the prover to bear on the guard verification of the LAMBDA object,
instead of relying just on the tau system.
Users are accustomed to executing :program mode functions at the
top-level of the ACL2 read-eval-print loop. Indeed, the prover itself and
the various event commands are mostly written in :program mode.
Furthermore, the evaluation theory is described as an extension of the proof
theory, i.e., as an axiomatic theory. And yet no part of that axiomatization
explains how :program mode functions are run! It simply isn't
important. The implementation supports it and no questions are asked. We,
the implementors of ACL2, view top-level evaluation of :program mode
functions as a convenience not affecting the consistency of the proof theory.
No inconsistency results from starting a non-terminating computation because
you can never inspect the result, whereas if you added the corresponding
definition as an axiom you might be able to prove something contradictory.
So we regard the seamless execution of :program mode functions as a
convenience to the user who might use them to inspect the ACL2 logical world,
gather data, experiment with constrained formal models by attaching
executable code to unspecified functions, prototype something to be
formalized, etc. In that spirit, we have arranged for apply$ to handle
:program mode functions provided they have badges. Badges are
critical because it means that execution of the functions won't ``go outside
the sandbox.'' However, apply$ runs :program mode functions in
safe-mode to ensure the functional substitutivity of apply$:
identical calls must always yield identical results.
It may seem counterintuitive that a top-level apply$ of a :logic
mode function cannot be executed unless defwarrant has succeeded but a
top-level apply$ of a :program mode function can be executed. As
noted earlier, the reason is simple: execution of :logic mode functions
is justified by the axioms of the evaluation theory while no such assurances
are offered for :program mode functions.
Logical Definitions
In the following definitions, apply$-userfn is an undefined function
that is constrained by warrants to describe the tameness requirement and
behavior of apply$ on specific function symbols. The functions
untame-apply$ and untame-ev$ are simply undefined functions for
giving unspecified values when untame objects are being used.
Function: apply$
(defun apply$ (fn args)
(declare (xargs :guard (apply$-guard fn args)))
(cond ((consp fn) (apply$-lambda fn args))
((apply$-primp fn)
(apply$-prim fn args))
((eq fn 'badge) (badge (car args)))
((eq fn 'tamep) (tamep (car args)))
((eq fn 'tamep-functionp)
(tamep-functionp (car args)))
((eq fn 'suitably-tamep-listp)
(ec-call (suitably-tamep-listp (car args)
(cadr args)
(caddr args))))
((eq fn 'apply$)
(if (tamep-functionp (car args))
(ec-call (apply$ (car args) (cadr args)))
(untame-apply$ fn args)))
((eq fn 'ev$)
(if (tamep (car args))
(ev$ (car args) (cadr args))
(untame-apply$ fn args)))
(t (apply$-userfn fn args))))
Function: apply$-lambda
(defun apply$-lambda (fn args)
(declare (xargs :guard (apply$-lambda-guard fn args)))
(apply$-lambda-logical fn args))
Macro: apply$-lambda-logical
(defmacro apply$-lambda-logical (fn args)
(declare (xargs :guard (symbolp fn)))
(cons
'ev$
(cons (cons 'lambda-object-body
(cons fn 'nil))
(cons (cons 'ec-call
(cons (cons 'pairlis$
(cons (cons 'lambda-object-formals
(cons fn 'nil))
(cons args 'nil)))
'nil))
'nil))))
Function: ev$
(defun ev$ (x a)
(declare (xargs :guard t))
(cond ((not (tamep x)) (untame-ev$ x a))
((variablep x)
(ec-call (cdr (ec-call (assoc-equal x a)))))
((fquotep x) (cadr x))
((eq (car x) 'if)
(if (ev$ (cadr x) a)
(ev$ (caddr x) a)
(ev$ (cadddr x) a)))
((eq (car x) 'apply$)
(apply$ 'apply$
(list (cadr (cadr x))
(ev$ (caddr x) a))))
((eq (car x) 'ev$)
(apply$ 'ev$
(list (cadr (cadr x))
(ev$ (caddr x) a))))
(t (apply$ (car x) (ev$-list (cdr x) a)))))
Function: ev$-list
(defun ev$-list (x a)
(declare (xargs :guard t))
(cond ((atom x) nil)
(t (cons (ev$ (car x) a)
(ev$-list (cdr x) a)))))
Function: apply$-guard
(defun apply$-guard (fn args)
(declare (xargs :guard t))
(if (atom fn)
(true-listp args)
(apply$-lambda-guard fn args)))
Function: apply$-lambda-guard
(defun apply$-lambda-guard (fn args)
(declare (xargs :guard t))
(and (consp fn)
(consp (cdr fn))
(true-listp args)
(equal (len (cadr fn)) (length args))))
Subtopics
- Lambda
- Lambda expressions, LAMBDA objects, and lambda$ expressions
- Warrant
- Giving apply$ permission to handle a user-defined function in proofs
- Defwarrant
- Issue a warrant for a function so apply$ can use it in proofs
- Badge
- Syntactic requirements on a function symbol to be used by apply$
- Lambda$
- Lambda object constructor for use with apply$
- Tame
- Definitions of the various notions of tameness
- Defbadge
- Issue a badge for a function so apply$ can evaluate with it
- Print-cl-cache
- Information about the cache supporting apply$
- Introduction-to-apply$
- Background knowledge on how to use apply$, defwarrant, etc.
- Well-formed-lambda-objectp
- Predicate for recognizing well-formed LAMBDA objects
- Rewriting-calls-of-apply$-ev$-and-loop$-scions
- How the rewriter handles apply$, ev$, and loop$ terms
- Mixed-mode-functions
- :logic mode functions can apply$ :program mode functions
- Explain-giant-lambda-object
- print data related to a large lambda object
- Gratuitous-lambda-object-restrictions
- Enforcement of logically unnecessary restrictions on :FN slots
- Scion
- A function ancestrally dependent on apply$
- Ilk
- Indicator of how an argument is used
- Ev$
- Evaluate a tame expression using apply$
- Translam
- Print the translation of a lambda$ expression
- Fn-equal
- Equivalence relation on tame functions
- Apply$-guard
- The guard on apply$
- L<
- Ordering on naturals or lists of naturals
- Apply$-lambda-guard
- The guard on apply$-lambda
- Apply$-userfn
- Undefined function used by apply$ on non-primitives
- Badge-userfn
- Undefined function used by badge on non-primitives
- Defun$
- Define a function symbol and generate a warrant
- Apply$-lambda
- Used by apply$ on LAMBDA objects
