一句话：以自足构造性方式重证简单类型λ演算中类型可归约层级定理：≤_{βη} 的序型为 ω+4，并细化出 ω+5 与 8 的层级。
论文研究简单类型 λ 演算中类型间由 λ 可定义单射诱导的可归约关系 ≤_{βη}：若存在从类型 A 的闭项到类型 B 的闭项的 λ 可定义单射，则 A ≤_{βη} B。Statman 曾证明该关系是序型为 ω+4 的良序。本文以自足、语法化、构造性且简化的方式重述并证明该结果，核心是引入更细的 ≤_h（单射须为 Böhm 变换）和更粗的 ≤_{h+}（有限族 Böhm 变换联合单射）。由此还得到 ≤_h 的序型为 ω+5、≤_{h+} 的序型为 8，并分析 ≤_{h+} 的等价类：五类对应典范项模型，一类为坍缩同类型所有元素的平凡模型，还有一类因许多类型无闭项而不构成模型。
In the Simply Typed $\lambda$-calculus Statman investigates the reducibility relation $\leq_{\beta\eta}$ between types: for $A,B \in \mathbb{T}^0$, types freely generated using $\rightarrow$ and a single ground type $0$, define $A \leq_{\beta\eta} B$ if there exists a $\lambda$-definable injection from the closed terms of type $A$ into those of type $B$. Unexpectedly, the induced partial order is the (linear) well-ordering (of order type) $\omega + 4$. In the proof a finer relation $\leq_{h}$ is used, where the above injection is required to be a B\"ohm transformation, and an (a posteriori) coarser relation $\leq_{h^+}$, requiring a finite family of B\"ohm transformations that is jointly injective. We present this result in a self-contained, syntactic, constructive and simplified manner. En route similar results for $\leq_h$ (order type $\omega + 5$) and $\leq_{h^+}$ (order type $8$) are obtained. Five of the equivalence classes of $\leq_{h^+}$ correspond to canonical term models of Statman, one to the trivial term model collapsing all elements of the same type, and one does not even form a model by the lack of closed terms of many types.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1711-05497,
title = {Statman's Hierarchy Theorem},
author = {Bram Westerbaan and Bas Westerbaan and Rutger Kuyper and Carst Tankink and Remy Viehoff and Henk Barendregt},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:19)2017}
}