We describe ongoing work investigating a convenient category of predomains and a probabilistic powerdomain construction suitable for statistical probabilistic programming semantics, as used in statistical modelling and machine learning. Our goal is to give adequate semantics to a probabilistic higher-order language with recursive types, and includes types for powers of real numbers and arbitrary measurable functions between them.

Specifically, we provide (1) a cartesian closed category; (2) whose objects are (pre)-domains; and (3) a commutative monad for continu- ous 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.

We 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-product-preserving omega-cpo-valued contra-variant functors; 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. We construct a commutative powerdomain construction by factorising the Lebesgue integral from the space of random elements to the space of countably additive linear integration operators.