No edit summary |
No edit summary |
||
Line 79: | Line 79: | ||
MemoID 6 (M91) : Values Stored: 111 (15 ms to compute), Reused 295 | MemoID 6 (M91) : Values Stored: 111 (15 ms to compute), Reused 295 | ||
Hashes computed: 1002, expansions reused: 0 | Hashes computed: 1002, expansions reused: 0 | ||
Memoization functions registered: 6, results reused: 1345 | |||
</pre> | |||
In verbose mode (<tt>-v</tt> flag for probcli) you also obtain information about individual stored results. | |||
<pre> | |||
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 | Memoization functions registered: 6, results reused: 1345 | ||
</pre> | </pre> |
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
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
The following points are relevant:
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