This is a talk I gave at the GT Scalp meeting in Lille on November 18th, 2024, based on common work with Xiaodong Jia and with Clément Théron.
Abstract
Is there any trouble with the probabilistic powerdomain monad?
In short, no.
The origin of the trouble seems to be the title of a 1998 paper by A. Jung and R. Tix entitled “the troublesome probabilistic powerdomain”. It seems that this has now come to be interpreted as justifying that one has to look beyond domain theory and dcpos to give semantics to higher-order probabilistic languages—and this interpretation is bogus.
There is simply no problem giving semantics to such languages in terms of plain old dcpo semantics. Even classical theorems such as soundness and adequacy hold, a topic that I will touch only briefly. One issue, though, is that the classical probabilistic powerdomain monad is not known to be commutative. This is easily solved by replacing it by a variant. The simplest one is the monad of minimal valuations, but there are other choices, too.
Although not all continuous valuations are minimal, enough of them are. This allows us to give semantics to a statistical programming language, with not just higher-order and probabilistic features, but also continuous distributions on exact real numbers (and soft conditioning): Lebesgue measure, and in fact any measure on the real numbers, induces a continuous valuation on the domain of exact reals that is in fact a minimal valuation.
I will finish the presentation by giving a proof that there are dcpos on which not all continuous
valuations are minimal; but this is hard to find, and not that simple to prove.
References
This is based on parts of the following papers:
- Jean Goubault-Larrecq, Xiaodong Jia and Clément Théron A Domain-theoretic Approach to Statistical Programming Languages. J. ACM 70(5): 35:1-35:63 (2023).
- 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
The full slides, with all animation steps; the shorter presentation, without them.
