Matching: the four equals signs

One sign that makes things equal

The single = does not compare its sides. It makes them the same by filling in whatever is still free: pair(X, Y) = pair(ada, tea) leaves X as ada and Y as tea, because that is the only way the two structures can match.

That process is called unification. Words and numbers must match exactly, a free variable matches anything, and two structures match only when their names, their sizes and all of their arguments match in turn.

Two free variables can be unified with each other: after X = Y, the two names stand for the same unbound value. Binding either one later binds both, because there is only one value behind the two names. This is how a rule can pass a fresh variable into a structure and fill it in later without knowing what it will become.

The neighbours of the equals sign

Four signs sit near it and they are worth keeping apart. =:= compares two numbers by value, so 3 =:= 3.0 is true. == compares two terms without binding anything at all. \= succeeds when the two sides cannot be matched, and \== succeeds when they are not already the same term.

Only = binds a variable. That is what lets a program ask a careful question — is this person a different one from that person — without disturbing a single fact.

\== and \= look similar and answer different questions. \== asks whether two terms are already different, without binding anything; \= asks whether they cannot be unified. With both sides free, X \== Y succeeds because two fresh variables are not yet the same term, while X \= Y fails because they could still be unified.

Matching from the outside in

When two structures meet, the engine compares their functors and arities first, then walks the arguments left to right. pair(ada, tea) = pair(Person, Drink) therefore binds Person before Drink, and pair(ada, tea) = pair(ada, Drink) leaves the first position alone because the atom already matches.

A variable can be bound only once in a unification. pair(X, X) = pair(ada, tea) fails, because the first argument would make X ada and the second would make it tea; there is no value that is both. That is how a pattern says two positions must hold the same thing. The single equals sign can also test a bound variable: X = ada succeeds or fails, and it never changes a value that is already there.

Unification walks into both terms and keeps going while the functors and arities match. box(point(1, 2), point(5, 6)) against box(point(A, B), point(C, D)) first matches box/2, then the two point/2 arguments, then the four numbers. If any position fails, the whole unification fails and every binding made during the attempt is undone, so you never see a half-filled pattern.

What happens underneath

The engine keeps a table of bindings for the variables it has seen. Unifying a variable with a value adds an entry; unifying two structures walks them and adds entries for the positions that are still free. A variable that is already bound is replaced by its value before the next comparison, which is why a later goal sees the name as the value it stands for.

On backtracking, the entries made since the last choice point are removed together. That is what makes a failed branch leave no trace: the variable that was bound inside it is free again when the engine tries the next alternative. The table is the reason Prolog can search without a separate undo step in your code.

A structure that fills itself in

main :-
    pair(X, Y) = pair(ada, tea),
    write('first '), write(X), nl,
    write('second '), write(Y), nl,
    ( 3 = 3.0 -> write('3 and 3.0 are one term')
              ; write('3 and 3.0 are different terms') ), nl,
    ( 3 =:= 3.0 -> write('but the same number')
                ; write('and different numbers') ), nl.
:- initialization(main).

Try these next

• Ask pair(X, Y) = pair(1, 2) and print both variables.
• Try pair(X, X) = pair(ada, tea) and explain the failure in one sentence.
• Replace =:= with == in the example and note which line changes.