Common Lisp
Common Lisp
The logic of ACL2 is based on Common Lisp.
Common Lisp is the standard list processing programming language. It is
documented in: Guy L. Steele, Common Lisp
The Language, Digital Press, 12 Crosby Drive, Bedford, MA 01730,
1990.
ACL2 formalizes only a subset of Common Lisp. It includes such familiar
Lisp functions as cons, car and cdr for creating and
manipulating list structures, various arithmetic primitives such as +,
*, expt and <=, and intern and symbol-name for
creating and manipulating symbols. Control primitives include cond,
case and if, as well as function call, including recursion. New
functions are defined with defun and macros with defmacro. See
programming for a list of the Common Lisp primitives
supported by ACL2.
ACL2 supports five of Common Lisp's datatypes:
* the precisely represented, unbounded numbers (integers, rationals, and
the complex numbers with rational components, called the ``complex rationals''
here),
* the characters with ASCII codes between 0 and 255
* strings of such characters
* symbols (including packages)
* conses
ACL2 is a large subset of the first-order applicative part of Common
Lisp. (Roughly speaking, a language is applicative if it follows the rules of
function application. For example, f(x) must be equal to f(x),
which means, among other things, that the value of f must not be affected
by ``global variables'' and the object x must not change over time.) It
does not support higher-order features of Common Lisp, like functional objects
and apply. It does not support Common Lisp primitives that have
side-effects such as setq, setf, the Common Lisp Object
System, etc. However, ACL2 does provide some special features that can be
used efficiently to do many of the same jobs as these omitted Common Lisp
primitives. The ACL2 system is largely implemented in the language it
supports.
