Ideally, a probabilistic programming language should admit a computable semantics. But languages often provide operators that denote uncomputable functions, such as comparison of real numbers. While the use of these uncomputable operators may result in uncomputable programs, a programmer can productively use these operators and still produce a computable program, such as one that compares a real number drawn from a normal distribution with 0.

We propose locale theory, and particularly non-spatial sublocales, as a constructive semantic framework for probabilistic programming. Whereas in measure theory, measurable spaces may not have a smallest probability-1 subspace (for a given probability distribution), some locales have smallest probability-1 sublocales, called random sublocales. Partial functions that almost surely terminate and discontinuous functions that are almost everywhere continuous become terminating and continuous, respectively, when restricted to random sublocales. We present a definition of disintegration and provide an example distribution where in locale theory, a unique continuous disintegration exists using random sublocales, whereas classically the disintegration is discontinuous and is only unique up to null sets.

Authors: Benjamin Sherman, Jared Tramontano, Michael Carbin

Extended Abstract: Constructive probabilistic semantics with non-spatial locales