Background knowledge in ACL2 programming for theorem prover tutorial

This brief review of the programming language is presented as a sequence of questions and answers meant to test your knowledge of the ACL2 programming language. If you want a gentle introduction to the programming language, see http://www.cs.utexas.edu/users/moore/publications/gentle-intro-to-acl2-programming.html.

Before we get started with the programming drill, let us remind you that
all we're interested in here is the language, not the ``program development
environment.'' It's impossible to program in ACL2 or any other language
without a decent environment, one that at the very least includes a way to
prepare and edit files of programs. The two most popular program development
environments among ACL2 users are Emacs

**Q**: What do you think this command does?

(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x)))))

**A**: It defines a function named

(rev x) = (if (endp x) nil (append (rev (cdr x)) (list (car x)))),

implicitly quantified for all

**Q**: Given the *formal
parameters*? What is the *body* of the definition? Write down a
*call* of *append* that occurs in the body of *actuals* of that call? **A**: The *formals* of *formal* here. The
*body* of *call* of

(append (rev (cdr x)) (list (car x)))

and the *actuals* of that call are, respectively,

**Q**: What do you get if you evaluate **A**:

**Q**: How did **A**: This is a trick question.

**Q**: What does **A**:

(#\C B "A" "ABC" (A B C)) (#\c B "a" "Abc" (C B A))

The first wrong answer above is wrong because Lisp is ``case insensitive''
only for symbols, not for character objects like

**Q**: In the question about what **A**: The phrase ``*x* evaluates to *y*'' treats
*x* as a *term* to be evaluated and *y* as an *object*.
*obj*, and you wish to create a term whose value is *obj*, then you
put a quote mark in front of it, *'obj*.

**Q**: Can **A**: Yes, every ACL2 function can be applied to any object. ACL2 is an
untyped programming language: every variable ranges over the entire universe
of objects. In normal usage,

**Q**: So what does **A**:

**Q**: Why? **A**: Because

(defun endp (x) (not (consp x)))

Thus, if

**Q**: So what does **A**:

(cons 'a (cons 'b (cons 'c 'd))).

That is, it is a list whose ``terminal marker'' is the atom

**Q**: What does **A**: That's a trick
question.

**Q**: What does **A**:
That is a trick question. There is no such object. In Lisp's ``dot
notation'' every dot must be followed by a well-formed object and then a close
parenthesis. Usually that ``well-formed object'' is an atom. If it is not an
atom, i.e., if it is a cons, then the entire expression could have been
written without that dot. For example,

**Q**: Do **A**: No.

**Q**: Do **A**: No.

**Q**: When are **A**: When the
terminal marker of

**Q**: Can you define a Lisp function that recognizes
**A**: Yes, but it is not necessary for the
user to define that concept because Common Lisp provides such a function which
is logically defined as follows:

(defun true-listp (x) (if (consp x) (true-listp (cdr x)) (equal x nil))).

This can be paraphrased:

**Q**: Can you write a Lisp formula that says ``If

**A**: Yes:

(implies (true-listp z) (equal (rev (rev z)) z)).

**Q**: Is this all there is to ACL2 programming? **A**: No! ACL2
provides many other features. For a full list of all the primitive functions
in ACL2 see programming

* `list`: build a *n* terms, e.g.,

* list*: build a non-*n* objects
from the values of *n+1* terms, e.g.,

* `and`, `or`, `not`, `implies`, `iff`: The
propositional connectives.

* `+`, `*`, `-`, `/`, `floor`, `mod`,
`<`, `<=`, `>=`, `>`: the Lisp elementary arithmetic
operators. Both

* `natp`, `integerp`, `rationalp`, `characterp`,
`stringp`, `symbolp`, `consp`: the recognizers for the
primitive data types. The first three recognize subsets of the ACL2 numeric
universe. The naturals are a subset of the integers, the integers are a
subset of the rationals, and the rationals are a subset of the objects
recognized by `ACL2-numberp`, which also includes the `complex-rationalp`s. The other recognizers listed above recognize characters,
strings, symbols, and conses.

* `cond`: a convenient way to write a cascading nest of

(cond ((not (natp x)) 'non-natural) ((equal x 0) 'zero) ((evenp x) 'positive-even) (t 'positive-odd))

abbreviates

(if (not (natp x)) 'non-natural (if (equal x 0) 'zero (if (evenp x) 'positive-even 'positive-odd))).

* `case`: a convenient way to case split on the identity of an
object.

(case key (non-natural -1) (zero 0) ((positive-even positive-odd) 'positive-natural) (otherwise 'unknown))

abbreviates

(cond ((eql key 'non-natural) -1) ((eql key 'zero) 0) ((member key '(positive-even positive-odd)) 'positive-natural) (t 'unknown)).

* user defined macros: using `defmacro`

* `mutual-recursion`: allows you to define mutually-recursive
functions.

* `mv` and `mv-let`: allow functions to return
``multiple-values''. In Lisp, such functions return vectors of values, the
vectors are represented as lists of values, but the implementations are
generally more efficient. For example,

(mv-let (a b c) (foo x) (bar a b c x))

evaluates

ACL2 also provides many other features, such as single-threaded objects
which may be ``destructively modified'' (see stobj `state`
**strongly** recommend that as a new user you stay away from
these features until you are good at proving theorems about elementary list
processing!

If this little drill made sense to you, you know enough of the programming
language to get started. Use your browser's **Back Button** now to return
to introduction-to-the-theorem-prover.

If you are uncomfortable with ACL2 programming, we recommend that you study http://www.cs.utexas.edu/users/moore/publications/gentle-intro-to-acl2-programming.html and http://www.cs.utexas.edu/users/moore/publications/acl2-programming-exercises1.html.

However, we strongly recommend that you first invest in learning either the Emacs or Eclipse-based ACL2-Sedan program development environments, since it is foolish to try to learn how to program in a stand-alone read-eval-print loop!

While getting started, many users find the Hyper-Card a handy index into the documentation for the ACL2 language:

http://www.cs.utexas.edu/users/moore/publications/hyper-card.html

Once you are comfortable with the ACL2 programming language, use your
browser's **Back Button** to return to introduction-to-the-theorem-prover.