13

ここで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)))))

関連する解説は次のように述べています。

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

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

それが話しているのは、現在、次のフレームバインディングが存在する可能性がある場所だと思います。

{?y = 4}

次に、？zから？yへのバインディングを「extendIfPossible」するように求められます。

その「*」チェックが存在する場合、「？z」を「？y」で拡張するように求められると、「？y」はすでに4にバインドされていることがわかり、「？z」を「4」で再帰的に統合しようとします。これにより、フレームを「？z=4」で拡張します。

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

？zがすでに他の何かにバインドされている場合、コードは「*」とマークされた部分に到達しないことに注意してください（？zがすでに一致していたものと統合するためにすでに再帰しているはずです）。

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

ここでの私の推論はすべて正しいですか？そうでない場合、正しいMGUを生成するために「*」チェックが必要な反例は何ですか？

4

2 に答える 2

5

それは良い質問です！

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

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

于 2009-09-04T22:06:10.753 に答える
0

それがなければ、最も一般的なユニファイアを取得できません。xとyを統合するという、まだやるべきことがあります。

于 2009-08-07T08:00:53.220 に答える