Unification
|
|
- This article is about the computer science topic. For other uses of the term, see Unification (disambiguation).
In mathematical logic, in particular as applied to computer science, a unification of two terms is a join (in the lattice sense) with respect to a specialisation order. That is, we suppose a preorder on a set of terms, for which t* ≤ t means that t* is obtained from t by substituting some term(s) for one or more free variables in t. The unification u of s and t, if it exists, is a term that is a substitution instance of both s and t. Any common substitution instance of s and t is also an instance of u.
For example, with polynomials, X2 and Y3 can be unified to Z6 by taking X = Z3 and Y = Z2.
Unification in Prolog
The concept of unification is one of the main ideas behind Prolog. It represents the mechanism of binding the contents of variables and can be viewed as a kind of one-time assignment. In Prolog, this operation is denoted by symbol "=".
- In traditional Prolog, a variable X which is uninstantiated—i.e. no previous unifications were performed on it—can be unified with an atom, a term, or another uninstantiated variable, thus effectively becoming its alias. In many modern Prolog dialects and in first-order logic calculi, a variable cannot be unified with a term that contains it; this is the so called occurs check.
- A Prolog atom can be unified only with the same atom.
- Similarly, a term can be unified with another term if the top function symbols and arities of the terms are identical and if the parameters can be unified simultaneously. Note that this is a recursive behaviour.
Due to its declarative nature, the order in a sequence of unifications is (usually) unimportant.
Note that in the terminology of first-order logic, an atom is a basic proposition and is unified similarly to a Prolog term.
Examples of unification
- A = A : Succeeds (tautology)
- A = B, B = abc : Both A and B are unified with the atom abc
- xyz = C, C = D : Unification is symmetric
- abc = abc : Unification succeeds
- abc = xyz : Fails to unify because the atoms are different
- f(A) = f(B) : A is unified with B
- f(A) = g(B) : Fails because the heads of the terms are different
- f(A) = f(B, C) : Fails to unify because the terms have different arity
- f(g(A)) = f(B) : Unifies B with the term g(A)
- f(g(A), A) = f(B, xyz) : Unifies A with the atom xyz and B with the term g(xyz)
- A = f(A) : Infinite unification, A is unified with f(f(f(f(...)))). In proper first-order logic and many modern Prolog dialects this is forbidden (and enforced by the occurs-check)
- A = abc, xyz = X, A = X : Fails to unify; effectively abc = xyz
References
- F. Baader and T. Nipkow, Term Rewriting and All That (http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/). Cambridge University Press, 1998.
- F. Baader and W. Snyder, Unification Theory (http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSnyderHandbook.ps.gz). In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning (http://rpc25.cs.man.ac.uk/manchester/handbook-ar/), volume I, pages 447–533. Elsevier Science Publishers, 2001.de:Unifikation (Logik)