Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

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 and the Eclipse-based ACL2-Sedan . The Sedan provides the most support for the new user, including real-time syntax checking and a facility for testing among many other features. But in this drill we're not interested in the program development environment, we're interested in your understanding of the ACL2 language.

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

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

`rev`

that takes one argument, treats
it like a list, and reverses the order of the elements in
that list. To figure this out from the definition, you have to know that
`append`

concatenates two lists. Logically speaking, the `defun`

of
`rev`

adds the axiom:
(rev x) = (if (endp x) nil (append (rev (cdr x)) (list (car x)))),implicitly quantified for all

`x`

.
**Q**: Given the `defun`

of `rev`

above, what are the *formal parameters*?
What is the *body* of the definition? Write down a *call* of *append*
that occurs in the body of `rev`

. What are the *actuals* of that call?
**A**: The *formals* of `rev`

is the list of variables after the first `rev`

in the `defun`

, namely `(x)`

. We say `x`

is the first (and only) *formal* here.
The *body* of `rev`

is the entire `if`

-expression. The only *call* of
`append`

in the body is

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

`(rev (cdr x))`

and
`(list (car x))`

.
**Q**: What do you get if you evaluate `(rev '(a b c d))`

? **A**:
`(D C B A)`

.

**Q**: How did `rev`

change the case of the elements, e.g., lowercase `a`

was in the input list but uppercase `A`

was in the output? **A**:
This is a trick question. `Rev`

doesn't change the case of the elements.
ACL2 is case-insensitive when dealing with symbols. The symbol `a`

is
read in as the symbol `A`

. Thus, when writing function names, for
example, we can write `rev`

, `Rev`

, `REV`

, or even `ReV`

and always be referring to the function `REV`

. By default, ACL2
prints symbols in uppercase.

**Q**: What does `(rev '((a b c) "Abc" "a" b #\c))`

return? **A**:
`(#\c B "a" "Abc" (A B C))`

. If you thought the answer was any of
these, then you need to think or read more carefully:

(#\C B "A" "ABC" (A B C))The first wrong answer above is wrong because Lisp is ``case insensitive'' only for symbols, not for character objects like(#\C B "A" "ABC" (C B A))

`#\c`

(the lowercase character c)
or for strings. Furthermore, `"A"`

is a string, not a symbol; it is different
from `A`

. The second wrong answer above is wrong because `rev`

does not
go into the individual elements of the list, it just reverses the order of the
elements. So it doesn't change the element `(A B C)`

to `(C B A)`

.
**Q**: In the question about what `(rev '(a b c d))`

returns, we put a quote
mark before the `(a b c d)`

but not before the answer, `(D C B A)`

.
Why? **A**: The phrase ``*x* evaluates to *y*'' treats
*x* as a *term* to be evaluated and *y* as an *object*.
`(Rev '(a b c d))`

is a term to be evaluated and denotes
a call of the function `rev`

on the value of the argument term
`'(a b c d)`

. The value of that argument term is the object `(a b c d)`

.
The value of the call of `rev`

is the object `(d c b a)`

.
If you have 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 `rev`

be applied to something other than a list? **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, `rev`

is applied to lists but there is nothing
about the syntax of the language that prevents it being applied to
non-lists.

**Q**: So what does `(rev 23)`

evaluate to? **A**: `Nil`

.

**Q**: Why? **A**: Because `(endp 23)`

is `t`

, because `endp`

is
defined:

(defun endp (x) (not (consp x)))Thus, if

`rev`

is applied to anything that is not a cons, it returns
`nil`

.
**Q**: So what does `(rev '(a b c . d))`

evaluate to? **A**: `(c b a)`

.
To explain why requires demonstrating that you know what `(a b c . d)`

means. It is the object computed by evaluating:

(cons 'a (cons 'b (cons 'c 'd))).That is, it is a list whose ``terminal marker'' is the atom

`D`

.
`Rev`

treats that list exactly as it treats the `nil`

-terminated
list of the same elements, `(a b c)`

, because `(endp 'D)`

