In case anyone is randomly interested, here are some of the obvious problems
with Barry Jay's formulation for higher-order pattern matching:
1) Including "let" abstraction in the abstract syntax is redundant. Consider,
"let x = y in z" is equivalent to "(at x use z) y", where "x" is in "var(z)". It
seems he may have abandoned this inclusion in more recent work...
2) Only linear patterns are reducible, in order to preserve confluence, even
though the "nonlinear patterns = non-confluence" problem only applies to untyped
calculi. The man should just subsume the typing scheme of the simply-typed
lambda calculus and reap the rewards of both considerably simpler reduction
semantics, and, well... a type discipline. For that matter, even for an untyped
calculus, enforcing an evaluation strategy (e.g. post-order traversal for
reduction of subterms) recovers confluence. Why do we like nonlinear patterns?
Allowing nonlinear patterns (e.g. "at (SUB x x) use 0" is "nonlinear" because
"x" appears twice in the pattern) allows one to do fun things with syntactic
equality, without adding additional constructs to the syntax.
3) Separation of "binding" and "free" variables? Not only does he use this
terminology in a very unintuitive way, but making the distinction at the
syntactic level is in fact unnecessary. Indeed, the distinction is only needed
to placate his bizarre reduction semantics (especially the "match-a" rule).