This is documentation for ACL2 Version 3.3
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.

PE    print the events named by a logical name

     Example:
     :pe fn   ; sketches the command that introduced fn and
              ; prints in full the event within it that created fn.

See LOGICAL-NAME.

Pe takes one argument, a logical name, and prints in full the event
corresponding to the name.  Pe also sketches the command responsible
for that event if the command is different from the event itself.  See
PC for a description of the format used to display a command.
To remind you that the event is inferior to the command, i.e., you can
only undo the entire command, not just the event, the event is indented
slightly from the command and a slash (meant to suggest a tree branch)
connects them.

If the given logical name corresponds to more than one event, then :pe
will print the above information for every such event.  Here is an
example of such behavior.

     ACL2 !>:pe nth
           -4270  (ENCAPSULATE NIL ...)
                  \
     >V            (VERIFY-TERMINATION NTH)

     Additional events for the logical name NTH:
      PV   -4949  (DEFUN NTH (N L)
                         "Documentation available via :doc"
                         (DECLARE (XARGS :GUARD (AND (INTEGERP N)
                                                     (>= N 0)
                                                     (TRUE-LISTP L))))
                         (IF (ENDP L)
                             NIL
                             (IF (ZP N)
                                 (CAR L)
                                 (NTH (- N 1) (CDR L)))))
     ACL2 !>

If you prefer to see only the formula for the given name, for example
if it is part of a large mutual-recursion, see PF.

PE!    deprecated (see PE)

Please see PE.  :Pe now has the functionality formerly provided
by :pe!.

PF    print the formula corresponding to the given name

     Examples:
     :pf (:definition fn) ; prints the definition of fn as an equality
     :pf fn               ; same as above

     :pf (:rewrite foo)   ; prints the statement of the rewrite rule foo
     :pf foo              ; same as above

pf takes one argument, an event name or a rune, and prints the formula
associated with name.  If the argument is the name of a macro
associated with a function name by macro-aliases-table, then the
function name is used as the argument.

PL    print the rules for the given name or term

     Examples:
     :pl foo     ; prints rules that rewrite some call of foo
     :pl (+ x y) ; prints rules that rewrite (+ x y)

Pl takes one argument, which should be a symbol or a term.  If the
argument is a function symbol (or a macro corresponding to a function;
see MACRO-ALIASES-TABLE), :pl displays the :rewrite,
:definition, and :meta rules that rewrite some term whose top function
symbol is the one specified.  Otherwise, :pl displays the :rewrite and
:definition rules that rewrite the specified term, followed by the
applicable :meta rules.  For :rewrite and :definition rules, :pl also
shows the substitution that, when applied to the left-hand side of the
rule, yields the specified term.  For :meta rules, only those are
displayed that meet two conditions: the application of the metafunction
returns a term different from the input term, and if there is a
hypothesis metafunction then it also returns a term.  (A subtlety: In
the case of extended metafunctions (see
EXTENDED-METAFUNCTIONS), a trivial metafunction context is used for
the application of the metafunction.)

The kinds of rules printed by :pl are :rewrite rules, :definition
rules, and meta rules (not, for example, :forward-chaining rules).  If
you want to see all :clause-processor rules, issue the command
:print-clause-processor-rules, and for trusted clause-processors,
(table trusted-clause-processor-table); see CLAUSE-PROCESSOR and
see DEFINE-TRUSTED-CLAUSE-PROCESSOR.

PR    print the rules stored by the event with the given name

     Examples:

     :pr fn ; prints the rules from the definition of fn (including any
            ; :type-prescription rule and :definition rule)

     :pr assoc-append ; if assoc-append is a rewrite rule, prints that rule

Also see PR!, which is similar but works at the command level
instead of at the event level, and see PL, which displays all
rewrite rules for calls of fn, not just those introduced at definition
time.

