A Cartesian Closed Category for Random Variables
Pietro Di Gianantonio, Abbas Edalat
TL;DR
This work delivers a Cartesian closed category of domains enriched with random variables to provide a semantic foundation for probabilistic programming. By representing random variables on a standard sample space $A$ (either $2^{\mathbb{N}}$ or $[0,1]$) and mapping them to the probabilistic power domain $P(D)$ via $T(r)=\nu\circ r^{-1}$, it constructs a strong, commutative monad of random variables that supports higher-order probabilistic semantics. The framework yields domain-theoretic integration, a domain-theoretic Fubini theorem, and computability results for Bayes' rule, while also delivering a probabilistic functional language (PFL) with both operational and denotational semantics grounded in this monadic structure. Together, these results address longstanding open problems in probabilistic domain theory and provide a rigorous, computable foundation for probabilistic programming within a coherent, higher-order setting.
Abstract
We present a novel, yet rather simple construction within the traditional framework of Scott domains to provide semantics to probabilistic programming, thus obtaining a solution to a long-standing open problem in this area. Unlike current main approaches that employ some probability measures or continuous valuations on non-standard or rather complex structures, we use the Scott domain of random variables from a standard sample space -- the unit interval or the Cantor space -- to any given Scott domain. The map taking any such random variable to its corresponding probability distribution provides an effectively given, Scott continuous surjection onto the probabilistic power domain of the underlying Scott domain, establishing a new basic result in classical domain theory. We obtain a Cartesian closed category by enriching the category of Scott domains to capture the equivalence of random variables on these domains. The construction of the domain of random variables on this enriched category forms a strong commutative monad, which is suitable for defining the semantics of probabilistic programming.