Computable de Finetti measures

We prove a computable version of the de Finetti 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.

► Computable exchangeable sequences have computable de Finetti measures.
► Exchangeable probabilistic programs can be transformed to not modify non-local state.
► A distribution on [0,1] is computable iff its moments are uniformly computable.