Представьте что у нас имеется два выражения, состоящие их переменных и констант. Ну или два дерева, ведь выражения однозначно представляются деревьями. И нам хочется сравнить эти два выражения или дерева. Это одно и тоже или разные вещи? В том смысле, что при каких-то значениях переменных выражения совпадают.
Такой алгоритм сопоставления назвали
унификацией. Когда-то на нём строили экспертные системы: помните язык Пролог? Алгоритм унификации пытается сделать два символических выражения равными, вычисляя объединяющую подстановку для этих выражений. Подстановка — это функция, заменяющая переменные другими выражениями. Очень важно, что она действует одинаково на все вхождения одной и той же переменной: если подстановка меняет одно вхождение переменной x на a, она должна заменить все вхождения x на a.
Объединяющая подстановка (или унификатор) для двух выражений e1 и e2 — это подстановка σ, такая что применение σ делает e1 и e2 структурно одинаковыми. Рассмотрим на примерах.
Пример 1:
простая унификация. Выражения f(x) и f(y) можно унифицировать, заменив y на x (или наоборот).
Тогда унификатор σ действует так:
σ(y) = x
σ оставляет остальные переменные без изменений.
Пример 2:
неудачная унификация. Выражения x + 1 и y + 2 нельзя унифицировать. Не стоит пытаться подставить 3 вместо x и 2 вместо y, чтобы оба выражения стали равны 4. Унификация требует символического равенства, а 1 не сопоставляется с 2.
Пример 3:
несколько возможных унификаторов. Для выражений f(x, y) и f(1, y) возможны разные унификаторы:
σ₁ = { x ↦ 1 } даёт результат f(1, y).
σ₂ = { x ↦ 1, y ↦ 5 } даёт f(1, 5).
Оснований менять y нет, поэтому σ₁ предпочтительнее.
Алгоритмы унификации обычно стремятся получить наиболее общий унификатор (most general unifier, MGU). Это когда делаются только необходимые подстановки. Все остальные унификаторы получаются из MGU путём добавления новых замен. В примере выше σ₁ — MGU, а σ₂ — его частный случай.
Красивая реализация унификации приведена как пример в книжке The Scheme Programming Language:
Section 12.10. A Unification Algorithm. Меньше сотни строчек с комментариями, но понять непросто:
unify.ss.
А давайте перепишем на смешной язык
Gisp. Который внутри тот же Scheme, но с синтаксисом Go. Мне кажется, гораздо яснее выходит.
( исходный код )
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
vak
