Decidability of bounded higher-order unification

作     者：Schmidt-Schauss, M Schulz, KU 

作者机构：JW Goethe Univ Frankfurt Inst Informat Fachbereich Biol & Informat D-60054 Frankfurt Germany Univ Munich CIS D-80538 Munich Germany 

出 版 物：《JOURNAL OF SYMBOLIC COMPUTATION》 (符号计算杂志)

年 卷 期：2005年第40卷第2期

页      面：905-954页

核心收录：

学科分类：08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：higher-order unification decision algorithms simply typed lambda calculus bounded unification problems exponent of periodicity 

摘      要：It is shown that unifiability of terms in the simply typed lambda calculus with beta and eta rules becomes decidable if there is a bound on the number of bound variables and lambdas in a unifier in eta-expanded beta-normal form. (c) 2005 Elsevier Ltd. All rights reserved.