# effective/constructive/algorithmic probability theory

What sort of "alternative" probability theories are out there in which the methods of proof are inherently constructive?

I know of a number of theorems that say that if you take an infinite sequence of i.i.d. random variables of thus-and-such a kind (let's say that they're fair bits, for definiteness), and use them in a specified fashion to generate a sequence of combinatorial objects of a particular sort, and rescale those combinatorial objects in a time-dependent fashion, then the rescaled objects converge to some sort of limit object with probability 1. However, the proofs that I know are ineffective, in the sense that the proofs don't give you a way to construct any particular infinite sequence of bits such that, if you use them as described above, the convergence occurs.

Well, sort of. In each case of this situation occurring, there's a way to "cheat" by using the theorem itself to guide the choice of bits; you can just choose your bits to have the behavior that you're trying to prove. Is there some principled way to rule out such "cheating"? When it comes to cheating, I believe that "I know it when I see it", but I don't know how to formulate a precise definition of cheating that captures my intuitions.

A web search turned up a talk on "Applications of Effective Probability Theory to Martin-Lof Randomness" (http://www.loria.fr/~hoyrup/icalp_slides.pdf), which is one example of the kind of theory I mean. Are there others?

• It might be helpful to add a lo.logic tag, since I think this is where much of this work is being done in. Apr 10, 2012 at 18:22
• There are a lot of similar efforts in this regard: algorithmic randomness, computable analysis, constructive math, and reverse mathematics. As Ed Dean pointed out, the theory of computation for analytic objects is fairly well-understood. What is left is to work out the details for each theorem. For example, if a theorem asserts the existence of an object, when is it computable? Is there a specific application/theorem you had in mind? (I work in these fields and I am very interested in what the computational concerns are of analysts, probabilists, and ergodic-theorists.) Apr 10, 2012 at 18:53
• I forgot to add proof mining to the above list. It is an application of proof theory which can be used to extract numerical bounded from (apparently) noneffective proofs. Apr 10, 2012 at 18:56
• @James: I took the liberty of adding the lo.logic tag as Jason suggested, since that might get you some feedback beyond my somewhat deflationary answer. May 2, 2012 at 12:51
• Is your question related to this one? mathoverflow.net/questions/141764/… Sep 16, 2013 at 10:03

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.