No edit summary |
No edit summary |
||
Line 23: | Line 23: | ||
fib(30)=1346269; | fib(30)=1346269; | ||
fib[28..30] = {514229,832040,1346269}; | fib[28..30] = {514229,832040,1346269}; | ||
30|->1346269 : fib; | |||
30|->1346268 /: fib; | |||
{x| 30|->x:fib} = {1346269}; | |||
END | END | ||
Line 32: | Line 35: | ||
* computation of relational image such as fib[28..30], which internally results in three function calls to fib | * 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 | * 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: | The following points are relevant: |
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.