Programming-knowledge-taken-for-granted
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 gentle-introduction-to-ACL2-programming.
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)))))
A: It defines a function named 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 actuals of that call are, respectively, (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
either of these, then you need to think or read more carefully:
(#\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 #\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 abbreviations 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-rationalps. The other recognizers listed above recognize characters,
strings, symbols, and conses.
* cond: a convenient way to write a cascading nest of ifs,
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
gentle-introduction-to-ACL2-programming
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.
