Я пытаюсь понять алгоритм унификации, описанный в SICP здесь
В частности, в процедуре "extend-if-possible" есть чек (первое место, помеченное звездочкой "*" ), которое проверяет, является ли "выражение" правой руки переменной, которая уже связана к чему-то в текущем кадре:
(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}
И затем попросят "extendIfPossible" привязку от? 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}. И если поведение не может быть гарантировано, зачем нужна дополнительная сложность?
Я правильно рассуждаю здесь? Если нет, то какой встречный пример, где проверка "*" необходима для создания правильного МГУ?
Это хороший вопрос!
Я думаю, причина в том, что вы не хотите заканчивать круговыми связями, такими как { ?x = ?y, ?y = ?x }. В частности, объединение (?x ?y) с (?y ?x) даст вам круговой фрейм выше, если вы опустили чек. С проверкой вы получите кадр {? X =? Y}, как ожидалось.
Циклические привязки в кадре плохие, потому что они могут вызывать функции, выполняющие подстановки с использованием фрейма, например instantiate, для запуска в бесконечном цикле.
Без этого вы не получите унифицированный общий. Все еще предстоит сделать работу: объединение x и y.