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)
Nearby terms:
UniCOMAL « unicos « Uniface « unification »
Unified Han » Unified Modeling Language » unifier
|
