|
Higher-Order Beta Matching with Solutions in Long Beta-Eta Normal Form
Kristian Støvring. June 2006 |
Abstract:
Higher-order matching is a special case of unification of
simply-typed lambda-terms: in a matching equation, one of the two sides
contains no unification variables. Loader has recently shown that
higher-order matching up to beta equivalence is undecidable, but decidability
of higher-order matching up to beta-eta equivalence is a long-standing open
problem.
We show that higher-order matching up to beta-eta equivalence is decidable if and only if a restricted form of higher-order matching up to beta equivalence is decidable: the restriction is that solutions must be in long beta-eta normal form Available as PostScript, PDF, DVI. |