Unification is pattern matching that works both ways
Why Prolog runs a program backwards, and what it costs.
Most languages match a pattern against a value. Prolog matches a pattern against a
pattern, binding whatever is missing on either side. That symmetry is why append/3
splits a list as happily as it joins one.
The rule
Two terms unify if some substitution makes them identical: a variable unifies with anything and binds to it; two atoms unify only if identical; two compound terms unify if functor, arity and every argument do.
?- foo(X, b) = foo(a, Y).
X = a,
Y = b.Nothing was called. The substitution is the answer.
Why backwards is free
append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).The head is matched by unification, not argument passing, so nothing distinguishes input from output:
?- append(X, Y, [1,2,3]).
X = [], Y = [1, 2, 3] ;
X = [1], Y = [2, 3] ;
X = [1, 2], Y = [3] ;
X = [1, 2, 3], Y = [] .Same clauses, four answers, no extra code.
What it costs
A trail of every binding, so backtracking can undo them. And = skips the occurs
check, so X = f(X) builds a cyclic term and the next write/1 hangs. Use
unify_with_occurs_check/2 when the terms are not obviously finite.