A domain-theoretic framework for conditional probability and Bayesian updating in programming

TL;DR

This paper develops a domain-theoretic framework for probabilistic programming that rigorously defines conditional probability and ensures computability, supporting practical implementation in probabilistic languages.

Contribution

It introduces a novel observable event-based approach to define conditional probability and demonstrates its computability within a new domain-theoretic framework.

Findings

Two methods for computing conditional probability are shown to be consistent.

The framework supports implementation in a probabilistic functional language.

Operational and denotational semantics are proven to be consistent.

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.