Name
Abstract | ||
|---|---|---|
In the Simply Typed A-calculus [Hin97, BDS13] Statman investigates the reducibility relation <=(beta eta)0, between types: for A, B is an element of T-0, types freely generated -> using and a single ground type 0, define A <=(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, see [Sta80a, Sta80b, Sta81, BDS13]. In the proof a finer relation <=(h) is used, where the above injection is required to be a Bohm transformation ([Bar84]), and an (a posteriori) coarser relation <=(h+), requiring a finite family of Bohm 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 w + 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, [BDS13]. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.23638/LMCS-13(4:19)2017 | LOGICAL METHODS IN COMPUTER SCIENCE |
DocType | Volume | Issue |
Journal | 13 | 4 |
ISSN | Citations | PageRank |
1860-5974 | 0 | 0.34 |
References | Authors | |
0 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bram Westerbaan | 1 | 12 | 2.25 |
| Bas Westerbaan | 2 | 11 | 1.22 |
| Rutger Kuyper | 3 | 6 | 3.72 |
| carst tankink | 4 | 28 | 4.65 |
| Remy Viehoff | 5 | 0 | 0.34 |
| Henk Barendregt | 6 | 588 | 92.49 |