为什么来自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).vs 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的所有变体共享的交互.