Hi, My paper "Higher order beta matching is undecidable" is available from http://homepages.ihug.co.nz/~suckfish/match It shows that the solvability of higher order matching problems, up to beta equivalence, is undecidable. Ralph.