Type checking and typability in domain-free lambda calculi
Type checking and typability in domain-free lambda calculi
复制标题
无域 lambda 演算中的类型检查和可打字性
DOI：
10.1016/j.tcs.2011.06.020
复制
发表时间：
2011
影响因子：
1.1
通讯作者：
H.Nakano
中科院分区：
文献类型：
--
作者：
K.Nakazawa;M.Tatsuta;Y.Kameyama;H.Nakano
本文证明了（1）具有否定、乘积和存在类型的无域lambda演算中类型检查的不可判定性和可类型化问题，（2）无域多态lambda演算中可类型化问题的不可判定性，（3）具有函数和存在类型的无域lambda演算中类型检查的不可判定性和可类型化问题.第一个和第三个结果证明了第二个结果和CPS翻译，减少这些问题在域自由的多态lambda演算的存在类型的域自由lambda演算。关键思想是具有存在类型的无域lambda演算在翻译图像上的保守性。
This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic lambda calculus, and (3) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with function and existential types. The first and the third results are proved by the second result and CPS translations that reduce those problems in the domain-free polymorphic lambda calculus to those in the domain-free lambda calculi with existential types. The key idea is the conservativity of the domain-free lambda calculi with existential types over the images of the translations.