{"docId":4089,"paperId":4074,"url":"https:\/\/lmcs.episciences.org\/4074","doi":"10.23638\/LMCS-13(4:19)2017","journalName":"Logical Methods in Computer Science","issn":"","eissn":"1860-5974","volume":[{"vid":315,"name":"Volume 13, Issue 4"}],"section":[],"repositoryName":"arXiv","repositoryIdentifier":"1711.05497","repositoryVersion":2,"repositoryLink":"https:\/\/arxiv.org\/abs\/1711.05497v2","dateSubmitted":"2017-11-16 12:43:14","dateAccepted":"2017-11-27 09:59:04","datePublished":"2017-11-27 10:00:50","titles":["Statman's Hierarchy Theorem"],"authors":["Westerbaan, Bram","Westerbaan, Bas","Kuyper, Rutger","Tankink, Carst","Viehoff, Remy","Barendregt, Henk"],"abstracts":["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."],"keywords":["Computer Science - Logic in Computer Science"]}