Pr takes one argument, a logical name, and prints the rules associated
with it.  In each case it prints the rune, the current enabled/disabled
status, and other appropriate fields from the rule.  It may be helpful
to read the documentation for various kinds of rules in order to
understand the information printed by this command.  For example, the
information printed for a linear rule might be:

       Rune:     (:LINEAR ABC)
       Status:   Enabled
       Hyps:     ((CONSP X))
       Concl:    (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X))
       Max-term: (ACL2-COUNT (CAR X))
       Backchain-limit-lst:    (3)

The hyps and concl fields for this rule are fairly self-explanatory,
but it is useful to see LINEAR to learn about maximal terms
(which, as one might guess, are stored under "Max-term").

Currently, this function does not print congruence rules or equivalence
rules.

The expert user might also wish to use find-rules-of-rune.  See
FIND-RULES-OF-RUNE.

PR!    print rules stored by the command with a given command descriptor

     Examples:

     :pr! fn ; prints the rules from the definition of fn (including any
             ; :type-prescription rule and :definition rule), as well as all other
             ; rules created by the command that created by fn (which could be
             ; many rules if, for example, fn was defined by an include-book
             ; command).

     :pr! :max ; prints all the rules stored by the most recent command

Also see PR, which is similar but works at the event level
instead of at the command level.

Pr takes one argument, a command descriptor, and prints the rules
created by the corresponding event.  In each case it prints the rune,
the current enabled/disabled status, and other appropriate fields from
the rule.  See PR for further details.

PUFF    replace a compound command by its immediate subevents

     Example Forms:
     ACL2 !>:puff :max
     ACL2 !>:puff :x
     ACL2 !>:puff 15
     ACL2 !>:puff "book"

     General Form:
     :puff cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command (see below).  Puff replaces the command at cd by the
immediate subevents of the command, executed as commands.  Puff then
prints, using pcs, the puffed region.

A "puffable" command is an encapsulate command, an include-book
command, or any command other than those consisting of a single
primitive event.  For example, since defun is a primitive event, a
defun command is not puffable.  But a macro form that expands into
several defun events is puffable.  The only primitive event commands
that are puffable are encapsulate and include-book commands.  A
puffable command contains (interesting) subevents, namely, the events
in the body of the encapsulate, in the file of the book included, or in
the command block.  Obscure exception: an encapsulate command generated
by the macro define-trusted-clause-processor is not puffable.

The puff command "lifts" the immediate subevents of the indicated
command so that they become commands themselves.  The command puff*
recursively puffs the newly introduced commands.  See PUFF*,
which also gives an example illustrating both puff and puff*.  Puff
undoes the command at cd and replaces it by its immediate subevents.
Thus, in general the length of the history grows when a puff command is
executed.  If puff causes an error (see below), the logical world
remains unchanged from its initial configuration.

The intended use of puff is to allow the user access to the events
"hidden" inside compound commands.  For example, while trying to prove
some theorem, p, about a constrained function, fn, one might find that
the encapsulate, cd, that introduced fn failed to include an important
constraint, q.  Without puff, the only way to proceed is to undo back
through cd, create a suitable encapsulate that proves and exports q as
well as the old constraints, re-execute the new encapsulate, re-execute
the events since cd, and then try p again.  Unfortunately, it may be
hard to prove q and additional events may have to be inserted into the
encapsulate to prove it.  It may also be hard to formulate the "right"
q, i.e., one that is provable in the encapsulate and provides the
appropriate facts for use in the proof of p.

Using puff, the user can erase the encapsulate at cd, replacing it by
the events in its body.  Now the formerly constrained function, fn, is
defined as its witness.  The user can experiment with formulations and
proofs of q suitable for p.  Of course, to get into the ultimately
desired state -- where fn is constrained rather than defined and q is
exported by an encapsulate at cd -- the user must ultimately undo back
to cd and carry out the more tedious program described above.  But by
using puff it is easier to experiment.

Similar applications of puff allow the user of a book to expose the
innards of the book as though they had all be typed as commands.  The
user might then "partially undo" the book, keeping only some of the
events in it.