=
`(endp nil)`

= `t`

.
**Q**: What does `(rev 1 2 3)`

evaluate to? **A**: That's a trick question.
`Rev`

takes one argument, not three. So `(rev 1 2 3)`

is an ill-formed term.

**Q**: What does `(rev '(a b c . d . nil))`

evaluate to? **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, `(a b c . (d e))`

is
an object, but it could be written `(a b c d e)`

.

**Q**: Do `(rev (rev x))`

and `x`

always evaluate to the same object? **A**:
No. `(Rev (rev 23))`

evaluates to `nil`

, not `23`

.

**Q**: Do `(rev (rev x))`

and `x`

always evaluate to the same object when
`x`

is a cons? **A**: No.
`(rev (rev '(a b c . d)))`

evaluates to `(a b c)`

, not `(a b c . d)`

.

**Q**: When are `(rev (rev x))`

and `x`

equal? **A**: When the terminal
marker of `x`

is `nil`

.

**Q**: Can you define a Lisp function that recognizes `nil`

-terminated lists?
**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:

`(true-listp x)`

means that if `x`

is a
`cons`

, its `cdr`

is a `true-listp`

and if `x`

is not a `cons`

, it
must be `nil`

. Thus, `(true-listp '(a b c))`

is `t`

and
`(true-listp '(a b c . d))`

is `nil`

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

is a `nil`

-terminated
list then reversing the result of reversing `z`

is `z`

''?

**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 . Some highlights for the beginner are mentioned below,
but all of the links below ought to be tagged with the sign.

* `list`

: build a `nil`

-terminated list from the values of *n* terms, e.g.,
`(list x (+ 1 x) (+ 2 x))`

returns `(3 4 5)`

if `x`

is `3`

.

* list*: build a non-`nil`

terminated list of *n* objects from the
values of *n+1* terms, e.g., `(list* x (+ 1 x) (+ 2 x) (* -1 x))`

returns
the list `(3 4 5 . -3)`

if `x`

is `3`

.

* `and`

, `or`

, `not`

, `implies`

, `iff`

: The propositional
connectives. `And`

and `or`

are allowed to take a varying number of arguments, e.g.,
`(and p q r)`

is just an abbreviation for `(and p (and q r))`

.
In Lisp, `and`

returns `nil`

if any of its arguments evaluates to `nil`

; otherwise
it returns the value of the last argument! Thus, `(and t t 3)`

returns `3`

! If you
object to the idea that `and`

is not Boolean, don't give it non-Boolean arguments!
Similarly, `or`

returns the value of the first argument that evaluates to
non-`nil`

, or `nil`

if they all evaluate to `nil`

. Both `and`

and `or`

can
be thought of as ``lazy'' in that they don't always have to evaluate all their arguments.
This is really accomplished by treating `and`

and `or`

as abbrevations for `if`

nests.

* `+`

, `*`

, `-`

, `/`

, `floor`

, `mod`

, `<`

, `<=`

, `>=`

, `>`

:
the Lisp elementary arithmetic operators. Both `+`

and `*`

allow varying numbers of
arguments. All the arithmetic operators default non-numeric arguments to `0`

. If you
don't like the idea that `(+ 1 2 t)`

is `3`

, don't ask `+`

to add `t`

to something!

* `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 `if`

s, e.g.,

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

you can introduce your own
abbreviations. We recommend you not do this until you're good at list processing
since macros are functions that build objects representing terms.

* `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 x y z)`

returns a ``vector'' consisting of the values of `x`

, `y`

, and `z`

.

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

`(foo x)`

, treats the result as a vector of three values, binds the variables
`a`

, `b`

, and `c`

to those three values, and evaluates and returns `(bar a b c x)`

.
ACL2 also provides many other features, such as single-threaded objects which may be
``destructively modified'' (see stobj , including a very special single-threaded
object that records the `state`

of the ACL2 system), file input and output (see io ),
applicative arrays (see arrays ) and property lists (see getprop ) and other
facilities necessary for it to be a practical programming language.
However, we **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.