This is documentation for ACL2 Version 3.2
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

Pages Written Especially for the Tours    Pages Written Especially for the Tours

The ACL2 Home Page is generated from ACL2's online documentation
strings.  (How else could we achieve the total integration of ACL2's
online documentation with the home page?)  This page is just an
artifact of the structure of our documentation strings:  each string
must belong to a "major section" of the documentation database.  This
page is not structured to be used by a person browsing via the Web.  It
contains, in an arbitrary order, the pages written specificially for
the Web user.

Furthermore, browsing the pages below via the ACL2 :DOC command or via
TexInfo is often unsatisfying because those browsers do not support gif
files and the notion of going "back" to a node just visited.  If you
wish to look at the pages below, we strongly recommend that you do so
via a HTML-based Web browser.  Indeed, you should simply visit ACL2's
Home Page and take one of the Tours.

Generally, the topics listed above will not be of use to the ACL2 user.

A Flying Tour of ACL2    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
          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.

Flying Tour:  About the ACL2 Home Page

A Sketch of How the Rewriter Works    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    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 Trivial Proof

A Typical State    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 pieces.

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

Flying Tour:  Functions for Manipulating these Objects

A Walking Tour of ACL2    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.

Walking Tour:  Common Lisp

ACL2 Characters    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    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    ACL2 Strings

Strings of ACL2 characters are written as sequences of characters
delimited by "double quotation marks" (").  To put a double quotation
mark in a string (or, any other character such as backslash or newline
that seems to cause problems), 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    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.  See Conversion 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    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.

Walking Tour:  Rewrite Rules are Generated from DEFTHM Events

ACL2 as an Interactive Theorem Prover    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.

See ACL2 as an Interactive Theorem Prover (cont) to continue.

ACL2 as an Interactive Theorem Prover (cont)    ACL2 as an Interactive Theorem Prover (cont)

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.

See ACL2 System Architecture to continue.

Walking Tour:  ACL2 System Architecture

ACL2 is an Untyped Language    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 (see About Types
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    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.

See Models in Engineering for more discussion of these
assertions in an engineering context.

Flying Tour:  Models of Computer Hardware and Software

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

Flying Tour:  What Is ACL2(Q)

About the Admission of Recursive Definitions    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, ensures 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 o-p <>, 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    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    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).

Walking Tour:  An Example of ACL2 in Use

An Example of ACL2 in Use    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.

Walking Tour:  How To Find Out about ACL2 Functions

Analyzing Common Lisp Models    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)))

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

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

See An Example Common Lisp Function Definition for a simple
example of Common Lisp.

Walking Tour:  An Example Common Lisp Function Definition

Common Lisp as a Modeling Language    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 see Common Lisp
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.

See Analyzing Common Lisp Models to continue.

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

Flying Tour:  Models of Computer Hardware and Software

