## Unification

### Terms

1. Constants and variables are terms.
2. A compound term consists of a functor characterized by its name and arity, or number of arguments. Each argument is a term. Syntactically a compound term has the form f(t1, ...., tn) where f is the functor's name and t1, ... , tn are its arguments.
Given two terms S and T, they unify if there exists a substitution s such that Ss =Ts, where Ss (resp.) Ts denotes the result of applying s to S (resp. T). The most general unifer of two terms S and T is a substitution m such that
1. Sm = Tm
2. If s is a substitution such that Ss=Ts then there is a substitution t such that s = m.t

The following algorithm produces the mgu if it exists.

### The Unification Algorithm

Input
Two terms T1 and T2 to be unified
Output
s, the mgu of T1 and T2 or failure
Algorithm
Initialize s to be empty
Initialize the stack to contain the equation T1 = T2
and failure to be false

while stack not empty and failure equals false do

pop X = Y from the stack

```    case
X is a variable that does not occur in Y:
substitute Y for X in the stack and in t
add X = Y to t.

Y is a variable that does not occur in X:
substitute X for Y in the stack and in t
add Y = X to t

X and Y are identical constants or variables:
continue

X is f(X1, ..., Xn) and Y is f(Y1, ... , Yn)
for some functor f and n > 1:
push Xi=Yi, i =1, ...n, on the stack
otherwise:
set failure to true.
```
if failure equals true , then output failure
else output t.

Note that this algorithm uses an occurs check so that it will not unify X and f(X).