Memoization for Functions

As of version 1.9.0-beta9 ProB allows you to annotate functions in the ABSTRACT_CONSTANTS section for memoization. Memoization is a technique for storing results of function applications and reusing the result if possible to avoid re-computing the function for the same arguments again.

To enable memoization you either need to

annotate the function in the ABSTRACT_CONSTANTS section with the pragma /*@desc memo */
set the preference MEMOIZE_FUNCTIONS to true. In this case ProB will try to memoize all functions in the ABSTRACT_CONSTANTS section, unless they are obviously small and finite and can thus be precomputed completely.

Take the following example:

 MACHINE MemoizationTests
 ABSTRACT_CONSTANTS
   fib /*@desc memo */,
   fact /*@desc memo */
 PROPERTIES
   fib = %x.(x:NATURAL |
            (IF x=0 or x=1 THEN 1
            ELSE fib(x-1)+fib(x-2)
            END))
   &
   fact = %x.(x:NATURAL|(IF x=0 THEN 1 ELSE x*fact(x-1) END))
 ASSERTIONS
   fib(30)=1346269;
   fib[28..30] = {514229,832040,1346269};
   30|->1346269 : fib;
   30|->1346268 /: fib;
   {x| 30|->x:fib} = {1346269};
 END

Memoization means that the recursive Fibonacci function now runs in linear time rather than in exponential time. Generally, memoization is useful for functions which are complex to compute but which are called repeatedly with the same arguments.

As can be seen above, memoization is active for

function calls such as fib(30) (which in turn calls fib(29) and fib(28) which are also memoized)
computation of relational image such as fib[28..30], which internally results in three function calls to fib
membership predicates of the form x|->y:fib, where x is a known value
non-membership predicates of the form x|->y/:fib, where x is a known value

The following points are relevant:

Memoization is currently only possible for functions declared in the ABSTRACT_CONSTANTS section
Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.
Memoized functions are often treated in a similar way to symbolic functions. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.
Memoization of a function f is currently not active for computations such as dom(f).
If a predicate requires the computation of the full function, e.g., ran(f), then the results will be stored and will be available for future function calls or in case the full value is needed again.

With the command-line version probcli you can use the -profile command to obtain some statistics about memoization. An example output is the following one:

--------------------------
ProB profile info after 9670 ms walltime (7217 ms runtime)
No source profiling information available
Recompile ProB with -Dprob_src_profile=true
No profiling information available
Recompile ProB with -Dprob_profile=true
MEMO Table:
Summary of reuse per memoization ID:
MemoID 1 (prime) : Values Stored: 999 (? ms to compute), Reused ?
MemoID 2 (fib) : Values Stored: 31 (? ms to compute), Reused ?
MemoID 3 (fact) : Values Stored: 11 (? ms to compute), Reused ?
MemoID 4 (evenupto) : Values Stored: 0 (? ms to compute), Reused ?
MemoID 5 (sum) : Values Stored: 1001 (? ms to compute), Reused ?
MemoID 6 (M91) : Values Stored: 111 (? ms to compute), Reused ?
Hashes computed: 1002, expansions reused: 0
Memoization functions registered: 6, results reused: 1345

If the compile time flag -Dprob_profile=true is set, the output is more detailed:

...
MEMO Table:
Summary of reuse per memoization ID:
MemoID 1 (prime) : Values Stored: 999 (336 ms to compute), Reused 1003
MemoID 2 (fib) : Values Stored: 31 (20 ms to compute), Reused 45
MemoID 3 (fact) : Values Stored: 11 (10 ms to compute), Reused 1
MemoID 4 (evenupto) : Values Stored: 0 (0 ms to compute), Reused 0
MemoID 5 (sum) : Values Stored: 1001 (16659 ms to compute), Reused 1
MemoID 6 (M91) : Values Stored: 111 (15 ms to compute), Reused 295
Hashes computed: 1002, expansions reused: 0
Memoization functions registered: 6, results reused: 1345

In verbose mode (-v flag for probcli) you also obtain information about individual stored results.

MEMO Table:
MemoID 1 stored FUNCTION prime 
     :  %x.(x : NATURAL|(IF !y.(y : 2 .. x - 1 => x mod y /= 0) THEN TRUE ELSE FALSE END))
MemoID 2 stored FUNCTION fib 
     :  %x.(x : NATURAL|(IF x : {0,1} THEN 1 ELSE MEMOIZE_STORED_FUNCTION(2)(x - 1) + MEMOIZE_STORED_FUNCTION(2)(x - 2) END))
...
MemoID 6 stored FUNCTION M91 
     :  %x.(x : INTEGER|(IF x > 100 THEN x - 10 ELSE MEMOIZE_STORED_FUNCTION(6)(MEMOIZE_STORED_FUNCTION(6)(x + 11)) END))
MemoID 1 (prime) result for argument 13
     :  TRUE
MemoID 1 (prime) result for argument 14
     :  FALSE
MemoID 1 (prime) result for argument 2
     :  TRUE
MemoID 1 (prime) result for argument 3
     :  TRUE
...
Memoization functions registered: 6, results reused: 1345