Scheinbar unnötiger Fall im Unifikationsalgorithmus in SICP

Question

Ich versuche, den Unifikationsalgorithmus in SICP here

Insbesondere in dem Verfahren „extend-if-möglich“ beschrieben, zu verstehen, gibt es eine Prüfung (die erste Stelle markiert mit Sternchen „*“), die, wenn die rechte Hand „Ausdruck“ zu sehen ist, überprüft eine Variable, die bereits etwas im aktuellen Rahmen gebunden ist:

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

der zugehörige Kommentar heißt es:

" Im ersten Fall, Wenn die Variable, die wir abzugleichen versuchen, nicht gebunden ist, aber der Wert, mit dem wir sie abzugleichen versuchen, selbst eine (andere) Variable ist, muss überprüft werden, ob der Wert gebunden ist, und wenn dies der Fall ist Wert. Wenn beide Parteien zu dem Spiel ungebunden sind, können wir entweder auf die andere binden.“

Allerdings habe ich nicht von einem Fall denken kann, wenn dies tatsächlich erforderlich ist.

Was darüber spricht, ich denken , ist, wo Sie können folgende Rahmenbindungen zur Zeit vorhanden haben:

{?y = 4} 

und werden dann gebeten, „extendIfPossible“ von einer Bindung z zu y

Damit „*“ vorhanden überprüfen, wenn aske?. d um "? z" mit "? y" zu erweitern, sehen wir, dass "? y" bereits an 4 gebunden ist und dann rekursiv versuchen "? z" mit "4" zu vereinheitlichen, was dazu führt, dass wir den Rahmen mit " ? z = 4 ".

Ohne die Prüfung würden wir am Ende den Rahmen mit nur "? Z =? Y" erweitern. Aber in beiden Fällen, solange? Z nicht bereits an etwas anderes gebunden ist, sehe ich das Problem nicht.

Hinweis: Wenn? Z bereits an etwas anderes gebunden wurde, dann erreicht der Code den mit "*" markierten Teil nicht (wir hätten bereits repliziert, mit was? Z bereits abgeglichen wurde).

Nachdem ich darüber nachgedacht habe, habe ich festgestellt, dass es eine Art Argument für die Erzeugung einer "einfachsten" MGU (Most General Unifier) ​​geben könnte. z.B. Vielleicht möchten Sie eine MGU mit einer minimalen Anzahl von Variablen, die sich auf andere Variablen beziehen ... das heißt, wir erzeugen lieber die Substitution {? x = 4,? y = 4} als die Substitution {? x =? y,? y = 4} ... aber ich denke nicht, dass dieser Algorithmus dieses Verhalten in jedem Fall garantieren würde, denn wenn du es bitten würdest, "(? x 4)" mit "(? y? y)" zu vereinheitlichen, würdest du immer noch enden mit {? x =? y,? y = 4}. Und wenn das Verhalten nicht garantiert werden kann, warum die zusätzliche Komplexität?

Ist meine Argumentation hier korrekt? Wenn nicht, was ist ein Zählerbeispiel, bei dem die "*" - Prüfung erforderlich ist, um eine korrekte MGU zu generieren?

Answer 1

Das ist eine gute Frage!

Ich denke der Grund ist, dass Sie nicht mit Kreisbindungen wie { ?x = ?y, ?y = ?x } enden möchten. Insbesondere würde die Vereinigung (?x ?y) mit (?y ?x) Ihnen den kreisförmigen Rahmen oben geben, wenn Sie die Prüfung ausgelassen hätten. Mit der Prüfung erhalten Sie den Rahmen {? X =? Y} wie erwartet.

Circular Bindings in einem Frame sind fehlerhaft, da sie dazu führen können, dass Funktionen, die Substitutionen mit dem Frame ausführen, wie z. B. instantiate, in einer Endlosschleife ausgeführt werden.

Answer 2

Ohne sie würden Sie nicht die allgemeinsten Unifier bekommen. Es würde noch viel zu tun geben: x und y vereinheitlichen.