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.
Comments