MEMOIZE

turn on memoization for one function
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
                                    ; condition
(memoize 'foo :condition 'test-fn)  ; memoize for args satisfying
                                    ; test-fn
(memoize 'foo :inline nil)          ; do not inline the definition
                                    ; of foo

General Form: (memoize fn ; memoizes fn and returns fn :condition condition ; optional (default t) :condition-fn condition-fn ; optional :hints hints ; optional :otf-flg otf-flg ; optional :inline inline ; optional (default t) )
where 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; condition-fn is either nil (the default) or else evaluates to a legal function symbol. Further restrictions are discussed below.

Generally fn must evaluate to a defined function symbol whose guards 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 (list condition-fn inline)). 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.

Memoize works for functions that have stobj arguments or return stobj values. However, in some cases the memoized version of the function may execute much less inefficiently than the unmemoized version.

Memoize causes an error if fn uses state as an explicit parameter.