• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
        • Defun
        • Verify-guards
        • Table
        • Mutual-recursion
        • Memoize
          • Memoize-partial
          • Protect-memoize-statistics
          • Profile-all
          • Profile-ACL2
          • Memoized-prover-fns
          • Unmemoize
          • Verify-guard-implication
          • Memsum
          • Set-bad-lisp-consp-memoize
          • Memoize-summary
          • Save-and-clear-memoization-settings
          • Never-memoize
          • Clear-memoize-tables
          • Clear-memoize-statistics
          • Clear-memoize-table
          • Restore-memoization-settings
        • Make-event
        • Include-book
        • Encapsulate
        • Defun-sk
        • Defttag
        • Defstobj
        • Defpkg
        • Defattach
        • Defabsstobj
        • Defchoose
        • Progn
        • Verify-termination
        • Redundant-events
        • Defmacro
        • Defconst
        • Skip-proofs
        • In-theory
        • Embedded-event-form
        • Value-triple
        • Comp
        • Local
        • Defthm
        • Progn!
        • Defevaluator
        • Theory-invariant
        • Assert-event
        • Defun-inline
        • Project-dir-alist
        • Partial-encapsulate
        • Define-trusted-clause-processor
        • Defproxy
        • Defexec
        • Defun-nx
        • Defthmg
        • Defpun
        • Defabbrev
        • Set-table-guard
        • Name
        • Defrec
        • Add-custom-keyword-hint
        • Regenerate-tau-database
        • Defcong
        • Deftheory
        • Defaxiom
        • Deftheory-static
        • Defund
        • Evisc-table
        • Verify-guards+
        • Logical-name
        • Profile
        • Defequiv
        • Defmacro-untouchable
        • Add-global-stobj
        • Defthmr
        • Defstub
        • Defrefinement
        • Deflabel
        • In-arithmetic-theory
        • Unmemoize
        • Defabsstobj-missing-events
        • Defthmd
        • Fake-event
        • Set-body
        • Defun-notinline
        • Functions-after
        • Macros-after
        • Dump-events
        • Defund-nx
        • Defun$
        • Remove-global-stobj
        • Remove-custom-keyword-hint
        • Dft
        • Defthy
        • Defund-notinline
        • Defnd
        • Defn
        • Defund-inline
        • Defmacro-last
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Programming
  • Hons-and-memoization
  • Events

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