PCF (Programming Computable Functions)

Origin. Dana Scott, "A type-theoretical alternative to ISWIM, CUCH, OWHY", written at Oxford in 1969, circulated as a manuscript for twenty-four years, and published in Theoretical Computer Science 121 (1993): a typed logic of computable functions with fixed points, proposed against the untyped calculi its title mocks. Gordon Plotkin, "LCF considered as a programming language" (Theoretical Computer Science 5, 1977, pp. 223–255), took the term language of Scott's logic, named it PCF, gave it an operational semantics, and proved the adequacy and full-abstraction theorems that set the field's agenda; Robin Milner, "Fully abstract models of typed λ-calculi" (Theoretical Computer Science 4, 1977, pp. 1–22), constructed the fully abstract model and left open the problem of describing it without syntax.

Models. The simply typed lambda calculus over ground types of naturals and booleans with a fixed-point combinator Y_σ at every type: the minimal higher-order language with general recursion, and the organism on which denotational semantics runs its experiments. Where System T's recursor keeps every term total and calibrates the calculus to Peano arithmetic, Y_σ makes every partial computable function definable and puts a divergent term at every type. The language matters for the mismatch it exposed: PCF's evaluation is sequential, the Scott model interpreting it is not, and the full abstraction problem — construct, without mentioning syntax, the model that matches observational equivalence exactly — organized domain theory, sequentiality theory and game semantics from 1977 until the game-semantic solutions of 2000 and Loader's undecidability theorem of 2001.

Formalism.

Types: σ ::= ι | o | σ → σ (ι the naturals, o the booleans)

Terms: variables, abstraction λx:σ. t, application, and the constants tt, ff : o 0 : ι, succ, pred : ι → ι, zero? : ι → o cond_σ : o → σ → σ → σ (σ ground) Y_σ : (σ → σ) → σ for every type σ.

Operational semantics: Call-by-name, deterministic. Programs are closed terms of ground type; M ⇓ c means M evaluates to the constant c. Y_σ t ⇝ t (Y_σ t) cond_σ tt t u ⇝ t, cond_σ ff t u ⇝ u

Scott model: ⟦ι⟧ = ℕ_⊥, ⟦o⟧ = 𝔹_⊥, ⟦σ → τ⟧ = the continuous functions, ordered pointwise by ⊑. Y_σ denotes the least-fixed-point operator f ↦ ⊔ₙ fⁿ(⊥). (Domain Theory.)

Adequacy: For programs, ⟦M⟧ = ⟦c⟧ iff M ⇓ c (Plotkin 1977).

Observational equivalence: M ≅ N iff C[M] ⇓ c exactly when C[N] ⇓ c, for every ground program context C[ ]. Milner's context lemma: applicative contexts — the term applied to arguments — suffice.

Full abstraction: A model is fully abstract when ⟦M⟧ = ⟦N⟧ iff M ≅ N. The Scott model is adequate but not fully abstract.

Parallel-or: por : o → o → o with por tt ⊥ = tt, por ⊥ tt = tt, por ff ff = ff. Continuous, hence an element of the model; definable by no PCF term, since every PCF-definable function is sequential. Two terms testing their argument against por's truth table are observationally equivalent yet denotationally distinct — the witness that full abstraction fails.

Restoring the match: PCF + por (equivalently the parallel conditional): the Scott model is fully abstract (Plotkin 1977). Adding also a continuous existential ∃ : (ι → o) → o makes every computable element of the model definable.

Symbols.

Metatheory. Plotkin's 1977 paper proved both halves of the mismatch: the Scott model is adequate — denotation determines evaluation at ground type — and full abstraction fails exactly at parallel-or, so the failure is a definability gap rather than a wrong equation, the model containing parallel functions no sequential program computes. Milner (1977) proved there is, up to isomorphism, exactly one fully abstract order-extensional continuous model and built it from the syntax by a term-model construction, which turned the full abstraction problem into the demand for a syntax-free construction of that one object. The sequentiality line answered partially: the Kahn–Plotkin sequential functions on concrete data structures ("Concrete domains", written 1978, published in Theoretical Computer Science 121, 1993) do not form a cartesian closed category, Berry's stable functions restore closure by weakening the condition, and the Berry–Curien sequential algorithms (Theoretical Computer Science 20, 1982, pp. 265–321) — the first cartesian closed category in semantics whose morphisms are not functions — keep sequentiality itself; their model is fully abstract not for PCF but for SPCF, PCF with control and errors (Cartwright, Curien and Felleisen, 1994). Game semantics answered fully: Abramsky, Jagadeesan and Malacaria ("Full abstraction for PCF", Information and Computation 163, 2000, pp. 409–470), with history-free strategies, and independently Hyland and Ong ("On full abstraction for PCF: I, II, and III", same issue, pp. 285–408), with innocent well-bracketed strategies — and Nickau independently again — built intensional models whose quotients by the intrinsic preorder are fully abstract, work recognized by the 2017 Alonzo Church Award; O'Hearn and Riecke (Information and Computation 120, 1995) reached full abstraction differently, by Kripke logical relations. Loader closed the question of an effective answer: observational equivalence for finitary PCF — the finite fragment over the booleans with divergence — is undecidable ("Finitary PCF is not decidable", Theoretical Computer Science 266, 2001, pp. 341–364), so no fully abstract model of PCF is effectively presentable and the game-semantic quotients are necessarily non-effective.

Applies to. The reference problem of denotational semantics: adequacy and full abstraction for richer languages — state, control, nondeterminism, probability — are posed and measured against the PCF case. Domain theory's central application (Domain Theory). Game semantics' founding problem and first success (Game Semantics). Higher-type computability, where PCF-definability over the partial continuous functionals is a basic notion (Longley and Normann, Higher-Order Computability, 2015). Sequentiality theory, from the Kahn–Plotkin sequential functions to the Berry–Curien sequential algorithms. The contrast class for total calculi: System T is PCF with the fixed points disciplined into a recursor.

Limitations. Loader's theorem bounds the whole enterprise: no effectively presentable fully abstract model of PCF exists, so every syntax-free description either fails full abstraction or fails effectivity, and the equivalence it would decide is undecidable already without numbers or recursion. The language is an idealization — call-by-name, no state, no control, no concurrency — and each added feature reopens full abstraction under different conditions: dropping innocence models state, dropping well-bracketing models control (Game Semantics). PCF is expressively weak in the other direction too: it defines no parallel function, so the Scott model's extra elements are invisible to it, and definability of all computable elements needs both por and ∃. Under propositions-as-types PCF is not a logic: Y_σ inhabits every type, so the Curry–Howard reading that individuates this division is void for it — PCF is a programming language whose types prove nothing.

© 2026 Lingenic LLC