PCF.Combinatory.ScottModelOfPCF
Tom de Jong, 31 May 2019
Updated comments on 21 June 2022.
Added examples at the end on 22 December 2022.
The denotational semantics of PCF based on pointed directed complete posets.
The flag --lossy-unification significantly speeds up the
typechecking of the line β¦ S {Ο} {Ο} {Ο} β§β = Sα΅αΆα΅α΅β₯ β¦ Ο β§ β¦ Ο β§ β¦ Ο β§ below.
(https://agda.readthedocs.io/en/latest/language/lossy-unification.html)
We consider the combinatory version of PCF here. This development was extended
to PCF with variables and Ξ»-abstraction by Brendan Hart in a final year project
supervised by MartΓn EscardΓ³ and myself. Notably, Brendan's extension contains
an Agda formalization of soundness and computational adequacy.
Brendan's code, using a previous version of our library, can be found
here: https://github.com/BrendanHart/Investigating-Properties-of-PCF.
The repository also contains Brendan's report describing the project:
https://github.com/BrendanHart/Investigating-Properties-of-PCF/blob/master/InvestigatingPropertiesOfPCFInAgda.pdf.
{-# OPTIONS --safe --without-K --lossy-unification #-}
open import MLTT.Spartan
open import UF.PropTrunc
open import UF.FunExt
open import UF.Subsingletons
module PCF.Combinatory.ScottModelOfPCF
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(pe : propext π€β)
where
open PropositionalTruncation pt
open import Naturals.Properties
open import UF.Base
open import UF.DiscreteAndSeparated
open import PCF.Combinatory.PCF pt
open import DomainTheory.Basics.Dcpo pt fe π€β
open import DomainTheory.Basics.Exponential pt fe π€β
open import DomainTheory.Basics.LeastFixedPoint pt fe π€β
open import DomainTheory.Basics.Pointed pt fe π€β
open import PCF.Combinatory.PCFCombinators pt fe π€β
open IfZeroDenotationalSemantics pe
open import DomainTheory.Lifting.LiftingSet pt fe π€β pe
open import Lifting.Construction π€β renaming (β₯ to πβ₯)
open import Lifting.Miscelanea π€β
open import Lifting.Miscelanea-PropExt-FunExt π€β pe fe
open import Lifting.Monad π€β hiding (ΞΌ)
β¦_β§ : type β DCPOβ₯ {π€β} {π€β}
β¦ ΞΉ β§ = π-DCPOβ₯ β-is-set
β¦ Ο β Ο β§ = β¦ Ο β§ βΉα΅αΆα΅α΅β₯ β¦ Ο β§
β¦_β§β : {Ο : type} (t : PCF Ο) β βͺ β¦ Ο β§ β«
β¦ Zero β§β = Ξ· zero
β¦ Succ β§β = πΜ succ , πΜ-continuous β-is-set β-is-set succ
β¦ Pred β§β = πΜ pred , πΜ-continuous β-is-set β-is-set pred
β¦ ifZero β§β = β¦
ifZeroβ¦
β¦ Fix {Ο} β§β = ΞΌ β¦ Ο β§
β¦ K {Ο} {Ο} β§β = Kα΅αΆα΅α΅β₯ β¦ Ο β§ β¦ Ο β§
β¦ S {Ο} {Ο} {Ο} β§β = Sα΅αΆα΅α΅β₯ β¦ Ο β§ β¦ Ο β§ β¦ Ο β§
β¦ _Β·_ {Ο} {Ο} s t β§β = [ β¦ Ο β§ β» , β¦ Ο β§ β» ]β¨ β¦ s β§β β© β¦ t β§β
Because Agda is a computational system, we can use it to directly compute the
value of terms in the model. We showcase a few examples illustrating this, as
suggested by Andrej Bauer during my viva on 20 December 2022.
private
tβ : PCF ΞΉ
tβ = β 7 β
recall-the-interpretation-of-ΞΉ : βͺ β¦ ΞΉ β§ β« οΌ π β
recall-the-interpretation-of-ΞΉ = refl
β¦tββ§-is-a-triple-representing-a-partial-element : β¦ tβ β§β
οΌ π , (Ξ» _ β 7) , π-is-prop
β¦tββ§-is-a-triple-representing-a-partial-element = refl
compute-the-value-of-β¦tββ§ : value β¦ tβ β§β β οΌ 7
compute-the-value-of-β¦tββ§ = refl
tβ : PCF ΞΉ
tβ = Pred Β· (Pred Β· (Succ Β· β 3 β))
β¦tββ§-is-a-triple-representing-a-partial-element : β¦ tβ β§β
οΌ π , (Ξ» _ β 2) , π-is-prop
β¦tββ§-is-a-triple-representing-a-partial-element = refl
We let Agda compute the witness (indicated by _) that β¦ tβ β§β is total.
compute-the-value-of-β¦tββ§ : value β¦ tβ β§β _ οΌ 2
compute-the-value-of-β¦tββ§ = refl
By computational adequacy (see the comments at the top of this file) and the
computation above, the term tβ reduces to the numeral β 2 β in PCF.
The term tβ encodes the program [Ξ» x . (if (0 == x) then 2 else (pred 5)) 3].
Notice how the extent of the partial element is no longer given by π but, as a
consequence of the constructions in our model, by the product π Γ π.
We let Agda compute the witness (indicated by _) that the type π Γ π is a
proposition.
tβ : PCF ΞΉ
tβ = ifZero Β· β 2 β Β· (Pred Β· β 5 β) Β· β 3 β
β¦tββ§-is-a-triple-representing-a-partial-element : β¦ tβ β§β
οΌ (π Γ π) , (Ξ» _ β 4) , _
β¦tββ§-is-a-triple-representing-a-partial-element = refl
compute-the-value-of-β¦tββ§ : value β¦ tβ β§β _ οΌ 4
compute-the-value-of-β¦tββ§ = refl
Next we show two examples using the S and K combinators. We first construct the
identity function I on an arbitrary type Ο of PCF using the well-known
definition I = S Β· K Β· K.
I : {Ο : type} β PCF (Ο β Ο)
I {Ο} = (S {Ο} {Ο β Ο} {Ο}) Β· K Β· K
tβ : PCF ΞΉ
tβ = I Β· β 7 β
compute-the-value-of-β¦tββ§ : value β¦ tβ β§β _ οΌ 7
compute-the-value-of-β¦tββ§ = refl
tβ
: PCF ΞΉ
tβ
= (I Β· Succ) Β· β 11 β
compute-the-value-of-β¦tβ
β§ : value β¦ tβ
β§β _ οΌ 12
compute-the-value-of-β¦tβ
β§ = refl
Finally, here are two examples that use the Fix combinator. We explain why we
can't quite compute results in these examples.
Note that this has been updated on 3 March 2026 by Tom de Jong. I am grateful to
Cass Alexandru for questions that led to these updates.
tβ : PCF ΞΉ
tβ = Fix Β· (K Β· β 0 β)
Recall that least fixed points are constructed by iterating an endomap and
starting with β₯. In the general case of a π₯-dcpo we need to lift the type of
natural numbers to a copy in π₯, which is why we have the type β' below. Of
course, since we are dealing with π€β-dcpos this lifing is unnecessary here, but
it is a consequence of applying the more general constructions.
open import UF.UniverseEmbedding
β' : π€β Μ
β' = Lift π€β β
_β² : β' β β
_β² = lower
β²_ : β β β'
β²_ = lift π€β
tβ-noteβ : is-defined β¦ tβ β§β
οΌ (β n κ β' , is-defined (iter β¦ ΞΉ β§ (n β²) β¦ K Β· β 0 β β§β))
tβ-noteβ = refl
tβ-noteβ : (n : β') β iter β¦ ΞΉ β§ (succ (n β²)) β¦ K Β· β 0 β β§β οΌ Ξ· 0
tβ-noteβ _ = refl
tβ-is-defined : is-defined β¦ tβ β§β
tβ-is-defined = β£ β² 1 , β β£
The below computation does not work, because extracting the value employs the
fact that we can factor a certain map through the proposition truncation and the
truncation is assumed axiomatically in our development. I would expect it to
work in Cubical Agda though.
compute-the-value-of-β¦tββ§ : value β¦ tβ β§β tβ-is-defined οΌ 0
compute-the-value-of-β¦tββ§ = refl
But it is provable of course:
value-of-β¦tββ§β : value β¦ tβ β§β tβ-is-defined οΌ 0
value-of-β¦tββ§β = οΌ-of-values-from-οΌ (eq β»ΒΉ)
where
eq : Ξ· 0 οΌ β¦ tβ β§β
eq = family-defined-somewhere-sup-οΌ β-is-set _ (β² 1) β
The interpretation of tβ is equal to β₯, because it is the least fixed point of
the identity on β¦ ΞΉ β§, but the issue is that iter is defined by pattern
matching, so while each application iter n is equal to π, we cannot
definitionally replace it by π.
tβ : PCF ΞΉ
tβ = Fix Β· (I {ΞΉ})
tβ-noteβ : is-defined β¦ tβ β§β
οΌ (β n κ β' , is-defined (iter β¦ ΞΉ β§ (n β²) β¦ I β§β))
tβ-noteβ = refl
tβ-noteβ : (n : β) β is-defined (iter β¦ ΞΉ β§ n β¦ I β§β) οΌ π
tβ-noteβ zero = refl
tβ-noteβ (succ n) = tβ-noteβ n
tβ-noteβ : (n : β') β is-defined (iter β¦ ΞΉ β§ (n β²) β¦ I β§β) οΌ π
tβ-noteβ n = tβ-noteβ (n β²)
But the following fails:
tβ-noteβ : (n : β') β is-defined (iter β¦ ΞΉ β§ (n β²) β¦ I β§β) οΌ π
tβ-noteβ n = refl
Therefore we cannot simply compute is-defined β¦ tβ β§β to be (Ξ£ n κ β' , π),
i.e. β' Γ π, which is equivalent to π of course.
β¦tββ§-is-not-defined : Β¬ (is-defined β¦ tβ β§β)
β¦tββ§-is-not-defined = β₯β₯-rec π-is-prop h
where
h : (Ξ£ n κ β' , is-defined (iter β¦ ΞΉ β§ (n β²) β¦ I β§β)) β π
h (n , d) = Idtofun (tβ-noteβ n) d
β¦tββ§-is-β₯ : β¦ tβ β§β οΌ πβ₯
β¦tββ§-is-β₯ = not-defined-β₯-οΌ β¦tββ§-is-not-defined