Higher-Order matching

http://www.reed.edu/~carlislp/ghc6-doc/users_guide/rewrite-rules.html
より

GHC currently uses a very simple, syntactic, matching algorithm for matching a rule LHS with an expression. It seeks a substitution which makes the LHS and expression syntactically equal modulo alpha conversion. The pattern (rule), but not the expression, is eta-expanded if necessary. (Eta-expanding the epression can lead to laziness bugs.) But not beta conversion (that's called higher-order matching).

ということらしい。とりあえず、右も左も分からんのだけど、Huet-Langのsecond-order matchingというのと、de Moor-Sittampalamによるアルゴリズムというのが有名っぽい。Huetの論文は古いらしいので、Web上では読めないっぽい。de Moore等の論文ってのは多分これ
Higher-order Matching for Program Transformation

自分で思いつくかどうかはともかく、やってること理解するのは難しくないかな。あとまあ、定理証明器書くなら、Higher-Order Unificationとかも必要になるような、ならんような。Higher-Oreder Unificationアルゴリズム最初に考案したのも、Huetらしい。おんなじ人？