Paper Info
Title
Higher-order beta matching with solutions in long beta-eta normal form
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.
Year
Venue
Keywords
2006
Nord. J. Comput.
unification variable,special case,long beta-eta normal form,higher-order beta,simply-typed lambda-terms,restricted form,beta equivalence,long-standing open problem,matching equation,higher-order matching,normal form,higher order
Field
DocType
Volume
Discrete mathematics,Combinatorics,Unification,Decidability,Equivalence (measure theory),Loader,If and only if,Beta (finance),Mathematics,Special case,Undecidable problem
Journal
13
Issue
Citations 
PageRank 
1
3
0.51
References 
Authors
17
1
Name
Order
Citations
PageRank
Kristian Støvring1646.91