На первый взгляд ненужный случай в алгоритме унификации в SICP

Question

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

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

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

Связанный комментарий гласит:

" В первом случае, если переменная, которую мы пытаемся сопоставить, не связана, но значение, с которым мы пытаемся сопоставить ее, само по себе является (другой) переменной, необходимо проверить, является ли значение связан, и если так, чтобы соответствовать его значению. Если обе стороны в матче не связаны, мы можем связать любую другую. & Quot;

Однако я не могу вспомнить случай, когда это действительно необходимо.

О чем идет речь, я думаю , это то место, где у вас могут быть следующие привязки кадров:

{?y = 4}

И затем их просят "extensionIfPossible" привязка от? z к? y.

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

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

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

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

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

Answer 1

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

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

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

Answer 2

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