# 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. – Jason Rute Apr 10 '12 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.) – Jason Rute Apr 10 '12 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. – Jason Rute Apr 10 '12 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. – Ed Dean May 2 '12 at 12:51
• Is your question related to this one? mathoverflow.net/questions/141764/… – Bas Spitters Sep 16 '13 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.