Lp-background-review-1-answers
Answers to background review of basic ACL2 knowledge
(defun abc (x)
(declare (xargs :mode :program
:guard (true-listp x)))
(cond
((endp x) nil)
(t (cons (cons '? (car x))
(abc (cdr x))))))
——————————
1: Informally, what happens if you type that expression at the
top-level of the ACL2 read-eval-print loop?
Answer: It defines abc as a Lisp program. Note the declare that
says the :mode is :program. By the way, when Lisp and ACL2 read
symbols, like abc, x, declare, etc., they automatically
convert them to UPPERCASE. So it doesn't matter if we write abc or
ABC, or Abc, etc.
——————————
2: More formally, how does the utterance above affect the ACL2
logic?
Answer: It doesn't. Defining a :program introduces no axioms into
the logic.
——————————
3: A little bit of Lisp knowledge will tell you that all terms are either
variables, constants (usually quoted), or calls of functions, where calls are
of the form (fn a1 ... an), where fn is a function symbol or
lambda object that takes n arguments and the ai are terms.
But the cond expression above is not of this form. Cond is a macro
that translates into a formal term. What formal term does the cond
expression translate to? And if you didn't know, how would you find out?
Answer: The expression
(cond
((endp x) nil)
(t (cons (cons '? (car x))
(abc (cdr x)))))
translates to
(if (endp x)
'nil
(cons (cons '? (car x))
(abc (cdr x))))
To see the translation of an expression use trans.
——————————
4: Let x be the object that prints as ((A . 1) (B . 2) (C . 3)).
What is the value of (car x) or is that a nonsensical question? Several
of the questions below are nonsensical!
Answer: (car x) is (A . 1) if x is ((A . 1) (B . 2) (C
. 3)).
——————————
5: Given the value of x in question 4, what is the value of
(true-listp x)?
Answer: T, because x is a nest of conses whose rightmost
terminal is NIL.
——————————
6: Given the value of x in question 4, what is the value of (cons
'? (car x))?
Answer: (? A . 1)
——————————
7: Given the value of x in question 4, what is the value of (cdr
x)?
Answer: ((B . 2) (C . 3))
——————————
8: What is the value (abc '((a . 1) (b . 2) (c . 3)))?
Answer: ((? A . 1) (? B . 2) (? C . 3))
——————————
9: What is the difference between '((a . 1) (b . 2) (c . 3)) and
((A . 1) (B . 2) (C . 3))?
Answer: '((a . 1) (b . 2) (c . 3)) is a constant term that evaluates
to the list ((A . 1) (B . 2) (C . 3)). The quote mark in front an
object forms a term that evaluates to that object. And remember, case is
generally irrelevant in symbols.
——————————
10: What is the value of (abc ((a . 1) (b . 2) (c
. 3)))?
Answer: That's a nonsensical question. (abc ((a . 1) (b . 2) (c
. 3))) is not a well-formed term. For example, (a . 1) is not a
function symbol or a lambda expression, or a macro.
——————————
11: How would you explain what abc is, i.e., how it “works” or
what it “does?”
Answer: The symbol ABC is the name of a Lisp program that takes one
argument and returns one result. It can be run, but nothing can be proved
about it because there are no axioms defining it. When abc is called on
x it copies the cdr-chain of x, adding the question mark
symbol to each new element.
——————————
12: What is the value of (abc 3 4 5)?
Answer: Nonsensical. ABC takes only one argument, not three.
——————————
13: What is the value of (abc '(3 . 4))?
Answer: Actually, it is ((? . 3)), but ACL2 won't evaluate (abc
'(3 . 4)) in the default configuration of the top-level read-eval-print
loop because (3 . 4) is not a true-listp. The guard on ABC
stipulates that the argument to ABC is “supposed” to be a
true-listp. So the read-eval-print loop causes a guard violation error.
We explain why the value of (abc '(3 . 4)) is actually ((? . 3)) in
the next answer.
——————————
14: How do you get ACL2 to compute and print the value of (abc '(3
. 4))?
Answer: The top-level read-eval-print loop has a parameter that controls
whether ACL2 checks the guards or not. By default, that parameter is set to
T, meaning it does check guards. But by executing
(set-guard-checking nil) the parameter is set to NIL and then
guards are not checked. With that setting, ACL2 evaluation just ignores the
guard and runs the body of the program.
So here is how (abc '(3 . 4)) is evaluated. First, it checks whether
endp holds on (3 . 4). The definition of endp is
atom, which means “is not a cons pair,” and (3 . 4) is a
cons pair. So the answer to the endp test is NIL and the
execution of (abc '(3 . 4)) branches to the (cons (cons '? (car
x)) (abc (cdr x))), where x is (3 . 4).
But the car and cdr of the pair (3 . 4) are 3 and
4 respectively. So the value of (abc '(3 . 4)) is (cons (cons
'? 3) (abc 4)).
But what is the value of (abc 4)? (Endp 4) is T because
4 is an atom. So the value of (cons (cons '? 3) (abc 4)) is
(cons (cons '? 3) NIL), which is printed as ((? . 3)).
——————————
15: How can you upgrade abc from a :program mode function to
a :logic mode function?
Answer: Invoke verify-termination like this (verify-termination abc).
——————————
16: What is the axiom added to the ACL2 logic when abc is
upgraded?
Answer:
<b>Definitional Axiom for ABC</b>
(abc x)
=
(if (endp x)
nil
(cons (cons '? (car x))
(abc (cdr x)))).
Note that the guard is irrelevant in the logic. (Abc x) is always
equal to the right-hand side of the axiom above (the “body” of abc),
regardless of what x is.
——————————
17: Is (true-listp (abc x)) a theorem in ACL2?
Answer: Yes! It may not seem so because the defun of abc
mentions the :guard of (true-listp x) and yet the conjecture here
doesn't constrain x. But guards of ACL2 functions are logically
irrelevant. The Definitional Axiom added for abc does not mention the
guard. So (true-listp (abc x)) is a theorem no matter what x
is!
Proof of (true-listp (abc x)) by induction on x:
Base Case: (atom x) ; i.e., x is not a consp
(true-listp (abc x))
= ; def abc
(true-listp (if (endp x) nil ...))
= ; def endp and (atom x).
(true-listp (if T nil ...))
= ; axiom about IF
(true-listp nil)
= ; def true-listp
T
Induction Step: (consp x)
Induction Hyp: (true-listp (abc (cdr x)))
(true-listp (abc x))
= ; def abc
(true-listp (if (endp x) nil (cons (cons '? (car x)) (abc (cdr x)))))
= ; def endp and (consp x)
(true-listp (if NIL nil (cons (cons '? (car x)) (abc (cdr x)))))
= ; axiom about IF
(true-listp (cons (cons '? (car x)) (abc (cdr x))))
= ; def true-listp
(true-listp (abc (cdr x)))
= ; Induction Hyp
T
Q.E.D.
If you ask ACL2 to do the proof (see the next question) its proof doesn't
mention induction. That's because when abc was defined ACL2 does a
little inductive reasoning to deduce the “type” of the output and deduced
that it is always a true-listp. That type inference essentially does
the inductive proof above.
——————————
18: What would you type to get ACL2 to try to prove it?
Answer:
(thm (true-listp (abc x)))
or
(defthm little-theorem-about-abc
(true-listp (abc x)))
——————————
19: How would you describe the behavior of the :logic function
def below? 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!
(defun def (x)
(if (endp x)
nil
(append (def (cdr x)) (list (car x)))))
Answer: It reverses x, i.e., it returns a list containing the
elements of x in reverse order. E.g., (def '(a b c)) returns (C
B A).
——————————
20: Define sq to square a number. E.g., (sq 9) returns 81
and (sq -1/2) returns 1/4.
Answer:
(defun sq (x) (* x x))
We could add a declaration, like (declare (xargs :guard (rationalp
x))) or (declare (xargs :guard (acl2-numberp x))). But we've chosen
to keep things simple here.
——————————
21: How would you describe the behavior of sq* below?
(defun sq* (x)
(if (endp x)
nil
(cons (sq (car x))
(sq* (cdr x)))))
Answer: It squares every element of x and returns the list of those
results in the same order. E.g., (sq* '(1 2 3 -1/2 #c(0 1))) is (1 4
9 1/4) -1.
——————————
22: What would you type to make ACL2 prove the following conjecture?
(equal (sq* (def x)) (def (sq* x)))
Answer: To get ACL2 to try to prove the theorem you could type
(defthm sq*-def
(equal (sq* (def x)) (def (sq* x))))
But ACL2 would fail to find the proof unless you'd proved some lemmas
about def. You might see a “checkpoint” like
*** Key checkpoint under a top-level induction
before generating a goal of NIL (see :DOC nil-goal): ***
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(EQUAL (DEF (SQ* (CDR X)))
(SQ* (DEF (CDR X)))))
(EQUAL (APPEND (SQ* (DEF (CDR X)))
(LIST (* (CAR X) (CAR X))))
(SQ* (APPEND (DEF (CDR X)) (LIST (CAR X))))))
What would that suggest you do?
What we'd do is prove the following lemma first and then try
sq*-def.
(defthm sq*-append
(equal (sq* (append a b))
(append (sq* a) (sq* b))))
When that lemma is available as a :rewrite rule during the
proof of sq*-def the checkpoint above would be further simplified, the
induction hypothesis of the sq*-def conjecture would be used, and the
proof of sq*-def would succeed.
The experienced ACL2 user would anticipate this in a simple problem
like this one. But in a messier problem the experienced user would just be
emotionally prepared for the proof attempt to fail and inspect the checkpoints
to try to figure out how to complete the proof. See the-method.
——————————
23: Prove (nat-listp (ghi 0 max)), where
(defun ghi (i max)
(declare (xargs :measure (nfix (- (+ 1 (nfix max)) (nfix i)))))
(let ((i (nfix i))
(max (nfix max)))
(cond ((> i max) nil)
(t (cons i (ghi (+ 1 i) max))))))
Answer: You can't prove (nat-listp (ghi 0 max)) by induction
with that 0 in one of the controlling arguments. You have to generalize
first.
(defthm nat-listp-ghi-lemma
(nat-listp (ghi i max)))
(defthm nat-listp-ghi
(nat-listp (ghi 0 max)))
——————————
That completes the answers to this review of basic ACL2 knowledge. If
your answers don't largely agree with ours, you're probably not yet ready to
read the material in the loop$-primer. We recommend that you take the
“Recursion and Induction” course (which should be somehow
linked in here!).
(Return to the Table of
Contents.)
