斯特曼的层次定理
摘要：类型化的简单形式的$\lambda$-演算中，Statman研究了类型之间的可规约关系$leq_{\eta\eta}$：对于$A，B \in \mathbb{T}^0$，自由生成的类型使用$ \rightarrow $和单个底类型$ 0 $，如果存在类型$A$的闭项到类型$B$的闭项之间的可λ定义的嵌入，则定义$A leq_{\eta\eta} B$。出乎意料的是，导致的偏序是（线性的）良序（顺序类型）$\omega + 4$。在证明中，使用了一个更细的关系$leq_h$，其中上述嵌入需要是B"ohm变换，并且还使用了一个（事后）较粗的关系$leq_{h^+}$，需要一个有限的B"ohm变换家族，这些变换是联合可逆的。我们以自包含的、句法的、具体化的和简化的方式呈现这一结果。同时还得到了关于$leq_h$（顺序类型$\omega + 5$）和$leq_{h^+}$（顺序类型$8$）的类似结果。$leq_{h^+}$的五个等价类与Statman的规范项模型对应，一个等价类对应于将同类型元素都折叠成一个的平凡项模型，而一个等价类由于缺乏许多类型的闭项而无法形成模型。
作者：Bram Westerbaan, Bas Westerbaan, Rutger Kuyper, Carst Tankink, Remy Viehoff, Henk Barendregt
论文ID：1711.05497
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22