Lp-background-review-2
Review of apply$ and related concepts
Below are some questions designed to review basic knowledge of
apply$ and related concepts used in the semantics of loop$. For
our answers see lp-background-review-2-answers.
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 expressions 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.” We recommend
that after you've read and answered the questions, you read our answers even
if you're pretty confident in your answers.
——————————
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!
——————————
2: How do you assign a badge and warrant to sq?
——————————
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$?
——————————
4: Can ghi be warranted? If so, what command do you type?
——————————
5: What is the name of the warrant function for ghi? Explain what
the warrant for ghi tells us.
——————————
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)))))
——————————
7: Is (equal (mno x 'cons y) (append x y)) a theorem?
——————————
8: The following defun is admissible but cannot be warranted.
Why?
(defun xyz (x) (apply$ x (list x)))
——————————
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))?
——————————
10: Is (nat-listp (ghi 'sq lst)) a theorem? If not, what theorem
does this suggest?
——————————
11: What is the value of the term below?
(ghi (lambda$ (e) (ghi 'sq e))
'((1 2 3)
(4 5 6)
(7 8 9)))
——————————
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?
——————————
13: Can jkl be warranted?
——————————
14: Is this a theorem? If not, what theorem does it suggest?
(implies (nat-listp-listp lst)
(nat-listp-listp (jkl lst)))
——————————
See lp-background-review-2-answers for our answers. If
your answers basically agree with ours we think you're ready to learn about
loop$, so go back to the loop$-primer. Otherwise, we strongly
recommend that you read introduction-to-apply$ and then apply$
before reading about loop$.
(Return to the Table of
Contents.)
