Вопрос
Каков наиболее эффективный алгоритм МГУ? Какова его временная сложность? Легко ли это описать как ответ?
Я пытался найти ответ в Google, но продолжаю находить частные .PDF, к которым я могу получить доступ только через подписку ACM.
Я нашел одно обсуждение в SICP: здесь
Объяснение того, что такое "самый общий алгоритм унификации": Возьмите два дерева выражений, содержащих "свободные переменные" и "константы"... например,
e1 = (+ x? (* y? 3) 5) e2 = (+ z? q? r?)
Затем алгоритм Most General Unifier возвращает самый общий набор привязок, который делает эти два эквивалентных выражения.
то есть.
mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5
Под "самым общим" вы могли бы вместо этого привязать (x = 1) и (z = 1), а также сделать эквивалент e1 и e2, но это было бы более конкретно.
В статье SICP подразумевается, что она достаточно дорога.
Для информации, причина, о которой я прошу, заключается в том, что я знаю, что вывод типа также включает в себя этот алгоритм объединения, и я хотел бы его понять.
Простой алгоритм, который используется на практике (например, в Prolog), экспоненциальен для патологических случаев.
Существует теоретически более эффективный алгоритм Мартелли и Монтанари (IIRC - линейный), но для простых случаев, которые происходят на практике, он намного медленнее, поэтому он мало используется.
Baader and Snyder опубликовали несколько алгоритмов унификации, как для синтаксического объединения, так и для эквациональной унификации.
Они заявляют, что их третий алгоритм синтаксической унификации (в разделе 2.3) работает в O (n alpha (n)), где alpha (n) является обратной функцией Аккермана - в практических ситуациях она эквивалентна небольшой константе.