episciences.org_4074_1635002486
1635002486
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
1860-5974
11
27
2017
Volume 13, Issue 4
Statman's Hierarchy Theorem
Bram
Westerbaan
Bas
Westerbaan
Rutger
Kuyper
Carst
Tankink
Remy
Viehoff
Henk
Barendregt
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.
11
27
2017
4074
arXiv:1711.05497
10.23638/LMCS-13(4:19)2017
https://lmcs.episciences.org/4074