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
**definitions**, **stating and proving theorems**, **guards and guard
verification**, and **top-level evaluation**. Finally we exhibit the
**formal definitions**

Here is a brief glossary of terms used in the semantics of

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 ilkNIL and is thus treated as an ordinary object.`badge`— an object associated with some function symbols indicating thatapply$ 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 tellingapply$ how each argument is treated. The ilks are:FN ,:EXPR andNIL . The association between a non-primitive function symbol and its badge is manged by`warrant`s. 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 beapply$ d. Badges are generated, when possible, by`defwarrant`. (Badges can be generated for: program mode functions by`defbadge`, allowingapply$ 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 ofapply$ on well-formed, guard verifiedLAMBDA 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 ofapply$ . All`warrant`s introduced bydefwarrant are assumed true in the evaluation theory but not in the proof theory. This means ACL2 can execute calls ofapply$ that arise in the evaluation of top-level input, but ACL2 cannot evaluate all calls ofapply$ 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 withapply$ ! See lambda for a discussion of three confusingly similar but different concepts: lambda expressions,LAMBDA objects, andlambda$ 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'' byapply$ .Apply$ treats any`consp`object in its first argument position as though it were aLAMBDA object. But it only gives sensible meanings to tameLAMBDA objects. And only well-formedLAMBDA objects are executed efficiently. But well-formedLAMBDA 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 enteringLAMBDA 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-formedLAMBDA objects into your terms by typing untranslated expressions that resemble lambda expressions. Thelambda$ expression(lambda$ (x) (+ 1 x)) essentially translates into the quotedLAMBDA object'(LAMBDA (X) (BINARY-+ '1 X)) . We say ``essentially'' becauselambda$ 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 translatedlambda$ . See also lambda for some clarifications.`scion`— a function that is ancestrally dependent onapply$ . In the early days ofapply$ 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 listapply$ 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 onapply$ 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,'' ``tameLAMBDA objects,'' and ``tame expressions.'' The last are expressions that are evaluable by an interpreter named`ev$`that is mutually-recursive withapply$ .Apply$ cannot handle all defineable functions: ACL2 is first order and ifapply$ 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 givesapply$ ``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 howapply$ 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.

To illustrate

**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: `loop$` statement.

