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

Posted 2023-02-22

【中文标题】太多的回溯：为啥这里有“重做”？

【英文标题】：Too much backtracking: why is there a "redo" here?太多的回溯：为什么这里有“重做”？

【发布时间】：2012-08-30 07:38:34

【问题描述】：

我在 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？我怎样才能避免它（当然，没有削减）？

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

【问题讨论】：

这只是您要询问的优化，给定的编译器可能有也可能没有。

好吧，一般来说，我认为优化一个人的代码是一个合法的编程问题，即使一个人只在一种编译器上编码（这里是 SWI）。但是，我刚刚更新了 SWI，我什至再也看不到这种行为了，所以它确实是 SWI 内部的，我想这个问题真的不感兴趣。抱歉吵了。

我在我的 SWI 安装上尝试了您的代码，但它确实没有尝试任何重做。它不仅是编译器，也是它的版本。我看到你更新了它；也许这是一个非常旧的版本。

是的，这绝对是版本问题（我不知道是哪一个，但从 5.10.4 开始已解决）。我会尽快发布答案并接受（由于我的声誉，我必须等待 8 小时），或者您可以这样做。

【参考方案1】：

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

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

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

【讨论】：

感谢您提供详细信息。我确认该问题在 5.10.4 版本中似乎已解决（但也可能在某些早期版本中）。

几年后再次查看 Prolog，我在 7.2.3 中再次看到这种行为......我不确定我是否爱上了这种语言的方式（以及预期的行为编译器和解释器）被指定。

【参考方案2】：

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

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

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

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

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

【讨论】：

不幸的是，这不是绿色剪辑。 greater_than(A,B) 工作方式不同。

这里没有“额外的选择点”：只有一种方法可以对有redo 的子句头部执行统一。这个程序不需要cut，显然只是SWI中的一个过渡性bug。

这不是错误。选择点从左到右，从上到下。 Prolog 编译器甚至不必在回溯之前查看适合的子句下的子句。如果现在 SWI 对其进行了优化，这并不意味着它之前是一个错误。