Unification 54432 220039081 2008-06-18T00:18:18Z ZX81 7326219 Reverted edits by [[Special:Contributions/70.235.81.50|70.235.81.50]] to last version by Hairy Dude (using [[WP:HG|Huggle]]) {{two other uses|the computer science topic|the idea of global unification|globalization}} In [[mathematical logic]], in particular as applied to [[computer science]], a '''unification''' of two terms is a ''join'' (in the [[lattice (order)|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 variable]]s 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''. If any common substitution instance of ''s'' and ''t'' is also an instance of ''u'', ''u'' is called ''minimal unification''. For example, with [[polynomial]]s, ''X'' <sup>2</sup> and ''Y'' <sup>3</sup> can be unified to ''Z''<sup>6</sup> by taking ''X'' = ''Z''<sup>3</sup> and ''Y'' = ''Z''<sup>2</sup>. ==Unification in logic programming and type theory== The concept of unification is one of the main ideas behind [[logic programming]], best known through the language [[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 the equality symbol <tt>=</tt>, but is also done when instantiating variables (see below). It is also used in other languages by the use of the equality symbol <tt>=</tt>, but also in conjunction with many operations including <tt>+</tt>, <tt>-</tt>, <tt>*</tt>, <tt>/</tt>. Unification is also the method used to perform [[type inference]]. # In traditional Prolog, a [[variable]] which is uninstantiated&mdash;i.e. no previous unifications were performed on it&mdash;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]], a variable cannot be unified with a term that contains it; this is the so called ''[[occurs check]]''. (In type theory, any type variable unifies with any type expression and is instantiated to that expression (subject to the occurs check where the theory specifies it).) # Two Prolog atoms can only be unified if they are identical. (In type theory, any two type constants unify only if they are the same type.) # Similarly, a term can be unified with another term if the top function symbols and [[Arity|arities]] of the terms are identical and if the parameters can be unified simultaneously. Note that this is a recursive behavior. (In type theory, any two type constructions unify only if they are applications of the same type constructor and all of their component types also recursively unify.) 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== ''In the convention of Prolog, atoms begin with lowercase letters.'' *''A'' = ''A'' : Succeeds ([[Tautology (logic)|tautology]]) *''A'' = ''B'', ''B'' = ''abc'' : Both ''A'' and ''B'' are unified with the atom ''abc'' *''abc'' = ''B'', ''B'' = ''A'' : As above (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, ''[http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/ ''Term Rewriting and All That''].'' Cambridge University Press, 1998. * F. Baader and W. Snyder, ''[http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSnyderHandbook.ps.gz ''Unification Theory''].'' In [[J.A. Robinson]] and A. Voronkov, editors, [[Handbook of Automated Reasoning]], volume I, pages 447–533. Elsevier Science Publishers, 2001. * [[Joseph Goguen]], ''[http://www-cse.ucsd.edu/~goguen/projs/sem.html ''What is Unification?''].'' * {{MathWorld | urlname=Unification | title=Unification | author=Alex Sakharov}} ==See also== *[[admissible rule]] [[Category:Automated theorem proving]] [[Category:Logic programming]] [[bg:Унификация]] [[de:Unifikation (Logik)]] [[fr:Unification]] [[ja:ユニフィケーション]] [[pl:Unifikacja]] [[pt:Unificação]] [[vi:Hợp nhất (lô gích)]] [[zh:合一]]