Definition
Unification
Unification is the problem of finding a substitution that makes two formal expressions equal.
Formally, for expressions
and , a substitution is a unifier iff In type inference, unification is used to solve type equations such as