### Entry #192

**Listening to:**
- Bax, symphony no. 3.

**Higher order matching, part II**. (

Part I.) Before even
discussing the algorithm, we have to decide on what it means to do
matching of function symbols. Consider the pattern

*X(a,b)*
and the term

*f(b,a)*. If all we allowed was the possibility
of instantiating

*X* with

*f* (or some other symbol),
then there wouldn't be a match here. But this is dull. In fact, it's
really just first order matching all over again. We could translate
every term of the form

*f(x*_{1},...x_{n})
(where any of the

*f* and the

*x*_{i} arguments
might be variables that could be instantiated) into

*app(f,x*_{1},...x_{n}). The

*app* would be a
``constant''; i.e., not instantiable, and the problem would be
entirely first-order.

Consider again our pattern *X(a,b)*, and the term
*f(b,a)*. Really, we'd like to be able to instantiate
*X* to the function that takes a pair of arguments, flips them,
and then passes the result onto *f*. In other words, let's
imagine that there's a function out there called *g*, and that
*g(x,y) = f(y,x)*, for all possible arguments *x* and
*y*. Then, instantiating *X* with *g* would do
the trick.

Notice how I did two things in the previous paragraph. First, I
came up with a description of what I wanted my function to do, and
then I invented a name for it (*g*). Now, this second step is
un-necessary if we use *lambda calculus* notation for writing
down functions. So, next time, I will talk about just that.

Comments