Computable de Finetti measures

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.

32 pages. Final journal version; expanded somewhat, with minor corrections. To appear in Annals of Pure and Applied Logic. Extended abstract appeared in Proceedings of CiE '09, LNCS 5635, pp. 218-231

References in corpus (3)

• Church: a language for generative models
• Graph limits and exchangeable random graphs
• On exchangeable random variables and the statistics of large graphs and hypergraphs

Cited by in corpus (9)

• Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
• A Convenient Category for Higher-Order Probability Theory
• Computability and analysis: the legacy of Alan Turing
• Probabilistic Computability and Choice
• On the computability of conditional probability
• Representations of measurable sets in computable measure theory
• On the close interaction between algorithmic randomness and constructive/computable measure theory
• Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
• On the computability of graphons