在 Prolog 中调试递归

Question

这是我的知识库：

numeral(0). 
numeral(succ(X))  :-  numeral(X).

这是我的查询：

numeral(X).

这是 SWI Prolog returns 在跟踪模式下的内容：

[trace]  ?- numeral(X).
   Call: (8) numeral(_3806) ? creep
   Exit: (8) numeral(0) ? creep
X = 0 ;
   Redo: (8) numeral(_3806) ? creep
   Call: (9) numeral(_4006) ? creep
   Exit: (9) numeral(0) ? creep
   Exit: (8) numeral(succ(0)) ? creep
X = succ(0) ;
   Redo: (9) numeral(_4006) ? creep
   Call: (10) numeral(_4010) ? creep
   Exit: (10) numeral(0) ? creep
   Exit: (9) numeral(succ(0)) ? creep
   Exit: (8) numeral(succ(succ(0))) ? creep
X = succ(succ(0))

我明白它是如何找到 X=0 答案的，我不完全明白它是如何获得的：X = succ(succ(0))。我知道这是正确的答案，但我不确定 Prologs 是如何搜索它的。

这是我的想法：当它打印 Call: (9) numeral(_4006) ? creep 时，它会尝试这个规则：numeral(succ(X)) :- numeral(X). 特别是它可能会替代 _4006 = succ(X) 然后它检查它是否仅在 numeral(X) 成立时成立，Prolog 根据 numeral(0) 进行检查，因此结果为 _4006 = succ(0)。

现在，如果我们要求另一个解决方案，它会再次返回 numeral(_4006)，但它猜测什么时候调用 numeral(_4010)。这里的分支过程是什么？

有没有办法了解更多详情？

P.S。这是摘自以下link

Answer 1

Prolog 通过回溯搜索。 Prolog 可以通过两种方式来满足 numeral(X) 调用：

with numeral(0) 在这种情况下它统一了 X 和 0；和
with numeral(succ(Y)) :- numeral(Y) 在这种情况下它将 X 与 succ(Y) 统一起来并进行递归调用。

我在这里使用了 Y 因为这也造成了混淆：子句中的变量是 局部作用域 在某种意义上说 X 在子句中, 与调用中的 X 不同。

现在如果 Prolog 回溯并旨在用子句满足谓词，那么这意味着 X = succ(Y) 和 Y 一个变量，但它需要用 [=22 进行额外的调用=] 正文中指定。

同样有两个选择：

with numeral(0) 在这种情况下它统一了 Y 和 0；和
with numeral(succ(Z)) :- numeral(Z) 在这种情况下，它将 Y 与 succ(Z) 统一起来并进行递归调用。

如果我们选择第一个，Y 设置为 0，因此 X = succ(Y) 因此 X = succ(0)。在后一种情况 X = succ(Y) 和 Y = succ(Z) 中，我们再次进行递归调用。

现在，如果我们再次使用 numeral(0) 的第一行，这意味着 Z 与 0 统一，因此 Z = 0，因此 [=39] =]，因此 X = succ(succ(0)).

在 Prolog 中调试递归

Debugging recursion in Prolog

debugging

recursion

trace

prolog