Learn

Unification is Prolog's core operation. The = operator unifies two terms — finds bindings that make them equal.

?- X = 5.
X = 5.

?- foo(X, b) = foo(a, Y).
X = a, Y = b.            %% structural matching

?- [H|T] = [1, 2, 3].
H = 1, T = [2, 3].

Unification is symmetric — order doesn't matter:

?- a = X.    %% same as X = a
X = a.

Two unbound variables unify:

?- X = Y.
X = Y.       %% both bound to the same fresh thing

Now whatever binds X also binds Y.

Pattern matching

first([X|_], X).
last([X], X).
last([_|T], X) :- last(T, X).

The predicate head is a pattern. Calling first([1,2,3], X) unifies [X|_] with [1,2,3] — gives X=1.

Occurs check

Naive unification has a bug:

?- X = f(X).
X = f(f(f(f(...)))).    %% infinite!

Most Prologs SKIP the occurs check by default for speed. Use unify_with_occurs_check/2 for safety, or :- set_prolog_flag(occurs_check, true).

=/2 vs ==/2 vs =:=/2

• X = Y — unify (binds variables)
• X == Y — already-bound equality (no unification)
• X =:= Y — numerical equality (2 + 2 =:= 4)
• X is Y — evaluate Y arithmetically and bind to X

?- 2 + 2 = 4.    %% FALSE — they're different terms!
?- 2 + 2 =:= 4.  %% true — both are 4 numerically
?- X is 2 + 2.   %% X = 4
?- 4 = X.        %% X = 4 — unification

This is one of Prolog's biggest gotchas — = doesn't evaluate arithmetic.

Practical patterns

Decompose terms:

?- point(X, Y) = point(3, 4).
X = 3, Y = 4.

Building structures:

?- T = book('Foundation', 'Asimov', 1951), T = book(_, Author, _).
T = book('Foundation', 'Asimov', 1951),
Author = 'Asimov'.

functor/3 — inspect compound terms:

?- functor(foo(a, b, c), F, N).
F = foo, N = 3.

?- functor(T, foo, 3).
T = foo(_, _, _).        %% builds a fresh structure

Unification is what makes Prolog declarative — you don't say HOW to compute, you say what's true and let unification do the work.