Puff operates as follows.  First, it determines the list of immediate
subevents of the command indicated by cd.  It causes an error if there
is only one subevent and that subevent is identical to the command --
i.e., if the command at cd is a primitive.  Next, puff undoes back
through the indicated command.  This not only erases the command at cd
but all the commands executed after it.  Finally, puff re-executes the
subevents of (the now erased) cd followed by all the commands that were
executed afterwards.

Observe that the commands executed after cd will generally have higher
command numbers than they did before the puff.  For example, suppose
100 commands have been executed and that :puff 80 is then executed.
Suppose command 80 contains 5 immediate subevents (i.e., is an
encapsulation of five events).  Then, after puffing, command 80 is the
first event of the puffed command, command 81 is the second, and so on;
104 commands appear to have been executed.

When puffing an encapsulate or include-book, the local commands are
executed.  Note that this will replace constrained functions by their
witnesses.

Finally, it is impossible to puff in the presence of include-book
commands involving certified files that have been altered since they
were included.  To be specific, suppose "arith" is a certified book
that has been included in a session.  Suppose that after "arith" was
included, the source file is modified.  (This might happen if the user
of "arith" is not its author and the author happens to be working on a
new version of "arith" during the same time period.)  Now suppose the
user tries to puff the command that included "arith".  The attempt to
obtain the subevents in "arith" will discover that the check sum of
"arith" has changed and an error will be caused.  No change is made in
the logical world.  A similar error is caused if, in this same
situation, the user tries to puff any command that occurred before the
inclusion of "arith"!  That is, puff may cause an error and leave the
world unchanged even if the command puffed is not one involving the
modified book.  This happens because in order to reconstruct the world
after the puffed command, puff must obtain the events in the book and
if the book's source file has changed there is no assurance that the
reconstructed world is the one the user intends.

Warning: We do not detect changes to uncertified books that have been
included and are then puffed or re-included!  The act of including an
uncertified book leaves no trace of the check sum of the book.
Furthermore, the act prints a warning message disclaiming soundness.
In light of this, :puff quietly "re-"executes the current contents of
the book.

PUFF*    replace a compound command by its subevents

     Example Forms:
     ACL2 !>:puff* :max
     ACL2 !>:puff* :x
     ACL2 !>:puff* 15
     ACL2 !>:puff* "book"

     General Form:
     :puff* cd

where cd is a command descriptor (see COMMAND-DESCRIPTOR) for a
"puffable" command.  See PUFF for the definition of "puffable"
and for a description of the basic act of "puffing" a command.  Puff*
is just the recursive application of puff.  Puff* prints the region
puffed, using pcs.

To puff a command is to replace it by its immediate subevents, each of
which is executed as a command.  To puff* a command is to replace the
command by each of its immediate subevents and then to puff* each of
the puffable commands among the newly introduced ones.

For example, suppose "ab" is a book containing the following

     (in-package "ACL2")
     (include-book "a")
     (include-book "b")

Suppose that book "a" only contained defuns for the functions a1 and a2
and that "b" only contained defuns for b1 and b2.

Now consider an ACL2 state in which only two commands have been
executed, the first being (include-book "ab") and the second being
(include-book "c").  Thus, the relevant part of the display produced by
:pbt 1 would be:

     1 (INCLUDE-BOOK "ab")
     2 (INCLUDE-BOOK "c")

Call this state the "starting state" in this example, because we will
refer to it several times.

Suppose :puff 1 is executed in the starting state.  Then the first
command is replaced by its immediate subevents and :pbt 1 would show:

     1 (INCLUDE-BOOK "a")
     2 (INCLUDE-BOOK "b")
     3 (INCLUDE-BOOK "c")

