As we have seen, Prolog tries to prove (answer) a query by looking for facts which match that query, or rules whose heads match the query and whose body can be proved. The way prolog matches terms is therefore crucial.
We have already seen how simple expressions such as lectures(alison,Course) can be matched to facts such as lectures(alison, ai) resulting in bindings such as Course=ai. In the above section we saw examples of a slightly more complex match, where terms with complex arguments were matched against each other, so
book(title(Name), author(Author))
matches:
book(title(lord_of_the_rings), author(tolkien))
with bindings:
Name = lord_of_the_rings
Author = tolkien
Prolog matches expressions in a purely structural way, with no evaluation of expressions, so:
?- 1+2 = 3
no
[Note: In prolog ``='' means ``matches with''. You can test matches by typing in queries such as the one above.]
Similarly the following won't match, as the two expressions have different structures:
?- X + 2 = 3 * Y.
no
However, the following match as they have the same structure:
?- X+Y = 1+2.
X = 1
Y = 2
?- 1+Y = X + 3.
X = 1
Y = 3
Note that there can be variables in both sides of a matched expression, as in the second example above.
For non-arithmetic examples, we have:
?- lectures(X, ai) = lectures(alison, Y).
X = alison
Y = ai
?- book(title(X), author(Y)) = book(Z, author(tolkien)).
Z = title(X)
Y = tolkien
(Actually, in prolog you'd get something looking a bit more complex in response to the above query, with maybe Z = title(_0) and X = _0, as prolog creates its own internal variables. This is equivalent to the bindings given above.)
Of course, prolog will normally be doing lots of matches in a row, as it tries to prove different subgoals in a rule. It then needs to use the variable bindings obtained in the matches so far when it does the next match. So we might have:
?- X+Y = 1+5, X=Y.
no
[Note: We can ask several queries in a row, with a comma in between them, just like in the body of a Prolog rule.]
X and Y get instantiated (bound) to 1 and 5 respectively in the first match (X+Y = 1+5), so the second match is effectively 1=5, which fails. However, the following will succeed:
?- X+Y = 1+5, Z = X.
Z = 1
Y = 5
X = 1
?- book(author(X)) = book(author(tolkien)),
famous(X) = famous(tolkien).
X = tolkien
?- X=Y, Y = alison.
X = alison
Y = alison
Note that if two uninstantiated (unbound) variables are matched (and therefore instantiated to each other) then as soon as one becomes instantiated to some term then the other automatically becomes instantiated to that term.
The algorithm for prolog's matching process is based on the unification algorithm proposed for automated theorem proving. Two terms match if you can instantiate variables to values in such a way that, if the variables in both terms were replaced by their instantiations, the two expressions would become identical. More details are available in your favourite prolog text book.