Abstract
Let PCFk denote the sublanguage of Plotkin’s PCF in which fixed point operators Yσ are admitted only for types σ of level ≤ k. We show that the languages PCFk form a strict hierarchy, in the sense that none of the Yσ for σ of level k + 1 are definable in PCFk up to observational equivalence. This answers a question posed by Berger in 1999. Our proof makes substantial use of the theory of nested sequential procedures (also called PCF B¨ohm trees) as expounded in the recent book of Longley and Normann.
Original language | English |
---|---|
Pages (from-to) | 1-51 |
Number of pages | 51 |
Journal | Logical Methods in Computer Science |
Volume | 14 |
Issue number | 3 |
DOIs | |
Publication status | Published - 21 Aug 2018 |