Contrast this with the execution of :puff* 1 in the starting state.
Puff* would first puff (include-book "ab") to get the state shown
above.  But then it would recursively puff* the puffable commands
introduced by the first puff.  This continues recursively as long as
any puff introduced a puffable command.  The end result of :puff* 1 in
the starting state is

     1 (DEFUN A1 ...)
     2 (DEFUN A2 ...)
     3 (DEFUN B1 ...)
     4 (DEFUN B2 ...)
     5 (INCLUDE-BOOK "c")

Observe that when puff* is done, the originally indicated command,
(include-book "ab"), has been replaced by the corresponding sequence of
primitive events.  Observe also that puffable commands elsewhere in the
history, for example, command 2 in the starting state, are not affected
(except that their command numbers grow as a result of the splicing in
of earlier commands).

RESET-KILL-RING    save memory by resetting and perhaps resizing the kill ring used by oops

By default, ACL2 holds on to old logical worlds when you undo commands
(see UBT), as documented elswhere; see OOPS.  You can
free up memory by deleting those old worlds using reset-kill-ring.

     Examples:
     (reset-kill-ring t state)   ; replace each element of the kill ring by nil
     (reset-kill-ring 2 state)   ; create a new kill ring of '(nil nil)
     (reset-kill-ring 0 state)   ; create a new kill ring that is empty
     (reset-kill-ring nil state) ; just return the length of the kill ring

     General form:
     (reset-kill-ring n state)

where n evaluates either to t, to nil, or to a nonnegative integer (a
natp).  If n evaluates to t, it is treated as the length of the current
kill ring.  If n is nil, then the length k of the current kill ring is
returned as a value triple (mv nil k state).  If n is a natp, then the
kill ring is replaced with a list of n nils.

In particular, use (reset-kill-ring 0 state) to avoid saving any old
logical worlds, at the cost of disabling the effect of the oops command.

U    undo last command, without a query

     Example:
     :u

The keyword command :u is the same as :ubt :max, but with related
queries suppressed appropriately.  :Oops will undo the last :u.  See
UBT, see UBU, see UBT!, and see UBU!.

