Memoize
Turn on memoization for a specified function
See hons-and-memoization for a general discussion of the
``hons-enabled'' features: memoization, 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 :stats nil) ; don't collect info for (memsum)
(memoize 'foo :ideal-okp t) ; memoize for raw Lisp even if foo is
; in :logic but not guard-verified
General Form:
(memoize fn ; memoizes fn and returns fn
:aokp t/nil ; optional (default nil)
:commutative t/lemma-name ; optional (default nil)
:condition condition ; optional (default t (unless :invoke))
:condition-fn condition-fn ; optional
:forget t/nil ; optional (default nil)
:hints hints ; optional, for verifying the
; guards of condition-fn
:ideal-okp t/:warn/nil ; optional (default nil)
:invoke nil/fn ; optional (default nil)
:memo-table-init-size size ; optional (default *mht-default-size*)
:otf-flg otf-flg ; optional, for verifying the
; guards of condition-fn
:recursive t/nil ; optional (default t)
:stats t/nil ; optional (default t (unless :invoke))
:total ; ; see :DOC memoize-partial
:verbose t/nil ; optional (default nil)
)
where 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; if it returns any stobjs; if it has been excluded by never-memoize; or if it is excluded because it is ``special'' in the sense
that it is in the "COMMON-LISP" package, it has no fixed output
signature (i.e., it is in the value of the list constant
(if return-last do$
read-user-stobj-alist), (if return-last do$
read-user-stobj-alist)), it has associated
raw-Lisp code, or it is used in the implementation of hons-and-memoization. A constrained function (typically, one that is
introduced in the signature of an encapsulate event) cannot be
memoized; in that case, one may wish to memoize its caller or attachment (see
defattach). A stobj can be an input of a memoized function, but in
that case, the memoization table for that stobj will be cleared every time
that stobj is updated.
By default, memoize does not store results when any attachments have
been used (see defattach). However, such results are stored when
memoize keyword parameter :aokp has value t. Note that for
purposes of this discussion, the use of a stored value for a subsidiary
function that was memoized with :aokp t is treated as the use of an
attachment, since ACL2 does not know whether or not an attachment was actually
used in that case.
We conclude by documenting keyword parameters not discussed above.
Keyword parameter :invoke is nil by default, but its value can be
a symbol, g. Examples may be found in community-books file
demos/memoize-invoke-input.lsp; for a tool built on this capability that
supports evaluation using proved input-output pairs for a function, see add-io-pairs. The effect of :invoke g is to replace every call of
fn by a call of g. However, there are some restrictions. The
function symbol fn must be in :logic mode, and the symbol g
must be a guard-verified :logic-mode function symbol with
the same signature as that of fn. There is the following proof
obligation: there must be a theorem in the current ACL2 world stating
the equality of calls of fn and g on a duplicate-free argument list;
for example, if the formals list of fn is (x1 ... xn), then the
theorem could be (equal (fn x1 .... xn) (g x1 ... xn)). If ACL2 finds no
such theorem, it will print a defthm event that you may wish to
submit. Next we describe a potential second proof obligation, which will
similarly be printed if it is not met. Let guard-fn be the guard
for fn, and let guard-g be the result of substituting the formals of
fn for the formals of g in the guard for g. If guard-fn
tautologically implies guard-g (for example, the two are equal or
guard-g is 'T), then there is no further proof obligation.
Otherwise, there must be a theorem in the current ACL2 world of the
form (implies guard-fn guard-g). See verify-guard-implication for
a utility that makes it easy for you to prove such a theorem. Finally,
contrary to the usual defaults, the values of keyword :recursive,
:condition and :stats default to nil. Indeed, it is an error
to specify a non-nil value for :recursive. The alternate defaults of
nil for :condition and :stats can avoid memoization overhead
when one simply wishes to call g in place of fn; you may override
those defaults if you actually want to save computed values and use
(memsum) to see statistics.
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.
A non-nil value for :commutative can be supplied if fn is a
binary function in :logic mode. Suppose that the memoize event is
successful, and consider a subsequent call of fn for which some argument
to fn is either a rational number or, in some host Lisps (currently
either CCL, or GCL Version 2.6.12 or later) a hons. (Indeed, for such
GCL versions this is true for any cons, not just 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. Note that because most output
is inhibited by default, you might wish to supply keyword argument :verbose
t if the event fails.
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
Note that for this handling of :aokp, the computation of a value
returned by function apply$-userfn or badge-userfn is
considered to have used an attachment.
The default value for :stats is essentially t. (Technically,
this can be subverted by using raw Lisp, to change the default by changing the
values of variables *record-xxx* introduced in ACL2 source file
memoize-raw.lisp.) When :stats has its default value (assuming the
above raw Lisp changes are not made) or value t, calls of memoized
functions will collect information that can be displayed by calling memsum. But if :stats is nil, this information will not be
collected, possibly resulting in better performance for the memoized
function. As of this writing, built-in memoized functions use :stats nil
to benefit performance.
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. However, this might not have the effect
you desire, because you will be memoizing the submitted version of the
function, not its executable-counterpart that is executed in the ACL2 loop and
on behalf of the prover (see evaluation). Thus, if you memoize an
ideal-mode function and then call it at the top-level of the ACL2 loop (or,
for example, it is called to evaluate a ground term arising in a proof or in
the evaluation of a metafunction in a proof), the effects of
memoization will not be felt because the raw Lisp code is not run unless
guards are verified.
There are circumstances in which the raw Lisp code of an ideal-mode function
is called. For example, if the ideal-mode function is called by a
:program mode function, evaluation can transfer to raw Lisp where
the effects of memoization will be felt.
A trick, described below, with ec-call can provide some of the
benefit of memoizing an ideal-mode function. The trick exploits the fact that
ec-call allows you to call an ideal-mode function within a guard-verified (``Common Lisp compliant'') :logic mode function
without having to verify guards for the ideal-mode function. The following
edited log illustrates the points above.
ACL2 !>(defun fib (n)
(declare (xargs :guard (natp n) :verify-guards nil))
(if (zp n)
0
(if (eql n 1)
1
(+ (fib (- n 1)) (fib (- n 2))))))
[[ .. output omitted .. ]]
FIB
ACL2 !>(memoize 'fib :ideal-okp t)
FIB
ACL2 !>(time$ (fib 38)) ; slow: uses only executable-counterpart
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited
on recursive calls of the executable-counterpart (i.e., in the ACL2
logic) of FIB. To check guards on all recursive calls:
(set-guard-checking :all)
To leave behavior unchanged except for inhibiting this message:
(set-guard-checking :nowarn)
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 3.91 seconds realtime, 3.90 seconds runtime
; (416 bytes allocated).
39088169
ACL2 !>(time$ (fib 38)) ; still slow; no results were stored before
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited
on recursive calls of the executable-counterpart (i.e., in the ACL2
logic) of FIB. To check guards on all recursive calls:
(set-guard-checking :all)
To leave behavior unchanged except for inhibiting this message:
(set-guard-checking :nowarn)
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 3.92 seconds realtime, 3.91 seconds runtime
; (416 bytes allocated).
39088169
ACL2 !>(defun fib-logic-wrapper (n) ; guard-verified
(declare (xargs :guard (natp n)))
(ec-call (fib n)))
[[ .. output omitted .. ]]
FIB-LOGIC-WRAPPER
ACL2 !>(memoize 'fib-logic-wrapper)
FIB-LOGIC-WRAPPER
ACL2 !>(time$ (fib-logic-wrapper 38)) ; slow; no fib results are stored
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited
on recursive calls of the executable-counterpart (i.e., in the ACL2
logic) of FIB. To check guards on all recursive calls:
(set-guard-checking :all)
To leave behavior unchanged except for inhibiting this message:
(set-guard-checking :nowarn)
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 3.92 seconds realtime, 3.91 seconds runtime
; (2,128 bytes allocated).
39088169
ACL2 !>(time$ (fib-logic-wrapper 38)) ; fast; fib-logic-wrapper result was stored
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 0.00 seconds realtime, 0.00 seconds runtime
; (16 bytes allocated).
39088169
ACL2 !>(time$ (fib-logic-wrapper 37)) ; slow; result only for 38 was stored
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited
on recursive calls of the executable-counterpart (i.e., in the ACL2
logic) of FIB. To check guards on all recursive calls:
(set-guard-checking :all)
To leave behavior unchanged except for inhibiting this message:
(set-guard-checking :nowarn)
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 2.42 seconds realtime, 2.42 seconds runtime
; (416 bytes allocated).
24157817
ACL2 !>(defun fib-program-wrapper (n) ; program mode function
(declare (xargs :guard (natp n) :mode :program))
(fib n))
Summary
Form: ( DEFUN FIB-PROGRAM-WRAPPER ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FIB-PROGRAM-WRAPPER
ACL2 !>(time$ (fib-program-wrapper 100)) ; fast because raw-Lisp fib is called
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 0.00 seconds realtime, 0.00 seconds runtime
; (7,600 bytes allocated).
354224848179261915075
ACL2 !>
Two non-nil values are allowed for keyword parameter :ideal-okp:
:warn and t. Both of these values allow memoization of ideal-mode
functions, but if :warn is supplied then a warning will take place at
memoization time, specifically for the resulting table event. 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.
The value of :verbose is nil by default, which avoids output that
is typically distracting. Otherwise verbose should be t. We can
see the types of output that are inhibited by default by using :trans1 as follows follows (most output elided here); see with-output.
ACL2 !>:trans1 (memoize 'nth :verbose nil)
(WITH-OUTPUT
:OFF (SUMMARY PROVE EVENT)
:GAG-MODE NIL
...
ACL2 !>
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.
Subtopics
- Memoize-partial
- Memoize a partial version of a limited (`clocked') function
- Protect-memoize-statistics
- Ensure the integrity of memoization statistics even upon aborts
- Profile-all
- profile essentially all functions
- Profile-ACL2
- profile essentially all ACL2 functions
- Memoized-prover-fns
- Memoize some theorem prover functions
- Unmemoize
- Turn off memoization for the specified function
- Verify-guard-implication
- Guard implication for memoize keyword :invoke
- Memsum
- Display all collected profiling and memoization info
- Set-bad-lisp-consp-memoize
- Turn off or on memoization of raw Lisp function bad-lisp-consp
- Memoize-summary
- Display all collected profiling and memoization info
- Save-and-clear-memoization-settings
- Save and remove the current memoization settings
- Never-memoize
- Mark a function as unsafe to memoize.
- Clear-memoize-tables
- Forget values remembered for all the memoized functions
- Clear-memoize-statistics
- Clears all profiling info displayed by (memoize-summary)
- Clear-memoize-table
- Forget values remembered for the given function
- Restore-memoization-settings
- Restore the saved memoization settings
