Major Section: EVENTS

This documentation topic relates to an experimental extension of ACL2 under development by Bob Boyer and Warren Hunt. See hons-and-memoization for a general discussion of memoization and the related features of hash consing and applicative hash tables.

Examples: (memoize 'foo) ; remember the values of calls ; of foo (memoize 'foo :condition t) ; same as above (memoize 'foo :condition '(test x)) ; memoize for args satisfying ; the given condition (memoize 'foo :condition-fn 'test) ; memoize for args satisfying ; a call of the given function (memoize 'foo :inline nil) ; do not inline the definition ; of foo

## Some Related Topics

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

`fn`

evaluates to a user-defined function symbol; `condition`

is
either `t`

(the default) or `'t`

or else evaluates to an expression whose
free variables are among the formal parameters of `fn`

; and
`condition-fn`

is either `nil`

(the default) or else evaluates to a legal
function symbol. Further restrictions and options are discussed below. Note
that all arguments are evaluated (but for the special handling of value `t`

for `:commutative`

, the argument must literally be `t`

; see below).
Generally `fn`

must evaluate to a defined function symbol whose
`guard`

s have been verified. However, this value can be the name of a
macro that is associated with such a function symbol;
see macro-aliases-table. That associated function symbol is the one called
``memoized'' in the discussion below, but we make no more mention of this
subtlety.

It is illegal to memoize a function that is already memoized. To turn off memoization, see unmemoize.

In the most common case, `memoize`

takes a single argument, which evaluates
to a function symbol. We call this function symbol the ``memoized function''
because ``memos'' are saved and re-used, in the following sense. When a call
of the memoized function is evaluated, the result is ``memoized'' by
associating the call's arguments with that result, in a suitable table. But
first an attempt is made to avoid such evaluation, by doing a lookup in that
table on the given arguments for the result, as stored for a previous call on
those arguments. If such a result is found, then it is returned without
further computation. This paragraph also applies if `:condition`

is
supplied but is `t`

or `'t`

.

If in addition `:condition-fn`

is supplied, but `:condition`

is not, then
the result of evaluating `:condition-fn`

must be a defined function symbol
whose guards have been verified and whose formal parameter list is the
same as for the function being memoized. Such a ``condition function'' will
be run whenever the memoized function is called, on the same parameters, and
the lookup or table store described above are only performed if the result
from the condition function call is non-`nil`

.

If however `:condition`

is supplied, then an attempt will be made to define
a condition function whose guard and formal parameters list are the same
as those of the memoized function, and whose body is the result, `r`

, of
evaluating the given `condition`

. The name of that condition function is
the result of evaluating `:condition-fn`

if supplied, else is the result of
concatenating the string `"-MEMOIZE-CONDITION"`

to the end of the name of
the memoized function. The condition function will be defined with
guard verification turned off, but that definition will be followed
immediately by a `verify-guards`

event; and this is where the optional
`:hints`

and `:otf-flg`

are attached. At evaluation time the condition
function is used as described in the preceding paragraph; so in effect, the
condition (`r`

, above) is evaluated, with its variables bound to the
corresponding actuals of the memoized function call, and the memoized
function attempts a lookup or table store if and only if the result of that
evaluation is non-`nil`

.

Calls of this macro generate events of the form
`(table memoize-table fn ((:condition-fn fn) (:inline i) ...))`

. When
successful, the returned value is of the form
`(mv nil function-symbol state)`

.

When `:inline`

has value `nil`

, then `memoize`

does not use the
definitional body of `fn`

in the body of the new, memoized definition of
`fn`

. Instead, `memoize`

lays down a call to the `symbol-function`

for
`fn`

that was in effect prior to memoization. Use value `t`

for
`:inline`

to avoid memoizing recursive calls to `fn`

directly from within
`fn`

.

If `:trace`

has a non-`nil`

value, then `memoize`

also traces in a
traditional Lisp style. If `:trace`

has value `notinline`

or
`notinline`

, then a corresponding declaration is added at the beginning of
the new definition of `fn`

.

A non-`nil`

value for `:commutative`

can be supplied if `fn`

is a
binary function. If the `memoize`

event is successful, then subsequently:
whenever each argument to `fn`

is either a rational number or a hons,
then when the evaluation of `fn`

on those arguments is memoized, the
evaluation of `fn`

on the swap of those arguments is, in essence, also
memoized. If `:commutative`

is supplied and is not `nil`

or `t`

, then
it should be the name of a previously-proved theorem whose formula states the
commutativity of `fn`

, i.e., is the formula `(equal (fn x y) (fn y x))`

for a pair `{x,y}`

of distinct variables. If `:commutative`

is `t`

-- but not merely an expression that evaluates to `t`

-- then an
attempt to prove such a lemma will be made on-the-fly. The name of the lemma
is the symbol in the same package as `fn`

, obtained by adding the suffix
`"-COMMUTATIVE"`

to the `symbol-name`

of `fn`

. If the proof
attempt fails, then you may want first to prove the lemma yourself with
appropriate hints and perhaps supporting lemmas, and then supply the name of
that lemma as the value of `:commutative`

.

If `:memo-table-init-size`

is supplied, then it should be a positive
integer specifying the initial size of an associated hash table.

If `:verbose`

is supplied, it should either be `nil`

, which will inhibit
proof, event, and summary output (see with-output), or else `t`

(the
default), which does not inhibit output. If the output baffles you, try

:trans1 (memoize ...)to see the single-step macroexpansion of your

`memoize`

call.
If `:commutative`

is supplied, and a non-commutative condition is provided
by `:condition`

or `:condition-fn`

, then although the results will be
correct, the extra memoization afforded by `:commutative`

is unspecified.

The default for `:forget`

is `nil`

. If `:forget`

is supplied, and not
`nil`

, then it must be `t`

, which causes all memoization done for a
top-level call of `fn`

to be forgotten when that top-level call exits.

`Memoize`

is illegal for a function whose arguments include `state`

or,
more generally, any stobj. Also, `memoize`

never allows attachments
to be used (see defattach); if an attachment is used during evaluation, then
the evaluation result will not be stored.