Читать книгу Введение в разработку собственного языка и компилятора. Создаем на Rust! - Андрей Невский - Страница 7

Одним из ключевых инструментов для реализации системы вывода типов является алгоритм унификации, предложенный Джоном А. Робинсоном в 1965 году [5]. Этот алгоритм играет центральную роль в определении типов переменных и выражений, позволяя находить наименьшую общую подстановку (унификатор) для двух выражений или устанавливать, что такая подстановка невозможна. Он стал основой для логического программирования, например, в языке Prolog, а также для автоматических систем вывода в искусственном интеллекте, и может быть полезен при проектировании нашего собственного языка.

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

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

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

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

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

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

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

𝑓 (𝑎,𝑥) =𝑓 (y,b)

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

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

• Сравниваем первый аргумент: а = y. Это предполагает подстановку y -> a

• Сравниваем второй аргумент: Это предполагает подстановку x-> b

• Итоговая подстановка: {y-> a, x-> b}. С этой подстановкой термы становятся идентичными: 𝑓 (𝑎,𝑏) =𝑓 (𝑎,𝑏) Таким образом, унификация успешна.

Когда алгоритм завершается с ошибкой?

Алгоритм не может найти унификатор, если термы имеют несовместимую структуру. Например, рассмотрим термы:

f (a) =g (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 не появляется в другом уравнении, то применяется замена [t/X] ко всем остальным уравнениям в E.

· Если уравнение имеет форму X = t, и t содержит переменную X, алгоритм завершится неудачей (это называется проверкой на самопоявление – occurs check).

· Если уравнение имеет форму t = X, и t не является переменной, то уравнение t = X удаляется из множества E, и добавляется уравнение X = t (меняем местами левую и правую часть уравнения).

· Возвращаемся к множеству уравнений E.

Когда алгоритм завершится успешно, множество E будет иметь вид:

X1 = r1, X2 = r2, …, Xm = rm

И эта замена будет являться наиболее общим унификатором для множества уравнений E.

Рассмотрим следующий пример на языке Standard ML:

val x = 1;

val y = x +2;

val z = y * 3;

Пусть X – тип x, Y – тип y, Z – тип z. Тогда:

x = 1 → X = int

y = x +2 → Y = int (так как + требует int для x и 2)

z = y * 3 → Z = int (так как * требует int для y и 3)

Итог: X = int, Y = int, Z = int.

В этой программе тип очевиден только для числа 1, который имеет тип int. Чтобы выполнить вывод типов, заменим неизвестные части на переменные типов. Пусть тип переменной x будет X, тип переменной y – Y, а тип переменной z – Z. Тогда множество типовых уравнений E будет следующим:

E = {X = Y, Y = Z, Z = int}

Теперь проведем унификацию для типов Z и int. Поскольку они совпадают, замена [int/Z] будет применена. После этого множество уравнений будет выглядеть так:

E = {X = Y, Y = int, Z = int}

Далее, рассматривая типы Y и int, мы применяем замену [int/Y]. После применения этой замены множество уравнений становится:

E = {X = int, Y = int, Z = int}

Теперь мы можем сделать вывод, что тип переменной x (то есть X) – это int.

В языке, который мы проектируем, алгоритм Мартелли и Монтанари может быть использован для расширения системы вывода типов, особенно при обработке более сложных выражений, включающих несколько переменных и операций. Хотя наш язык ограничивается типами int и bool, этот подход позволит нам автоматически определять типы переменных и выражений, таких как x+y или x == (1+2), минимизируя необходимость явного указания типов. Такой механизм обеспечит строгую типизации и упростит разработку компилятора, который мы реализуем в последующих главах .

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