I will describe ongoing work investigating a convenient category of pre-domains and a probabilistic powerdomain construction suitable for statistical probabilistic programming semantics, as used in statistical modelling and machine learning. Specifically, we provide (1) a cartesian closed category; (2) whose objects are (pre)-domains; and (3) a commutative monad for probabilistic choice and Bayesian conditioning. Jones and Plotkin have shown that conditions (2)--(3) hold when one restricts attention to continuous domains, and Jung and Tix have proposed to search for a suitable category of continuous domains possessing all three properties (1)--(3), a question that remains open to date.
I propose an alternative direction, considering spaces with separate, but compatible, measure-theoretic and domain-theoretic structures. On the domain-theoretic side, we require posets with suprema of countably increasing chains (omega-cpos). On the measure-theoretic side, we require a quasi-Borel space (qbs) structure, a recently introduced algebraic structure suitable for modelling higher-order probability theory. There are three equivalent characterisations of this category given by: imposing an order-theoretic separatedness condition on countable-preserving omega-cpo-valued presheaves; internal omega-cpos in the quasi-topos of quasi-Borel spaces; and an essentially algebraic presentation. The category of these omega-qbses validates Fiore and Plotkin's axiomatic domain theory, yielding semantics for recursive types. To conclude, I will describe a commutative powerdomain construction given by factorising the Lebesgue integral from the space of random elements to the space of sigma-linear integration operators.
Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming