Unification

Unification is the process of finding solutions to equations.

Intuition

Suppose we have a finite set of equations

  l_1 = r_1 \quad \ldots \quad l_n = r_n

between terms l_i and r_i.

The exact nature of l_i and r_i may vary: they might be first-order terms, or they might be terms of the \lambda-calculus. What is important is that they have some free variables x_1, \ldots x_m.

Unification looks for a substitution \sigma that maps each free variable x_i to a term such that all these equations l_i[\sigma] = r_i[\sigma] hold. 'Holding' can mean a number of things:

• it might mean that l_i and r_i are syntactically identical (this was the original sense)
• it might also mean that the terms l_i[\sigma] and r_i[\sigma] are provably equal up to some equational theory Plotkin 1972.

History

Please expand.

See also

• Higher-order unification

References

Please expand.