Decidability of bounded higher-order unification

摘要

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 η-expanded β-normal form.