Bram Westerbaan ; Bas Westerbaan ; Rutger Kuyper ; Carst Tankink ; Remy Viehoff et al. - Statman's Hierarchy Theorem

lmcs:4074 - Logical Methods in Computer Science, November 27, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:19)2017
Statman's Hierarchy TheoremArticle

Authors: Bram Westerbaan ; Bas Westerbaan ; Rutger Kuyper ; Carst Tankink ; Remy Viehoff ; Henk Barendregt

    In the Simply Typed λ-calculus Statman investigates the reducibility relation βη between types: for A,BT0, 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.


    Volume: Volume 13, Issue 4
    Published on: November 27, 2017
    Accepted on: November 16, 2017
    Submitted on: November 16, 2017
    Keywords: Computer Science - Logic in Computer Science

    Classifications

    Consultation statistics

    This page has been seen 3412 times.
    This article's PDF has been downloaded 642 times.