UBT    undo the commands back through a command descriptor

     Examples:
     :ubt :max      ; undo back through the most recent command
                    ; (which just means undo the most recent command)
     :ubt :x        ; same as :ubt :max
     :u             ; same as :ubt :max with no questions asked
     :ubt fn        ; undo back through the introduction of fn
                    ; (including all the other events in fn's block)
     :ubt 5         ; undo back through the fifth command executed
     :ubt (:max -4) ; undo back through the most recent five commands
     :ubt (:x -4)   ; undo back through the most recent five commands

See COMMAND-DESCRIPTOR.

Ubt takes one argument, a command descriptor, and undoes the commands
from :max (aka :x) through the one described.  See
COMMAND-DESCRIPTOR.  Pbt will print the commands that ubt will undo.
:Oops will undo the undo.  See OOPS.

Ubt can cause errors or queries.  To avoid these, see UBT!.

It is important to remember that a command may create several events.
That is, the command that introduces fn1 may also introduce fn2.
Undoing the command that created either of these will undo them both.
The events created by a command constitute the command's "block" and we
can only undo entire blocks.  Use pcb to print the command block of a
command if you wish to see what will be lost by undoing the command.

Ubt will not undo into "prehistory".  :Ubt 1 will undo all of your
commands.  But :ubt -5 will cause an error, warning you that :ubt
cannot undo system initialization.

See U for how to undo just the latest command, and see
UBU and see UBU! for how to undo back up to, but not
including, the current command.

UBT!    undo commands, without a query or an error

     Example:
     :ubt! :x-4

The keyword command :ubt! is the same as :ubt, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the error triple returned by :ubt!  will always have a
first component of nil.  :Oops will undo the last :ubt!.  See
UBT, see UBU, and see U.

UBT-PREHISTORY    undo the commands back through the last reset-prehistory event

This command is only used to eliminate a reset-prehistory event.  If
your most recent reset-prehistory event does not have a flag argument
of t, then :ubt-prehistory undoes all command back through, and
including, that reset-prehistory event.

UBU    undo the commands back up to (not including) a command descriptor

     Examples:
     :ubu :x-3      ; undo the last three commands (same as :ubt :x-2)
     :ubu (:x -3)   ; same as above
     :ubu fn        ; undo back up to, but not including the introduction of fn
                    ; (so fn will continue to be defined)
     :ubu 5         ; undo back up to, but not including, the fifth command
                    ; executed (leaving the first five commands in place)

See COMMAND-DESCRIPTOR.

Ubu takes one argument, a command descriptor, and undoes the commands
from :max (aka :x) up to, but not including, the indicated command.
See COMMAND-DESCRIPTOR.

Ubu can cause errors or queries.  To avoid these, see UBU!.

Also see UBT, which is similar but also undoes the indicated
command.  As for :ubt, :oops will undo the undo (see OOPS) and
ubu will not undo into "prehistory".

See U for how to undo just the latest command, and see
UBT and see UBT! for how to undo back through (that is,
including) the current command.

UBU!    undo commands, without a query or an error

     Example:
     :ubu! :x-4

The keyword command :ubu! is the same as :ubu, but with related queries
suppressed appropriately, and with a guarantee that it is "error-free."
More precisely, the error triple returned by :ubu!  will always have a
first component of nil.  :Oops will undo the last :ubu!.  Also see
UBU, see UBT, and see U.

HONS-AND-MEMOIZATION    hash cons, function memoization, and applicative hash tables

Bob Boyer and Warren Hunt have developed a canonical representation for
ACL2 data objects and a function memoization mechanism to facilitate
reuse of previously computed results.  This facility includes
procedures to read and print ACL2 expressions in such a way that
repetition of some ACL2 objects is eliminated, thereby permitting a
kind of on-the-fly file compression.  The implementation does not alter
the semantics of ACL2 except to add a handful of definitions.

Much of the documentation for this topic is taken from the paper
"Function Memoization and Unique Object Representation for ACL2
Functions" by Robert S. Boyer and Warren A. Hunt, Jr., which has
appeared in the Sixth International Workshop on the ACL2 Theorem Prover
and Its Applications, ACM Digital Library, 2006.

You can build an experimental version of ACL2 that includes hash cons,
function memoization, and fast association lists (applicative hash
tables).  An easy way is to include the following with a make command:

     ACL2_HONS=h

So for example, to make an executable image and also documentation
(which will appear in subdirectories doc/EMACS and doc/HTML):

     make large DOC ACL2_HONS=h

In the implementation of the ACL2 logic, ACL2 data objects are
represented by Common Lisp objects of the same type, and the ACL2
pairing operation is internally implemented by the Common Lisp cons
function.  In Common Lisp, cons is guaranteed to provide a new pair,
distinct from any previously created pair.  We have defined a new ACL2
function HONS that is logically identical to the ACL2 cons function,
but whose implementation usually reuses an existing pair if its
components are identical to the components of an existing pair.  A
record of ACL2 HONS objects is kept, and when an ACL2 function calls
hons ACL2 searches for an existing identical pair before allocating a
new pair; this operation been called "hash consing".

It appears that hash consing was first conceived by A. P. Ershov in
1957, to speed up the recognition of common subexpressions.  Ershov
showed how to collapse trees to minimal DAGs by traversing trees bottom
up, and he used hashing to eliminate the re-evaluation of common
subexpressions.  Later, Eiichi Goto implemented a Lisp system with a
built-in hash consing operation: his h-CONS cells were rewrite
protected and free of duplicate copies, and Goto used this hash consing
operation to facilitate the implementation of a symbolic algebra system
he developed.

Memoizing functions also has a long history.  In 1967, Donald Michie
proposed using memoized functions to improve the performance of machine
learning.  Rote learning was improved by a learning function not
forgetting what it had previously learned; this information was stored
as memoized function values.

The use of hash consing has appeared many times.  For instance, Henry
Baker using hash consing to improve the performance of the well-known
Boyer rewriting benchmark.  Baker used both hash consing and function
memoization to improve the speed of the Takeuchi function, exactly in
the spirit of our implementation, but without the automated,
system-wide integration we report here.

The ACL2 implementation permits memoization of user-defined functions.
During execution a user may enable or disable function memoization on an
individual function basis, may clear memoization tables, and may even
keep a stack of memoization tables.  This facility takes advantage of
our implementation where we keep one copy of each distinct ACL2 data
object.  Due to the functional nature of ACL2, it is sufficient to have
at most one copy of any data structure; thus, a user may arrange to
keep data canonicalized.  This implementation extends to the entire
ACL2 system the benefits enjoyed by BDDs: canonicalization,
memoization, and fast equality check.

We have defined various algorithms using these features, and we have
observed, in some cases, substantial performance increases.  For
instance, we have implemented unordered set intersection and union
operations that operate in time roughly linear in the size of the sets.
Without using arrays, we defined a canonical representation for
Boolean functions using ACL2 objects.  We have investigated the
performance of rewriting and tree consensus algorithms to good effect,
and we believe function memoization offers interesting opportunities to
simplify algorithm definition while simultaneously providing
performance improvements.

We recommend that users focus at first on the logical definitions of
hons and other primitives rather than their underlying Common Lisp
implementations.  Integrated with this memoization system is a
performance monitoring system, which can provide real-time feedback on
the operation and usefulness of hons and function memoization.  For a
more detailed description of these tools, please see the ACL2 2006
workshop paper mentioned above.

The Fibonacci function is a small example that demonstrates the utility
of function memoization.  The following definition exhibits a runtime
that is exponential in its input argument.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (mbe
        :logic
        (cond ((zp x) 0)
              ((= x 1) 1)
              (t (+ (fib (- x 1)) (fib (- x 2)))))
        :exec
        (if (< x 2)
            x
          (+ (fib (- x 1)) (fib (- x 2))))))

