:- module(_,_).

% Dynamic program modification example: using lemmas
% --------------------------------------------------

% The Fibonacci sequence: 0, 1, and then:
% element n is element n-1 + element n-2
% i.e., 0 1 1 2 3 5 8 13 21 ...

% First version, applying directly the definition: 

fib(0, 0). 
fib(1, 1). 
fib(N, F) :-  
    N > 1,        
    N1 is N - 1, 
    N2 is N - 2, 
    fib(N1, F1), 
    fib(N2, F2),  
    F is F1 + F2. 

% Same, in functional notation: 
:- use_package(fsyntax).
:- fun_eval arith(true).

ffib(0) := 0.
ffib(1) := 1.
ffib(N) := ~ffib(N-1) + ~ffib(N-2) :- N>1.

% A version that records 'lemmas' (things already proved)

% We define a table (with a dynamic predicate) that holds the
% first two elements, i.e., for N=0 and N=1: 
:- dynamic lemma_fib/2.
lemma_fib(0, 0). 
lemma_fib(1, 1). 

% To compute the rest: 
lfib(N, F) :-
    % First check if we the Nth element in the table, 
    % and we take it from there. 
    lemma_fib(N, F),
    !. 
lfib(N, F) :- 
    % Else, we compute the Nth number...
    N > 1,   
    N1 is N - 1,  
    N2 is N - 2, 
    lfib(N1, F1), 
    lfib(N2, F2), 
    F is F1 + F2,     
    % ...and once we have it we record it: 
    assert(lemma_fib(N, F)). 

% Try (comare the computation time!): 
% ?- fib(30,Y).
% ?- fib(31,Y).
% ?- fib(32,Y).
% ?- fib(35,Y).
%  ...
% ?- lfib(30,Y).
% ?- lfib(35,Y).
% ?- lfib(200,Y).
% ?- lfib(1000,Y).
%  ...