unification

views updated Jun 11 2018

unification An operation on well-formed formulas, namely that of finding a most general common instance. The formulas can be terms or atomic formulas (see predicate calculus). A common instance of two formulas A and B is a formula that is an instance of both of them, i.e. that can be obtained from either by some consistent substitution of terms for variables. As an example let A and B be the following:

A = p(f(u),v)

B = p(w,g(x))

Let u, v, w, x, y, z be variables, and c, d constants. Consider the substitution that replaces u, v, w, x respectively by the terms y, g(z), f(y), z. This substitution, when applied to A and B, transforms them both into the same formula I1, where

I1 = P(f(y), g(z))

Hence the above is a common instance of A and B. It is however only one of infinitely many: other common instances of A and B include

I2 = P(f(z),g(y))

I3 = P(f(y),g(y))

I4 = P(f(f(y)),g(g(z)))

I5 = P(f(c),g(d))

Note that I2, I3, I4, I5 are themselves instances of I1. In fact any common instance of A and B is an instance of I1 and therefore I1 is called a most general common instance of A and B. Of the formulas above, the only other one that is a most general common instance is I2. I5 would also be one if c and d were variables rather than constants; indeed the y and z of I1 could be any two distinct variables. In some cases A and B have no common instance; two examples of this are

A = P(f(u),v)

B = P(g(w),x)

and

A = P(f(u),u)

B = P(w,f(w))

If A and B do have a common instance however, they must have a most general one. There are algorithms (the original one being Robinson's, 1965) for deciding whether a given A and B have a common instance, and if so finding a most general one. Robinson's motivation for describing unification was its role in resolution theorem proving. Resolution was at one time associated with “general problem-solving” techniques in artificial intelligence. More recently it has provided the conceptual basis for the logic programming language Prolog. Another use of unification is in compile-time type-inference, especially for polymorphic types.

unification

views updated Jun 11 2018

u·ni·fi·ca·tion / ˌyoōnəfiˈkāshən/ • n. the process of being united or made into a whole.DERIVATIVES: u·ni·fi·ca·tor·y / -ˈkātərē/ adj.

More From encyclopedia.com