On this tour you will learn a little about what ACL2 is for rather than how ACL2 works. At the bottom of the ``page'' (which may extend beyond the end of your screen) there is a small ``flying tour'' icon. Click on it to go to the next page of the tour.

The tour visits the following topics sequentially.

The Flight Plan* This Documentation * What is ACL2? * Mathematical Logic * Mechanical Theorem Proving * Mathematical Models in General * Mathematical Models of Computing Machines Formalizing Models Running Models Symbolic Execution of Models Proving Theorems about Models * Requirements of ACL2 The User's Skills Training Host System

We intend the tour to take about 10 minutes of your time. Some pages on the tour contain pointers to other documents. You need not follow these pointers to stay on the tour.

Below we show the first target term, extracted from the current conjecture. Below it we show the associativity rule.

The variables of the rewrite rule are **instantiated** so that the
**left-hand side** of the rule matches the target:

variable term from target a x1 b x2 c (app x3 x4)

Then the target is **replaced** by the instantiated **right-hand side**
of the rule.

Sometimes rules have **hypotheses**. To make a long story short,
if the rule has hypotheses, then after matching the left-hand side,
the rewriter instantiates the hypotheses and rewrites them recursively.
This is called **backchaining**. If they all rewrite to true, then
the target is replaced as above.

For more details on how the ACL2 rewriter works, see Boyer and Moore's
book **A Computational Logic**, Academic Press, 1979.

This warning sign, which usually appears as ``'', indicates that the link it marks takes you into ACL2's online documentation.

The documentation is a vast graph of documented topics intended to
help the *user* of ACL2 rather than the *potential user*. If
you are exploring ACL2's home page to learn about the system,
perhaps you should go back rather than follow the link marked with
this sign. But you are welcome to explore the online documentation
as well. Good luck.

Observe that the states in typical models talk about

booleansintegersvectorsrecordscachesbitssymbolsarraysstacksfilescharactersstringssequencestablesdirectories

These objects are **discrete** rather than **continuous**;
furthermore they are built incrementally or **inductively** by
repeatedly using primitive operations to put together smaller peices.

The functions we need to manipulate these objects do things like
**concatenate**, **reverse**, **sort**, **search**, **count**, etc.

On this tour you will learn a little more about the ACL2 logic, the theorem prover, and the user interface.

This time we will stick with really simple things, such as the associativity of list concatenation.

We assume you have taken the Flying Tour but that you did not necessarily follow all the ``off-tour'' links. So this tour may revisit some pages you've seen. Just click on the Walking Tour icon at the bottom of each page.

On this tour you will see many more links marked . We would
like to **discourage** you from following these links right
now. However we **encourage** you to **note them**. Basically, the
sign here illustrates the documentation and introduces you to
its main entry points. Once you have started to **use** ACL2 you can
take the Walking Tour again but pursue more of the indicated links.

ACL2 accepts 256 distinct characters, which are the characters
obtained by applying the function `code-char`

to each
integer from 0 to 255. Among these, Common Lisp designates certain
ones as `*standard-characters*`

, namely those of the form
`(code-char n)`

where n is from 33 to 126, together with
`#\Newline`

and `#\Space`

. The actual standard characters may
be viewed by evaluating the constant expression
`*standard-chars*`

.

