How to implement the Fibonacci sequence in successor arithmetics for all argument modes?

Question

The following Prolog program defines a predicate fib/2 for computing the Fibonacci number of an integer in successor arithmetics:

fib(0, 0).
fib(s(0), s(0)).
fib(s(s(N)), F) :-
  fib(N, F1),
  fib(s(N), F2),
  sum(F1, F2, F).

sum(0, N, N).
sum(s(N1), N2, s(S)) :-
  sum(N1, N2, S).

It works with queries in this argument mode:

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

It also works with queries in this argument mode:

?- fib(s(0), F).
   F = s(0)
;  false.

It also works with queries in this argument mode:

?- fib(N, F).
   N = F, F = 0
;  N = F, F = s(0)
;  N = s(s(0)), F = s(0)
;  N = s(s(s(0))), F = s(s(0))
;  N = s(s(s(s(0)))), F = s(s(s(0)))
;  …

But it exhausts resources with queries in this argument mode:

?- fib(N, s(0)).
   N = s(0)
;  N = s(s(0))
;
Time limit exceeded

How to implement the Fibonacci sequence in successor arithmetics for all argument modes?

Answer 1

The naive recursive implementation of fib/2 provided in my other answer has a time complexity of O(φ^N) where φ is the golden ratio i.e. exponential time. Here is a tail recursive implementation of fib/2 which has a time complexity of O(N) i.e. linear time:

fib(N, F) :-
  fib(N, 0, s(0), F, F).

fib(0, A, _, A, _).
fib(s(0), _, B, B, _).
fib(s(s(N)), A, B, s(F), s(X)) :-
  sum(A, B, S),
  fib(s(N), B, S, s(F), X).

sum(0, N, N).
sum(s(N1), N2, s(S)) :-
  sum(N1, N2, S).

Sample queries

The most general query (all arguments are free):

?- fib(N, F).
   F = N, N = 0
;  F = N, N = s(0)
;  F = s(0), N = s(s(0))
;  F = s(s(0)), N = s(s(s(0)))
;  F = s(s(s(0))), N = s(s(s(s(0))))
;  F = N, N = s(s(s(s(s(0)))))
;  F = s(s(s(s(s(s(s(s(0)))))))), N = s(s(s(s(s(s(0))))))
;  F = s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), N = s(s(s(s(s(s(s(0)))))))
;  …

Queries with a first argument that is free:

?- fib(N, 0).
   N = 0
;  false.

?- fib(N, s(0)).
   N = s(0)
;  N = s(s(0))
;  false.

?- fib(N, s(s(0)).
   N = s(s(s(0)))
;  false.

?- fib(N, s(s(s(0))).
   N = s(s(s(s(0))))
;  false.

?- fib(N, s(s(s(s(s(0)))))).
   N = s(s(s(s(s(0)))))
;  false.

?- fib(N, s(s(s(s(s(s(s(s(0))))))))).
   N = s(s(s(s(s(s(0))))))
;  false.

Queries with a second argument that is free:

?- fib(0, F).
   F = 0
;  false.

?- fib(s(0), F).
   F = s(0)
;  false.

?- fib(s(s(0)), F).
   F = s(0)
;  false.

?- fib(s(s(s(0))), F).
   F = s(s(0))
;  false.

?- fib(s(s(s(s(0)))), F).
   F = s(s(s(0)))
;  false.

?- fib(s(s(s(s(s(0))))), F).
   F = s(s(s(s(s(0)))))
;  false.

Answer 2

The failure slice causing universal non-termination when the first argument of fib/2 is unbound is

fib(s(s(N)), F) :-
  fib(N, F1),
  false,
  fib(s(N), F2),
  sum(F1, F2, F).

The reason is that only the first argument is restricted in the recursive call fib(N, F1), so if it is unbound the restriction does not apply.

cTI proves that

fib(A,B)terminates_if b(A).

To allow universal termination when the first argument is unbound, one should restrict the second argument in the recursive call and therefore the second argument should be bound for the restriction to apply:

fib(N, F) :-
  fib(N, F, F).

fib(0, 0, _).
fib(s(0), s(0), _).
fib(s(s(N)), F, s(X)) :-
  fib(N, F1, X),
  fib(s(N), F2, X),
  sum(F1, F2, F).

sum(0, N, N).
sum(s(N1), N2, s(S)) :-
  sum(N1, N2, S).

cTI proves that

fib(A,B)terminates_if b(A);b(B).

So now the query terminates:

?- fib(N, s(0)).
   N = s(0)
;  N = s(s(0))
;  false.

Answer 3

This answer computes the fibonacci number "bottom up" using the two previous computed values, so that it will only make one recursive tail call:

fib(0, 0).
fib(s(0), s(0)).
fib(s(s(X)), F):-
  fib(X, 0, s(0), F, F).
  
fib(0, F_2, F_1, _, F):-
  sum(F_2, F_1, F).
fib(s(X), F_2, F_1, s(Y), F):-
  sum(F_2, F_1, F_0),
  fib(X, F_1, F_0, Y, F).

sum(0, Y, Y).
sum(s(X), Y, s(Z)):- 
  sum(X, Y, Z).

At least in SWI with default configuration it exhausts resources computing the fibonacci(37) building the addition term in sum/3.