Этот алгоритм не только обрабатывает пары терминов, но и эффективно решает задачи унификации для систем уравнений, состоящих из нескольких терминов. Он проверяет, возможно ли выполнить унификацию для заданного множества уравнений типов, и, в случае успеха, возвращает наиболее общий унификатор – набор подстановок, делающих все уравнения идентичными.
Этот подход особенно полезен для реализации систем вывода типов в языках программирования, таких как наш, где требуется автоматическое определение типов выражений и переменных.
Из множества уравнений 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 будет следующим: