A Flying Tour of ACL2

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

A Sketch of How the Rewriter Works

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.

A Tiny Warning Sign

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.

A Trivial Proof

A Typical State

Observe that the states in typical models talk about

booleans    integers   vectors     records   caches
bits        symbols    arrays      stacks    files
characters  strings    sequences   tables    directories

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.

A Walking Tour of ACL2

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 Characters

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 .

ACL2 Conses or Ordered Pairs

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.

ACL2 Strings

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.

ACL2 Symbols

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.

ACL2 System Architecture

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.

ACL2 as an Interactive Theorem Prover

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.

ACL2 as an Interactive Theorem Prover (continued)

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.

ACL2 is an Untyped Language

The example

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

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.

About Models

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.

About Types

The universe of ACL2 objects includes objects of many different types. For example, 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.

About the ACL2 Home Page

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.

About the Admission of Recursive Definitions

You can't just add any formula as an axiom or definition and expect the logic to stay sound! The purported ``definition'' of 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.

About the Prompt

The string ``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.

An Example Common Lisp Function Definition

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

An Example of ACL2 in Use

To introduce you to ACL2 we will consider the app function discussed in the Common Lisp page, except we will omit for the moment the declare form, which in ACL2 is called a guard. We will deal with guards later.

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 of app,
  * what one simple theorem about app looks like, 
  * how ACL2 proves the theorem, and
  * how that theorem can be used in another proof.
Along the way we will talk about the definitional principle, types, the ACL2 read-eval-print loop, and how the theorem prover works.

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.

Analyzing Common Lisp Models

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)))
(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.''

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

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

Common Lisp as a Modeling Language

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.

Conversion to Uppercase

When symbols are read by Common Lisp they are converted to upper case. Note carefully that this remark applies to the characters in symbols. The characters in strings are not converted upper case.

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 2/4 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.

Corroborating Models

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.