Unification

Unification (=) is Prolog's core operation: it makes two terms identical by binding variables.

6.1 Rules of unification

Two atoms/numbers unify if they're identical.

A variable unifies with any term (and becomes bound to it).

Two compound terms unify if they have the same functor and arity, and all corresponding arguments unify.

Unification is two-way (unlike one-way pattern matching in functional languages).

?- foo = foo.                    % true
?- foo = bar.                    % false
?- X = foo.                      % X = foo
?- point(X, 2) = point(1, Y).    % X = 1, Y = 2
?- f(X, X) = f(a, b).            % false (X can't be both)
?- f(X, g(Y)) = f(h(Z), g(Z)).   % X = h(Z), Y = Z
?- [H|T] = [1, 2, 3].            % H = 1, T = [2, 3]
?- date(D, M, 2026) = date(25, october, Y).   % D = 25, M = october, Y = 2026

6.2 The occurs check

Standard unification skips the occurs check for efficiency. Enable globally: set_prolog_flag(occurs_check, true) (or error).

?- X = f(X).                     % SWI: X = f(X) — creates a cyclic (rational) term
?- unify_with_occurs_check(X, f(X)).   % false — logically correct

6.3 Not-unifiable & identity

?- a \= b.         % true: cannot unify
?- X \= a.         % false (X could be a) — careful with unbound variables!
?- X == Y.         % false: not identical (both unbound, distinct)
?- X = Y, X == Y.  % true

6.4 Unification as computation

% Matching geometric shapes
vertical(line(point(X, _), point(X, _))).
horizontal(line(point(_, Y), point(_, Y))).

?- vertical(line(point(1, 1), point(1, 3))).   % true
?- horizontal(line(point(1, 1), point(2, Y))). % Y = 1