Background knowledge on how to use `apply$`, `defwarrant`, etc.

The paper ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann and
J Strother Moore best explains the basic logical and practical ideas behind
`apply$` for detailed documentation on

The unreachable goal of this work is to allow the ACL2 user to pass
`functions' as objects and to apply them. That goal is unreachable because
ACL2 remains a first order system. However, we can identify a certain
syntactic class of ordinary ACL2 objects, called the `tame
functions' (which are in fact *not* functions but are merely symbols and
list expressions) and we can allow names of functions with certain tameness
properties to be passed around and used as functions.

``Tameness'' imposes strict rules on how functional arguments are used.
We'll discuss it further below but tame functions are recognized by the

The fundamental question raised by

The ACL2 primitives can be built in. The logical definition of

(apply$ 'car (list a)) = (car a)

and

(apply$ 'assoc-equal (list a b)) = (assoc-equal a b).

But user-defined functions are problematic because once

Intuitively, if you have defined the

forall a1...an : (apply$ 'foo (list a1...an)) = (foo a1...an).

It will turn out that using new axioms for this purpose is a bad idea.
Hiding the link between `local`. We illustrate this problem
later in this doc topic. But for that reason, the suppositions extending
`warrant`s.''

Warrant (Merriam-Webster): (noun) a commission or document giving authority to do something....

In our case, a warrant for `badge` of

But there is a fundamental logical problem: it is not always possible to
satisfy such suppositions. There may be no way that

(defun russell (x y) (not (apply$ x (list y y)))).

This definition of

forall x,y : (apply$ 'russell (list x y)) = (russell x y)

then we would have this classical problem with self-reference:

(russell 'russell 'russell) = {def russell} (not (apply$ 'russell (list 'russell 'russell))) = {warrant russell} (not (russell 'russell 'russell))

which is contradictory.

This problem is addressed by introducing the notion of ``tameness.''
Tameness is a syntactic property of terms and functions that implies that it
is ok to ``extend''

It should be pretty clear that if the user defines an ACL2 function that
in no way depends on

(defun sq (x) (* x x))

then the hypothesis

forall x : (apply$ 'SQ (list x)) = (sq x)

is satisfiable: we could have introduced

For example, consider the following function, which maps a given function over a list and collects the results.

(defun collect$ (fn lst) (if (endp lst) nil (cons (apply$ fn (list (car lst))) (collect$ fn (cdr lst)))))

Our definition of tameness considers `(collect$ 'SQ lst)` to be a
tame expression, even though `(collect$ 'SQ lst)` is a tame
expression, then `'(LAMBDA (LST) (COLLECT$ 'SQ LST))` is a tame
function and thus

(collect$ '(LAMBDA (LST) (COLLECT$ 'SQ LST)) z)

is a tame expression. So, for example, at the top-level of ACL2 one can do this:

ACL2 !>(collect$ '(LAMBDA (LST) (COLLECT$ 'SQ LST)) '((1 2 3) (4 5 6) (7 8 9))) ((1 4 9) (16 25 36) (49 64 81))

Of course, this presumes we have defined `(collect$ 'SQ lst)`.) To use
`defun$`, which is just an ordinary `defun`
followed by a `defwarrant` command. If you've already defined the
function and then realize you wish to

`logic` mode definition and
produces a badge and a warrant, if possible. Also relevant is the `defbadge` command which issues a badge for a function (if possible) but does
not issue a warrant. Its primary purpose is to allow

We explain further via an annotated example, starting from scratch but
from the basic background just sketched. For many additional examples, see
community-books

**Note carefully:** the directory

To get started, define two ordinary ACL2 functions, one that squares its argument and the other that reverses its argument.

(defun sq (x) (* x x)) (defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x)))))

**Lesson 0:** Learn about

**Lesson 1:** To use

(include-book "projects/apply/top" :dir :system)

**Lesson 2:** To allow

(defwarrant sq) (defwarrant rev)

`Defwarrant` checks that its argument, *fn*, is a defined
function symbol that satisfies certain restrictions on how it uses its
arguments, restrictions that enable us to define the tameness predicates and
that allow *fn* does not obey our rules. But if
*fn*
that describes which formals are treated as ``functions.'' Henceforth, we'll
say such formals have ``ilk'' `warrant` for
*fn* that specifies the `badge` and the conditions under which
*fn*.

**Lesson 3:** We'll say more about tameness, badges, and warrants
later. You already know that warrants can only be issued for `state` or stobj arguments and so
cannot call any function that takes

**Lesson 4:** If you want to define a function and immediately call

