prolog - 为什么 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 的所有变体所共享的交互。