## 2.1 Matching

When working with knowledge base KB4 in the previous chapter, we introduced the term matching. We said, e.g. that Prolog matches `woman(X)` with `woman(mia)`, thereby instantiating the variable `X` to `mia`. We will now have a close look at what matching means.

Recall that there are three types of term:

1. Constants. These can either be atoms (such as `vincent`) or numbers (such as `24`).

2. Variables.

3. Complex terms. These have the form: `functor(term_1,...,term_n)`.

We are now going to define when two terms match. The basic idea is this:

 Two terms match, if they are equal or if they contain variables that can be instantiated in such a way that the resulting terms are equal.

That means that the terms `mia` and `mia` match, because they are the same atom. Similarly, the terms `42` and `42` match, because they are the same number, the terms `X` and `X` match, because they are the same variable, and the terms `woman(mia)` and `woman(mia)` match, because they are the same complex term. The terms `woman(mia)` and `woman(vincent)`, however, do not match, as they are not the same (and neither of them contains a variable that could be instantiated to make them the same).

Now, what about the terms `mia` and `X`? They are not the same. However, the variable `X` can be instantiated to `mia` which makes them equal. So, by the second part of the above definition, `mia` and `X` match. Similarly, the terms `woman(X)` and `woman(mia)` match, because they can be made equal by instantiating `X` to `mia`. How about `loves(vincent,X)` and `loves(X,mia)`? It is impossible to find an instantiation of `X` that makes the two terms equal, and therefore they don't match. Do you see why? Instantiating `X` to `vincent` would give us the terms `loves(vincent,vincent)` and `loves(vincent,mia)`, which are obviously not equal. However, instantiating `X` to mia, would yield the terms `loves(vincent,mia)` and `loves(mia,mia)`, which aren't equal either.

Usually, we are not only interested in the fact that two terms match, but we also want to know in what way the variables have to be instantiated to make them equal. And Prolog gives us this information. In fact, when Prolog matches two terms it performs all the necessary instantiations, so that the terms really are equal afterwards. This functionality together with the fact that we are allowed to build complex terms (that is, recursively structured terms) makes matching a quite powerful mechanism. And as we said in the previous chapter: matching is one of the fundamental ideas in Prolog.

Here's a more precise definition for matching which not only tells us when two terms match, but one which also tells us what we have to do to the variables to make the terms equal.

1. If `term1` and `term2` are constants, then `term1` and `term2` match if and only if they are the same atom, or the same number.

2. If `term1` is a variable and `term2` is any type of term, then `term1` and `term2` match, and `term1` is instantiated to `term2`. Similarly, if `term2` is a variable and `term1` is any type of term, then `term1` and `term2` match, and `term2` is instantiated to `term1`. (So if they are both variables, they're both instantiated to each other, and we say that they share values.)

3. If `term1` and `term2` are complex terms, then they match if and only if:

1. They have the same functor and arity.

2. All their corresponding arguments match

3. and the variable instantiations are compatible. (I.e. it is not possible to instantiate variable `X` to `mia`, when matching one pair of arguments, and to then instantiate `X` to `vincent`, when matching another pair of arguments.)

4. Two terms match if and only if it follows from the previous three clauses that they match.

Note the form of this definition. The first clause tells us when two constants match. The second term clause tells us when two terms, one of which is a variable, match: such terms will always match (variables match with anything). Just as importantly, this clause also tells what instantiations we have to perform to make the two terms the same. Finally, the third clause tells us when two complex terms match.

The fourth clause is also very important: it tells us that the first three clauses completely define when two terms match. If two terms can't be shown to match using Clauses 1-3, then they don't match. For example, `batman` does not match with `daughter(ink)`. Why not? Well, the first term is a constant, the second is a complex term. But none of the first three clauses tell us how to match two such terms, hence (by clause 4) they don't match.

Patrick Blackburn, Johan Bos and Kristina Striegnitz
Version 1.2.5 (20030212)