Computable exchangeable sequences have computable de finetti measures

Abstract

We prove a uniformly computable version of de Finetti's theorem on exchangeable sequences of real random variables. In the process, we develop machinery for computably recovering a distribution from its sequence of moments, which suffices to prove the theorem in the case of (almost surely) continuous directing random measures. In the general case, we give a proof inspired by a randomized algorithm which succeeds with probability one. Finally, we show how, as a consequence of the main theorem, exchangeable stochastic processes in probabilistic functional programming languages can be rewritten as procedures that do not use mutation. © 2009 Springer Berlin Heidelberg.