Каков оптимальный алгоритм "самый общий унификатор"?

Вопрос

Каков наиболее эффективный алгоритм МГУ? Какова его временная сложность? Легко ли это описать как ответ?

Я пытался найти ответ в 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 подразумевается, что она достаточно дорога.

Для информации, причина, о которой я прошу, заключается в том, что я знаю, что вывод типа также включает в себя этот алгоритм объединения, и я хотел бы его понять.

Ответ 1

Простой алгоритм, который используется на практике (например, в Prolog), экспоненциальен для патологических случаев.

Существует теоретически более эффективный алгоритм Мартелли и Монтанари (IIRC - линейный), но для простых случаев, которые происходят на практике, он намного медленнее, поэтому он мало используется.

Ответ 2

Baader and Snyder опубликовали несколько алгоритмов унификации, как для синтаксического объединения, так и для эквациональной унификации.

Они заявляют, что их третий алгоритм синтаксической унификации (в разделе 2.3) работает в O (n alpha (n)), где alpha (n) является обратной функцией Аккермана - в практических ситуациях она эквивалентна небольшой константе.