unification
The generalisation of {pattern matching} that is the {logic programming} equivalent of {instantiation} in
{logic}. When two {term}s 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 {recursive}ly 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)