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
                                    ;   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



General Form:
(memoize fn                         ; memoizes fn and returns fn
         :condition    condition    ; optional (default t)
         :condition-fn condition-fn ; optional
         :hints        hints        ; optional, for verifying the
                                    ;   guards of condition-fn
         :otf-flg      otf-flg      ; optional, for verifying the
                                    ;   guards of condition-fn
         :inline       inline       ; optional (default t)
         :commutative  t/lemma-name ; optional (default nil)
         :forget       t/nil        ; optional (default nil)
         :memo-table-init-size size ; optional (default *mht-default-size*)
         :verbose      t/nil        ; 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; 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 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 ((: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.