A domain-theoretic framework for conditional probability and Bayesian updating in programming
Pietro Di Gianantonio, Abbas Edalat
TL;DR
This work develops a domain-theoretic foundation for probabilistic programming that makes conditional probability computable in the presence of continuous distributions. It introduces PER-based random-variable and valuation monads, extended to arbitrary sample spaces to support score-based Bayesian updating, and replaces classical conditioning with observable disjoint-open-event pairs to recover monotone, computable conditioning. The authors establish a natural bridge between random variables and valuations, prove equivalence between scoring-based and density-based conditioning, and implement a probabilistic functional language (PFL) with both operational and denotational semantics and an adequacy theorem. The framework supports exact real-number computation, integrates continuous distributions with constructive semantics, and offers a principled approach to higher-order probabilistic programming with formally grounded conditioning. This provides a rigorous, computable foundation for building and reasoning about probabilistic languages and inference mechanisms in a domain-theoretic setting.
Abstract
We present a domain-theoretic framework for probabilistic programming that provides a constructive definition of conditional probability and addresses computability challenges previously identified in the literature. We introduce a novel approach based on an observable notion of events that enables computability. We examine two methods for computing conditional probabilities -- one using conditional density functions and another using trace sampling with rejection -- and prove they yield consistent results within our framework. We implement these ideas in a simple probabilistic functional language with primitives for sampling and evaluation, providing both operational and denotational semantics and proving their consistency. Our work provides a rigorous foundation for implementing conditional probability in probabilistic programming languages.