On Typability for Rank-2 Intersection Types with Polymorphic Recursion
On Typability for Rank-2 Intersection Types with Polymorphic Recursion
复制标题
具有多态递归的 2 阶交集类型的可打字性
DOI：
10.1109/lics.2006.41
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. Aiken
中科院分区：
文献类型：
--
作者：
Tachio Terauchi;A. Aiken
我们证明了 2 阶交集类型的自然形式的多态递归类型的可打字性是不可判定的。我们的证明涉及将可打字性描述为上下文无关语言（CFL）图问题，这可能是独立的兴趣，以及图灵机有界问题的简化。我们还展示了类型系统的一个属性，它与不可判定性结果结合起来，反驳了对 Milner-Mycroft 类型系统的误解。我们还展示了相关程序分析问题的不可判定性
We show that typability for a natural form of polymorphic recursive typing for rank-2 intersection types is undecidable. Our proof involves characterizing typability as a context free language (CFL) graph problem, which may be of independent interest, and reduction from the boundedness problem for Turing machines. We also show a property of the type system which, in conjunction with the undecidability result, disproves a misconception about the Milner-Mycroft type system. We also show undecidability of a related program analysis problem