Казалось бы, ненужный случай в алгоритме унификации в SICP

Question

Я пытаюсь понять алгоритм объединения, описанный в SICP здесь

В частности, в процедуре "extend-if-возможный" есть проверка (первое место, помеченное звездочкой "*"), которая проверяет, является ли правое выражение "выражение" переменной, которая уже связана с чем-то в текущий кадр:

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

И затем просят "расширить IfPossible" привязки от? Z к? Y.

С этой проверкой "*", когда ее просят расширить "? Z" с помощью "? Y", мы видим, что "? Y" уже привязан к 4, а затем рекурсивно пытаемся объединить "? Z" с "4", что приводит к расширению кадра с "?z = 4".

Без проверки мы в конечном итоге расширили бы фрейм просто "? Z =? Y". Но в обоих случаях, пока? Z еще не связан с чем-то другим, я не вижу проблемы.

Обратите внимание, что если? Z уже был привязан к чему-то другому, то код не достигает части, отмеченной "*" (мы бы уже вернулись к объединению с тем, с чем? Z уже было сопоставлено).

Подумав об этом, я понял, что может быть какой-то аргумент для генерации "самого простого" MGU (Most General Unifier). например, вы можете захотеть MGU с минимальным количеством переменных, относящихся к другим переменным... то есть мы бы лучше сгенерировали замену {?x = 4,?y = 4}, чем замену {?x =?y,?y = 4}... но я не думаю, что этот алгоритм гарантировал бы такое поведение в любом случае, потому что если бы вы попросили его объединить "(?x 4)" с "(?y?y)", то вы бы все равно в конечном итоге с {? x =? y,? y = 4}. И если поведение не может быть гарантировано, почему дополнительная сложность?

Все мои рассуждения верны? Если нет, то каков встречный пример, где проверка "*" необходима для генерации правильного MGU?

Answer 1

Это хороший вопрос!

Я думаю, причина в том, что вы не хотите заканчивать круговыми привязками, такими как { ?x = ?y, ?y = ?x }, В частности, объединяющий (?x ?y) с (?y ?x) даст вам круговую рамку выше, если вы опустите чек. С проверкой вы получите кадр {? X =? Y}, как и ожидалось.

Круговые привязки в кадре плохие, потому что они могут вызывать функции, выполняющие замены с использованием кадра, такие как instantiate, чтобы запустить в бесконечном цикле.

Answer 2

Без этого вы бы не получили самый общий объединитель. Будет еще много работы: объединение х и у.