Унификация по Робинсону
В исходной статье Робинсона алгоритм звучит не особо ясно.
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Бегая глазами по исходникам unify.gisp и по описанию, вроде всё однозначно соответствует, разве нет? Дело же не в количестве строк, а в лёгкости понимания.Step 2. Check Whether Unification Is Complete
- Start with a substitution σ₀ = ∅.
- Let k = 0.
- Continue to Step 2.
Step 3. Find a Disagreement
- 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 4. Process the 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.
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):
2. If both are variables but different:
- 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.
3. If both are compound expressions with different functors or different arity:
- Substitute one variable with the other, compose as above, and repeat Step 2.
4. If both are compound expressions with the same functor and arity:
- Unification fails; the set has no unifier, and the algorithm terminates unsuccessfully.
- Add their corresponding arguments to the set of expressions being unified.
- Return to Step 2.








