Unification is one of the basic mechanisms incorporated in Prolog. Prolog can compare arbitrarily complex terms and unify them – if applicable.
Unification in fact means a procedure of pattern matching for terms. It is achieved by replacing variables with appropriate terms. Such a replacement is called substitution.
A substitution is a mapping of variables into terms; normally, only few variables are affected. Hence, substitutions are specified as sets of pairs of the form <variable>/<term>. In general, σ={X1/t1,X2/t2,…,Xn/tn} denotes a substitution replacing variables X1,X2,…,Xn with terms t1,t2,…,tn. It is important that all the variables are replaced with the appropriate terms simultaneously.
For example, σ={X/a,Y/f(b),Z/V} is a well-defined substitution. Such a substitution can be applied to any term/atom. For example, when applied to atom p(X,Y,Z) it produces an instance of it of the form p(a,f(b),V).
Having a pair of terms/atoms the unification algorithm compares them top-down in a subsequent manner and tries to find a unifying substitution, i.e. such that makes the terms/atoms identical.
For example, the following pairs can be unified by applying an appropriate unifying substitution:
| First term | Second term | Unifying substitution | Resulting instance |
|---|---|---|---|
| a | a | {} | a |
| X | a | {X/a} | a |
| X | Y | {X/Z,Y/Z} | Z |
| X | f(a) | {X/f(a) | f(a) |
| f(X) | f(a) | {X/a} | f(a) |
| f(X) | f(f(a)) | {X/f(a)} | f(f(a)) |
| g(X,f(b)) | g(f(a),Y) | {X/f(a),Y/f(b)} | g(f(a),f(b)) |
Obviously, some terms cannot be unified. For example two different constants (a,b), or two terms having different functional symbol or numeber of arguments (arity) (f(X),g(X,Y)). Also terms such as f(a,b) and f(X,X) cannot be unified.
A more detailed explanation can be found in unification.