Skip to content

PCF

PCF/PCF.All.html is the root of a section of this website showing an Agda formalization of the denotational semantics of the PCF language.

PCF/html/PCF.All.html is the root of the orginal HTML pages generated by Agda from (potentially literate) source code in the GitHub repository.

PCF.pdf is a highlighted PDF listing of all the Agda modules.

About PCF

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)

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).

A direct transcription of Plotkin's definition to Agda is available in this repo at PCF.All (see also the generated PDF). The code imports various modules from the [standard Agda library v2.1], and typechecks with Agda v2.6.4.3 using the (blatantly unsafe) workarounds and postulates in the Domains module.

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. ↩