Caso apparentemente inutile nell'algoritmo di unificazione in SICP

Question

Sto cercando di capire l'algoritmo di unificazione descritto in SICP qui

In particolare, nella procedura "estende-se-possibile", c'è un segno di spunta (il primo posto contrassegnato da asterix "*") che sta verificando se la mano destra "espressione". è una variabile che è già associata a qualcosa nel frame corrente:

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

I commenti associati indicano:

" Nel primo caso, se la variabile che stiamo cercando di abbinare non è vincolata, ma il valore che stiamo cercando di abbinare è di per sé una (diversa) variabile, è necessario verificare se il valore è associato e, in tal caso, corrispondere al suo valore. Se entrambe le parti della partita non sono vincolate, potremmo vincolarci a vicenda. & Quot;

Tuttavia, non riesco a pensare a un caso in cui questo è effettivamente necessario.

Di cosa sta parlando, penso , è dove potresti avere attualmente i seguenti collegamenti di frame:

{?y = 4}

E poi viene chiesto di " extensionIfPossible " un'associazione da? z a? y.

Con questo " * " controlla presente, quando ti viene chiesto di estendere "? z " con "? y " ;, vediamo che "? y " è già associato a 4, quindi cerca in modo ricorsivo di unificare "? z " con " 4 " ;, che risulta con noi estendendo il frame con "? z = 4 " ;.

Senza il controllo, finiremmo per estendere il frame solo con "? z =? y " ;. Ma in entrambi i casi, finché? Z non è già legato a qualcos'altro, non vedo il problema.

Nota, se? z era già stato associato a qualcos'altro, il codice non raggiunge la parte contrassegnata con " * " (avremmo già ricominciato a unificarci con ciò a cui? z era già stato abbinato).

Dopo averci riflettuto, mi sono reso conto che potrebbe esserci una sorta di argomento per generare un "più semplice" MGU (Most General Unifier). per esempio. potresti volere un MGU con un numero minimo di variabili che si riferiscono ad altre variabili ... cioè preferiamo generare la sostituzione {? x = 4,? y = 4} rispetto alla sostituzione {? x =? y,? y = 4} ... ma non credo che questo algoritmo garantirebbe questo comportamento in ogni caso, perché se gli chiedessi di unificare " (? x 4) " con " (? y? y) " allora finiresti comunque con {? x =? y,? y = 4}. E se il comportamento non può essere garantito, perché la complessità aggiuntiva?

Il mio ragionamento qui è tutto corretto? In caso contrario, qual è un contro esempio in cui " * " il controllo è necessario per generare un corretto MGU?

Answer 1

Questa è una buona domanda!

Penso che il motivo sia che non vuoi finire con associazioni circolari come {? x =? y,? y =? x} . In particolare, unificare (? X? Y) con (? Y? X) ti darebbe la cornice circolare sopra se omettessi il controllo. Con il segno di spunta, ottieni il frame {? X =? Y} come previsto.

I collegamenti circolari in un frame sono errati, perché possono causare funzioni che eseguono sostituzioni utilizzando il frame, come istanza , in un ciclo infinito.

Answer 2

Senza di essa, non otterresti il ?? più generale unificatore. Ci sarebbe ancora del lavoro da fare: unificare x e y.