|
|
|---|
|
|
|
|---|
A Gentle Introduction to ACL2 Programming
ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. “ACL2” denotes “A Computational Logic for Applicative Common Lisp”. The ACL2 programming language is a subet of side-effect free Common Lisp. Mathematically speaking, all ACL2 programs are functions. When two calls of a function supply the same objects as inputs the calls return the same results. If all you want to do is define ACL2 functions and run them, you don't need to know how to use ACL2 as a theorem prover. This introduction is all you need.
If you haven't installed ACL2 on your machine, do so, by following the instructions at “Obtaining, Installing, and License” on the ACL2 Home Page. As those instructions make clear, to run ACL2 you'll need a Common Lisp implementation. The instructions name several suitable ones.
In addition to the installation instructions, the Home Page has a wealth of
documentation. You should visit “The User's Manuals”. There
you'll see several versions of the manual, depending on whether you want
information about utilities developed by users. But we recommend that
newcomers just look at the basic “ACL2 User's Manual”. Explore it
briefly just so you know how to find more information. For example, type
“defun” into the Jump to box and hit return. You'll see details
of how to define functions and there are many links in that discussion to
related topics. But don't try to understand
The interface to the ACL2 system is a read-eval-print loop. It prints a prompt. You type some command and hit return. It reads and evaluates your command. It prints the results. And then it prompts you for your next input.
You could use ACL2 with no other interface. But most users prefer an enviroment in which they can prepare a command by editing the text before submitting it. We use an Emacs shell buffer for that. Other users use ACL2s, which is an Eclipse plug-in. This guide doesn't discuss the interface further and we just assume you can submit commands and see the output. The examples we provide are from our Emacs interface.
ACL2 is implemented (largely) in ACL2. That is, almost all the system code is written in the ACL2 subset of Common Lisp. The examples provided here were prepared under ACL2 Version 8.5. Your output should be logically equivalent though the text may look a little different.
Now fire up your ACL2. You should see a prompt that looks like this
ACL2 !>
Type “:program” and a return.
ACL2 !>:program ACL2 p!>
The
Now type “
ACL2 !>:program ACL2 p!>(+ 2 2) 4 ACL2 p!>(+ 1 2 3 4) 10 ACL2 p!>(car '(hello world)) HELLO ACL2 p!>(cdr '(hello world)) (WORLD) ACL2 p!>(cons 'hello '(world)) (HELLO WORLD) ACL2 p!>
Sometimes computations cause errors, most commonly due to type violations or resource limitations. See the sections Type Errors and Stack Overflow below.
Here is an ACL2 program that takes a linear list of numbers and constructs a linear list of their squares. We've annotated it with Lisp comments. ACL2 ignores the comments. We'll explain the syntax later. For now we'll just interpret what this whole definition means.
(defun square-all (x)
; Make a list of the squares of the elements of the list x.
(cond
((endp x) ; If x is empty,
nil) ; return the empty list.
(t ; Otherwise,
(cons (* (car x) (car x)) ; square the first element and
(square-all (cdr x)))))) ; cons it onto the front of
; the squares of the rest.
If you aren't sure what a “linear list” is just hang in and
we'll get to it. But you've probably figured out that
Here is what it looks like if you submit the
ACL2 !>:program
...
ACL2 p!>(cons 'hello '(world))
(HELLO WORLD)
ACL2 p!>(defun square-all (x)
(cond ((endp x) nil)
(t (cons (* (car x) (car x))
(square-all (cdr x))))))
Summary
Form: ( DEFUN SQUARE-ALL ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SQUARE-ALL
ACL2 p!>
Once
ACL2 p!>(square-all '(1 2 3 4 5)) (1 4 9 16 25) ACL2 p!>(square-all nil) NIL ACL2 p!>(square-all '(-9 3/4 #c(0 5))) (81 9/16 -25) ACL2 p!>
ACL2 supports five very simple but rather abstract types of data:
Objects of each type are distinct. That is, no number is a character or a string or a symbol or a pair. Etc.
All of these objects are “first class” in the sense that you can pass them in as values to functions, return them as values from functions, and store them in lists and trees.
Many operators are provided for each type. Each operator is a function.
No ACL2 operator or function can modify, mutate, or otherwise alter the objects passed in as arguments.
Since you're probably more familiar with conventional programming languages
than functional (side-effect free) ones, let's talk operationally for a
moment. (This is a disservice to you! The operational view is more
complicated than the abstract mathematical view!) ACL2 is implemented on top
of a von Neumann architecture. So what happens “behind the
scenes” when the ACL2 function
ACL2 expressions are just nests of function calls. For example
Before we discuss ACL2 expressions further we must discuss the important issue of how you write down constants of each of the five types.
A few examples suffice to illustrate the common ways to enter numeric
constants:
We will list some operations on numbers later.
Here are examples of how to write character objects:
Strings are delimited by the double quote mark, e.g.,
This leaves us with symbols and conses. Two symbols are easy to
understand because they have counterparts in most programming languages:
Before we discuss other ACL2 functions however we must deal at length with symbols and conses. Many first-time Lisp programmers do not really understand the idea of symbols as data or the idea of lists and trees as data.
Symbols are sequences of alphabetic letters, signs and digits. So
Technically, a symbol can contain any sequence of characters and there are rules for writing symbols down so as to distinguish them from other constants. Using certain “escape” conventions you can actually write symbols containing spaces and parentheses, symbols composed entirely of digits, and symbols with other “weird” characters. But we will not go into these conventions in this introduction. We will limit ourselves to symbols that “look like” what you probably expect. Most often, symbols start with an alphabetic character and then contain just alphabetic characters, signs and digits. The first space, newline or parenthesis you encounter while reading a symbol marks the end of the symbol and isn't part of it.
All programming languages (except binary machine code) have symbols at the syntactic level. Symbols are used to denote variables, functions, operations, keywords, etc., in the syntax of most programming languages. This is true in ACL2 too. But ACL2 is a little different in that it also provides symbols as data objects. That is, in addition to familiar data objects like numbers and strings, ACL2 provides symbols as a kind of data structure that can be manipulated. For example, a symbol can be converted to a string object, or decomposed into its constituent characters, or several symbols can be concatenated to create a longer symbol. But in this introduction we will just pass symbols around, compare them to other objects, and create lists (conses) containing symbols as elements.
As noted,
Symbols are more complicated than described above because in addition to
their names they belong to “packages.” For example, there might be
a symbol named
There is a special package called the
When we write symbols, case is unimportant (unless that previously
mentioned “escape” convention is used). When reading a symbol all
characters are all uppercased. That is, ACL2 reads the symbol
ACL2 p!>'(Here is a list of SymBols!) (HERE IS A LIST OF SYMBOLS!) ACL2 p!>'(This list contains a |Weird Symbol|) (THIS LIST CONTAINS A |Weird Symbol|) ACL2 p>
ACL2 provides ways to construct symbols from strings, ways to construct strings from lists of character objects, and ways to construct character objects from integers. But elementary ACL2 programs rarely construct new symbols, strings and characters dynamically. The symbols, strings and characters manipulated during most program executions are entered initially in the input data (e.g., by reading a command line or input file). Therefore, we do not bother to describe how to “create” symbols, strings and characters and none of our examples create these objects dynamically.
We first discuss how to write down “cons pairs” and “
list objects”. Later we will describe the operations on them. There
are many ways to write the same list constant. This should not be surprising;
the same thing is true of numeric constants. Consider the fact that
Most programming languages support the idea of some kind of record structure with fields containing other objects. The only such record structure in ACL2 is the ordered pair or cons pair. A cons pair is just a pair of two objects. Sometimes we call a cons pair a “list pair” or a “dotted pair” or simply a “list.”
Any two objects may be put together into a cons pair. The cons pair
containing the integer
* / \ 1 2
or might be written in Cartesian coordinate notation as <
The tree we might draw as
* / \ 1 * / \ 2 3
or write in coordinate notation as <
Similarly,
*
/ \
/ \
* *
/ \ / \
1 2 3 4
or <<
The notation we are using to write list objects is called dot notation. It is a straightforward translation of the familiar coordinate notation in which parentheses replace the brackets and a dot replaces the comma.
But there are other ways to write these conses. This should not be
surprising. How many ways can you think of to write the number
Similarly, ACL2 has two rules that allow us to write cons pairs in a variety of ways. The first rule provides a special way to write trees like:
* / \ 1 nil
namely, you can write
The second rule provides a special way to write a cons pair that contains
another cons pair in the cdr. The rule allows us to write
Thus, the tree
*
/ \
1 *
/ \
2 *
/ \
3 nil
can be written in any of the following ways.
(1 . (2 . (3 . nil))) (1 . (2 . (3))) (1 . (2 3)) (1 2 3)
It can also be written in many other ways, e.g.,
Binary trees that terminate in
The linear list
The following is a linear list of pairs.
*
/ \
* \
/ \ \
A 1 *
/ \
* \
/ \ \
B 2 *
/ \
* \
/ \ \
C 3 nil
This list can be written
((A . 1) . ((B . 2) . ((C . 3) . NIL))).
By the way, lists such as the one above are so common they
have a name. They are called association lists or
alists and are used as keyed tables. The list above associates
the key
Lists are often used to represent more elaborate data structures. For example, an “account” might consist of a name, an id number, a balance and a list of transactions, laid out like this:
*
/ \
/ \
/ \
* *
/ \ / \
/ \ / \
name id bal trans
An example of an account object might be
(("John Smith" . 123456789) ; Name and id
.
(1254 . ; balance in cents
((DEPOSIT (1 21 1999) 1000) ; transactions
(WITHDRL (1 30 1999) 850)
(WITHDRL (2 5 1999) 215))))
Rather than refer to these four components in terms of the
We've seen that the basic idiom for defining a new function in ACL2 is to write
(defun f (v1 ... vn) body)
where
With a few exceptions, an expression is either
Variable symbols are written in the same way that symbol objects are
written, except
There are two kinds of constant expressions: those that can just be written
as ordinary objects and those that must be quoted. Character objects,
strings, numbers,
Function calls are written by writing an open parenthesis, the name of the
function and the n argument expressions, all separated by whitespace,
followed by a close parenthesis. For example
Consider the list object
*
/ \
CAR \
*
/ \
X NIL.
This object can be written as
We have said that an expression is either a variable, a constant, or a
function call of a function symbol of arity
An example expression is
(cons (cons 'square-all (cons x nil))
(cons '=
(cons (square-all x) nil)))
provided
Expressions have values computed with respect to an environment
assigning values to variable symbols. For example, if
((SQUARE-ALL (1 2 3)) = (1 4 9)).
Here is the algorithm for determining the value of an expression in an
environment. The value of a variable is just looked up in the environment.
The value of a constant expression is the obvious object. The value of a call
of a defined function is computed by (a) evaluating the n argument
expressions to obtain a sequence of n objects, (b) creating a new
environment in which the function's n parameters are assigned those
respective objects, and then (c) evaluating the body expression of the
function in that new environment. The value of a call of a primitive
function, like
For example, suppose we have added this definition
(defun sq (x) (* x x))
and we are in an environment where
(sq (+ 1 x)) = ; evaluate argument of sq, when x = 5 (sq 6) = ; evaluate body of sq, when x = 6 36.
The ACL2 system starts up with over eight thousand known functions, 32 of
which are primitive (defined by special code rather than definitions). The
rest are defined. Here is a brief summary of a few useful primitives. We
have biased this list to encourage merely integer arithmetic and list
processing. Some of the functions mentioned below are not actually primitive
but are defined as simple compositions of primitives. For example,
(IF p1
x1
(IF p2
x2
(IF ...
...
y)))
You can learn more about these functions by executing them on some sample
data. For example, the value of
Perhaps more interestingly, the value of
Most of your function definitions in ACL2 will fall into certain common
schemes. Here is an informal description of the three most common
schemes. We define the function
(defun visit (lst ...)
(cond ((endp lst) ...) ; No elements left to process.
(t . ; Some elements to process:
.
.
(car lst) ; do something with this element
(visit (cdr lst) ...) ; and visit the rest.
.
.
.)))
We illustrate this scheme in the next section.
(defun visit (tree ...)
(cond ((atom tree) ...) ; The tree is a leaf: do something.
(t . ; The tree is an interior node:
. tree ; do something with it,
.
(visit (car tree) ...) ; visit nodes in left branch, and
. (visit (cdr tree) ...) ; visit nodes in right branch.
.
.)))
Visiting every element of a linear list is just the
special case of exploring a binary tree in which we visit only the successive
subtrees along the
(defun visit (n ...)
(cond ((zp n) ...) ; N “is” 0: finish up!
(t . ; N is a positive integer:
. n ; do something with it, and
.
(visit (- n 1) ...) ; visit the naturals below it.
.
.
.)))
The reason “is” is in quotation marks above is that
When you define a recursive function you often have the choice of computing the results “on the way up” or “on the way down.”
Suppose
(defun sum-up (x)
(cond ((endp x) 0)
(t (+ (car x) (sum-up (cdr x))))))
(defun sum-down (x temp)
(cond ((endp x) temp)
(t (sum-down (cdr x) (+ (car x) temp)))))
For example
Note that
In many applications, the
Of course, sometimes information about the elements already visited is
necessary to decide how to process subsequent ones, in which case the
Finally, when these two functions are compiled in a straightforward way,
the recursion in
ACL2 is applicative so it does not have assignment statements. But it is
possible to use “local variables” to save intermediate results.
Here is a function that computes x^4 + y^4, i.e., the sum of the fourth
powers of
(defun x4y4 (x y)
(let ((x2 (* x x)) ; Let x2 be x^2 and, “simultaneously,”
(y2 (* y y))) ; let y2 be y^2.
(+ (* x2 x2) ; Compute x^4 by squaring x^2 and
(* y2 y2)))) ; add it to y^4 computed similarly.
For example,
While
(let* ((x2 (* x x)) ; Let x2 be x^2, and then
(x4 (* x2 x2)) ; let x4 be x2^2, and then
(x8 (* x4 x4))) ; let x8 be x4^2.
x8) ; Return x8.
computes
Here is an example of a common use of
(defun depth (x)
(cond ((atom x) 0)
(t (let ((left-depth (depth (car x)))
(right-depth (depth (cdr x))))
(if (< left-depth right-depth)
(+ 1 right-depth)
(+ 1 left-depth))))))
Just to illustrate the definition and list notation, consider the tree
*
/ \
/ \
* *
/ \ / \
a * e *
/ \ / \
b * f g
/ \
c d
The longest branches in this tree have length four and terminate in either
((a . (b . (c . d))) . (e . (f . g)))
or equivalently as
The expression
We could have defined this function this way:
(defun depth (x)
(cond ((atom x) 0)
(t (if (< (depth (car x))
(depth (cdr x)))
(+ 1 (depth (cdr x)))
(+ 1 (depth (car x)))))))
But this would execute less efficiently because after recurring into both the
car and cdr of
Still a third way to define
(defun depth (x)
(cond ((atom x) 0)
(t (+ 1 (max (depth (car x))
(depth (cdr x)))))))
where
The next several functions all illustrate the “visiting every element of a linear list” recurrence scheme.
(defun mem (e x)
; Return t or nil according to whether e is an element of x.
(cond ((endp x) nil)
((equal e (car x)) t)
(t (mem e (cdr x)))))
Equivalently:
(defun mem (e x)
(if (endp x)
nil
(if (equal e (car x))
t
(mem e (cdr x)))))
or even
(defun mem (e x)
(and (not (endp x))
(or (equal e (car x))
(mem e (cdr x)))))
(Recall our caveat about multiple definitions of the same function. If you want to try one of these definitions in ACL2, fine. If you want to try all three, you'll have to give them distinct names.)
For all three of the above definitions, the following examples hold:
ACL2 p!>(mem 'd '(a b c d e f g)) T ACL2 p!>(mem 'd '(a b c e f g)) NIL ACL2 p!>
Here is a function to concatenate two lists together:
(defun app (x y)
(if (endp x) ;;; If x is exhausted,
y ;;; then return y
(cons (car x) ;;; else, cons the first element of x onto
(app ;;; the list obtained by recursively appending
(cdr x) ;;; the rest of x
y)))) ;;; to y.
Here are some examples of
ACL2 p!>(app '(1 2 3) '(a b c d)) (1 2 3 A B C D) ACL2 p!>(app '(1 2 3) nil) (1 2 3) ACL2 p!>(app (app '(1 2 3) '(4 5 6)) '(7 8 9)) (1 2 3 4 5 6 7 8 9) ACL2 p!>
Here is a function to find the first pair in an alist (if any) that binds a given key.
(defun lookup (key alist)
(cond ((endp alist) nil) ;;; If alist empty, return nil,
((equal key (car (car alist))) ;;; elseif the first pair contains key,
(car alist)) ;;; then return the first pair,
(t (lookup key (cdr alist))))) ;;; else look in the rest of alist.
Here are some examples.
ACL2 p!>(lookup 'b '((a . 1)(b . 2) (c . 3))) (B . 2) ACL2 p!>(lookup 'd '((a . 1)(b . 2) (c . 3))) NIL ACL2 p!>(lookup 'b '((a . 1)(b . 2) (b . 3))) (B . 2) ACL2 p!>
Note that only the first binding of the key matters.
Here is a function to “change” the value of a key in an alist. Note that it does not modify the alist but produces a new alist.
(defun store (key val alist)
(cond
((endp alist) ;;; If alist is empty,
(list (cons key val))) ;;; then return an alist with one binding,
((equal key (caar alist)) ;;; elseif the first pair binds key,
(cons (cons key val) ;;; then add the new binding to
(cdr alist))) ;;; the rest of the alist,
(t (cons (car alist) ;;; else cons this pair onto the result
(store ;;; of recursively putting a new binding
key val ;;; of key to val in
(cdr alist)))))) ;;; the rest of alist.
ACL2 p!>(store 'b 7 '((a . 1) (b . 2) (c . 3))) ((A . 1) (B . 7) (C . 3)) ACL2 p!>(store 'x 26 '((a . 1) (b . 2))) ((A . 1) (B . 2) (X . 26)) ACL2 p!>(store 'c 3 '((a . 1) (b . 2) (x . 26))) ((A . 1) (B . 2) (X . 26) (C . 3))
It is important to recall that ACL2 is functional (side-effect free)!
Despite its name,
ACL2 p!>(let* ((alist1 '((a . 1) (b . 2) (c . 3)))
(alist2 (store 'b 7 alist1)))
(list (lookup 'b alist1)
(lookup 'b alist2)))
((B . 2) (B . 7))
ACL2 p!>
The above expression binds
Here is a function to count the number of tips of a binary tree. This function illustrates the “visiting every node of a binary tree” scheme.
(defun count-tips (x)
(cond ((atom x) 1) ;;; X is a tip: it counts 1.
(t (+ (count-tips (car x)) ;;; X is a node: sum the counts
(count-tips (cdr x)))))) ;;; of the left and right subtrees.
The function above does the computation “on the way up.”
Here is a version that does it “on the way down.”
(defun count-tips (x temp)
(cond ((atom x) (+ 1 temp)) ;;; X is a tip: add its count to temp.
(t ;;; Otherwise, x is a node: Read the
;;; nest of two calls below inside-out:
;;; Count the tips in (car x) and add
;;; that into temp. Use the result as
;;; temp when you count the tips in
;;; (cdr x).
(count-tips (cdr x)
(count-tips (car x)
temp)))))
This function has one tail recursive call.
Let
*
/ \
/ \
* *
/ \ / \
a * e *
/ \ / \
b * f g
/ \
c d
which we can write as
ACL2 requires that subroutines be defined before they are used in other definitions. So what do you do if you have two functions, f and g, and f calls g and g calls f? You define them together. This is called mutual recursion.
The example below shows a very inefficient way to factor a number into a list of primes.
(mutual-recursion
(defun factors (n)
; Collect the prime factors of n.
(factors-below n (- n 1)))
(defun factors-below (n m)
; Return the prime factors of n that are less than or equal to m.
(cond ((or (zp m)
(equal m 1))
(list n))
((integerp (/ n m))
(app (factors (/ n m))
(factors m)))
(t (factors-below n (- m 1)))))
)
We can read this as follows. To determine the
We can run
It is sometimes useful to define functions that return more than one
result. Here is an example of a function that produces and uses multiple
values. The function explores a binary tree and counts (in its second
argument,
(defun node-and-tip-count (x nodes tips)
(cond
((atom x) ;;; X is a tip. Return a vector (list) of
(mv nodes ;;; two results: the number of nodes seen
(+ 1 tips)) ;;; and the number of tips seen (plus 1 for x).
)
(t ;;; X is a cons node.
(mv-let (nodes-in-car tips-in-car)
(node-and-tip-count (car x) nodes tips)
;;; The two lines above locally bind the variables
;;; nodes-in-car and tips-in-car to the number of
;;; nodes and tips, respectively, computed by the
;;; recursive call of this function on (car x)
;;; and the current running counts of nodes and tips.
;;; Then, below, we count the number of nodes and
;;; tips in (cdr x), starting with the counts for
;;; the car (and adding one for the node x).
(node-and-tip-count (cdr x)
(+ 1 nodes-in-car)
tips-in-car)))))
For example,
(node-and-tip-count '((a . b) . (c . d)) 0 0) = (3 4)
Thus, the tree in question has 3 cons nodes and 4 (non-cons) tips.
If you want to use multiple values you should read the ACL2 documentation on that topic.
The ACL2 programming language is untyped. Objects have types that can be
checked at runtime with predicates like
But when you start up ACL2, the read-eval-print loop is configured to
check types as it evaluates. Errors are signaled if types are violated.
However, if you want it to just plow into ill-typed data and get whatever
result the defaults produce, you can use the
ACL2 p!>(+ 2 2) 4 ACL2 p!>(+ 2 T) ACL2 Error in TOP-LEVEL: The guard for the function call (BINARY-+ X Y), which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)), is violated by the arguments in the call (BINARY-+ 2 T). See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 p!>:set-guard-checking nil Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 p>(+ 2 T) 2 ACL2 p>(CAR 'ABC) NIL ACL2 p>
Note that the prompt changes after the
Sometimes a computation will consume more space than your machine has.
For example, the following function constructs a list of
(defun nils (n)
(if (zp n)
nil
(cons nil (nils (- n 1)))))
We can run it on small values of
(nils 10) = (nil nil nil nil nil nil nil nil nil nil)
So that we don't have to read long lists of
ACL2 p!>(len (nils 10)) 10 ACL2 p!>(len (nils 100)) 100 ACL2 p!>(len (nils 1000)) 1000 ACL2 p!>(len (nils 10000)) 10000 ACL2 p!>(len (nils 100000)) 100000 ACL2 p!>(len (nils 1000000)) 1000000 ACL2 p!>(len (nils 10000000)) *********************************************** ************ ABORTING from raw Lisp *********** ********** (see :DOC raw-lisp-error) ********** Error: Stack overflow on value stack. ... :q ACL2 p!>
But that last test, where we attempt to produce a list of ten million
If you are interested in doing ``large'' calculations with ACL2 you will have to learn about how to compile definitions and how to use declarations to optimize code. Those topics are beyond the scope of this document.
However, often you can just code up a more efficient algorithm. For
example, the following tail-recursive version of
(defun nils (n ans)
(if (zp n)
ans
(nils (- n 1) (cons nil ans))))
So now
ACL2 p!>(len (nils 10000000 nil)) 10000000 ACL2 p!>(len (nils 100000000 nil)) 100000000 ACL2 p!>(len (nils 1000000000 nil)) 1000000000 ACL2 p!>
Of course, it will eventually use up all the memory.
The tests above sort of suggest we're interested in the question “Does
The ACL2 system includes a theorem prover. Below we show the commands you need to execute to answer the question in the affirmative. We've elided the output from these commands.
ACL2 p!>:logic
ACL2 !>(verify-termination nils)
...
ACL2 !>(defthm lemma-about-nils
(implies (natp n)
(equal (len (nils n ans))
(+ n (len ans)))))
...
ACL2 !>(defthm main-theorem-about-nils
(implies (natp n)
(equal (len (nils n nil)) n)))
...
That is, switch back into logic mode, admit
So maybe you should learn to prove theorems about your functions? If so, see “Recursion and Induction”.
You should be ready at this point to use ACL2 as a programming language to implement lots of simple list processing algorithms. Remember to go to the ACL2 User's Manual on the ACL2 Home Page to learn about other functions and features. If you need advice, check out the ACL2 Help list under the Mailing Lists link. The users who have volunteered to help are very responsive.
One final piece of advice: it is always best to code the simplest algorithm you can. Do not needlessly complicate your code. Optimize for performance only after confirming that the straightforward implementation is too inefficient for your application.