This is a talk I gave at Hunan University, Changsha, Hunan, China, on April 14th, 2022, based on common work with Xiaodong Jia.
Continuous valuations are a close cousin of measures which have had some success in denotational semantics. They enjoy a Fubini-Tonelli-type theorem on Top, the category of topological spaces, and this is fine: this allows us to swap the order of integration, and semantically, this means that we can draw two independent random variables in the order we wish.
However, the denotational semantics of programs operates in the smaller (full) subcategory Dcpo of dcpos, and, perhaps surprisingly, such a Fubini-Tonelli theorem is not known in that context—except on continuous dcpos, but that causes other problems.
There are solutions to this conundrum. Instead considering all continuous valuations, we may consider minimal valuations, or Heckmann’s larger class of point-continuous valuations. Rather to the point, there are Fubini-Tonelli theorems for those restricted classes of continuous valuations, which were discovered pretty recently, and they suffice to give semantics of expressive, higher-order probabilistic programming languages.
This raises the following natural question: are all those notions of valuations on dcpos distinct, or are they all the same? Every minimal valuation is point-continuous, and every point-continuous valuation is continuous. We show that the three notions are distinct, by showing that:
- There is a continuous valuation on the Johnstone dcpo (a famous counterexample in domain theory) which is not minimal, while all of them are point-continuous.
- There is a continuous valuation on the Smyth powerdomain of the Sorgenfrey line (a famous counterexample in topology) which is not point-continuous.
This is based on the following paper:
- Jean Goubault-Larrecq and Xiadong Jia, Separating minimal valuations, point-continuous valuations, and continuous valuations, Mathematical Structures in Computer Science, Volume 31 Issue 6, published online 07 December 2021 (available from https://arxiv.org/abs/2109.00426).
Slides and videos
- Introduction, continuous valuations (8:02)
- Fubini-Tonelli theorems, and the problem at hand (11:48)
- A computer scientist’s perspective (11:45)
- Minimal and point-continuous valuations (11:35)
- Separating minimal from point-continuous valuations (14:51)
- Separating point-continuous from continuous valuations (13:54)
- Conclusion (3:32)