在 Prolog 中调试递归答案

【问题标题】：Debugging recursion in Prolog在 Prolog 中调试递归
【发布时间】：2018-10-25 20:03:48
【问题描述】：

这是我的知识库：

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

这是我的查询：

numeral(X).

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

[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)。这里的分支过程是什么？

有没有办法获得更多细节？

附：这取自以下link

【问题讨论】：

标签： debugging recursion prolog trace

【解决方案1】：

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

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

我在这里使用了Y，因为这也会造成混淆：子句中的变量是局部范围的，因为子句中的X 与@ 不是同一个变量987654330@在通话中。

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

同样有两种选择：

与numeral(0) 在这种情况下，它将Y 与0 统一起来；和
与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，因此Y = succ(0)，因此X = succ(succ(0))。

【讨论】：