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 :recursive nil) ; don't memoize recursive calls
(memoize 'foo :aokp t) ; attachments OK for stored results
(memoize 'foo :ideal-okp t) ; memoize even if foo is in :logic mode
; but has not been guard-verified
Some Related Topics
fn evaluates to a user-defined function symbol; condition is
either t (the default), 't, nil, or 'nil, 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. 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.
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 keyword argument :condition-fn is supplied, but :condition is not,
then the result of evaluating :condition-fn must be a defined function
symbol whose formal parameter list and guard are the same as for the
function being memoized. If fn is in :logic mode, then
guards must have been verified for :condition-fn. 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.
Suppose however that :condition is supplied. If the value supplied is
t or 't, then the lookup and table store described above are always
done. If the value is nil or 'nil, then this lookup and table store
are never done, although statistics may be gathered; see profile. Now
consider other values for :condition. 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.
Note that fn can be either a :logic mode function or a
:program mode function. However, only the corresponding raw Lisp
function is actually memoized, so guard violations can defeat
memoization, and :logic mode functions without their guards
verified will only be memoized when called by :program mode
functions. (See guards-and-evaluation for more information about guards and
evaluation in ACL2.) If fn is a :logic mode function and
:condition is supplied and not t or nil, then the condition must
be a guard-verified function.
Calls of this macro generate events of the form
(table memoize-table fn ((:condition-fn fn) ...)). When successful, the
returned value is of the form (mv nil function-symbol state).
Suppose that a function is already memoized. Then it is illegal to memoize
that function. Moreover, if the function was memoized with an associated
condition (i.e., was memoized with keyword :condition or
:condition-fn having value other than t or nil), then it is also
illegal to convert the function from :program to :logic
mode (see verify-termination). To turn off memoization, see unmemoize.
Memoize is illegal for a function if its arguments include state or
if it returns any stobjs. 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.
We conclude with by documenting keyword parameters not discussed above.
Keyword parameter :recursive is t by default, which means that
recursive calls of fn will be memoized just as ``top-level'' calls of
fn. When :recursive is instead set to nil, memoization is only
done at the top level. Using :recursive nil is similar to writing a
wrapper function that just calls fn, and memoizing the wrapper instead of
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 in :logic mode. 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 :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.
If :memo-table-init-size is supplied, then it should be a positive
integer specifying the initial size of an associated hash table.
Argument :aokp is relevant only when attachments are used; see defattach
for background on attachments. When :aokp is nil, the default,
computed values are not stored when an attachment was used, or even when an
attachment may have been used because a function was called that had been
memoized using :aokp t. Otherwise, computed values are always stored,
but saved values are not used except when attachments are allowed. To
summarize:
aokp=nil (default): ``Pure'', i.e., values do not depend on attachments - Fetch: always legal - Store: only store resulting value when attachments were not used aokp=t: ``Impure'', i.e., values may depend on attachments - Fetch: only legal when attachments are allowed (e.g., not during proofs) - Store: always legal
If :ideal-okp is supplied and not nil, then it is permitted to
memoize an ``ideal-mode'' function: one in :logic mode whose
guards have not been verified. In general, it is ill-advised to memoize
an ideal-mode function, because its calls are typically evaluated ``in the
logic'' without calling a memoized ``raw Lisp'' version of the function.
However, if the function is called by a :program mode function,
evaluation can transfer to raw Lisp before reaching the call of the memoized
function, in which case memoization will take place. For such situations you
can provide value :warn or t for keyword parameter :ideal-okp.
Both of these values allow memoization of ideal-mode functions, but if
:warn is supplied then a warning will take place. Note that you may set
the key :memoize-ideal-okp of the acl2-defaults-table to value
t or :warn to change the default, but if parameter :ideal-okp is
supplied, the acl2-defaults-table value is ignored.
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.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.