*scions
of* *scions*: functions in which

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

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 `warrant` for `tame`ness
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 `lambda$`
expressions (and user-typed quoted

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

ACL2 !>(apply$ (list 'lambda '(x) (cons 'foo '(x))) '(5))

with the same result. There is nothing unsound about this.

A peculiar aspect of *before* they are well-formed *become* well-formed if the world is appropriately extended, e.g., the
appropriate *become* ill-formed by
an undo. So at runtime `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

For a summary of how the rewriter handles

; [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))))

**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

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 **However**, these naive
specifications are guaranteed only if either (i) `badge` and `badge` for further discussion of condition (i). As for (ii), rather than
explain ``well-formed `lambda$` expressions when you want to

The ilks of `defwarrant` is used successfully on scions — functions that
somehow call

**guards and guard verification** in a subsequent
section.

**Note for Experts**: Technically, *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 `lambda$` and by enforcing full blown well-formedness checks
— not just tameness checks — in translate on every quoted

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 `ev$`, but is never otherwise
touched. Finally, ilk

Generally speaking, if you want to be able to `defun` and then call `defwarrant` on
the function name, or use `defun$`, which is a convenient abbreviation
for the above sequence of events. But

We summarize the specification of

(apply$ 'foldr '((1 2 3) ; actual 1 cons ; actual 2 (4 5 6))) ; actual 3

The badge of

(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

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

Let *v* be the *i *th formal parameter of a badged function
*fn*. If the badge says that *v* has ilk *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 *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 `Ev$` is the natural notion of evaluation in this context: look up the
values of variables in the alist argument to `tamep`.

If the badge says a formal *v * has ilk *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

(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 `warrant`.

ACL2 !>:pe apply$

The definition is mutually recursive with

`apply$-lambda`: used byapply$ to handle the case when the first argument toapply$ is aLAMBDA object.`ev$`: used byapply$-lambda to evaluate the body of aLAMBDA object in an environment binding the object's formal variables to the actuals.`ev$-list`: used byev$ to evaluate a list of expressions in an environment binding formals to actuals.

`apply$-userfn`: used byapply$ when it is asked to apply anything other than aLAMBDA object or a built-in function symbol. In the evaluation theory, we attach a function toapply$-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 toapply$-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 theoryapply$-userfn remains undefined. The value of(apply$-userfn 'fn ...) , and thus of(apply$ 'fn ...) , is specified by a special hypothesis, called the ``warrant forfn .'' You can't prove anything interesting about the behavior ofapply$ on a user-defined function symbolfn unless the warrant forfn is a governing hypothesis. We discuss warrants in`warrant`. See also`defwarrant`.untame-apply$ : used byapply$ when it is asked to deal with a situation in which tameness is violated.untame-ev$ : used byev$ when it is asked to deal with a situation in which tameness is violated.

In one sense,

But in a deeper sense, if you want

The macro

So the question becomes ``What rules must a `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 atbooks/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

**Note for Experts**: One may wonder why it is possible to warrant a
function,

Because

To emphasize this point, suppose

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

The warranted version of the little theorem above is easily proved.

(thm (implies (warrant sq) (equal (apply$ 'sq '(5)) 25)))

Here

(warrant sq) <--> (force (apply$-warrant-sq)) <--> (((badge 'SQ) = '(APPLY$-BADGE 1 1 . T)) & ((apply$ 'SQ args) = (sq (car args))))

Note that the `warrant` macro `force`s the warrants for the
functions listed. But logically

Thus, the warrant for

If you try to prove the unwarranted version of the little theorem about

[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

So there are four lessons here:

**Lesson 1:** When stating theorems involving `(warrant `*fn1 fn2 ... fnk*`)` typically listing every
function symbol that appears inside a quoted constant destined for
`translam` and `trans`.)

**Lesson 2:** You need not worry that adding warrant hypotheses makes
your theorems vacuously valid! There is a model of

**Lesson 3:** If a proof involving

**Lesson 4:** If a proof involving

- Is
fn defined and in:logic mode? Iffn 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`. Iffn is warranted then it is possiblefn is not the problem. Maybe the warrant forfn was not provided as a hypothesis? Normally, missing warrant hypotheses are forced, but the proof might have failed for other reasons before the warrant forfn was forced. But you should ask whether forcing is disabled; see`force`. - If you see
(apply$ 'fn ...) then perhaps the rewrite ruleAPPLY$-fn is disabled. That rule is the one that forces the warrant forfn and it was proved whenfn 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 `loop$` is being used in recursive calls and the

As noted,

Note also that mixed-mode-functions, i.e.,

But guards arise in another way in connection with

Let's define and warrant a well-guarded version of ``square'',

(defun$ squ (n) (declare (xargs :guard (natp n))) (* n n))

(thm (implies (warrant squ) (equal (apply$ 'SQU (list x)) (* x x))))

Do we need need to require

However, now let's do a top-level evaluation of this

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? `set-guard-checking`.

A similar guard violation error is signalled if a guarded

But now consider

(defun$ strange (x) (declare (xargs :guard t)) (apply$ 'SQU (list x)))

This succeeds and

Guard verification does not ignore guards of a quoted lambda object being

(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 `print-cl-cache`). But guards of

(defun$ stranger (x) (declare (xargs :guard (natp x))) (apply$ (lambda$ (e) (SQU e)) (list x)))

cannot be guard verified because the

(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

While `loop$` statement like

(loop$ for e in lst collect (SQU e))

similar treatment is given. In particular, the

(loop$ for e in lst collect :guard (natp e) (SQU e))

can be and is compiled into a Common Lisp `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

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

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

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

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

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.

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 `lambda$` expressions —
provided the tameness restrictions are met. This is in contrast to
opportunities for evaluation of ground

In this section we focus on calls of *not*
sufficient for evaluation when using `defbadge` and guarantees-of-the-top-level-loop for discussion of this case. In short:
evaluation involving

Evaluation of `lambda$` expressions (which is to say,
on the quoted well-formed `lambda$` produces).
So consider a call of

If the tameness restrictions are met, `print-cl-cache`) and if the query reveals that we
have not yet tried to verify the guards of this

**Note:**An important distinction between the runtime handling of
function symbols versus `defun` or a subsequent *on the fly*! The reason for
this distinction is that we anticipate that many `verify-guards`

If

If the guard check of `set-guard-checking` has been configured.

Finally, if

We discuss the cache that supports `print-cl-cache`. See also the discussion of guard verification in `lambda$`. It should be noted that a `verify-guards` event. This brings the full power
of the prover to bear on the guard verification of the

Users are accustomed to executing *provided they have badges*. Badges are
critical because it means that execution of the functions won't ``go outside
the sandbox.'' However, `safe-mode` to ensure the functional substitutivity of

It may seem counterintuitive that a top-level

In the following definitions,

**Function: **

(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: **

(defun apply$-lambda (fn args) (declare (xargs :guard (apply$-lambda-guard fn args))) (apply$-lambda-logical fn args))

**Macro: **

(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: **

(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: **

(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: **

(defun apply$-guard (fn args) (declare (xargs :guard t)) (if (atom fn) (true-listp args) (apply$-lambda-guard fn args)))

**Function: **

(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))))

- Lambda
- Lambda expressions,
LAMBDA objects, andlambda$ 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$ - Well-formed-lambda-objectp
- Predicate for recognizing well-formed
LAMBDA objects - Introduction-to-apply$
- Background knowledge on how to use
`apply$`,`defwarrant`, etc. - Rewriting-calls-of-apply$-ev$-and-loop$-scions
- How the rewriter handles
apply$ ,ev$ , andloop$ terms - Mixed-mode-functions
: `logic`mode functions can`apply$`: `program`mode functions- 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$ onLAMBDA objects