Pozornie niepotrzebny przypadku algorytmu zjednoczeniowego w SICP

Question

Próbuję zrozumieć algorytm jednoczenia opisany w SICP here

W szczególności, w ramach procedury „Extend-jeśli-to możliwe”, nie ma wyboru (pierwsze miejsce oznaczone gwiazdką „*”), który sprawdza, czy prawa ręka „ekspresja” to zmienna, która jest już związany z czymś w bieżącej ramce:

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

państwa stowarzyszone komentarz:

" W pierwszym przypadku, jeśli zmienna, którą próbujemy dopasować, nie jest powiązana, ale wartość, którą próbujemy dopasować, sama jest zmienną (inną), konieczne jest sprawdzenie, czy wartość jest związana, a jeśli tak, to dopasowanie jej wartość. Jeśli obie strony do meczu są niezwiązany możemy wiązać albo do drugiej.”

Jednak nie mogę myśleć o przypadku, gdy jest to rzeczywiście konieczne.

Co to mówisz, myślę, jest gdzie może mieć następujące powiązania ramki aktualnie obecne:

{?y = 4} 

a następnie są proszeni o „extendIfPossible” wiążącej od z do y

z tym „*” sprawdzić obecny, gdy aske?. d, aby rozszerzyć "? z" o "? y", widzimy, że "? y" jest już powiązane z 4, a następnie rekursywnie próbujemy ujednolicić "? z" z "4", co powoduje, że rozszerzamy ramkę o " ? z = 4 ".

Bez czeku, skończyłoby się rozszerzenie ramki tylko "? Z =? Y". Ale w obu przypadkach, tak długo, jak? Z nie jest już związany z czymś innym, nie widzę problemu.

Uwaga, jeśli? Z miał już, było już powiązane z czymś innym, wtedy kod nie dotarł do części oznaczonej "*" (musielibyśmy już powrócić do ujednolicenia z tym, do czego? Z został już dopasowany).

Po przemyśleniu tego, zdałem sobie sprawę, że może istnieć jakiś argument do generowania "najprostszego" MGU (Most General Unifier). na przykład możesz chcieć MGU z minimalną liczbą zmiennych odnoszących się do innych zmiennych ... to znaczy, chcielibyśmy raczej wygenerować podstawienie {? x = 4,? y = 4} niż podstawienie {? x =? y,? y = 4} ... ale nie sądzę, że ten algorytm zagwarantowałby takie zachowanie w każdym przypadku, ponieważ gdybyś poprosił o ujednolicenie "(? x 4)" z "(? y? yyy)", to nadal byś chciał kończy się na {? x =? y,? y = 4}. A jeśli zachowanie nie może być zagwarantowane, dlaczego dodatkowe złożoności?

Czy moje rozumowanie tutaj jest poprawne? Jeśli nie, jaki jest przeciwny przykład, gdzie czek "*" jest konieczny do wygenerowania poprawnejMGU?

Answer 1

To dobre pytanie!

Myślę, że powodem jest to, że nie chcesz kończyć się wiązaniami kołowymi, takimi jak { ?x = ?y, ?y = ?x }. W szczególności ujednolicenie (?x ?y) z (?y ?x) dałoby kołową ramkę powyżej, jeśli pominięto czek. Po sprawdzeniu otrzymasz ramkę {? X =? Y} zgodnie z oczekiwaniami.

Wiązania kołowe w ramce są złe, ponieważ mogą powodować, że funkcje wykonujące podstawienia za pomocą ramki, takie jak instantiate, będą działać w nieskończonej pętli.

Answer 2

Bez tego nie można uzyskać najbardziej ogólnego unifierów. Nadal będzie praca do zrobienia: zunifikowanie x i y.