|
|
|---|
|
|
|
|---|
Introduction to programming in ACL2 for Lisp users
The documentation topic, ACL2-built-ins, as well as its parent topic, programming, are starting points for a rich collection of primitives and features in the ACL2 programming language. In the present topic (below) we give a succinct introduction to that language for those who are already reasonably familiar with Common Lisp, or perhaps another Lisp. Follow the hyperlinks if you want to drill down; for example, we mention multiple values below but say very little about them, instead providing links to topics that explain their handling in a little more depth.
The documentation for ACL2 and its community-books provides a rich set of topics for further exploration. This particular topic is intended to serve only as a brief introduction to programming in ACL2 for those who know Lisp, especially Common Lisp. Supplementary reading that may interest a few readers includes ``A Precise Description of the ACL2 Logic'' (Matt Kaufmann and J Moore, April, 1998).
The ACL2 (``A Computational Logic for Applicative Common Lisp'')
programming language is essentially a subset of Common Lisp — albeit
with some useful extensions — that is applicative: the value
returned by a function depends only on its inputs, not state. (There is an
ACL2 notion of state, introduced briefly below; but that state must be
passed as an explicit argument.) Many commonly-used functions and special
forms in the applicative subset of Common Lisp are also in ACL2, such as (to
name just a very few) car, cons, nth, append,
let, and let*. A few others are not directly included in ACL2
because they have incomplete specifications in Common Lisp, such as pairlis; according to the Common Lisp HyperSpec: ``The new pairs may appear
in the resulting association list in either forward or backward order.'' Many
such functions tend to have close analogues in ACL2, named by concatenating
In the ACL2 read-eval-print loop, you can define functions and macros with defun and defmacro just as in Common Lisp, with some restrictions (see for example name) and also some additional declare forms.
Only certain Lisp data types are supported for programming in ACL2: numbers
that are either rational numbers or complex numbers with rational
coefficients (see numbers-introduction); the characters
constructed with
In particular, arrays are not directly supported as an ACL2 datatype (except for strings). However, ACL2 supports an applicative notion of array, which is logically an association list but has an associated Lisp array that provides fast reads in single-threaded programs. See arrays. If your code creates an array and does many more reads to it than writes, or even if there are rarely two writes to the same index (as when writes are primarily to initialize the array), then ACL2 arrays may perform well. Otherwise you may get significantly better performance, avoiding the consing done by writes (to build the association list), by using a different sort of representation of arrays in ACL2: single-threaded objects, or stobjs; see stobj.
Structures can be simulated in ACL2 using suitable macros. For a simple such macro that is built into ACL2, together with alternatives to it, see defrec.
If you are using ACL2 as a programming language but you do not intend to
prove anything about your code, at least not at first, then you might be
well-served by using program mode. In this mode, ACL2 will admit the
definition if syntactic checks succeed, in particular without requiring a
proof of termination for recursive definitions. You can specify the mode
directly in a declaration (see xargs for how to specify
When you are ready to reason about your functions, you can use
Many Common Lisp functions should only be applied to certain types of
objects: for example, car should only be applied to a cons pair or
Beginning ACL2 programmers should probably ignore guards, at least initially. Otherwise, see xargs for how to specify a guard; also see verify-guards.
The analogues of Common Lisp utilities
ACL2 provides a notion of state that is useful for certain kinds of
programming. As mentioned above, the state must be passed explicitly because
of the applicative nature of ACL2; indeed, it must be passed as the variable,
ACL2 does not provide
Another way for Lisp programmers to get answers to ``How do I do this in ACL2'' questions is to query the acl2-help mailing list. You can sign up via a link on the ACL2 home page. Moreover, that could be a good place to request or suggest improvements to this documentation topic! Also see history for some ways to query the current session.
Finally, here are a few specific alternatives to Common Lisp utilities.