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.