Унификацию помните?

Представьте что у нас имеется два выражения, состоящие их переменных и констант. Ну или два дерева, ведь выражения однозначно представляются деревьями. И нам хочется сравнить эти два выражения или дерева. Это одно и тоже или разные вещи? В том смысле, что при каких-то значениях переменных выражения совпадают.

Такой алгоритм сопоставления назвали унификацией. Когда-то на нём строили экспертные системы: помните язык Пролог? Алгоритм унификации пытается сделать два символических выражения равными, вычисляя объединяющую подстановку для этих выражений. Подстановка — это функция, заменяющая переменные другими выражениями. Очень важно, что она действует одинаково на все вхождения одной и той же переменной: если подстановка меняет одно вхождение переменной 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. Мне кажется, гораздо яснее выходит.

( исходный код )

Унификация по Робинсону

Вынесу из комментов, где chaource предложил реализацию на Хаскеле.

В исходной статье Робинсона алгоритм звучит не особо ясно.

The following process, applicable to any finite nonempty set A of well-formed expressions, is called the Unification Algorithm:

• Step 1. Set σ₀ = ε and k = 0, and go to step 2.
• Step 2. If Aσₖ is not a singleton, go to step 3. Otherwise, set σ_A = σₖ, and terminate.
• Step 3. Let Vₖ be the earliest, and Uₖ the next earliest, in the lexical ordering of the disagreement set Bₖ of Aσₖ. If Vₖ is a variable, and does not occur in Uₖ, set σₖ₊₁ = σₖ {Uₖ / Vₖ}, add 1 to k, and return to step 2. Otherwise, terminate.

Переведём на современный язык.

Step 1. Initialization

• Start with a substitution σ₀​ = ∅.
• Let k = 0.
• Continue to Step 2.

Step 2. Check Whether Unification Is Complete

• Apply the current substitution σₖ to the entire set A, producing Aσₖ.
• If all resulting expressions in Aσₖ are identical, the algorithm stops and returns σₖ as the most general unifier.
• Otherwise proceed to Step 3.

Step 3. Find a Disagreement

• Identify the first position (in a left-to-right, top-down scan) where two expressions in Aσₖ differ.
• Let the disagreeing subexpressions be p and q.

Step 4. Process the Disagreement

Depending on the form of p and q:
1. If one is a variable and it does not occur inside the other term (occurs-check in modern terminology):

• Construct a substitution that maps that variable to the other term.
• Compose this substitution with the current one to produce Aσ_k+1.
• Increment k; return to Step 2.
2. If both are variables but different:

• Substitute one variable with the other, compose as above, and repeat Step 2.
3. If both are compound expressions with different functors or different arity:

• Unification fails; the set has no unifier, and the algorithm terminates unsuccessfully.
4. If both are compound expressions with the same functor and arity:

• Add their corresponding arguments to the set of expressions being unified.
• Return to Step 2.

Бегая глазами по исходникам unify.gisp и по описанию, вроде всё однозначно соответствует, разве нет? Дело же не в количестве строк, а в лёгкости понимания.