SICPの統合アルゴリズムで一見不要なケース

Question

SICP こちら

特に、プロシージャ「extend-if-possible」では、右手「式」が正しいかどうかを確認するチェック（アスタリスク「*」でマークされた最初の場所）があります。現在のフレーム内の何かに既にバインドされている変数です：

(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)))))

関連するコメントの状態：

＆quot;最初のケースでは、一致させようとしている変数がバインドされていないが、それと一致させようとしている値自体が（異なる）変数である場合、値を確認する必要がありますバインドされ、バインドされている場合、その値に一致します。試合の両当事者が拘束されていない場合、どちらか一方を拘束することができます。＆quot;

ただし、これが実際に必要な場合は考えられません。

それが何を言っているのか、私は考える、あなたが現在存在する以下のフレームバインディングがあるかもしれません：

{?y = 4}

そして、「extendIfPossible」に尋ねられます; ？zから？yへのバインディング。

その＆quot; *＆quot; 「？z」を拡張するように求められたら、存在を確認します。 ＆quot;？y＆quot;を使用すると、＆quot;？y＆quot;が表示されます。はすでに4にバインドされており、再帰的に「？z」を統一しようとします。 ＆quot; 4＆quot;で、これは＆quot;？z = 4＆quot;でフレームを拡張した結果です。

チェックなしでは、「？z =？y」だけでフレームを拡張することになります。しかし、どちらの場合でも、？zが既に他のものにバインドされていない限り、問題は見当たりません。

注：？z が既に他のものにバインドされている場合、コードは＆quot; *＆quot;とマークされた部分に到達しません。 （？zがすでに一致していたものと統一するために、すでに再帰していました）。

考え直した後、「最も単純な」生成に何らかの議論があるかもしれないことに気付きました。 MGU（Most General Unifier）。例えば他の変数を参照する変数の数が最小のMGUが必要な場合があります。つまり、置換{？x =？y、？ y = 4} ...しかし、このアルゴリズムがどのような場合でもこの動作を保証するとは思わない。なぜなら、「（？x 4）」を統合するように要求した場合。 ＆quot;（？y？y）＆quot;その後、{？x =？y、？y = 4}になります。動作を保証できない場合、なぜ追加の複雑さが必要ですか？

ここでの推論はすべて正しいですか？そうでない場合、＆quot; *＆quot; 正しい MGUを生成するにはチェックが必要ですか？

Answer 1

これはいい質問です！

その理由は、 {？x =？y、？y =？x} のような循環バインディングになりたくないからだと思います。特に、（？x？y）を（？y？x）と統合すると、チェックを省略した場合に上記の円形フレームが表示されます。チェックにより、フレーム{？x =？y}が期待どおりに取得されます。

フレーム内の循環バインディングは、 instantiate などのフレームを使用して置換を実行する関数が無限ループで実行される可能性があるため、不良です。

Answer 2

それなしでは、最も一般的な統合子は得られません。まだやるべきことがあります：xとyを統合します。