Hi Edward, Thanks for your interest in `RandProc`. I'm very interested in continuing this conversation with you, but I think I'd better read the papers you recommend, below first, so that I can do so intelligently. ;-) In the mean time, I do have these rather imprecise thoughts: (Please, see in-line below.) Looking forward to much more conversation with you (and others), -db On Jul 3, 2011, at 9:35 AM, Edward Kmett wrote:

On Sun, Jul 3, 2011 at 11:05 AM, David Banas wrote: v0.4 of `RandProc` has just been posted to Hackage: http://hackage.haskell.org/package/randproc

[NB: I transfered this discussion from haskell to haskell-cafe, and started another thread]

I have been spending some time exploring constructive probability theory in Haskell, and I have a couple of observations about working with random processes in a constructive setting:

Necessarily because you are working in Haskell, a constructive setting, your σ-algebras can't be actual σ-algebras! =/ Yes, I realize I've taken some rather arrogant liberty in calling my function `checkSigma`, for instance.

Notably, they aren't closed under countable union/intersection/complement, but merely finite union/intersection/complement, and Gray and Davisson's horrified objections from the bottom of page 39 on Random Processes applies:

If a class of sets is only a field rather than a σ-field, that is, if it satisfies only (3.1) and (3.2), then there is no guarantee that the class will contain all limits of sets. Hence, for example knowing that a class of sets contains all half-open intervals of the form (a,b] for a and b finite does not ensure that it will also contain points or singleton sets! In fact, it is straightforward to show that the collection of all such half-open intervals together with the complements of such sets and all finite unions of the intervals and complements forms a field. The singleton sets, however, are not in the field. (See exercise 3.4)

Thus if we tried to construct a probability theory based on only a field, we might have probabilites defined for events such as (a,b) meaning "the output voltage of a measurement is between a and b" yet not have probabilities defined for a singleton set {a} meaning "the output voltage is exactly a." By requiring that the event space be a σ-field instead of only a field, we are assured that all such limits are indeed events.

So, my hope was that, by providing for a `Point` sample, in addition to `Range`, I'd gotten around this issue, although I confess that I really haven't thought it through.

This limitation, while from some perspective annoying is intrinsic to tackling the problem intuitionistically. Practically, this means you need to be careful when rederiving most of the later results, because you are limited to what you can prove in a constructive measure theory.

In particular the approaches of YK Chan, Brian Weatherson, and Glenn Shafer to intuitionistic probability theory are probably appropriate reading. I will read these. Thanks for the references!

Personally, I don't think this is all that bad, we get some nice properties by being in a constructive setting. Weatherson noted that your measure becomes additive without problems from Dutch book arguments in an intuitionistic setting, because P(A v not A) is not necessarily 1!

I'm enforcing this condition in my `checkProbMeas` function; should I relax this?

You may recall that recall that additivity would imply that P(A v B) = P(A) + P(B), given that A and B are disjoint, but that it tends to fall apart in classical probability theory.

I've been assuming the above true, in general. I didn't realize that it was "fragile". Could you point me to a reference on this, please?

Intuitionistically, however, this is fine. That is to say that if you placed bets that payed out with market rate interest at a rational booking agent on both whether P = NP and P /= NP, it isn't just as good as having placed a bet on truth, because intuitionistically it is possible that neither of those bets may ever pay out, but in a classical setting P (P = NP v P /= NP) = P(True) = 1, so we lose additivity to gain the excluded middle.

I'm sorry, but I'm lost here. Is there a simple example, which illustrates this?

The cost of additivity is giving up or refining a lot of results from that text that talk about the limit of a random process. That and that the "σ-fields" in question are mere fields. ;)

So, as I was writing this module and realizing that I wasn't really testing sigma fields, but only fields, I asked myself, "How might Haskell be used to prove, in a finite amount of time, some property of a countably infinite set of samples?" Obviously, it can't be done in the straight forward fashion, but is there some way to specify properties of the countably infinite set, as opposed to the actual set itself, which might make this possible? Perhaps, a cool application for a DSL? (Sorry, I realize that's really vague.)

I am interested in exploring the consequences of this further.

Me, too. So glad you responded!

-Edward