Lp-background-review-2-answers
Answers to the review of apply$ and related concepts
Below are our answers to the Review of apply$ and related
concepts. If your answers basically agree with ours, we think you're ready
to follow the discussion in loop$-primer. If not, we recommend that
you read introduction-to-apply$ and then apply$ before reading
about loop$.
But our answers are sometimes quite long and elaborate — more like
little lectures on the subject than just answers. So don't expect to
reproduce our answers. It's up to you to decide if you know this stuff. As
you use loop$, ACL2 will print warnings and error messages about
functions not having badges or warrants or expression not being tame. We
don't want your reaction to be “Ack! What's that all about?” We want it to
be at least “Oh yes, I remember now.” So we recommend that you read these
little mini-lectures in full.
——————————
Consider these events, executed as the first three events in new ACL2
sessions.
(include-book "projects/apply/top" :dir :system)
(defun sq (x)
(declare (xargs :guard (natp x)))
(* x x))
(defun ghi (fn lst)
(declare (xargs :guard (and (apply$-guard fn '(nil))
(true-listp lst))))
(cond
((endp lst) nil)
(t (cons (apply$ fn (list (car lst)))
(ghi fn (cdr lst))))))
The three events are executed without error and sq and ghi are
admitted in :logic mode. By the way, we're naming certain functions in
these reviews with consecutive letters of the alphabet, e.g., abc,
def, ghi, jkl, mno, etc. These names are not mnemonic or
acronyms. Don't read anything into the names! Note that unlike the review
of elementary ACL2 features (see lp-background-review-1),
here we define (sq x) with a guard of (natp x). Both sq and
ghi are guard verified upon admission.
——————————
1: What is the value of (ghi 'sq '(1 2 3))? Hint: This is a trick
question!
Answer: Note that ghi is a scion of apply$. It calls
apply$, passing in the first argument of ghi as the “function” to
apply$. The evaluation of the above term fails with an error message
because sq is a user-defined :logic mode function but has
not been warranted (see defwarrant). :Logic mode
functions must be warranted to be applied (with apply$) at the top-level
of the ACL2 read-eval-print loop. Furthermore, if you ever try to prove a
theorem whose proof requires expansion of the applications (with apply$)
of such functions, their warrants must be provided as hypotheses. We'll get
to that later.
By the way, :program mode functions must be badged (see defbadge) to be applied at the top-level, but they need
not be warranted (because :program mode functions cannot be warranted or
used meaningfully in conjectures to be proved). See guarantees-of-the-top-level-loop for a discussion of the badge and warrant
restrictions enforced by top-level evaluation.
——————————
2: How do you assign a badge and warrant to sq?
Answer: (defwarrant sq).
Defwarrant assigns both a badge and a warrant to its argument, which
must be a :logic mode function satisfying certain restrictions on how it
uses its arguments and how the termination of the function is justified. If the
function cannot be badged or cannot be warranted, an error is printed.
Defbadge just assigns a badge and can work on :program or
:logic mode functions.
——————————
3: What is the name of the “warrant function for sq?” What does
(warrant sq) abbreviate? What does (warrant sq) imply about
badge and apply$?
Answer: The warrant function for sq is named apply$-warrant-sq,
which is a 0-ary predicate. (Warrant sq) is just an abbreviation for a
call of apply$-warrant-sq and if more than one function symbol appears
after the symbol warrant then it expands to the conjunction of each of
their predicates. We'll show an example later.
Apply$-warrant-sq is introduced as a constrained function using
defun-sk. Here is the event in question, but the details here are
not critical to the present discussion.
(defun-sk apply$-warrant-sq ()
(forall (args)
(and
(equal (badge-userfn 'sq) '(apply$-badge 1 1 . t))
(equal (apply$-userfn 'sq args)
(sq (car args)))))
:constrain t)
What is critical is the role that (apply$-warrant-sq) plays in the
following theorem, which is proved as a :rewrite rule by
(defwarrant sq).
(defthm apply$-sq
(implies (force (apply$-warrant-sq))
(and (equal (badge 'sq)
'(apply$-badge 1 1 . t))
(equal (apply$ 'sq args)
(sq (car args))))))
which allows the prover to reduce (badge 'sq) to (apply$-badge 1 1
. t) and to reduce any instance of (apply$ 'sq args) to (sq (car
args)).
The badge of sq tells the prover that sq is a function
of one argument that returns one result. The “ . t” means “all the
arguments are ordinary objects,” i.e., never treated like “functions.”
The second part of the rule above will reduce the typical application of
sq, e.g., (apply$ 'sq (list e)), to (sq e).
Finally, note that name of the rule is apply$-sq, both the badge
and apply$ reductions are conditional on the warrant hypothesis for
sq, and that the warrant hypothesis is forced.
——————————
4: Can ghi be warranted? If so, what command do you type?
Answer: Yes! Just type (defwarrant ghi).
——————————
5: What is the name of the warrant function for ghi? Explain what
the warrant for ghi tells us.
Answer: The warrant function for ghi is named
apply$-warrant-ghi. (warrant ghi) abbreviates
(apply$-warrant-ghi), and, by the way, (warrant sq ghi ...) expands
to
(and (apply$-warrant-sq)
(apply$-warrant-ghi)
...).
The rule apply$-ghi is proved by defwarrant.
(defthm apply$-ghi
(and (implies (force (apply$-warrant-ghi))
(equal (badge 'ghi)
'(apply$-badge 2 1 :fn nil)))
(implies (and (force (apply$-warrant-ghi))
(tamep-functionp (car args)))
(equal (apply$ 'ghi args)
(ghi (car args) (car (cdr args)))))))
Notice that apply$-ghi is really two :rewrite rules, both
conditioned on the forced warrant for ghi.
The first rule tells us what the badge of ghi is. In
particular we see that the first argument of ghi has “ilk”
:fn, which means that argument is treated as a function and can
eventually be applied with apply$. Arguments of ilk :fn are never
treated as ordinary objects. The badge of ghi also tells us the second
argument has ilk nil, which means it is an ordinary object (and is never
treated as a function). The details are in defbadge.
Note that the second conjunct of the apply$-ghi rule above rewrites
instances of (apply$ 'ghi args) and would rewrite (apply$ 'ghi (list
x y)) to (ghi x y). However, it can only be used if the first
argument passed to ghi, namely x above, is a tame function.
Ilks, warrants, and tameness are concepts that are critical to the soundness
of ACL2's handling of apply$. For details see apply$.
——————————
6: The following definition is admissible. Can it be warranted?
(defun mno (x y z)
(if (endp x)
z
(apply$ y
(list (car x)
(mno (cdr x) y z)))))
Answer: Yes. Its badge is determined to be (apply$-badge 3 1 nil :fn
nil).
For example,
(mno '(1 2 3) 'cons '(4 5 6))
=
(cons 1 (mno '(2 3) 'cons '(4 5 6)))
=
(cons 1 (cons 2 (mno '(3) 'cons '(4 5 6))))
=
(cons 1 (cons 2 (cons 3 (mno 'nil 'cons '(4 5 6)))))
=
(cons 1 (cons 2 (cons 3 '(4 5 6))))
=
'(1 2 3 4 5 6)
In fact, mno is more often named “foldr” in the functional
programming literature.
——————————
7: Is (equal (mno x 'cons y) (append x y)) a theorem?
Answer: Yes! You might think we need to add the warrant hypothesis for
cons since (apply$ 'cons ...) must be expanded to do the proof.
However, most ACL2 primitives, like cons, are built into the definition
of apply$ and warrants are not necessary for them. In fact, the
primitives don't have warrant functions. E.g., (apply$ 'cons (list x
y)) is (cons x y), unconditionally. The complete list of apply$
primitives may be exhibited by evaluating
(append '(BADGE TAMEP TAMEP-FUNCTIONP SUITABLY-TAMEP-LISTP
APPLY$ EV$)
(strip-cars *badge-prim-falist*)).
However, user-defined function symbols need warrants in order to be
applied (with apply$). But not all user-defined symbols can be
warranted.
——————————
8: The following defun is admissible but cannot be warranted.
Why?
(defun xyz (x) (apply$ x (list x)))
Answer: It is impossible to classify the argument x. Is it a
function or is it an ordinary object? It's used both ways. (Defwarrant
xyz) fails.
In order for apply$ to be able to handle a function symbol certain
restrictions must hold. These restrictions guarantee that there is a model
that makes all warrants true. Here's a way to think about it. Imagine that
apply$ is defined as a big case analysis that enumerates all the
functions that apply$ can handle and calls them appropriately. That big
definition of apply$ has some measure that explains why it terminates
— a fairly messy measure given that apply$ can all ghi which
calls apply$. Now imagine you want to define a new function, e.g.,
xyz, and change the definition of that big apply$ to include all
the old functions plus xyz. You'll need to weave the measure of
xyz into the measure of the big apply$. Defwarrant enforces
restrictions that tell us this is possible. Of course, the restrictions are
overly restrictive: to be perfect defwarrant would have to solve the
halting problem.
While the failure of (defwarrant xyz) prevents us from being able to
use apply$ to apply xyz, it is possible to evaluate some calls of
xyz and to prove theorems about them.
(thm
(equal (xyz '(lambda (x) (len x))) 3)
In the proof of the theorem above, xyz applied the given lambda
object to itself and computed that its length is 3.
——————————
9: Recall ghi as defined at the beginning of this review. Assume
sq has been warranted. What is the value of (ghi 'sq '(1 2
3))?
Answer: (1 4 9).
Recall that an earlier question established that ghi can be warranted
and one might think warranting ghi is necessary for (ghi 'sq '(1 2
3)) to be evaluated without error. But that's untrue. Ghi is not
being applied (with apply$) here, so whether it has been warranted or
not is irrelevant. However, sq is being applied.
——————————
10: Is (nat-listp (ghi 'sq lst)) a theorem? If not, what theorem
does this suggest?
Answer: No, it's not a theorem as written. For example (ghi 'sq '(-1/2
#c(0 1))) has the value (1/4 -1), although to get that value computed
by the top-level read-eval-print loop you have to turn off guard
checking (see set-guard-checking).
The following is a theorem.
(implies (and (warrant sq)
(nat-listp lst))
(nat-listp (ghi 'sq lst)))
The warrant hypothesis for sq is necessary because to prove
anything interesting about (apply$ 'sq ...) we need the warrant for
sq. The nat-listp hypothesis is necessary because otherwise
sq may not return a natural number.
——————————
11: What is the value of the term below?
(ghi (lambda$ (e) (ghi 'sq e))
'((1 2 3)
(4 5 6)
(7 8 9)))
Answer: ((1 4 9) (16 25 36) (49 64 81)).
Lambda$ is an interesting ACL2 feature. It translates the body
term and constructs a lambda object suitable for apply$.
The ghi term above is also interesting. It shows that the outer call
of ghi can successfully apply$ the lambda object which itself
calls ghi on sq.
——————————
12: Suppose you want to define jkl to be something like what's shown
below and you want the guards verified.
(defun jkl (lst)
(declare (xargs :guard ...))
(ghi (lambda$ (e) (ghi 'sq e)) lst)))
Notice that the body of jkl is the doubly nested ghi term just
tested, except now instead of applying it to a constant list we're applying
it to the argument of jkl.
What is the appropriate :guard and do you have to make other
modifications to the suggested defun of jkl?
Answer: First, we define a predicate that recognizes a list of
nat-listps, i.e., a list of lists, where each element of each of the
inner lists is a natural number.
(defun nat-list-listp (lst)
(declare (xargs :guard (true-listp lst)))
(if (endp lst)
t
(and (nat-listp (car lst))
(nat-list-listp (cdr lst)))))
We could warrant nat-list-listp with (defwarrant
nat-list-listp) if we wanted to, but because it is only used in a guard
below, a warrant is not necessary. If we intend to apply it with apply$
we would need a warrant and we can always warrant it when needed.
We can then define jkl with the :guard shown below. The
true-listp conjunct of the guard below is necessary because
nat-list-listp has true-listp as its guard. But note that we also
modified the lambda$ expression to express the guard on its local
variable e.
(defun jkl (lst)
(declare (xargs :guard (and (true-listp lst)
(nat-list-listp lst))))
(ghi (lambda$ (e)
(declare (xargs :guard (nat-listp e)))
(ghi 'sq e))
lst))
Jkl is guard verified upon admission. Consider what that means. In
particular, every time sq is called it is called on something satisfying
the guard of sq. The guard proof obligations generated for a nest of
functions using apply$ can be quite messy.
——————————
13: Can jkl be warranted?
Answer: Yes. (defwarrant jkl) succeeds. A key observation is that
the lambda$ expression in its definition is a tame function (see
tame). That is syntactically determined because the body of the
lambda$ is (ghi 'sq e), ghi requires a tame function as its
first argument, and sq is a tame function.
——————————
14: Is this a theorem? If not, what theorem does it suggest?
(implies (nat-list-listp lst)
(nat-list-listp (jkl lst)))
Answer: It is not quite a theorem as written. We need to add warrant
hypotheses for the functions being applied with apply$. Note that
jkl is not being applied, so we don't need its warrant. The outer
ghi in the definition of jkl is also not being applied. But the
lambda$ expression passed as an argument to the outer ghi is
being applied by the outer ghi, and to evaluate the body of that
lambda object we apply$ ghi, so we need the warrant for
ghi there. Furthermore, that inner ghi will apply sq. So we
need the warrant for that.
Thus, the following is indeed a theorem.
(implies (and (warrant ghi sq)
(nat-list-listp lst))
(nat-list-listp (jkl lst)))
For some heuristic advice on how to figure out the necessary warrants, see
the section “Determining the Necessary Warrants” in see warrant.
However, if you omit the warrant hypotheses ACL2 will often “remind” you
at the end of failed proof attempts by exhibiting checkpoints derived from
forcing the warrants when apply$ rules are applied. If the warrants are
omitted in this particular theorem checkpoints require proving both
(apply$-warrant-sq) and (apply$-warrant-ghi).
Finally, one might worry that it is impossible for all the listed warrants
to be true at once, so perhaps listing a bunch of warrants might make your
theorems vacuously valid. But defwarrant ensures that there is a model
of the ACL2 logic in which all warrants are valid. Thus, adding warrant
hypotheses in no way makes your theorems less meaningful.
——————————
If your answers basically agree with ours you should proceed on to lp-section-2. Otherwise, we strongly recommend that you read introduction-to-apply$ and then apply$ before reading about
loop$.
(Return to the Table of
Contents.)
