6 - The Language PCF

Summary

In chapter 4, we have provided semantics for both typed and untyped λ-calculus. In this chapter we extend the approach to typed λ-calculus with fixpoints (λY-calculus), we suggest formal ways of reasoning with fixpoints, and we introduce a core functional language called PCF [Sco93, Plo77]. PCF has served as a basis for a large body of theoretical work in denotational semantics. We prove the adequacy of the interpretation with respect to the operational semantics, and we discuss the full abstraction problem, which has triggered a lot of research, both in syntax and semantics.

In section 6.1, we introduce the notion of cpo-enriched CCC's, which serves to interpret the λY-calculus. In section 6.2, we introduce fixpoint induction and show an application of this reasoning principle. In section 6.3, we introduce the language PCF, define its standard denotational semantics and its operational semantics, and we show a computational adequacy property: the meaning of a closed term of basic type is different from ⊥ if and only if its evaluation terminates. In section 6.4, we address a tighter correspondence between denotational and operational semantics, known as the full abstraction property. In section 6.5, we introduce Vuillemin's sequential functions, which capture first order PCF definability. In section 6.6, we show how a fully abstract model of PCF can be obtained by means of a suitable quotient of an (infinite) term model of PCF.