Unification
The one mechanism behind pattern matching, assignment and parameter passing.
The = operator does not assign. It asks Prolog to make two terms identical by choosing values for variables. This is unification, and it is how Prolog matches queries against facts and rule heads.
Rules of unification:
- Identical atoms and numbers unify.
- A variable unifies with anything (and becomes that thing).
- Two compound terms unify if they have the same functor and arity, and their arguments unify one by one.
?- X = hello?- hello = hello?- hello = world?- f(X, b) = f(a, Y)?- point(X, Y) = point(1, 2)?- f(a) = g(a)?- f(a, b) = f(a)Once bound, always bound
Within one query a variable keeps its value. If the same variable appears twice, both places must agree:
?- f(X, X) = f(a, b)?- f(X, X) = f(a, Y)?- X = Y, Y = 5?- X = 1, X = 2That last query is why Prolog "variables" are not mutable boxes: you can't re-assign X. You can only learn more about it.
Matching inside structures
Unification looks inside terms, so you can pull things apart:
?- person(name(Given, Family), age(A)) = person(name(ada, lovelace), age(36))?- [First | Rest] = [1, 2, 3]The [First | Rest] pattern splits a list into its head and tail, you'll use it constantly.
Three kinds of "equal"
| goal | meaning |
|---|---|
A = B | try to unify A and B (may bind variables) |
A \= B | succeed if A and B cannot unify |
A == B | succeed if A and B are already identical (no binding) |
?- X == Y?- X = Y?- a \= b?- f(X) == f(X)Unification in rule heads
When Prolog calls a predicate it unifies the goal with each clause head. So heads are patterns. This one-line predicate says "two things are the same":
same(X, X).?- same(a, a)?- same(a, b)?- same(f(Y), f(1))Exercise: Swap a pair
Write a single fact swap/2 that swaps the two components of a pair(A, B) term, so that swap(pair(1, 2), X) gives X = pair(2, 1). No body needed, unification does the work.