10.23638/LMCS-13(4:19)2017
https://lmcs.episciences.org/4074
Westerbaan, Bram
Bram
Westerbaan
Westerbaan, Bas
Bas
Westerbaan
Kuyper, Rutger
Rutger
Kuyper
Tankink, Carst
Carst
Tankink
Viehoff, Remy
Remy
Viehoff
Barendregt, Henk
Henk
Barendregt
Statman's Hierarchy Theorem
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.
episciences.org
Computer Science - Logic in Computer Science
arXiv.org - Non-exclusive license to distribute
2017-11-27
2017-11-27
2017-11-27
eng
journal article
arXiv:1711.05497
10.48550/arXiv.1711.05497
1860-5974
https://lmcs.episciences.org/4074/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 13, Issue 4
Researchers
Students