Prolog中的統一

Question

這是一個關於Prolog統一過去的問題。 我們應該說，如果他們統一，然後實例化。

f(a,g(b,a)) and f(X,g(Y,X)) 

這統一相當= X，G（B，A）= G（Y，X）及頗爲直截了當

f(g(Y),h(c,d)) and f(X,h(W,d)) 

我不認爲這一個統一，因爲克（Y ）=/X，儘管h（c，d）與h（W，d）一致。雖然X = g（Y）是否可能，因爲大寫X直到它找到解決方案？

Answer 1

是的，它確實是統一的，它是這樣做的，因爲g(Y)是一個要評估的術語，以及a - 在您指出的第一個示例中。

您可以檢查評估在序言中解釋：

?- f(g(Y),h(c,d)) = f(X,h(W,d)). 
X = g(Y), 
W = c. 

統一進程工作在深度優先的方式，統一會員並返回每個可用的答案，直到沒有進一步的組合是可能的。

這意味着統一方法被調用f(g(Y),h(c,d)) = f(X,h(W,d))，即找出可用匹配數：g(Y) = X, h(c, d) = h(W, d)。

然後，在g(Y) = X上執行統一，即由於不再有可能的減少，所以返回X = g(Y)。

然後，調用相同的方法h(c, d) = h(W, d)，它給你c = W，並沒有其他匹配，從而導致，因此，在W = c。

返回統一後的答案，通常返回false指向沒有匹配/進一步匹配成爲可能時的點。

正如CapelliC指出的那樣，在統一過程之後，變量Y仍未被綁定。統一是在未結合的變量，這意味着執行：

• 的h(c, d) = h(W, d)返回h(_) = h(_)統一，並且這允許統一繼續，因爲h是一個術語，而不是未結合的變種;

• 統一的d = d是一個術語的匹配，並沒有形成歸屬 - 或綁定;

• 的c = W形式的歸屬，和可變W統一被綁定到術語c，因爲它沒有前結合 - 否則會被執行的比較;

• 的X = g(Y)統一簡單綁定綁定變量X的名詞g(Y)，並g(Y)是一個未綁定變量的一個術語，因爲沒有可供統一到g(Y)。

問候！