It is shown that unifiability of terms in the simply typed lambda calculus with β and η rules becomes decidable if there is a bound on the number of bound variables and lambdas in a unifier in η-long β- normal form.
CITATION STYLE
Schmidt-Schauß, M., & Schulz, K. U. (2002). Decidability of bounded higher-order unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2471, pp. 522–537). Springer Verlag. https://doi.org/10.1007/3-540-45793-3_35
Mendeley helps you to discover research relevant for your work.