I want to explain higher order matching. But before I can even get onto this, I should first discuss first order matching. Here goes: if I have the term f(X,a), is there any way of instantiating the variable X so as to make the term the same as f(b,a)? Obviously there is; just set X to be b. Similarly, it should be easy to see that there is a match between the pattern term f(X,g(Y)) (where the variables we are allowed to instantiate are X and Y; the convention is that the upper-case letters are variables that can be matched, and that the lower-case letters can’t be instantiated) and the term f(h(a),g(c)). Equally, there is clearly no way to match the pattern f(X) to g(a). There are more interesting ways to fail too. Consider trying to match the pattern f(X,g(X)) against f(a,g(b)). This can’t succeed because we would have to simultaneously instantiate X to a and b.
There’s a pretty easy algorithm for determining whether or not a match exists between a pattern and a term. Basically, the two terms need to be traversed in parallel with an environment being maintained along-side to record what instantiations you’ve made so far. When you come to a variable in the pattern term, you first check to see if that variable has already been instantiated. If so, check if its instantiation is the same as the thing you’re matching against; if not, fail. If the variable hasn’t been instantiated so far, record it as being instantiated with the concrete term you're matching against.
The thing that makes this first order matching is the fact that variables in the pattern term mustn’t take arguments. In other words, f(X(a),Y) is an illegal pattern because of the use of X as a function (taking argument a). Next time I will explain how the shift to the higher order problem is done.