如何在所有参数模式的后继算术中实现斐波那契数列?

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

以下 Prolog 程序定义了一个谓词 fib/2,用于计算后继算术中整数的斐波那契数:

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).

它适用于此参数模式下的查询:

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

它也适用于此参数模式下的查询:

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

它也适用于此参数模式下的查询:

?- 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)))
;  …

但是在这种参数模式下查询会耗尽资源:

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

如何在所有参数模式的后继算术中实现斐波那契数列?

fib/2的第一个参数未绑定时导致通用非终止的失败切片是

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

原因是只有第一个参数在递归调用中受到限制fib(N, F1),所以如果它是未绑定的,则限制不适用。

cTI proves

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

要在第一个参数未绑定时允许通用终止,应限制递归调用中的第二个参数,因此应绑定第二个参数以应用限制:

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那个

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

现在查询终止:

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

此答案使用前两个计算值“自下而上”计算斐波那契数,因此它只会进行一次递归尾调用:

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).

至少在具有默认配置的 SWI 中,它耗尽了计算 fibonacci(37) 在 sum/3 中构建加法项的资源。

has a time complexity of O(φ^N) where φ is the golden ratio 中提供的 fib/2 的简单递归实现,即指数时间。这是 fib/2 的尾递归实现,其时间复杂度为 O(N) 即线性时间:

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).

示例查询

最一般的查询(所有参数都是免费的):

?- 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)))))))
;  …

第一个参数为空的查询:

?- 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.

第二个参数是免费的查询:

?- 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.