Unification¶

"Love is the supreme unifying principle of life." - Martin Luther King, Jr.

Although Prolog can feel very "declarative", using Prolog effectively requires understanding how Prolog works under the hood. There are two fundamenatal technologies required to execute queries in Prolog; the first is unification.

Unification¶

Unification is the process of giving values to (undefined) variables so that two terms or formulas become literally equal.

For example, if Prolog is working on the goal

pairs(A, walnut).

and it encounters the database fact

pairs(apple, walnut).

then Prolog use the fact to prove the goal by unifying match by setting

A = apple.

Unification is different from variable assignments in languages like Python or Java in two key ways:

First, Prolog variables start out uninitalized, but if they have value we cannot change it.

(Later on we'll see there are cases where "backtracking" resets variables to be uninitialized, which and then we can set a different value for the variable, but the general rule holds: if the variable has a value, we cannot reassign to the variable.)

So if we have already decided that A = apple and later in the same run of the program we try to unify the query
```
pairs(A, ginger).
```
with the database fact
```
pairs(banana, ginger).
```
this second unification will fail! Once we have decided that A = apple there's no difference between pairs(A, ginger) and pairs(apple, ginger), and there's no way for unification to make pairs(apple, ginger) the same as pairs(banana, ginger) since apple and banana are constants, not variables.
More interestingly, unification is bidirectional. The two terms being unified can have variables on either or both sides, and unification will set as many variables as necessary to make the terms equal. For example, if we unify the query
```
pairs(A,walnut).
```
with the database fact
```
pairs(X,X).
```
then Prolog could decide
```
A = X, X = walnut.
```
successfully turning both into pairs(walnut,walnut) (since if A is defined to be the same as X , and X is defined to be walnut, then A is automatically the same as walnut`).

An even more interesting case arises if we unify the query
```
pairs(A,B).
```
with the database fact
```
pairs(X,X).
```
Here Prolog could set
```
A = X, X = B.
```
leaving B uninitalized; turning both into pairs(B,B) is enough to make them the same.

Previous: 4.1 Logic Programming

Next: 4.3 Depth-First Search