The standard character constants are written by writing a hash mark followed by a backslash (#\) followed by the character.

The function `characterp`

recognizes characters. For more
details, See characters .

The function `cons`

creates an ordered pair. `Car`

and `cdr`

return the first and second components,
respectively, of an ordered pair. The function `consp`

recognizes ordered pairs.

Ordered pairs are used to represent lists and trees. See any Common Lisp documentation for a discussion of how list constants are written and for the many list processing functions available. Also, see programming where we list all the ACL2 primitive functions.

Here are some examples of list constants to suggest their syntax.

'(a . b) ; a pair whose car is 'a and cdr is 'b '(a . nil) ; a pair whose car is 'a and cdr is nil '(a) ; another way to write the same thing '(a b) ; a pair whose car is 'a and cdr is '(b) '(a b c) ; a pair whose car is 'a and cdr is '(b c) ; i.e., a list of three symbols, a, b, and c. '((a . 1) (b . 2)) ; a list of two pairs

It is useful to distinguish ``proper'' conses from ``improper'' ones,
the former being those cons trees whose right-most branch terminates with
`nil`

. A ``true list'' (see true-listp ) is either `nil`

or a proper cons. `(A b c . 7)`

is an improper cons and hence not a
true list.

Strings of ACL2 characters are written as sequences of characters delimited by ``double quotation marks'' ("). To put such a character in a string, escape it by preceding it with a backslash.

The function `stringp`

recognizes strings and `char`

will fetch the nth character of a string. There are many
other primitives for handling strings, such as `string<`

for
comparing two strings lexicographically. We suggest you
See programming where we list all of the primitive ACL2
functions. Alternatively, see any Common Lisp language
documentation.

Common Lisp's symbols are a data type representing words. They are
frequently regarded as atomic objects in the sense that they are not
frequently broken down into their constituents. Often the only
important properties of symbols is that they are not numbers,
characters, strings, or lists and that two symbols are not equal if
they look different (!). Examples of symbols include `PLUS`

and
`SMITH::ABC`

. All function and variable names in ACL2 are symbols.
When symbols are used as constants they must be quoted, as in
`'PLUS`

.

The symbol `T`

is commonly used as the Boolean ``true.'' The
symbol `NIL`

is commonly used both as the Boolean ``false'' and as
the ``empty list.'' Despite sometimes being called the ``empty
list'' `NIL`

is a **symbol** not an ``empty cons.'' Unlike other
symbols, `T`

and `NIL`

may be used as constants without quoting
them.

Usually, symbols are written as sequences of alphanumeric characters
other than those denoting numbers. Thus, `A12`

, `+1A`

and `1+`

are symbols but `+12`

is a number. Roughly speaking, when symbols
are read lower case characters are converted to upper case, so we
frequently do not distinguish `ABC`

from `Abc`

or `abc`

.
Click here for information about case conversion
when symbols are read. However, any character can be used in a
symbol, but some characters must be ``escaped'' to allow the Lisp
reader to parse the sequence as a symbol. For example, `|Abc|`

is
a symbol whose first character is capitalized and whose remaining
characters are in lower case. `|An odd duck|`

is a symbol
containing two #\Space characters. See any Common Lisp documentation
for the syntactic rules for symbols.

Technically, a symbol is a special kind of pair consisting of a
package name (which is a string) and a symbol name (which is also a
string). (See symbol-package-name and see symbol-name
.) The symbol SMITH::ABC is said to be in package "SMITH"
and to have the symbol name "ABC". The symbol `ABC`

in package
"SMITH" is generally not equal to the symbol `ABC`

in package
"JONES". However, it is possible to ``import'' symbols from one
package into another one, but in ACL2 this can only be done when the
package is created. (See defpkg .) If the
`current-package`

is "SMITH" then `SMITH::ABC`

may be
more briefly written as just `ABC`

. `Intern`

``creates''
a symbol of a given name in a given package.

The user interacts with the theorem prover by giving it definitions, theorems and advice (e.g., ``use this lemma.''), often in the form of books books .

The theorem prover uses the rules in the library of books the user has selected.

The theorem prover prints its proof attempts to the user.

When a theorem is proved it is converted to a rule under the control of the user's rule-classes .

**The informed user can make ACL2 do amazing things.**

The ACL2 theorem prover finds proofs in the ACL2 logic. It can be automatic. But most often the user must help it.

The user usually guides ACL2 by suggesting that it first prove key
**lemmas**. Lemmas are just theorems used in the proofs of other theorems.

Click here to continue.

Theorems, lemmas, definitions, and advice of various sorts can be stored in books .

When a theorem or definition is stored in a book, the user can
specify **how** it should be used in the future. When viewed this
way, theorems and definitions are thought of as **rules**.

The ACL2 theorem prover is **rule driven**. The rules are
obtained from books.

Click here to continue.

The example

ACL2 !>illustrates the fact that ACL2's logic is untyped (click here for a brief discussion of the typed versus untyped nature of the logic).(app '(a b c) 27)(A B C . 27)

The definition of `app`

makes no restriction of the arguments to lists.
The definition says that if the first argument satisfies `endp`

then return the second argument. In this example, when `app`

has recursed
three times down the `cdr`

of its first argument, `'(a b c)`

, it
reaches the final `nil`

, which satisfies `endp`

, and so 27 is returned.
It is naturally consed into the emerging list as the function returns from
successive recursive calls (since `cons`

does not require its arguments
to be lists, either). The result is an ``improper'' list, `(a b c . 27)`

.

You can think of `(app x y)`

as building a binary tree by replacing
the right-most tip of the tree `x`

with the tree `y`

.

ACL2 is used to construct mathematical models of computer hardware and software (i.e., ``digital systems'').

A **mathematical model** is a set of mathematical formulas used to
predict the behavior of some artifact.

The use of mathematical models allows **faster** and **cheaper** delivery
of **better** systems.

Models need not be **complete** or **perfectly accurate** to be useful to the
trained engineer.

Click here for more discussion of these assertions in an engineering context.

`t`

is a ``symbol'' and 3 is an ``integer.''
Roughly speaking the objects of ACL2 can be partitioned into the
following types:

Numbers`3, -22/7, #c(3 5/2)`

Characters`#\A, #\a, #\Space`

Strings`"This is a string."`

Symbols`'abc, 'smith::abc`

Conses (or Ordered Pairs)`'((a . 1) (b . 2))`

When proving theorems it is important to know the types of object
returned by a term. ACL2 uses a complicated heuristic algorithm,
called `type-set`

, to determine what types of objects a
term may produce. The user can more or less program the
`type-set`

algorithm by proving `type-prescription`

rules.

ACL2 is an ``untyped'' logic in the sense that the syntax is not
typed: It is legal to apply a function symbol of n arguments to any
n terms, regardless of the types of the argument terms. Thus, it is
permitted to write such odd expressions as `(+ t 3)`

which sums the
symbol `t`

and the integer 3. Common Lisp does not prohibit such
expressions. We like untyped languages because they are simple to
describe, though proving theorems about them can be awkward because,
unless one is careful in the way one defines or states things,
unusual cases (like `(+ t 3)`

) can arise.

To make theorem proving easier in ACL2, the axioms actually define a
value for such terms. The value of `(+ t 3)`

is 3; under the ACL2
axioms, non-numeric arguments to `+`

are treated as though they
were 0.

You might immediately wonder about our claim that ACL2 is Common
Lisp, since `(+ t 3)`

is ``an error'' (and will sometimes even
``signal an error'') in Common Lisp. It is to handle this problem that
ACL2 has **guards**. We will discuss guards later in the Walking Tour.
However, many new users simply ignore the issue of guards entirely.

You should now return to the Walking Tour.

The ACL2 Home Page is integrated into the ACL2 online documentation. Over 1.5 megabytes of text is available here.

The vast majority of the text
is user-level documentation. For example, to find out about rewrite
rules you could click on the word ``rewrite .''
**But before you do that** remember that you must then use your browser's
**back** commands to come back here.

The tiny warning signs mark pointers that lead out of the
introductory-level material and into the user documentation. If you are
taking the Flying Tour, we advise you to **avoid** following such pointers the
first time; it is easy to get lost in the full documentation unless
you are pursuing the answer to a specific question. If you do wander down
these other paths, remember you can **back** out to a page containing the
Flying Tour icon to resume the tour.

At the end of the tour you will have a chance to return to The Flight Plan where you can revisit the main stops of the Flying Tour and explore the alternative paths more fully.

Finally, every page contains two icons at the bottom. The ACL2 icon leads you back to the ACL2 Home Page. The Index icon allows you to browse an alphabetical listing of all the topics in ACL2's online documentation.

`APP`

must have several properties to be admitted to the logic as a new
axiom
The key property a recursive definition must have is that the recursion terminate. This, along with some syntactic criteria, insures us that there exists a function satisfying the definition.

Termination must be proved before the definition is admitted. This is done in general by finding a measure of the arguments of the function and a well-founded relation such that the arguments ``get smaller'' every time a recursive branch is taken.

For `app`

the measure is the ``size'' of the first argument, `x`

,
as determined by the primitive function `acl2-count`

. The
well-founded relation used in this example is `e0-ordinalp`

, which is the standard ordering on the ordinals less than
``epsilon naught.'' These particular choices for `app`

were made
``automatically'' by ACL2. But they are in fact determined by
various ``default'' settings. The user of ACL2 can change the
defaults or specify a ``hint'' to the `defun`

command to
specify the measure and relation.

You should now return to the Walking Tour.

`ACL2 !>`

'' is the ACL2 prompt.
The prompt tells the user that an ACL2 command is expected. In addition, the prompt tells us a little about the current state of the ACL2 command interpreter. We explain the prompt briefly below. But first we talk about the command interpreter.

An ACL2 command is generally a Lisp expression to be evaluated.
There are some unusual commands (such as :q for **quitting**
ACL2) which cause other behavior. But most commands are read,
evaluated, and then have their results printed. Thus, we call the
command interpreter a ``read-eval-print loop.'' The ACL2 command
interpreter is named `LD`

(after Lisp's ``load'').

A command like **(defun app (x y) ...)** causes ACL2 to evaluate the
defun function on **app**, **(x y)** and **...**. When
that command is evaluated it prints some information to the terminal
explaining the processing of the proposed definition. It returns
the symbol `APP`

as its value, which is printed by the command
interpreter. (Actually, `defun`

is not a function but a macro
which expands to a form that involves `state`

, a necessary
precondition to printing output to the terminal and to ``changing''
the set of axioms. But we do not discuss this further here.)

The `defun`

command is an example of a special kind of command
called an ``event.'' Events are those commands that
change the ``logical world'' by adding such things as axioms or
theorems to ACL2's data base. See world . But not
every command is an event command.

A command like **(app '(1 2 3) '(4 5 6 7))** is an example of a
non-event. It is processed the same general way: the function
**app** is applied to the indicated arguments and the result is
printed. The function **app** does not print anything and does not
change the ``world.''

A third kind of command are those that display information about the current logical world or that ``backup'' to previous versions of the world. Such commands are called ``history'' commands.

What does the ACL2 prompt tell us about the read-eval-print loop?
The prompt ```ACL2 !>`

'' tells us that the command will be read
with `current-package`

set to `"ACL2"`

, that guard checking
(see set-guard-checking ) is on (```!`

''), and that we are at
the top-level (there is only one ```>`

'').
For more about the prompt, see default-print-prompt .

You should now return to the Walking Tour.

Consider the binary trees `x`

and `y`

below.

In Lisp, `x`

is written as the list `'(A B)`

or, equivalently, as
`'(A B . NIL)`

. Similarly, `y`

may be written `'(C D E)`

.
Suppose we wish to replace the right-most tip of `x`

by the entire tree `y`

. This is denoted `(app x y)`

, where `app`

stands for ``append''.

We can define `app`

with:

(defun app (x y); Concatenate x and y.(declare (type (satisfies true-listp) x)); We expect x to end in NIL.(cond ((endp x) y); If x is empty, return y.(t (cons (car x); Else, copy first node(app (cdr x) y))))); and recur into next.

If you defined this function in some Common Lisp, then to run
`app`

on the `x`

and `y`

above you could then type

(app '(A B) '(C D E))and Common Lisp will print the result

`(A B C D E)`

.`app`

function discussed
in the Common Lisp page, Here is the definition again

(defun app (x y)(cond ((endp x) y)(t (cons (car x)(app (cdr x) y)))))

The next few stops along the Walking Tour will show you

* how to use the ACL2 documentation, * what happens when the above definition is submitted to ACL2, * what happens when you evaluate calls ofAlong the way we will talk about the`app`

, * what one simple theorem about`app`

looks like, * how ACL2 proves the theorem, and * how that theorem can be used in another proof.

When we complete this part of the tour we will introduce the notion of
**guards** and revisit several of the topics above in that context.

To analyze a model you must be able to reason about the operations and relations involved. Perhaps, for example, some aspect of the model depends upon the fact that the concatenation operation is associative.

In any Common Lisp you can confirm that

(app '(A B) (app '(C D) '(E F)))and

(app (app '(A B) '(C D)) '(E F)))both evaluate to the same thing,

`(A B C D E F)`

.
But what distinguishes ACL2 (the logic) from applicative Common Lisp (the
language) is that in ACL2 you can **prove** that the concatenation
function `app`

is associative when its arguments are true-lists,
whereas in Common Lisp all you can do is test that proposition.

That is, in ACL2 it makes sense to say that the following formula is a ``theorem.''

TheoremAssociativity of App (implies (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))))

Theorems about the properties of models are proved by symbolically
manipulating the operations and relations involved. If the
concatenation of sequences is involved in your model, then you may
well need the theorem above in order to that your model has some
particular property.

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 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.

Click here for a simple example of Common Lisp.

In ACL2 we have adopted Common Lisp as the basis of our modeling language.
If you have already read our brief note on Common Lisp and recall
the example of `app`

, please proceed. Otherwise
click here for an exceedingly brief introduction to
Common Lisp and then come **back** here.

In Common Lisp it is very easy to write systems of formulas that
manipulate discrete, inductively constructed data objects. In building
a model you might need to formalize the notion of sequences and define
such operations as concatenation, length, whether one is a permutation
of the other, etc. It is easy to do this in Common Lisp. Furthermore,
if you have a Common Lisp ``theory of sequences'' you can **run**
the operations and relations you define. That is, you can execute
the functions on concrete data to see what results your formulas produce.

If you define the function `app`

as shown above and then type

(app '(A B) '(C D E))in any Common Lisp, the answer will be computed and will be

`(A B C D E)`

.
The **executable** nature of Common Lisp and thus of ACL2 is very handy
when producing models.

But executability is not enough for a modeling language because the purpose of models is to permit analysis.

Click here to continue.

To type a symbol containing lower case characters you can enclose the
symbol in vertical bars, as in `|AbC|`

or you can put a ``backslash''
before each lower case character you wish to preserve, as in `A\bC`

.
`|AbC|`

and `A\bC`

are two different ways of writing the same
symbol (just like 4/2 and 1/2 are two different ways of writing the
same rational). The symbol has three characters in its name, the
middle one of which is a lower case b.

After producing a model, it must be **corroborated** against
reality. The Falling Body Model has been corroborated by a vast
number of experiments in which the time and distance were measured
and compared according to the formula. In general all models must
be corroborated by experiment.

The Falling Body Model can be derived from deeper models, namely Newton's laws of motion and the assertion that, over the limited distances concerned, graviation exerts a constant acceleration on the object. When the model in question can be derived from other models, it is the other models that are being corroborated by our experiments.

Because nature is not formal, we cannot **prove** that our models
of it are correct. All we can do is test our models against
nature's behavior.

Such testing often exposes restrictions on the applicability of our models. For example, the Falling Body Model is inaccurate if air resistance is significant. Thus, we learn not to use that model to predict how long it takes a feather to fall from a 200 foot tower in the earth's atmosphere.

In addition, attempts at corroboration might reveal that the model is actually incorrect. Careful measurements might expose the fact that the gravitational force increases as the body falls closer to earth. Very careful measurements might reveal relativistic effects. Technically, the familiar Falling Body Model is just wrong, even under excessive restrictions such as ``in a perfect vacuum'' and ``over small distances.'' But it is an incredibly useful model nonetheless.

There are several morals here.

**Models need not be complete to be useful.**

**Models need not be perfectly accurate to be useful.**

**The user of a model must understand its limitations.**