斐波那契数列 - 全局堆栈错误

Fibonacci numbers - Out of global stack error

考虑这个简单的 Prolog 程序:

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

我已经测试了 plus,它似乎可以正常工作。让我们看看 fib 是否也能正常工作...

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

一切正常,直到我想打印出第三个数字,恰好是 2!

我知道以这种方式模拟 Peano 算法远非有效,而且这里使用的指数算法也不是最优的,尽管如此,我拒绝相信性能问题会这么早就出现,当我只计算第三个数字。所以我的程序肯定会循环,所以它是错误的。

...为什么会循环?怎样才能让它停止循环?

简答:循环是因为plus(0, s(0), X).会产生true,然后循环。

如果我们看一下 trace,我们会看到:

[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
   <b>Call: (10) plus(0, s(0), _912) ? creep</b>
   ...
   Exit: (9) plus(s(0), s(0), s(s(0))) ? creep
   Exit: (8) fib(s(s(s(0))), s(s(0))) ? creep
true .

但是解释器在该谓词中回溯并旨在找到更多解决方案。这是因为您的 nat(Z) 每次都得出下一个值,然后解释器调用 plus(X, Y, Z) 来检查是否匹配,但每次都失败。

我们可以看到当我们追踪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
   <b>Fail: (9) plus(0, 0, s(0)) ? creep</b>
   Redo: (10) nat(_888) ? creep

当然 none 的答案 nat(Z) 将建议一旦 plus(0, s(0), X) 成功。

然而,无论如何都没有理由调用 nat(Z),因为最终递归调用将落入将验证 nat(X) 的基本案例中,因此我们可以像这样实现它:

plus(X, 0, X) :- nat(X).
plus(X, s(Y), s(Z)) :- <b>plus(X, Y, Z)</b>.

第一个参数上使用不同的模式通常也更有效:

plus(<b>0</b>, X, X) :- nat(X).
plus(<b>s(X)</b>, Y, s(Z)) :- <b>plus(X, Y, Z)</b>.