The recursion hierarchy for PCF is strict

John Longley

doi:10.23638/LMCS-14(3:8)2018

John Longley - The recursion hierarchy for PCF is strict

lmcs:1543 - Logical Methods in Computer Science, August 21, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:8)2018

The recursion hierarchy for PCF is strictArticle

Authors: John Longley

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öhm trees) as expounded in the recent book of Longley and Normann.

https://doi.org/10.23638/LMCS-14(3:8)2018

Source: arXiv.org:1607.04611

Volume: Volume 14, Issue 3

Published on: August 21, 2018

Accepted on: June 21, 2018

Submitted on: July 22, 2016

Keywords: Computer Science - Logic in Computer Science,03B70

Licence: Attribution 4.0 International (CC BY 4.0)