Я пытаюсь понять алгоритм объединения, описанный в 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?