爲什麼Prolog會將變量與直接插入的結果匹配失敗？

Question

我在做一個Prolog程序，它可以找到一組列表的一個子集。這個子集必須符合一些特定的條件，其中一個方面是子集的列表不能相同。什麼是困惑我的是，當我試圖找到變量匹配，X，如果我把它們插入到查詢到位X的例如生成返回錯誤結果：

?- containsSet(2, [[3],[7],[7]], X). 
X = [[3], [7]] ; 
X = [[3], [7]] ; 
X = [[7], [7]] ; 
false. 

?- containsSet(2, [[3],[7],[7]], [[7],[7]]). 
false. 

怎麼可能呢如果在直接插入時返回false，可能會將X與[[7]，[7]]匹配。

containsSet的思想是找到在匹配位置中沒有匹配元素的長度爲N的子集（在本例中爲2）（即，子集中沒有兩個列表具有相同的第一個元素，或者相同第二元素等）。在上面的例子中，[7]和[7]中的第一個（也是唯一）元素匹配，所以它返回false。

Answer 1

首先，祝賀我在初學者的問題中看到的最具說明性和合理性的觀察結果之一！

一方面，它是聯合是邏輯上可交換的最基本和最着名的屬性之一。另一方面，許多Prolog初學者沒有意識到使用諸如(\+)/1之類的非單調謂詞幾乎總是破壞這樣的基本不變量。你注意到在這裏發生了一些非常意外的事情，並且你期待Prolog有更正確的行爲。幸運的是，針對這些問題的聲明性解決方案現在比Prolog系統中更廣泛地傳播。

首先考慮，如果你在程序中使用(\+)/1很快出現了一些問題：

 
?- X = d, \+ member(X, [a,b,c]). 
X = d. 

的是，如果我們只是靠結合的交換性交流的目標，我們得到的不同答案：

 
?- \+ member(X, [a,b,c]), X = d. 
false. 

這表明(\+)/1是不單調的：它可能會導致更普遍失敗查詢雖然更具體查詢產生的解決方案：

 
?- \+ member(X, [a,b,c]). 
false. 

?- \+ member(d, [a,b,c]). 
true. 

因此，非單調謂詞導致各種雜質和違反聲明語義。聲明，知道有解決方案，我們當然期望成功更一般的查詢，但失敗。

在這個具體的，可以指定一個術語是從列表中的所有其他條款不同，使用約束dif/2。 dif/2適用於所有方向，如果其參數是變量，也會產生正確的答案。例如：

not_member(X, Ls) :- maplist(dif(X), Ls). 

這個定義保留相結合的交換性，因爲我們深深的渴望，事實上，從純邏輯關係預期：

 
?- not_member(X, [a,b,c]), X = d. 
X = d. 

?- X = d, not_member(X, [a,b,c]). 
X = d. 

由於not_member/2只使用純謂詞，你已確保—已經建設—，它只給出聲明正確的答案。

對於聲明性的關於你的代碼的推理，我贊成你的方法，我建議你留在Prolog的純單調子集中。有關更多信息，請參閱logical-purity和prolog-dif。