Как работает алгоритм унификации?

Алгоритм унификации Робинсона анализирует два терма (выражения или типовые конструкции) и пытается найти такую подстановку, которая сделает их идентичными. Процесс выполняется пошагово следующим образом:

• Разбор на подвыражения: Алгоритм разбивает входные термы на их составные части, такие как функции, переменные и константы, чтобы сравнить их структуру.

• Пошаговая унификация: Алгоритм последовательно проверяет термы и переменные, начиная с их корневых элементов. Если термы имеют одинаковую структуру (например, оба являются вызовами функции с одинаковым именем), унификация продолжается для их аргументов.

• Применение подстановок: Если в одном терме встречается переменная, а в другом – конкретное значение, алгоритм заменяет переменную этим значением. Например, если у нас есть переменная X и значение a, подстановка X -> a применяется ко всем вхождениям Х.

• Проверка совместимости: Алгоритм оценивает, можно ли сделать термы идентичными с помощью подстановок. Если подстановка успешно приводит к равенству термов, унификация завершается успешно. Если же обнаруживается противоречие, процесс завершается с ошибкой.

Рассмотрим пример унификации двух термов:

Алгоритм выполняет следующие шаги:

• Сравниваем корневые функции: обе стороны имеют функцию 𝑓 значит, структура совпадает, и мы продолжаем анализ аргументов.

• Сравниваем первый аргумент: а = 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 году Альберто Мартелли и Уго Монтанари предложили улучшенную версию алгоритма унификации Робинсона, адаптированную для работы с более сложными выражениями и множествами уравнений типов.

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