Unification is Prolog's approach to matching terms. It is more powerful than Haskell style pattern matching.

• Variables may appear more than once.
• Terms may have variables inside them.

For example, we can unify foo(3, [X, Y | T]) with foo(Z, [1, 2, 3, 4]) using a goal involving the = operator.

?- foo(3, [X, Y | T]) = foo(Z, [1, 2, 3, 4]).
X = 1,
Y = 2,
T = [3, 4],
Z = 3.

Let \(\mbox{unify}(T_1, T_2)\) be the conditions under which two terms unify.

• If \(T_1\) and \(T_2\) are constants, they unify if they are the same value, otherwise unification fails.
• If \(T_1\) is a variable then unification success with \(T_1\) being instantiated to \(T_2\).
• If \(T_2\) is a variable then unification success with \(T_2\) being instantiated to \(T_1\).
• Otherwise, \(T_1\) and \(T_2\) are complex terms.
  • Let \(T_1 = N_1(A_1, A_2, \ldots, A_n)\) where \(N_1\) is the name (functor) and \(A_1, A_2, \ldots, A_n)\) are the arguments.
  • Let \(T_2 = N_1(B_1, B_2, \ldots, B_m)\) where \(N_1\) is the name (functor) and \(B_1, B_2, \ldots, B_m)\) are the arguments.
  • The two terms unify if:
    • The names \(N_1\) and \(N_2\) are the same,
    • The arity (number of arguments) is the same (\(m=n)\), and
    • Corresponding argument terms unify: \(\mbox{unify}(A_i, B_i)\)

Functor/Arity Notation

Prolog uses a notation such as name/arity to refer to a term with given name and number of arguments. Names may be reused with different numbers of arguments.