The recursion hierarchy for PCF is strict
John Longley

TL;DR
This paper proves that in Plotkin's PCF, restricting fixed point operators to types of bounded levels creates a strict hierarchy, with higher-level fixed points not definable from lower levels, answering a previously open question.
Contribution
It establishes the strictness of the hierarchy of sublanguages of PCF based on type levels, using nested sequential procedures and answering Berger's question.
Findings
Hierarchy of PCF sublanguages is strict.
Fixed point operators at level k cannot be defined from lower levels.
Uses nested sequential procedures to prove the hierarchy's strictness.
Abstract
We consider the sublanguages of Plotkin's PCF obtained by imposing some bound k on the levels of types for which fixed point operators are admitted. We show that these languages form a strict hierarchy, in the sense that a fixed point operator for a type of level k can never be defined (up to observational equivalence) using fixed point operators for lower types. This answers a question posed by Berger. 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
