Computable de Finetti measures

TL;DR

This paper develops a computable version of de Finetti's theorem, enabling automatic transformation of exchangeable stochastic processes into non-modifying procedures within probabilistic programming, and establishes a link between computability of distributions and their moments.

Contribution

It introduces a computable de Finetti's theorem and characterizes computable distributions on the unit interval via their moments.

Findings

Exchangeable processes can be transformed into procedures without non-local state.

A distribution on the unit interval is computable iff its moments are uniformly computable.

Theoretical foundations for computable probabilistic programming are strengthened.

Abstract

We prove a computable version of de Finetti's theorem on exchangeable sequences of real random variables. As a consequence, exchangeable stochastic processes expressed in probabilistic functional programming languages can be automatically rewritten as procedures that do not modify non-local state. Along the way, we prove that a distribution on the unit interval is computable if and only if its moments are uniformly computable.