%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% The following Xcerpt program computes      %%
%% all (:-)) Fibonacci numbers                %%
%% ------------------------------------------ %%
%% Since there are infinitly many Fibonacci numbers
%% the following goal can not terminate if evaluated 
%% against all integers (as parameters for the 
%% fib rule). We are currently working on an iterative
%% evaluation for Xcerpt programs (like in Prolog) which 
%% should report infinite, but enumerable results 
%% on-the-fly instead of trying to compute all answers
%% and then reporting them. In the case of the current
%% prototype we choose to limit the integers that form 
%% the base for the computation and thus ensure termination.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
GOAL
 result[ all var RESULT ]
FROM
 var RESULT -> fib[[]]
END

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Rekursive Definition of Fibonacci-Numbers  %%
%%                                            %%
%% For this collection of rules to terminate, we have to
%% provide a proper grounding. This grounding is provided
%% by the successor over integers, cf. Peano axioms.
%% Clearly this is not a very "practical" formulation. 
%% A specialized, generative addition predicate would be 
%% needed for a better formulation. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%% Base case 1: fib(0) = 0
CONSTRUCT
 fib[ "null" , "null" ]
END

%%%% Base case 2: fib(1) = 1
CONSTRUCT
 fib[ "eins" , "eins" ]
END

%%%% Recursive case: fib(x) = fib(x-1)+fib(x-2)
CONSTRUCT
 fib[ var X , var Y ]
FROM
 and[
  succ[var X, var X_1],
  succ[var X_1, var X_2] ,
  fib[ var X_1 , var Y_1 ],
  fib[ var X_2 , var Y_2 ],
  addition[ var Y_1 , var Y_2 , var Y ]
 ]
END


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Recursive Generative Addition      %%
%% Again, Xcerpt currently lacks a built-in
%% generative addition, thus we have to provide 
%% it based on the successor function of integers.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Base case: x+0=x
CONSTRUCT
 addition[ var X , "zero" , var X]
END

%%%% Recursive case: x+y'=z' & succ(y', y) & succ(z', z) & x+y=z
CONSTRUCT
 addition[ var X , var YP , var ZP]
FROM
 and[
  succ[ var YP , var Y ] ,
  succ[ var ZP , var Z ] ,
  addition[ var X , var Y , var Z ]
 ]
END

%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Integers and successor function over Integers
%% succ should, of course, be recursive, but as described above
%% on infinitely many integers there are inifinitely many Fibonacci 
%% numbers and thus the program does not terminate and reports nothing
%% (given the current prototype). Therefore, we limit ourselves to 0-5.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
CONSTRUCT "zero"                   END

CONSTRUCT succ["one" , "zero" ]    END

CONSTRUCT succ["two" , "one" ]     END

CONSTRUCT succ["three" , "two" ]   END

CONSTRUCT succ["four" , "three" ]  END

CONSTRUCT succ["five" , "four" ]   END