Thursday, 5 July 2001

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(x1,...xn) (where any of the f and the xi arguments might be variables that could be instantiated) into app(f,x1,...xn). 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.