Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, April 13, 2009 - 3:30pm

Cameron Freer

MIT

Location

University of Pennsylvania

DRL 4C8

We prove a uniformly computable version of de Finetti's theorem. The classical result states that an exchangeable sequence of real random variables is a mixture of independent and identically distributed (i.i.d.) sequences of random variables. Moreover, there is a measure-valued random variable, called the directing random measure, conditioned on which the random sequence is i.i.d. The distribution of the directing random measure is essentially unique and is called the de Finetti measure. We show that computable exchangeable sequences of real random variables have computable de Finetti measures. In the process, we show that a distribution on [0,1]^\omega is computable if and only if its moments are uniformly computable, 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. We also apply the computable de Finetti theorem to show how exchangeable stochastic processes in probabilistic functional programming languages can be rewritten as procedures that do not use mutation. This is joint work with Daniel Roy.