Skip to content

PCF (Plotkin 1977)

PCF is a call-by-name simply-typed λ-calculus equipped with one or two base types (usually natural numbers and Booleans) and a fixed point combinator. In essence, PCF is the simplest lazy, purely functional programming language. (PLS Lab)

The Agda code of a lightweight formalization of the denotational semantics of PCF is available on GitHub.

The following highlighted listings of the code were generated using Agda.

  • Modules: hyperlinked web pages of the formalization

  • Library: hyperlinked web pages of imported standard Agda library modules

  • HTML: the hyperlinked HTML pages generated by Agda

  • PDF: a PDF listing of the formalization

Variants of PCF

PCF and its denotational semantics were orginally defined by Dana Scott in 1969 (Scott 1993) including combinators (S, K) instead of λ-abstraction. Gordon Plotkin subsequently defined a denotational semantics for PCF including λ-abstraction (Plotkin 1977).

Many authors have defined denotational semantics for PCF (PLS Lab). Recently, Tom de Jong has given a definition in Agda (DomainTheory.ScottModelOfPCF) based on the DomainTheory modules from the TypeTopology library. The syntax follows (Scott 1993) by including combinators instead of λ-abstraction.

De Jong's semantics of PCF was extended to PCF with variables and λ-abstraction by Brendan Hart in a final year project supervised by Martín Escardó and De Jong (Hart 2020).1 Hart used De Bruin indices for variables.

The definitions of the denotations of PCF terms given by De Jong and Hart illustrate the notational overhead that arises in Agda when using the DomainTheory modules, compared to the definitions given by Scott and Plotkin.

  1. Both De Jong and Hart deviate slightly from Scott's original semantics of the predecessor function by defining it to return zero when applied to zero, instead of being undefined. ↩