Definitions

unified field theory

Attempt to describe all fundamental interactions between elementary particles in terms of a single theoretical framework (a “theory of everything”) based on quantum field theory. So far, the weak force and the electromagnetic force have been successfully united in electroweak theory, and the strong force is described by a similar quantum field theory called quantum chromodynamics. However, attempts to unite the strong and electroweak theories in a grand unified theory have failed, as have attempts at a self-consistent quantum field theory of gravitation.

officially Holy Spirit Association for the Unification of World Christianity

Religious movement founded (1954) in South Korea by Sun Myung Moon. Influenced by yin-yang principles and Korean shamanism, it seeks to establish divine rule on earth through the restoration of the family, based on the union of the Lord and Lady of the Second Advent (believed to be Moon and his wife, Hak Ja Han). It strives to fulfill what it asserts to be the uncompleted mission of Jesus—procreative marriage. The church has been criticized for its recruitment policies (said to include brainwashing) and business practices. Its mass marriage ceremonies have gained press attention. Its worldwide membership is about 200,000 in more than 100 countries.

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. If any common substitution instance of s and t is also an instance of u, u is called minimal unification.

For example, with polynomials, X 2 and Y 3 can be unified to Z6 by taking X = Z3 and Y = Z2.

Definition of unification for first-order logic

Let p and q be sentences in first-order logic.

UNIFY(p,q) = U where subst(U,p) = subst(U,q)

Where subst(U,p) means the result of applying substitution U on the sentence p. Then U is called a unifier for p and q. The unification of p and q is the result of applying U to both of them.

Let L be a set of sentences, for example, L = {p,q}. A unifier U is called a most general unifier for L if, for all unifiers U' of L, there exists a substitution s such that applying s to the result of applying U to L gives the same result as applying U' to L:

subst(U',L) = subst(s,subst(U,L)).

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 =, but is also done when instantiating variables (see below). It is also used in other languages by the use of the equality symbol =, but also in conjunction with many operations including +, -, *, /. Unification is also the method used to perform type inference.

1. In traditional Prolog, a variable 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, 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).)
2. 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.)
3. 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 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.

French computer scientist Gérard Huet gave an algorithm for unification in typed lambda calculus in 1973. There have been many developments in unification theory since then.

Examples of unification

In the convention of Prolog, atoms begin with lowercase letters.

• A = A : Succeeds (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