## 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 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.) – Jason Rute 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. – Jason Rute 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. – Ed Dean May 2 2012 at 12:51

A recent paper that gives the sort of effective result you're after is Freer and Roy's Computable exchangeable sequences have computable de Finetti measures. From their introduction:

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 an (almost surely unique) 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 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.

Like the work of Hoyrup and Rojas that you point to in your question, this paper operates under the type-2 theory of effectivity (TTE) framework for computable analysis (for more on which see e.g. Weihrauch's text Computable Analysis), though unlike Hoyrup and Rojas' work, notions from algorithmic randomness are not employed here.

I know you said you're after a theory for ruling out the "cheating" you describe. Really, there's nothing special about probability theory here, and I think computability theory itself (coming in this setting in the guise of TTE) is already what you want in order to determine when "cheating" is generally necessary. It just boils down to proving, for a given theorem, either (1) you can always compute the conclusion data from the hypothesis data, or (2) there are instances where it cannot be computed.

The Freer and Roy paper is an instance of the former; an instance of the latter can actually be found in a more recent paper of theirs, with Nate Ackerman, on conditional probability. From the abstract: "We ... show that there are computable joint distributions with noncomputable conditional distributions, ruling out the prospect of general inference algorithms, even inefficient ones. Specifically, we construct a pair of computable random variables in the unit interval such that the conditional distribution of the first variable given the second encodes the halting problem."

-