An Application of Computable Distributions to the Semantics of Probabilistic Programs

TL;DR

This paper investigates how Type-2 computable distributions can provide a rigorous semantic foundation for probabilistic programming languages with continuous distributions, linking computability, semantics, and implementation.

Contribution

It introduces a framework encoding computable distributions in Haskell and models probabilistic languages using topological domains, connecting computability with practical implementation.

Findings

Encoding of computable distributions in Haskell

Modeling probabilistic semantics with topological domains

Implications for implementing conditioning in probabilistic programs

Abstract

In this chapter, we explore how (Type-2) computable distributions can be used to give both (algorithmic) sampling and distributional semantics to probabilistic programs with continuous distributions. Towards this end, we sketch an encoding of computable distributions in a fragment of Haskell and show how topological domains can be used to model the resulting PCF-like language. We also examine the implications that a (Type-2) computable semantics has for implementing conditioning. We hope to draw out the connection between an approach based on (Type-2) computability and ordinary programming throughout the chapter as well as highlight the relation with constructive mathematics (via realizability).