Below we show how the ACL2 time$ utility can measure the time to
execute a call to the fib function (with some editing to avoid noise
from the underlying Common Lisp implementation).  Memoize is actually an
ACL2 macro that expands to a call of the ACL2 function used to identify
a function for memoization; see MEMOIZE.  This function also
accepts a well-formed term that must be true in order for the system to
memoize a call of the memoized function; to ensure that an instance of
the term is safe for evaluation in Common Lisp, a check is performed
that if the guard of the memoized function is satisfied, then this
instance will execute without error.

     ACL2 !>(time$ (fib 40))

     ... took 2,641 milliseconds (2.641 seconds) to run with 8 available CPU cores.
     During that period, 2,644 milliseconds (2.644 seconds) were spent in user mode
                         0 milliseconds (0.000 seconds) were spent in system mode
      16 bytes of memory allocated.
     102334155
     ACL2 !>(memoize 'fib)

     Summary
     Form:  ( TABLE MEMOIZE-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)

     Summary
     Form:  ( PROGN (TABLE MEMOIZE-TABLE ...) ...)
     Rules: NIL
     Warnings:  None
     Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
      FIB
     ACL2 !>(time$ (fib 40))

     ... took 19 milliseconds (0.019 seconds) to run with 8 available CPU cores.
     During that period, 20 milliseconds (0.020 seconds) were spent in user mode
                         0 milliseconds (0.000 seconds) were spent in system mode
      539,088 bytes of memory allocated.
      193 minor page faults, 0 major page faults, 0 swaps.
     102334155
     ACL2 !>(time$ (fib 100))

     ... took 0 milliseconds (0.000 seconds) to run with 8 available CPU cores.
     During that period, 0 milliseconds (0.000 seconds) were spent in user mode
                         0 milliseconds (0.000 seconds) were spent in system mode
      5,760 bytes of memory allocated.
      3 minor page faults, 0 major page faults, 0 swaps.
     354224848179261915075
     ACL2 !>(unmemoize 'fib)

We see that once the function fib is identified as a function for which
function calls should be memoized, the execution times are substantially
reduced.  Finally, we can prevent fib from being further memoized; in
fact, unmemoize erases the previously memoized values.

The implementation of hash consing, memoization, and applicative hash
tables involves several facets: canonical representation of ACL2 data,
function memoization, and the use of Lisp hash tables to improve the
performance of association list operations.  We discuss each of these
in turn, and we mention some subtle interrelationships.  Although it is
not necessary to understand the discussion in this section, it may
permit some users to better use this implementation.  This discussion
may be confusing for some ACL2 users as it makes references to Lisp
implementation features.

The ACL2 system is actually implemented as a Lisp program that is
layered on top of a Common Lisp system implementation.  ACL2 data
constants are implemented with their corresponding counterparts in
Common Lisp; that is, ACL2 cons pairs, strings, characters, numbers,
and symbols are implemented with their specific Common Lisp
counterparts.  This choice permits a number of ACL2 primitive functions
to be implemented with their corresponding Common Lisp functions, but
there are indeed differences.  ACL2 is a logic, and as such, it does
not specify anything to do with physical storage or execution
performance.  When ACL2 is used, the knowledgeable user can write
functions to facilitate the reuse of some previously computed values.

Recall the three mechanisms under discussion: hash consing, function
memoization, and fast association list operations.  The function
memoization mechanism takes advantage of the canonical representation
of data objects provided by the hons operation as does the fast
association list operation mechanism.  Each time hons is invoked, its
arguments are themselves converted, if necessary, to uniquely
represented objects.

The ACL2 universe is recursively closed under the cons pairing operation
and the atoms.  Hash consing (hons) is logically identical to cons, but
a set of tables is used to record each hons pair.  In fact, the
implementation provides a stack of such tables; thus a new environment
of tables can be requested, used, and then released; see
HONS-LET.  When a hons pair is requested, the implementation checks,
in the current set of tables, whether the requested pair already
exists.  If not, a new pair is created and a record of that pair is
made; otherwise, a reference to the previously created pair is
returned.  Thus, any data object created with hons has a unique
representation, as does every subcomponent.  We also arrange for
strings to have a unique representation -- only one copy of each
different string is kept -- and when any previously unseen string is an
argument to hons, we add the string to a unique table of strings.  A
system-wide benefit of having a canonical representation for data is
that equality comparisons between any two data objects can be done in
constant time.

The definition of hons in no way changes the operation of cons -- hons
creates a cons pair.  When asked to create a hons, the implementation
checks to see if there is a cons with the same car and cdr as the hons
being requested.  Thus, the only difference between the results of a
hons call and a corresponding cons call is a notation in some invisible
(to the ACL2 logic) tables where we record which cons elements are also
hons elements.  Since a hons is nothing but a cons, the operation of
car and cdr is unchanged.  In fact, the implementation is designed so
that at any time it is safe to clear the table identifying which cons
elements are also considered hons elements.

User-defined functions with defined and verified guards can be memoized.
When a function is memoized, a user-supplied condition restricts the
domain when memoization is attempted.  When the condition is satisfied,
memoization is attempted (assuming that memoization for the function is
presently enabled); otherwise, the function is just evaluated.  Each
memoized function has a hash table that is used to keep track of a
unique list of function arguments paired with their values.  If
appropriate, for each function the corresponding table is checked to
see if a previous call with exactly the same arguments already exists
in the table: if so, then the associated value is returned; if not,
then the function is evaluated and a new key-value pair is added to the
table of memoized values so that some future call will benefit from the
memoization.  With ACL2 user functions memoization can be dynamically
enabled and disabled.  There is an ACL2 function that clears a specific
memoization table.  And finally, just as with the hons table, a stack
of these function memoization tables is maintained; that is, it is
possible to memoize a function, use it a bit, set the memoized values
aside, start a new table, use it, and then return to the original table.

We next discuss the fast lookup operation for association lists.  When
a pair is added to an association list using the functions hons-acons or
hons-acons!, the system also records the key-value pair in an associated
hash table.  As long as a user only used these two functions when
placing key-value pairs on an association list, the key-value pairs in
the corresponding hash table will be synchronized with the key-value
pairs in the association list.  Later, if hons-get is used to look up a
key, then instead of performing a linear search of the association list
we consult the associated hash table.  If a user does not strictly
follow this discipline, then a linear search may be required.  In some
sense, these association lists are much like ACL2 arrays, but without
the burden of explicitly naming the arrays.  The ACL2 array compress1
function is analogous to the functions hons-shrink-alist and
hons-shrink-alist!.  There are user-level ACL2 functions that allow the
associated hash tables to be cleared and removed.

REFERENCES

Baker, Henry G., The Boyer Benchmark at Warp Speed . ACM Lisp Pointers
V,3 (Jul-Sep 1992), pages 13-14.

Baker, Henry G., A Tachy 'TAK'.  ACM Lisp Pointers Volume 3,
July-September, 1992, pages 22-23.

Robert S. Boyer and Warren A. Hunt, Jr., Function Memoization and
Unique Object Representation for ACL2 Functions, in the Sixth
International Workshop on the ACL2 Theorem Prover and Its Applications,
ACM Digital Library, 2006.

A. P. Ershov.  On Programming of Arithmetic  Operations.  In the
Communications of the ACM, Volume 118, Number 3, August, 1958, pages
427-430.

Eiichi Goto, Monocopy and Associative Algorithms in Extended Lisp,
TR-74-03, University of Toyko, 1974.

Richard P. Gabrial.  Performance and Evaluation of Lisp Systems.  MIT
Press, 1985.

Donald Michie.  Memo functions: a Language Feature with Rote Learning
Properties.  Technical Report MIP-R-29, Department of Artificial
Intelligence, University of Edinburgh, Scotland, 1967.

Donald Michie.  Memo Functions and Machine Learning.  In Nature,
Volumne 218, 1968, pages 19-22.

HONS    hash cons

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION.

Logically, hons is merely another name for cons, i.e., the following is
an ACL2 theorem.

     (equal (hons x y) (cons x y))

However, hons creates a special kind of cons pair, which we call a hons
pair or, for short, hons.

Hons generally runs slower than cons because in creating a hons, an
attempt is made to see whether a hons already exists with the same car
and cdr.  This involves search and the use of hash-tables.  In the worst
case, honsing can be arbitrarily slow, but our experience in OpenMCL is
that honsing is generally about 20 times as slow as consing.

In our implementation, every hons really is a cons pair, but not every
cons pair is a hons, as can be determined by using eq in raw Common
Lisp.  For example, consider this interaction in raw Common Lisp.

     ? (setq x (cons 1 2))
     (1 . 2)
     ? (setq y (hons 1 2))
     (1 . 2)
     ? (setq z (hons 1 2))
     (1 . 2)
     ? (eq y z)
     T
     ? (eq x y)
     NIL

HONS-LET    push a temporary, new environment for hash consing

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION.

The value of (hons-let form) is the same as the value of form.
However, in the former case a new hons environment is temporarily
created, where no hash conses are stored.  The pre-existing hons
environment is restored upon exit from the evaluation of a hons-let
expression.

We may write more on this topic, especially upon request.

MISCELLANEOUS    a miscellany of documented functions and concepts
               (often cited in more accessible documentation)

Perhaps as the system matures this section will become more structured.

ABORT!    to return to the top-level of ACL2's command loop

When (abort!) is evaluated inside of ACL2's command loop, the current
computation is aborted and control returns to the top of the command
loop, exactly as though the user had interrupted and aborted the
current computation.

Logically speaking, (abort!) = nil.  But imagine that it is defined in
such a way that it causes a stack overflow or other resource exhaustion
when called.