Title of article
Decidability of bounded higher-order unification
Author/Authors
Manfred Schmidt-Schau?، نويسنده , , Klaus U. Schulz، نويسنده ,
Issue Information
روزنامه با شماره پیاپی سال 2005
Pages
50
From page
905
To page
954
Abstract
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.
Keywords
Higher-order unification , Decision algorithms , Bounded unificationproblems , Exponent of periodicity , Simply typed lambda calculus
Journal title
Journal of Symbolic Computation
Serial Year
2005
Journal title
Journal of Symbolic Computation
Record number
805864
Link To Document