Алгоритм выполняет следующие шаги:
• Сравниваем корневые функции: обе стороны имеют функцию 𝑓 значит, структура совпадает, и мы продолжаем анализ аргументов.
• Сравниваем первый аргумент: а = y. Это предполагает подстановку y -> a
• Сравниваем второй аргумент: Это предполагает подстановку x-> b
• Итоговая подстановка: {y-> a, x-> b}. С этой подстановкой термы становятся идентичными: 𝑓 (𝑎,𝑏) =𝑓 (𝑎,𝑏) Таким образом, унификация успешна.
Когда алгоритм завершается с ошибкой?
Алгоритм не может найти унификатор, если термы имеют несовместимую структуру. Например, рассмотрим термы:
Здесь корневые функции 𝑓 и 𝑔 различаются, что делает унификацию невозможной. Алгоритм завершиться с ошибкой, поскольку подстановка, которая могла бы сделать эти термы идентичными, не существует.
В языке, который мы проектируем, алгоритм унификации Робинсона может быть использован для вывода типов выражений, таких как x+1 или x == (1+2), где типы переменных могут неизвестными на момент анализа. Например, если переменная x используется в выражении x+1, алгоритм проверит, что оба операнда имеют тип int, и свяжет тип x с int, если это возможно. Такой подход позволит нашей системе типов автоматически определять типы, минимизируя необходимость явного их указания, и обеспечит строгую типизацию, как описано в разделе 1.1.2.
Этот алгоритм станет важным компонентом нашей системы вывода типов, особенно при реализации проверки типов и компиляции, которые мы рассмотрим в последующих главах. Для более глубокого понимания можно обратиться к работам Робинсона [5] и его последователи, включая улучшенные версии алгоритма, приложенные Мартелли и Монтанари [4] которые оптимизируют процесс унификации для более сложных выражений.
Алгоритм унификации Мартелли и Монтанари
В 1982 году Альберто Мартелли и Уго Монтанари предложили улучшенную версию алгоритма унификации Робинсона, адаптированную для работы с более сложными выражениями и множествами уравнений типов.
Этот алгоритм не только обрабатывает пары терминов, но и эффективно решает задачи унификации для систем уравнений, состоящих из нескольких терминов. Он проверяет, возможно ли выполнить унификацию для заданного множества уравнений типов, и, в случае успеха, возвращает наиболее общий унификатор – набор подстановок, делающих все уравнения идентичными.
Этот подход особенно полезен для реализации систем вывода типов в языках программирования, таких как наш, где требуется автоматическое определение типов выражений и переменных.
Из множества уравнений E выбирается одно уравнение. Если уравнение имеет форму X = t, где переменная X не появляется в других уравнениях множества E, оно не выбирается. Если множество E состоит из уравнений вида:
X1 = r1, X2 = r2, …, Xm = rm
и переменные X1, X2, …, Xm не появляются в терминах r1, r2, …, rm, то унификация завершена успешно.
Выбираем уравнение и выполняем следующие шаги:
· Если уравнение имеет форму f (l1, …, lk) = f (m1, …, mk), то оно удаляется из множества E, а уравнения l1 = m1, …, lk = mk добавляются в множество E.
· Если уравнение имеет форму f (l1, …, lk) = g (m1, …, mk), и f и g различны, то алгоритм завершится неудачей.
· Если уравнение имеет форму X = X, то оно удаляется из множества E.
· Если уравнение имеет форму X = t, и термин t не содержит переменной X, и X не появляется в другом уравнении, то применяется замена
