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. See also http://www.cs.cmu.edu/Web/Groups/AI/html/cltl/cltl2.html.

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 very small subset of full Common Lisp. ACL2 does not include the Common Lisp Object System (CLOS), higher order functions, circular structures, and other aspects of Common Lisp that are non-applicative. 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.