为什么 swipl 的响应不一致？

Question

我想了解为什么与swipl 的交互似乎不一致。

这是一个典型的例子。假设我查阅了包含以下定义的知识库：

acc_max([H|T], A, Max) :- H  > A, acc_max(T, H, Max).
acc_max([H|T], A, Max) :- H =< A, acc_max(T, A, Max).
acc_max([], A, A).

max([H|T], Max) :- acc_max(T, H, Max).

下面是我在提示符下键入max([0, 1, 2], X). 并按Enter 后屏幕的样子：

?- max([0, 1, 2], X).
X = 2 ▮

（▮表示光标的位置。）

特别注意，解释器的下一个提示还没有出现。

这是我输入 ; 后屏幕的样子：

?- max([0, 1, 2], X).
X = 2 ;
false.

?- ▮

现在我终于得到了解释器的提示。

相比之下，下面显示了我在提示符下键入max([2, 0, 1], X). 并按Enter 后屏幕的样子：

?- max([2, 0, 1], X).
X = 2.

?- ▮

请注意，这一次我立即得到了解释器的提示 - 我不需要键入 ;。另外，没有false。

我发现了许多其他类似的不一致（例如，有时输出 true. 会显示在屏幕上，但在其他类似情况下却不会）。

作为 Prolog 的新手，我发现这种不一致令人不安（更不用说令人沮丧了，因为它们不断提醒我，我真的不知道发生了什么 )。

有没有一种简单的方法来合理化这些不一致？

或者，是否有一些 Prolog 实现比 SWI-Prolog 提供更一致和可预测的交互？

Answer 1

因此，正如@lurker 所说，这是选择点的结果 - 存在尚未评估的规则的情况，这可能会产生更多解决方案。

让我们看一个更简单的例子，max([0,1],X). 与 max([1,0],X).。

max([0,1],X).:

这转到acc_max([1],0,X).，它与acc_max([H|T], A, Max) :- 规则匹配。我们按照它们出现的顺序评估它们：

首先我们看到1 > 0 为真，然后调用acc_max([],1,X)。这仅匹配acc_max([], A, A).，因此我们将 X 与 1 统一。我们有一个解决方案！但我们也有一个尚未评估的规则。这是你看到的地方：

X = 1 ▮

所以现在我们输入 ;，然后评估第二个 acc_max([H|T], A, Max) :- 规则。我们看到1 =< 0 不正确，所以这条规则失败了。我们现在没有规则可以尝试，所以事实证明没有更多的解决方案。因此：

X = 1 ;
false.

现在我们来看看max([1,0],X).：

现在是acc_max([0],1,X).。同样，我们有两个规则，按照它们出现的顺序进行评估：

首先我们看到0 > 1 不正确，所以第一个规则失败，我们评估第二个。

现在我们看到0 =< 1 为真，并调用acc_max([],1,X)。这仅匹配 acc_max([], A, A).，因此我们将 X 与 1 统一（再次）。我们有解决方案，这次我们没有未评估的规则（即没有未探索的选择点）。所以现在我们看到了：

X = 1.

...因为在 Prolog 的“头脑”中毫无疑问没有其他解决方案。如果您要颠倒规则的顺序：

acc_max([], A, A).
acc_max([H|T], A, Max) :- H =< A, acc_max(T, A, Max).
acc_max([H|T], A, Max) :- H  > A, acc_max(T, H, Max).

...您也会看到行为反转。

希望这有助于证明这种是一致且可预测的交互，并且应该由 Prolog 的所有变体共享。