在SICP

Question

統一算法看似不必要的情況下

我想了解SICP here

特別描述的，在程序的統一算法「延長-IF-可能」，有一個檢查（第1名標有星號「*」），其檢查，看看是否右手「表達」是已經被綁定到的東西在當前幀中一個變量：

(define (extend-if-possible var val frame) 
    (let ((binding (binding-in-frame var frame))) 
    (cond (binding 
     (unify-match 
     (binding-value binding) val frame)) 
     ((var? val)      ; *** why do we need this? 
     (let ((binding (binding-in-frame val frame))) 
     (if binding 
      (unify-match 
       var (binding-value binding) frame) 
      (extend var val frame)))) 
     ((depends-on? val var frame) 
     'failed) 
     (else (extend var val frame))))) 

相關的評註的狀態：

「在第一種情況下，如果我們試圖匹配的變量沒有被綁定，但是我們試圖匹配它的值本身就是一個（不同的）變量，那麼就必須檢查該值是否被綁定，如果匹配值。如果雙方的比賽是未綁定的，我們可以結合或者其他。」

不過，我想不出一個案例中，這實際上是必要的。

什麼是它的談論，我認爲，在這裏，你可能有當前存在以下框架綁定：

{?y = 4} 

，然後被要求「extendIfPossible」從Z A結合到y

連稱「*」檢查目前，當aske？。 d將「？z」擴展爲「？y」，我們看到「？y」已經綁定到4，然後遞歸地嘗試將「？z」與「4」統一起來，這導致我們將幀擴展爲「 ？z = 4「。

沒有檢查，我們最終會延長框架，只是「？z =？y」。但是在這兩種情況下，只要？z沒有被綁定到別的東西上，我就沒有看到問題。請注意，如果？z 已有已被綁定到其他東西，那麼代碼不會到達標記爲「*」的部分（我們已經遞歸與已經匹配的內容進行了統一）。

經過深思熟慮後，我意識到可能存在某種用於生成「最簡單」MGU（最一般統一體）的論點。例如你可能想要一個具有最少數量變量的MGU來引用其他變量......也就是說，我們寧願生成替換{？x = 4，？y = 4}而不是替換{？x =？y，？ y = 4} ...但我不認爲這個算法會在任何情況下保證這種行爲，因爲如果你要求它將「（？x 4）」與「（？y？y）」統一起來，那麼你仍然會最終得到{？x =？y，？y = 4}。如果行爲無法得到保證，爲什麼會增加複雜性？

我的推理在這裏都是正確的嗎？如果不是，那麼需要使用「*」檢查以產生正確的 MGU的反例是什麼？

Answer 1

這是一個很好的問題！

我認爲原因是你不想以循環綁定結束，如{ ?x = ?y, ?y = ?x }。尤其是，統一(?x ?y)與(?y ?x)會給你上面的圓形框架，如果你省略了支票。通過檢查，您可以按預期得到框架{？x =？y}。

幀中的循環綁定是不好的，因爲它們可能會導致使用幀執行替換的函數（例如instantiate）在無限循環中運行。

Answer 2

沒有它，你不會得到最一般的統一。還有工作要做：統一x和y。