Каков оптимальный алгоритм “наиболее общего объединения”?

Question

Этот Вопрос

Какой алгоритм MGU наиболее эффективен?Какова его временная сложность?Достаточно ли это просто описать как ответ на переполнение стека?

Я пытался найти ответ в Google, но продолжаю находить приватные .PDF-файлы, доступ к которым я могу получить только через подписку ACM.

Я нашел одно обсуждение в SICP: здесь

Объяснение того, что такое "наиболее общий алгоритм объединения":Возьмем два дерева выражений, содержащих "свободные переменные" и "константы"...например ,

 e1 = (+ x? (* y? 3) 5)
 e2 = (+ z? q? r?)

Затем наиболее общий алгоритм объединения возвращает наиболее общий набор привязок, который делает два выражения эквивалентными.

т. е.

mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5

Под "наиболее общим" вы могли бы вместо этого связать (x = 1) и (z = 1), и это также сделало бы e1 и e2 эквивалентными, но это было бы более конкретно.

Статья SICP, по-видимому, подразумевает, что это достаточно дорого.

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

Answer 1

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

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

Answer 2

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

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