		Search-engine friendly clone of the ACL2 documentation.

Lp-section-1

Lp-background-review-1

Background review of basic ACL2 knowledge

Here are some questions to review basic features of ACL2.

——————————

Consider the expression below and answer the following questions about it, without running ACL2! We're looking for informal answers largely in agreement with ours, not perfect answers. If you want to see the questions together with our answers, see lp-background-review-1-answers.

(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?

——————————

2: More formally, how does the utterance above affect the ACL2 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 it translate to? And if you didn't know, how would you find out?

——————————

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!

——————————

5: Given the value of x in question 4, what is the value of (true-listp x)?

——————————

6: Given the value of x in question 4, what is the value of (cons '? (car x))?

——————————

7: Given the value of x in question 4, what is the value of (cdr x)?

——————————

8: Recall we defined abc above. What is the value (abc '((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))?

——————————

10: What is the value of (abc ((a . 1) (b . 2) (c . 3)))?

——————————

11: How would you explain what abc is, i.e., how it “works” or what it “does?”

——————————

12: What is the value of (abc 3 4 5)?

——————————

13: What is the value of (abc '(3 . 4))?

——————————

14: How do you get ACL2 to print the value of (abc '(3 . 4))?

——————————

15: How can you upgrade abc from a :program mode function to a :logic mode function?

——————————

16: What is the axiom added to ACL2 when abc is upgraded?

——————————

17: Is (true-listp (abc x)) a theorem in ACL2?

——————————

18: What would you type to get ACL2 to try to prove it?

——————————

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)))))

——————————

20: Define sq to square a number. E.g., (sq 9) returns 81 and (sq -1/2) returns 1/4.

——————————

21: How would you describe the behavior of sq* below?

(defun sq* (x)
  (if (endp x)
      nil
      (cons (sq (car x))
            (sq* (cdr x)))))

——————————

22: What would you type to make ACL2 prove the following conjecture?

(equal (sq* (def x)) (def (sq* x)))

——————————

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))))))

——————————

For our answers see lp-background-review-1-answers. If your answers don't basically agree with ours, you're probably not yet ready to read this material on loop$. We recommend that you read the topic, recursion-and-induction.

If your answers largely agree with ours, go back to the lp-section-1.

(Return to the Table of Contents.)