交集类型的三阶存在性再探（扩展版）
计算机科学中的逻辑
2017-08-22 v2 计算复杂性
摘要
我们重新审视三阶交集类型存在性（Urzyczyn 2009）的不可判定性结果，追求两个目标。首先，我们强化了先前结果，证明对于秩3和阶3的类型，交集类型存在性是不可判定的，即在证明搜索期间无需引入新的函数依赖（新指令）。其次，我们明确了直接模拟图灵机计算所需的原则，而先前的构造使用了高度并行且非确定的计算模型。由于我们的构造比现有不走弯路的方法更简洁，我们认为它对于更好地理解交集类型存在性的表达能力是有价值的。
引用
@article{arxiv.1705.06070,
title = {Rank 3 Inhabitation of Intersection Types Revisited (Extended Version)},
author = {Andrej Dudenhefner and Jakob Rehof},
journal= {arXiv preprint arXiv:1705.06070},
year = {2017}
}