Statman's Hierarchy Theorem
share
In the Simply Typed λ-calculus Statman investigates the reducibility relation ≤_βη between types: for A,B ∈T^0, types freely generated using → and a single ground type 0, define A ≤_βη B if there exists a λ-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) ω + 4. In the proof a finer relation ≤_h is used, where the above injection is required to be a Böhm transformation, and an (a posteriori) coarser relation ≤_h^+, requiring a finite family of Böhm transformations that is jointly injective. We present this result in a self-contained, syntactic, constructive and simplified manner. En route similar results for ≤_h (order type ω + 5) and ≤_h^+ (order type 8) are obtained. Five of the equivalence classes of ≤_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.
READ FULL TEXT