Is there a Fubini-Tonelli-type theorem for continuous valuations on Dcpo?

This is a talk I gave at Hunan University, Changsha, Hunan, China, on April 14th, 2022, based on common work with Xiaodong Jia.

Abstract

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.