作为序列的无穷交类型：对 Klop 问题的新解答
计算机科学中的逻辑
2016-10-21 v1
摘要
我们给出了无穷 lambda 演算中弱规范化项的类型论刻画。为此，我们将 lambda 演算的标准量化（具有非幂等交）类型指派系统适配到我们的无穷演算中。我们的工作为 Klop 的 HHN 问题提供了新的答案，即探寻是否存在一个刻画遗传头规范化（HHN）lambda 项的类型系统。Tatsuta 证明了 HHN 无法被有限类型系统刻画。我们证明，赋予一种称为可逼近性（approximability）的有效性条件的无穷类型系统能够实现这一点。
引用
@article{arxiv.1610.06409,
title = {Infinitary Intersection Types as Sequences: a New Answer to Klop's Question},
author = {Pierre Vial},
journal= {arXiv preprint arXiv:1610.06409},
year = {2016}
}
备注
32 pages