Evaluating App on Sample Input    Evaluating App on Sample Input

     ACL2 !>(app nil '(x y z))
     (X Y Z)

     ACL2 !>(app '(1 2 3) '(4 5 6 7))
     (1 2 3 4 5 6 7)

     ACL2 !>(app '(a b c d e f g) '(x y z))   ; see Conversion for an explanation
     (A B C D E F G X Y Z)

     ACL2 !>(app (app '(1 2) '(3 4)) '(5 6))
     (1 2 3 4 5 6)

     ACL2 !>(app '(1 2) (app '(3 4) '(5 6)))
     (1 2 3 4 5 6)

     ACL2!>(let ((a '(1 2))
                 (b '(3 4))
                 (c '(5 6)))
             (equal (app (app a b) c)
                    (app a (app b c))))
     T

As we can see from these examples, ACL2 functions can be executed more
or less as Common Lisp.

The last three examples suggest an interesting property of app.

Walking Tour:  The Associativity of App

Flawed Induction Candidates in App Example    Flawed Induction Candidates in App Example

Induction on a is unflawed:  every occurrence of a in the conjecture

     (equal (app (app a b) c)
            (app a (app b c)))

is in a position being recursively decomposed!

Now look at the occurrences of b.  The first (shown in bold below) is
in a position that is held constant in the recursion of (app a b).  It
would be "bad" to induct on b here.

     (equal (app (app a b) c)
            (app a (app b c)))

Free Variables in Top-Level Input    Free Variables in Top-Level Input

     ACL2 !>(equal (app (app a b) c)
                   (app a (app b c))))

     ACL2 Error in TOP-LEVEL:  Global variables, such as C, B, and A, are
     not allowed. See :DOC ASSIGN and :DOC @.

ACL2 does not allow "global variables" in top-level input.  There is no
"top-level binding environment" to give meaning to these variables.

Thus, expressions involving no variables can generally be evaluated,

     ACL2 !>(equal (app (app '(1 2) '(3 4)) '(5 6))
                   (app '(1 2) (app '(3 4) '(5 6))))
     (1 2 3 4 5 6)

but expressions containing variables cannot.

There is an exception to rule.  References to "single-threaded objects"
may appear in top-level forms.  See STOBJ <>.  A
single-threaded object is an ACL2 object, usually containing many
fields, whose use is syntactically restricted so that it may be given
as input only to certain functions and must be returned as output by
certain functions.  These restrictions allow single- threaded objects
to be efficiently manipulated.  For example, only a single copy of the
object actually exists, even though from a logical perspective one
might expect the object to be "copied on write."

The most commonly used single-threaded object in ACL2 is the ACL2
system state, whose current value is always held in the variable state
<>.

ACL2 provides a way for you to use state to save values of computations
at the top-level and refer to them later.  See assign <> and @ <>.

Functions for Manipulating these Objects    Functions for Manipulating these Objects

Consider a typical "stack" of control frames.

Suppose the model required that we express the idea of "the most recent
frame whose return program counter points into MAIN."

The natural expression of this notion involves

function application - "fetch the return-pc of this frame"

case analysis -  "if the pc is MAIN, then ..."

iteration or recursion - "pop this frame off and repeat."

The designers of ACL2 have taken the position that a programming
language is the natural language in which to define such notions,
provided the language has a mathematical foundation so that models can
be analyzed and properties derived logically.

is the language supported by ACL2.  See Common Lisp for an
optional and very brief introduction to Common Lisp.

Flying Tour:  Modeling in ACL2

Guards    Guards

Common Lisp functions are partial; they are not defined for all
possible inputs.  But ACL2 functions are total.  Roughly speaking, the
logical function of a given name in ACL2 is a completion of the Common
Lisp function of the same name obtained by adding some arbitrary but
"natural" values on arguments outside the "intended domain" of the
Common Lisp function.

ACL2 requires that every ACL2 function symbol have a "guard," which may
be thought of as a predicate on the formals of the function describing
the intended domain.  The guard on the primitive function car <>, for
example, is (or (consp x) (equal x nil)), which requires the argument
to be either an ordered pair or nil.  We will discuss later how to
specify a guard for a defined function; when one is not specified, the
guard is t which is just to say all arguments are allowed.

But guards are entirely extra-logical:  they are not involved in the
axioms defining functions.  If you put a guard on a defined function,
the defining axiom added to the logic defines the function on all
arguments, not just on the guarded domain.

So what is the purpose of guards?

The key to the utility of guards is that we provide a mechanism, called
"guard verification," for checking that all the guards in a formula are
true.  See VERIFY-GUARDS.  This mechanism will attempt to prove
that all the guards encountered in the evaluation of a guarded function
are true every time they are encountered.

For a thorough discussion of guards, see the paper [km97] in the ACL2
bibliography.

Guessing the Type of a Newly Admitted Function    Guessing the Type of a Newly Admitted Function

When a function is admitted to the logic, ACL2 tries to "guess" what
type of object it returns.  This guess is codified as a term that
expresses a property of the value of the function.  For app the term is

     (OR (CONSP (APP X Y))
         (EQUAL (APP X Y) Y))

which says that app returns either a cons or its second argument.  This
formula is added to ACL2's rule base as a type-prescription <> rule.
Later we will discuss how rules are used by the ACL2 theorem prover.
The point here is just that when you add a definition, the data base of
rules is updated, not just by the addition of the definitional axiom,
but by several new rules.

You should now return to the Walking Tour.