unification

programming The generalisation of pattern matching that is

the logic programming equivalent of instantiation in

logic. When two terms are to be unified, they are

compared. If they are both constants then the result of

unification is success if they are equal else failure. If one

is a variable then it is bound to the other, which may be any

term (which satisfies an "occurs check"), and the

unification succeeds. If both terms are structures then each

pair of sub-terms is unified recursively and the unification

succeeds if all the sub-terms unify.

The result of unification is either failure or success with a

set of variable bindings, known as a "unifier". There may

be many such unifiers for any pair of terms but there will be

at most one "most general unifier", other unifiers simply

add extra bindings for sub-terms which are variables in the

original terms.

(1995-12-14)