The recursion hierarchy for PCF is strict

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Pages (from-to)1-51
Number of pages51
JournalLogical Methods in Computer Science
Volume14
Issue number3
DOIs
Publication statusPublished - 21 Aug 2018

Fingerprint

Dive into the research topics of 'The recursion hierarchy for PCF is strict'. Together they form a unique fingerprint.

Cite this