Unification in Prolog

Analogy categoryAnalogies

Unification is the mechanism Prolog uses to match two terms: two terms unify if there is a substitution of variables that makes them syntactically identical. It replaces assignment as the fundamental operation in Prolog and underlies every fact and rule match performed during query resolution.

🏏

Cricket analogy: Deciding two field placements are 'the same' only if every fielder stands in the identical spot is like Prolog unification -- two terms unify only when every corresponding part lines up exactly, whether directly equal or made equal by binding a variable.

Unifying Atoms, Numbers, and Variables

Identical atoms unify only with themselves, and identical numbers unify only with the same number -- there is no implicit coercion. An unbound variable unifies with anything and becomes bound to that term for the remainder of the current computation branch, and two unbound variables unify by becoming linked to each other.

🏏

Cricket analogy: The atom 'kohli' only unifies with the atom 'kohli', just as a jersey number 18 only matches player records for that exact number -- no two different fixed identities are ever treated as the same in Prolog.

prolog

?- kohli = kohli.
true.

?- kohli = dhoni.
false.

?- X = 42.
X = 42.

?- X = kohli, Y = X.
X = kohli,
Y = kohli.

?- f(X, b) = f(a, Y).
X = a,
Y = b.

Unifying Compound Terms and Lists

Two compound terms unify only if their functor name and arity match; if they do, each corresponding pair of arguments is unified recursively. Lists are just compound terms built from the [Head|Tail] (cons) functor, so list unification is structural unification applied recursively down the list's spine.

🏏

Cricket analogy: Comparing two scorecards structured as match(team1, team2, Score) unifies only when both team names and the functor match, and then the Score arguments are unified in turn -- team, arity, and every argument all have to line up.

The Occurs Check

Standard unification does not verify whether a variable being bound already occurs inside the term it is unifying with, so it can silently build a cyclic (infinite) term. unify_with_occurs_check/2 performs this extra verification and correctly fails when it would create such a self-referential structure, at the cost of extra computation on every call.

🏏

Cricket analogy: Ignoring whether a player is accidentally listed as their own substitute would create a nonsensical self-referencing lineup -- the way unification without an occurs check can bind a variable to a term containing itself, creating a cyclic, infinite structure.

SWI-Prolog's default =/2 does not perform an occurs check, so ?- X = f(X). succeeds and silently creates a cyclic (rational) term rather than failing. If you need mathematically sound unification that rejects such self-referential bindings, use unify_with_occurs_check/2, or set the Prolog flag occurs_check to true or error for stricter behavior -- at the cost of the extra check's performance overhead on every unification.

Unification is Prolog's core matching operation: two terms unify if there is a substitution of variables that makes them identical.
Atoms and numbers unify only with themselves; an unbound variable unifies with anything and becomes bound to it.
Compound terms unify only if their functor and arity match, after which corresponding arguments are unified recursively.
Lists unify structurally via the [Head|Tail] pattern, which is itself just compound term unification under the hood.
Unification is symmetric and can bind variables on either side of the = operator.
Default unification (=/2) does not check for cyclic terms; unify_with_occurs_check/2 does, at extra computational cost.
Unification, not assignment, is what makes Prolog variables behave differently from variables in imperative languages.