太多的回溯：为什么这里有“重做”？

Question

我在 Prolog 中做一个非常简单的练习，在跟踪中有一些我不明白的东西。该程序是对表示为后继的整数的“大于”（>）：

greater_than(succ(_), 0).
greater_than(succ(A), succ(B)) :-
  greater_than(A, B).

我的问题：我不明白为什么请求 greater_than(succ(succ(succ(0))),succ(0)) 在以下跟踪中生成 redo：

[trace] ?- greater_than(succ(succ(succ(0))),succ(0)).
Call: (6) greater_than(succ(succ(succ(0))), succ(0)) ? creep
Call: (7) greater_than(succ(succ(0)), 0) ? creep
Exit: (7) greater_than(succ(succ(0)), 0) ? creep
Exit: (6) greater_than(succ(succ(succ(0))), succ(0)) ? creep
true ;
Redo: (7) greater_than(succ(succ(0)), 0) ? creep
Fail: (7) greater_than(succ(succ(0)), 0) ? creep
Fail: (6) greater_than(succ(succ(succ(0))), succ(0)) ? creep
false. 

为什么这里有redo？我怎样才能避免它（当然，没有削减）？

顺便说一句，在你问之前：不，这不是某种家庭作业......

Answer 1

好的，所以这是给定编译器/版本组合可能有也可能没有的编译器优化。

更高版本的 SWI 没有这个问题。它可能与子句索引有关。这种行为会出现在没有索引的实现上，或者只有第一个参数上的索引。

但显然，"SWI-Prolog provides `just-in-time' indexing over multiple arguments"。 SWI 5.6.56 手册states“最多可以索引 4 个参数”。所以它可能索引不止一个。

Answer 2

有一个重做的原因是prolog不能推断（不检查它），如果按照下一个子句，会有一个替代解决方案。诚然，在这种情况下，它只是一个头部统一检查（并不是说这总是微不足道的），但它可能需要很长时间（甚至永远不会终止）。

现在，这正是您应该使用 cut 的地方：您知道额外的选择点不会产生解决方案（因此您不会更改语义 - 绿色 cut）。或者（但它主要是覆盖剪切的语法糖）您可以使用 if-then-else：

greater_than(succ(A), B):-
    B = succ(BI) ->
    greater_than(A,BI)
    ; B = 0.

并不是说这仍然会进行额外的计算，而 cut 可以避免这些计算。

PS：我怀疑有人会认为这是家庭作业 XD