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.

Comments