Introduction-to-apply$
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$. We refer to the paper simply as ``the paper.'' Supplemental
material on the logical foundations of apply$ can be found in the community-books directory books/projects/apply-model/. Also see apply$ for detailed documentation on apply$ that complements the
introduction below, to be read carefully when you're ready to use apply$
in your own projects. We suggest that you not follow all the links in
introductory discussion and instead read it linearly as you might a paper.
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
:logic mode function tamep-functionp and the paper gives explanatory
details.
The fundamental question raised by apply$ is ``How can apply$
know the correspondence between an ordinary ACL2 object, like a symbol or a
list, and the ACL2 function the user means to apply?'' For example, if the
user defines the function my-append, how can apply$ know that
(apply$ 'MY-APPEND (list a b)) should expand to (my-append a b)?
The ACL2 primitives can be built in. The logical definition of apply$
includes a big case split that recognizes about 800 ACL2 primitives, so that
for example:
(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 apply$ has been
defined in the ACL2 sources it cannot be extended to handle new symbols.
Intuitively, if you have defined the n-ary function foo then you
would expect (apply$ 'foo (list a1...an)) to be (foo a1...an). One
way to arrange that might be to leave apply$ undefined on the symbol
foo but to assume, as by an axiom or hypothesis,
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 apply$ and new symbols in axioms raises a
problem with ACL2's notion of local. We illustrate this problem
later in this doc topic. But for that reason, the suppositions extending
apply$ will take the form of hypotheses to be added to conjectures in
which the behavior of apply$ on new symbols is important. These
hypotheses are called ``warrants.''
Warrant (Merriam-Webster): (noun) a commission or document giving
authority to do something....
In our case, a warrant for fn gives apply$ permission to apply
fn under some circumstances, by asserting a universally quantified
conditional equality about apply$'s behavior on 'fn. It also tells
apply$ and the tameness predicates things like how many arguments
fn takes and how it uses them by asserting the badge of
'fn. The badge of fn is an ACL2 object that contains various
tokens interpretable by apply$ and the tameness predicates.
But there is a fundamental logical problem: it is not always possible to
satisfy such suppositions. There may be no way that apply$ could handle
fn. An example of a fn for which that hypothesis is unsatisfiable
is
(defun russell (x y) (not (apply$ x (list y y)))).
This definition of russell is not recursive: it does not call itself.
So this definition is admissible. But if we had a warrant for apply$
and that warrant were as simple as
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'' apply$ to handle them.
It should be pretty clear that if the user defines an ACL2 function that
in no way depends on apply$, e.g., a function like:
(defun sq (x) (* x x))
then the hypothesis
forall x : (apply$ 'SQ (list x)) = (sq x)
is satisfiable: we could have introduced sq before apply$ and
then defined apply$ in the first place to handle that particular
symbol.
Sq is a particularly simple example of a tame function. One
challenge in this work has been to extend the notion of tameness so that it
includes a lot of what a normal ACL2 programmer might want in apply$
while maintaining the soundness of the resulting theory.
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$ calls apply$. The reason we
can allow this is that in this particular call of collect$ the function
to be applied is itself tame. But if (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 sq and collect$ and have
analyzed them to make sure they have the appropriate tameness properties.
(Note that collect$ is not tame, but the way it uses its ``functional''
argument is crucial to the tameness of (collect$ 'SQ lst).) To use
apply$ to full advantage we need to have analyzed every relevant
function definition so we know which arguments are treated like functions and
whether they are used in accordance with our restrictions. So if you're
defining a function you intend to apply$ it is convenient to define it
with the new command 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 apply$ it, you can call
defwarrant yourself.
Defwarrant analyzes a :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 :program mode
functions to analyzed and badged so they can be safely executed by
apply$ at the top-level ACL2 loop. But the present discussion focuses
primarily on the logical machinery, which requires warrants.
We explain further via an annotated example, starting from scratch but
from the basic background just sketched. For many additional examples, see
community-books books/projects/apply/report.lisp which is a
certified book containing the examples in the paper.
Note carefully: the directory books/projects/apply-model/,
mentioned earlier in conjunction with the paper, is different from the
directory books/projects/apply/ just mentioned! The former directory
concerns the logical foundations of apply$ as they stood when the paper
was written. The latter is more directly relevant to ACL2 users and provides
useful lemmas about apply$ as it is axiomatized and implemented today.
It also includes many example theorems.
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 apply$ by reading this tutorial
introduction. But this tutorial mentions many undefined concepts: tameness,
warrants, badges, ilks. These concepts are intertwined with apply$ and
warrants through mutual recursion, constraints, rewrite rules, etc.. So we
decided not to try to define them here as we go along, though the links
provided do provide definitive descriptions. So please tolerate the use of
undefined words here — we'll try to give you a sense of what they
mean.
Lesson 1: To use apply$, be sure to include the following book
of lemmas. These lemmas are important not just to proving theorems about
apply$ but to defining functions that use apply$.
(include-book "projects/apply/top" :dir :system)
Lesson 2: To allow apply$ to ``work'' on a function symbol the
symbol must be ``warranted.'' Actually, of course, you can pass anything to
apply$ and the axioms will reduce it to some value: ACL2 is untyped and
all functions are total! But apply$ won't work in the logic as you
expect if the first argument to apply$ is not warranted! (And
apply$ won't work as you expect for top-level evaluation if its first
argument is not at least badged.) To issue warrants (and badges) for sq
and rev do:
(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 apply$ to ``work'' without causing logical contradictions.
Defwarrant causes an error if fn does not obey our rules. But if
defwarrant does not cause an error it produces a ``badge'' for fn
that describes which formals are treated as ``functions.'' Henceforth, we'll
say such formals have ``ilk'' :FN. In addition to computing a
badge, non-erroneous calls of defwarrant produce a warrant for
fn that specifies the badge and the conditions under which
apply$ ``works'' on the function symbol fn.
Lesson 3: We'll say more about tameness, badges, and warrants
later. You already know that warrants can only be issued for :logic
mode functions because the function symbol is used as a function in the
logical definition of the warrant. But you might as well learn four major
limitations of apply$:
(i) Apply$ does not take state or stobj arguments and so
cannot call any function that takes STATE or stobj arguments. (ii)
Apply$ cannot call a function whose measure, well-founded relation, or
domain predicate depends on apply$. (iii) Apply$ cannot call a
function that itself uses apply$ unless that function's measure is a
natural number or a lexicographic combination of naturals formed with
llist as defined in the Community Books at books/ordinals/. (iv)
Apply$ cannot call a function that itself uses apply$ if that
function was defined mutually recursively. Another way of saying all this is
that defwarrant will cause an error if you try to warrant a function
violating (i), (ii), (iii) or (iv).
Lesson 4: If you want to define a function and immediately call
defwarrant on it you can use the handy macro defun$. We'll use
defun$ freely below.
Lesson 5: You can define functions that take warranted
``functions'' as arguments and apply$ them. Here is a function that
applies its first argument to every element of its second argument and
collects the results. We sometimes call functions like collect$
``mapping functions'' because they map another function over some range. We
would call them ``functionals'' except that suggests ACL2 is higher-order and
it is not! So we most often call them scions of apply$. In
ordinary English usage, a ``scion'' is a descendent of an important family or
individual; our scions are ``descendents'' of apply$ and inherit its
power and restrictions.
(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 :FN because it is used
exclusively as a ``function:'' it reaches the first argument of apply$
and is untouched otherwise. The second argument has ilk NIL and we say
it's ``ordinary.'' It is never used as a function.
Note: We define collect$ with defun$ simply to illustrate
defun$. Unless we mean to pass collect$ to apply$ or to some
scion in the future, there is no reason to have a warrant for collect$.
Had we defined collect$ with the ordinary defun and realized later
that we want to pass 'COLLECT$ into a slot of ilk :FN, we could get
a warrant for collect$ by calling (defwarrant collect$).
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 lst satisfies its :FN argument
fn.
By the way, both collect$ and always$ are pre-defined in
ACL2 because they are part of the support for the 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 objects.
These are just quoted list expressions that start with the symbol LAMBDA
and look like lambda-expressions. But quoted LAMBDA objects have to
have fully translated bodies and meet other restrictions so apply$ can
interpret them. You cannot use macros like + or cond and must you
quote all constants. We urge you not to type quoted LAMBDA objects by
hand! Instead, we provide a macro, 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 objects,
and lambda$ expressions. Read carefully! See 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 apply$. For
a complete list of the built-ins evaluate
(append '(BADGE TAMEP TAMEP-FUNCTIONP SUITABLY-TAMEP-LISTP
APPLY$ EV$)
(strip-cars *badge-prim-falist*))
You can freely use these ACL2 primitives with apply$ and in your
lambda$ expressions, without warrants.
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 collect$-append talks about an arbitrary
fn. The definition of apply$ is completely irrelevant to this
theorem! Once collect$-append has been proved can be instantiated with
anything for fn. This is demonstrated when the thm above is
proved: the proof is just to rewrite with collect$-append.
Lesson 11: But when your theorems depend on the behavior of
apply$ on particular user-defined functions, you will need to provide
hypotheses stipulating the behavior of apply$ on those values. Those
hypotheses are the warrants for the (non-primitive) function symbols
involved. Here is an example: If lst is a list of integers and we
square every element by mapping over it with sq then the result is a
list of naturals — but this theorem depends on the fact that (apply$
'SQ (list x)) is (sq x), which is what the warrant for sq tells
us. Thus, the warrant for sq is required as a hypothesis!
(defthm all-natp-collect$-sq
(implies (and (warrant sq)
(always$ 'INTEGERP lst))
(always$ 'NATP (collect$ 'SQ lst))))
Note that this theorem uses the scion always$ to express the ideas of
``list of integers'' and ``list of naturals.'' Note also that we don't need
to provide warrants for integerp or natp because they are ACL2
primitives and thus built into the behavior of apply$.
Lesson 12: Warrants solve the ``LOCAL problem.'' Imagine the
trouble we'd be in if the theorem above did not require a warrant on sq.
We could get away with this:
(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 thm is invalid since
(sq -2) here is -8 and yet the thm is trivially proved by
appealing to the unwarranted theorem exported from the encapsulate.
If we could prove the unwarranted theorem we could export it because it
does not mention or depend on the function sq, it just mentions the
constant 'SQ. Fortunately, we cannot actually prove the unwarranted
version of the theorem because there is no a priori connection between
(apply$ 'SQ (list x)) and (sq x). And if we add the warrant for
sq to the defthm in the encapsulate we can prove the theorem but we
cannot export it because the warrant ancestrally depends on locally defined
function sq.
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$ expression,
'(LAMBDA (X) (BINARY-* X X)), even though they are equivalent
if understood as functions. See the discussion at fn-equal.
Lesson 14: Recall Lesson 0! Before you start to use apply$
outside of this simple demo script, we advise you to read the documentation
for apply$.
An Advanced Lesson: We conclude this tutorial by defining one of
the most useful scions and proving a couple of theorems illustrating its
flexibility: foldr.
(defun$ foldr (lst fn init)
(if (endp lst)
init
(apply$ fn
(list (car lst)
(foldr (cdr lst) fn init)))))
Note that foldr maps over the list in its first argument, applying
its second argument to two things: successive elements of the list and the
result of recursively calling itself on the rest of the list. It returns its
third argument when the list is empty.
When its functional argument is cons foldr is just the
concatenation of its other two arguments:
(defthm foldr-cons
(equal (foldr x 'cons y)
(append x y)))
We do not need a warrant for cons because it is built into
apply$. In fact, the built-ins don't have warrants but if you
unnecessarily list a primitive in a warrant expression, like (warrant
foldr cons), it just ignores the primitives that are built into
apply$.
By supplying a certain lambda expression we can use foldr to
reverse its first argument:
(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 lambda$ expression calls foldr. Because of this,
we must provide the warrant for foldr since that inner foldr will
be applied by the outer foldr. This illustrates an important point:
scions can apply other scions, including themselves, as long as the
applications are tame.
