Abstract
In the previous chapter, we considered NSPs as abstract algorithms for sequential higher-order computation, and showed that the partial type structures admitting a well-behaved (liberal) interpretation of NSPs are exactly those with least fixed point operators. In the present chapter, we will develop an alternative perspective on essentially the same computability notion that takes least fixed points as primitive— a perspective conveniently embodied by Plotkin’s language PCF as introduced in Subsection 3.2.3. Like Kleene’s S1–S9, PCF offers a syntactic calculus for defining NSPs (and elements of other type structures), but in contrast to S1–S9 it is codingfree and hence cleaner to work with as a ‘programming language’. Indeed, PCF has in practice proved valuable as a basis for the design of functional programming languages such as Standard ML and Haskell.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Longley, J., Normann, D. (2015). PCF and Its Models. In: Higher-Order Computability. Theory and Applications of Computability. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47992-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-47992-6_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47991-9
Online ISBN: 978-3-662-47992-6
eBook Packages: Computer ScienceComputer Science (R0)