为什么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).，并创下输入：

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

（该▮表示光标的位置。）

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

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

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

?- ▮ 

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

相比之下，下面我给我的屏幕看起来像后，我在提示符下键入max([2, 0, 1], X).什么，并创下输入：

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

?- ▮ 

注意，这一次我得到了解释器的提示马上 - 我做不需要输入;。此外，没有false。我发现许多其他类似的不一致（例如，有时输出true.显示在屏幕上，但在其他类似的情况下它不会）。

作为一个初来乍到Prolog的，我觉得这种不一致令人不安的（更不用提沮丧，因为他们不断地提醒我真的不知道发生了什么事情的）。

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

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

Answer 1

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

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

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

这正好acc_max([1],0,X).，这两个acc_max([H|T], A, Max) :-规则相匹配。我们按照它们出现的顺序对它们进行评估：

首先我们看到1 > 0为true，并调用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为true，并调用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的所有变体共享的交互。