**Lesson 5:** You can define functions that take warranted
``functions'' as arguments and

(defun$ collect$ (fn lst) (if (endp lst) nil (cons (apply$ fn (list (car lst))) (collect$ fn (cdr lst)))))

In this definition, the first argument has ilk *never* used as a function.

Note: We define

Here's another useful scion:

(defun$ always$ (fn lst) (if (endp lst) t (and (apply$ fn (list (car lst))) (always$ fn (cdr lst)))))

It checks that every element of

By the way, both `loop$` statment.

**Lesson 6:** You can run scions on warranted function symbols:

ACL2 !>(collect$ 'SQ '(1 -2 3 -4)) (1 4 9 16) ACL2 !>(collect$ 'rev '((1 2 3) (4 5 6) (7 8 9))) ((3 2 1) (6 5 4) (9 8 7))

**Lesson 7:** You can run scions on tame quoted `lambda$`, that allows you to write
in untranslated form as you would a lambda expression in ACL2.

**Lesson 8:** There are three very similar looking but very different
notions used in this documentation: lambda expressions, `lambda` for some
definitions and disambiguation help.

; Don't type this: ACL2 !>(collect$ '(LAMBDA (X) (IF (< X '0) (BINARY-* '10 X) (SQ X))) '(1 -2 3 -4)) (1 -20 9 -40) ; Type this instead! ACL2 !>(collect$ (lambda$ (X) (if (< x 0) (* 10 x) (sq x))) '(1 -2 3 -4)) (1 -20 9 -40)

**Lesson 9:** Almost all ACL2 primitives are known to

(append '(BADGE TAMEP TAMEP-FUNCTIONP SUITABLY-TAMEP-LISTP APPLY$ EV$) (strip-cars *badge-prim-falist*))

You can freely use these ACL2 primitives with

**Lesson 10:** You can prove and use theorems about scions.

(defthm collect$-append (equal (collect$ fn (append a b)) (append (collect$ fn a) (collect$ fn b)))) (thm (equal (collect$ (lambda$ (x) (sq (sq x))) (append c d)) (append (collect$ (lambda$ (x) (sq (sq x))) c) (collect$ (lambda$ (x) (sq (sq x))) d))))

Notice that the lemma

**Lesson 11:** But when your theorems depend on the behavior of

(defthm all-natp-collect$-sq (implies (and (warrant sq) (always$ 'INTEGERP lst)) (always$ 'NATP (collect$ 'SQ lst))))

Note that this theorem uses the scion

**Lesson 12:** Warrants solve the ``

(encapsulate nil (local (defun sq (x) (* x x))) (defthm unwarranted-all-natp-collect$-sq (implies (always$ 'INTEGERP lst) (always$ 'NATP (collect$ 'SQ lst))))) (defun sq (x) (* x x x)) (thm (implies (always$ 'INTEGERP lst) (always$ 'NATP (collect$ 'SQ lst))))

This would be a disaster because the final

If we could prove the unwarranted theorem we could export it because it
does not mention or depend on the function `'SQ`. Fortunately, we cannot actually prove the unwarranted
version of the theorem because there is no *a priori* connection between

**Lesson 13:** While we may have given the impression that we've
provided a convenient fragment of second-order functionality in ACL2 its
limitations will annoy you! For example, when ACL2 tries to use the
lemma

(defthm all-natp-collect$-sq (implies (and (warrant sq) (always$ 'INTEGERP lst)) (always$ 'NATP (collect$ 'SQ lst))))

it just employs its usual first-order matching algorithm. Thus, the lemma won't apply to

(always$ 'NATP (collect$ (lambda$ (x) (* x x)) lst))

because the constant symbol `'SQ` is not the same as the constant
list generated by translating ` '(LAMBDA (X) (BINARY-* X X))`, even though they are equivalent
if understood as functions. See the discussion at

**Lesson 14:** Recall Lesson 0! Before you start to use

**An Advanced Lesson:** We conclude this tutorial by defining one of
the most useful scions and proving a couple of theorems illustrating its
flexibility:

(defun$ foldr (lst fn init) (if (endp lst) init (apply$ fn (list (car lst) (foldr (cdr lst) fn init)))))

Note that

When its functional argument is

(defthm foldr-cons (equal (foldr x 'cons y) (append x y)))

We do not need a warrant for

By supplying a certain

(defthm foldr-can-be-rev (implies (warrant foldr) (equal (foldr x (lambda$ (x y) (foldr y 'cons (cons x nil))) nil) (rev x))))

Note that the