The recursion hierarchy for PCF is strict

Research output: Working paper


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 for each k, there are closed programs of PCFk +1 that are not observationally equivalent to any programs of PCFk. 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öhm trees) as expounded in the forthcoming book of Longley and Normann.
Original languageEnglish
Number of pages48
Publication statusPublished - Jul 2015

Publication series

NameInformatics Research Report
PublisherSchool of Informatics


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

Cite this