`Memoize` a partial version of a limited (`clocked') function

See memoize for relevant background. Here we describe a
utility that supports effective memoization for functions that have been
introduced by `defun`, as follows, under certain restrictions.

(defun fn-limit (x1 ... xn limit) (declare ...) ; optional, as usual for defun ; ; (if (zp limit) <base> (let ((limit (1- limit))) <body>)))

Here

Such use of a ``limit'' argument to obtain termination is an old trick that pre-dates ACL2. Such ``limited'' functions have traditionally often been called ``clocked'' functions. In this documentation we refer to such a function as a ``total'' function, because the limit argument guarantees that its evaluation terminates. We will be generating a corresponding ``partial'' function that avoids the limit argument, and hence might not terminate — but when it does, it computes the desired value, and uses memoization to do so, which can speed up computation.

We organize the rest of this topic as follows: General Form, Basic Example, Example with Mutual Recursion, Detailed Documentation, and Optional Technical Remarks.

(memoize-partial fn+ ; see below :kwd1 val1 ... :kwdn valn)

where the supplied `memoize`. In the simplest case, `mutual-recursion` and the general case for

The following example from community-book file
`memoize-partial`. Consider the Collatz
Conjecture, sometimes known as the 3n+1 problem. For any positive integer

(defun collatz-limit (n limit) (declare (xargs :guard (and (natp n) (natp limit)) :measure (acl2-count limit))) (if (zp limit) (prog2$ (er hard? 'collatz-limit "Limit exceeded!") 0) (let ((limit (1- limit))) (if (int= n 1) 0 (1+ (collatz-limit (if (evenp n) (floor n 2) (1+ (* 3 n))) limit))))))

A moment's reflection suggests that if this algorithm terminates, then
there are no cycles, so memoization from a single call will be useless.
However, memoization can be useful if we make distinct calls. But memoization
might not be very useful even then, because after we save the result of a call

(memoize-partial collatz)

Under the hood this generates, essentially, the following Common Lisp definition, which is to be memoized.

(defun collatz (n) (if (int= n 1) 0 (1+ (collatz (if (evenp n) (floor n 2) (1+ (* 3 n)))))))

Since the

(DEFCHOOSE COLLATZ-LIMIT-CHANGE (LARGE) (N LIMIT) (AND (NATP LARGE) (<= LIMIT LARGE) (NOT (EQUAL (COLLATZ-LIMIT N LIMIT) (COLLATZ-LIMIT N LARGE))))) (DEFCHOOSE COLLATZ-LIMIT-STABLE (LIMIT) (N) (AND (NATP LIMIT) (EQUAL (COLLATZ-LIMIT N LIMIT) (COLLATZ-LIMIT N (COLLATZ-LIMIT-CHANGE N LIMIT))))) (DEFUN COLLATZ (N) (DECLARE (XARGS :GUARD (LET ((LIMIT 0)) (DECLARE (IGNORABLE LIMIT)) (AND (NATP N) (NATP LIMIT))))) (COLLATZ-LIMIT N (NFIX (COLLATZ-LIMIT-STABLE N))))

The upshot is a logical definition of

We note that the call `table` event as well as the form `memoize` other
than indirectly using

See community-book file

The following example, also from community-book file
`mutual-recursion`. (The suffix ``

(mutual-recursion (defun evenlp-bdd (x bound) (declare (xargs :guard (natp bound))) (if (zp bound) 'ouch (let ((bound (1- bound))) (if (consp x) (oddlp-bdd (cdr x) bound) t)))) (defun oddlp-bdd (x bound) (declare (xargs :guard (natp bound))) (if (zp bound) 'ouch (let ((bound (1- bound))) (if (consp x) (evenlp-bdd (cdr x) bound) nil))))) (memoize-partial ((evenlp evenlp-bdd) (oddlp oddlp-bdd)))

Notice that this time the argument of

Recall that in the first example, the `defchoose`, and then function `defun`. In the
present example such a trio of functions is introduced for each of the
functions defined in the corresponding

(DEFCHOOSE EVENLP-BDD-CHANGE (LARGE) (X BOUND) (AND (NATP LARGE) (<= BOUND LARGE) (NOT (EQUAL (EVENLP-BDD X BOUND) (EVENLP-BDD X LARGE))))) (DEFCHOOSE EVENLP-BDD-STABLE (BOUND) (X) (AND (NATP BOUND) (EQUAL (EVENLP-BDD X BOUND) (EVENLP-BDD X (EVENLP-BDD-CHANGE X BOUND))))) (DEFUN EVENLP (X) (DECLARE (XARGS :GUARD (LET ((BOUND 0)) (DECLARE (IGNORABLE BOUND)) (NATP BOUND)))) (EVENLP-BDD X (NFIX (EVENLP-BDD-STABLE X)))) (DEFCHOOSE ODDLP-BDD-CHANGE (LARGE) (X BOUND) (AND (NATP LARGE) (<= BOUND LARGE) (NOT (EQUAL (ODDLP-BDD X BOUND) (ODDLP-BDD X LARGE))))) (DEFCHOOSE ODDLP-BDD-STABLE (BOUND) (X) (AND (NATP BOUND) (EQUAL (ODDLP-BDD X BOUND) (ODDLP-BDD X (ODDLP-BDD-CHANGE X BOUND))))) (DEFUN ODDLP (X) (DECLARE (XARGS :GUARD (LET ((BOUND 0)) (DECLARE (IGNORABLE BOUND)) (NATP BOUND)))) (ODDLP-BDD X (NFIX (ODDLP-BDD-STABLE X))))

The corresponding Common Lisp functions, to be executed for guard-verified calls of

(DEFUN EVENLP (X) (IF (CONSP X) (ODDLP (CDR X)) T)) (DEFUN ODDLP (X) (DECLARE (IGNORABLE X)) (IF (CONSP X) (EVENLP (CDR X)) NIL))

Recall the General Form

(memoize-partial fn+ ; see below :kwd1 val1 ... :kwdn valn)

where the supplied `memoize`. We discuss later below how
`cond` in place of `if`,
where here

(if (zp limit) <base> (let ((limit (1- limit))) <body>))

Moreover, each limit variable occurring in

Let us refer to each specified function as the ``total'' function. A
successful invocation admits a sequence of three definitions for each total
function, which we call the ``changed'', ``stable'', and ``partial'' function.
Here are those three definitions, where ``

(DEFCHOOSE <changed> (LARGE) (... LIMIT) (AND (NATP LARGE) (<= LIMIT LARGE) (NOT (EQUAL (<total> ... LIMIT) (<total> ... LARGE))))) (DEFCHOOSE <stable> (LIMIT) (...) (AND (NATP LIMIT) (EQUAL (<total> ... LIMIT) (<total> ... (<change> ... LIMIT))))) (DEFUN <partial> (...) (DECLARE (XARGS :GUARD (LET ((LIMIT 0)) (DECLARE (IGNORABLE LIMIT)) <guard_of_total>))) (<total> ... (NFIX (<stable> ...))))

Under the hood, however, a Common Lisp definition is installed for

(defun <partial> (...) <body'>

We turn now to the first argument of

(<partial> <total> :change <change> :stable <stable> :kwd1 val1 ... :kwdn valn)

The symbols `memoize`. There should be a single tuple in the singly
recursive case. In the case that the partial functions were defined by a
`car`s) must also be

The keyword/value pairs of the tuple are optional. The default for

There are some abbreviations allowed for

- A symbol
fn forfn+ abbreviates the list(fn) , which is an abbreviation as noted below. - If
fn+ is a list(t1 ... tk) , then eachti that is a symbol, sayfn , abbreviates the tuple(fn fn-limit) , wherefn-limit is obtained by adding the suffix"-LIMIT" tofn , to create a symbol in the same package as that offn .

Consider our first example,

(collatz collatz-limit :change collatz-limit-change :stable collatz-limit-stable)

Note that the keyword value `profile` the
recursive calls are also affected by the

We conclude this section by discussing restrictions pertaining to stobjs. Recall that memoization is illegal (other than profiling) for
functions that return a stobj or have the ACL2 state as an input.
Those same restrictions apply to `non-exec` wrapped around
the body.

Warning: These are technical remarks that are completely optional.

Our general remark is to invite readers who want to dive below the user
level, including implementation and foundational issues, to read the comment
entitled ``Essay on Memoization with Partial Functions
(Memoize-partial)'' in ACL2 source file

Our more specific remark concerns generated Common Lisp definitions.
Recall that in the Basic Example above, we say that the Common Lisp definition
of

(defun collatz (n) (if (int= n 1) 0 (1+ (collatz (if (evenp n) (floor n 2) (1+ (* 3 n)))))))

We say ``essentially'' because the actual Common Lisp definition of

(DEFUN COLLATZ (N) (DECLARE (IGNORABLE N)) (FLET ((COLLATZ-LIMIT (N LIMIT) (DECLARE (IGNORE LIMIT)) (COLLATZ N))) (DECLARE (INLINE COLLATZ-LIMIT)) (LET ((LIMIT 0)) (DECLARE (IGNORABLE LIMIT)) (IF (INT= N 1) 0 (1+ (COLLATZ-LIMIT (IF (EVENP N) (FLOOR N 2) (1+ (* 3 N))) LIMIT))))))

A little reflection will conclude that these two definitions are equivalent. The latter, however, avoids a macroexpansion issue discussed in the aforementioned Essay.