爲什麼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的所有變體共享的交互。