Fibonacci numbers - Out of global stack error

Question

Consider this simple Prolog program:

nat(0).
nat(s(X)) :- nat(X).
plus(X, 0, X) :- nat(X).
plus(X, s(Y), s(Z)) :- nat(X), nat(Y), nat(Z), plus(X, Y, Z).
fib(0, 0).
fib(s(0), s(0)).
fib(s(s(K)), Z) :- fib(s(K), Y), fib(K, X), plus(X, Y, Z).

I already tested plus and it seems to be working. Let's see if fib works okay as well...

?- fib(0, 0).
true.

?- fib(s(0), s(0)).
true ;
false.

?- fib(s(s(0)), s(0)).
true ;
false.

?- fib(s(s(s(0))), s(s(0))).
true ;
ERROR: Out of global stack

Everything works splendidly until I want to print out the 3rd number, which happens to be 2!

I understand that simulating the Peano arithmetic this way is far from effective, and also that an exponential algorithm that is being used here is suboptimal, nonetheless I refuse to believe that performance issues kick in that early, when I'm only computing the third number. Therefore my program surely loops and therefore it is wrong.

... why does it loop? and what does it take to make it stop looping?

Answer 1

Short answer: It loops because plus(0, s(0), X). will produce true, and then loop.

If we take a look at the trace, we see:

[trace]  ?- fib(s(s(s(0))), s(s(0))).
   Call: (8) fib(s(s(s(0))), s(s(0))) ? creep
   Call: (9) fib(s(s(0)), _902) ? creep
   Call: (10) fib(s(0), _906) ? creep
   Exit: (10) fib(s(0), s(0)) ? creep
   Call: (10) fib(0, _910) ? creep
   Exit: (10) fib(0, 0) ? creep
   Call: (10) plus(0, s(0), _912) ? creep
   ...
   Exit: (9) plus(s(0), s(0), s(s(0))) ? creep
   Exit: (8) fib(s(s(s(0))), s(s(0))) ? creep
true .

But the interpreter backtracks in that predicate and aims to find more solutions. This is due to the fact that your nat(Z) each time comes up with a next value, and then the interpreter calls plus(X, Y, Z) to check if that matches, but each time it fails.

We can see that when we trace plus(0, s(0), X):

[trace]  ?- plus(0, s(0), X).
   Call: (8) plus(0, s(0), _676) ? creep
   Call: (9) nat(0) ? creep
   Exit: (9) nat(0) ? creep
   Call: (9) nat(0) ? creep
   Exit: (9) nat(0) ? creep
   Call: (9) nat(_884) ? creep
   Exit: (9) nat(0) ? creep
   Call: (9) plus(0, 0, 0) ? creep
   Call: (10) nat(0) ? creep
   Exit: (10) nat(0) ? creep
   Exit: (9) plus(0, 0, 0) ? creep
   Exit: (8) plus(0, s(0), s(0)) ? creep
X = s(0) ;
   Redo: (9) plus(0, 0, 0) ? creep
   Fail: (9) plus(0, 0, 0) ? creep
   Redo: (9) nat(_884) ? creep
   Call: (10) nat(_888) ? creep
   Exit: (10) nat(0) ? creep
   Exit: (9) nat(s(0)) ? creep
   Call: (9) plus(0, 0, s(0)) ? creep
   Fail: (9) plus(0, 0, s(0)) ? creep
   Redo: (10) nat(_888) ? creep

Of course none of the answers nat(Z) will propose will succeed once plus(0, s(0), X) has succeeded.

There is however no reason to call nat(Z) anyway, since eventually the recursive call will land in the basecase that will validate nat(X), so we can implement it like:

plus(X, 0, X) :- nat(X).
plus(X, s(Y), s(Z)) :- plus(X, Y, Z).

It is also typically more efficient to use different patterns on the first parameter:

plus(0, X, X) :- nat(X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).