How do we express measurable spaces using type theory?

A measurable space $(X,\mathcal X)$ consists of a set $X$ equipped with a $\sigma$-algebra of subsets $\mathcal X$. I would like to write computer programs involving measurable spaces, but to the best of my knowledge, no language (including Haskell) has the ability to deal with completely unstructured sets. On the other hand, type theory is an alternate foundation for mathematics which is well-grounded computationally.

Given a measurable space $(X,\mathcal X)$, is there an equivalent presentation using Martin-Löf dependent type theory?

With no constraints on the measurable space, the answer is probably no; a counterexample would be appreciated. What if $\mathcal X$ is a countably generated $\sigma$-algebra?

-
Just out curiosity: what kind of computer programs do you have in mind? Something to do with measure (probability) theory, e.g., probabilistic computations over some uncountable domain? – Matteo Mio Jun 18 '13 at 18:36
Haskell can at least model hereditarily finite sets: that's a fairly simple recursive data type (a hereditarily finite set is a finite list of hereditarily finite sets, more or less). – Qiaochu Yuan Jun 18 '13 at 20:15
@Matteo: yes, that's exactly the point. Furthermore, I want to have the flexibility of dealing with arbitrary belief hierarchies. e.g., a space $X$, its space of measures $M(X, \mathbb R)$, the space of measures over that $M( M(X, \mathbb R), \mathbb R)$, etc. – Tom LaGatta Jun 19 '13 at 4:47
@Qiaochu: thank you! I did not know this. So this is a way to model any arbitrary finite set, correct? ncatlab.org/nlab/show/hereditarily+finite+set – Tom LaGatta Jun 19 '13 at 4:51

If you clarify your question, I can modify this answer to be better. (I am sure you won't like my answer. The best answer is this is not practical, except in the simplest of settings. Or you are interested in this from a logical perceptive, in which case you need to learn the background. Or you care about probability, in which case the usual sigma-algebras are not the way to go.)

Question: What do you mean by presentation?

There are many meanings of a presentation of a mathematical object. Almost all mathematical objects can be represented in type theory. So a trivial answer is yes, you can represent measure spaces in type theory. Given a type $X$, you can make a new type $\mathtt{SigmaAlgebra}(X)$ that depends on $X$, and can be understood as the sigma-algebras of $X$. Rather than going into the details, it is important to note that this is all a formalism. If I know nothing about $X$ then I only know the most basic properties about $\mathtt{SigmaAlgebra}(X)$.

Update: Here is a clarification of the last paragraph. Type theory can be used as a foundation of mathematics. This is the foundations used in formal theorem provers including HOL Light, Isabelle, and Coq. The last one is most closely related to Martin-Löf type theory. It is possible to define a type $\mathtt{SigmaAlgebra}(X)$ by taking all elements of $Bool \rightarrow Bool \rightarrow X$ (that is the powerset of the powerset of $X$) that are closed under the axioms of sigma-algebras. It is difficult to explain if you have never seen a formal theorem prover before, so I might suggest you learn one if you are really interested in this.

However, if you are looking to take any measurable space, and encode it as a specific representation (finitely-many bits of the computer memory), then of course it is not possible. There are way too many sigma-algebras to represent each as a finite bitstring in a computer. Not just more than countable, more than continuum many sigma-algebras on the reals for example.

Question: What do you want to do with these sigma-algebras?

You could be talking about formal theorem proving, but I assume you want to compute with these objects. Is this computation for probability or descriptive set theory? The choice of ideal computable representations is very different in each case.

Also, this brings me to my next question?

Question: What do you want to compute?

What are you going to do with these spaces? Did you want to construct the sigma-algebra generated by a collection of sets? Did you want to see if a particular set is in the sigma-algebra? Did you want to see if two sigma-algebras are equal? Did you want to define maps and ask where certain points map to? Did you want to compare elements of a sigma-algebra to see if they are the same?

With out answers to the above, I can't give you much help. But here are two ways to theoretically represent measurable spaces.

Approach 1: Assume $X$ is a complete separable metric space. Then $X$ can be represented by the distances between some dense countable subset (think the rationals in the reals). This is an infinite object, so you need to represent it as a function which on inputs $i,j,k$ gives the distance between the $i$th and $j$th "rational point" up to an error of $2^{-k}$.

Then you can represent each Borel set by its Borel code. Again, you can really only represent the Borel sets that have computable codes, since the code may be infinite. Again this representation is a function which returns Borel codes.

Then you can represent countably generated sigma-algebas that are subsets of the Borel sigma algebra, by taking a computable sequence of Borel sets, and using them as the representation of the sigma algebra.

However, this has many problems. I can't tell if two sigma algebras are the same. I can't tell if two sets are the same, I can't tell if a set is in a sigma-algebra. Hence, there isn't much that can be computed about this object.

Approach 2: (I am being quite sketchy on the details.) Assume there is also a probability measure. Just assume it is the Lebsegue measure on the unit interval. Then you can represent measurable sets (up to a.e. equivalence) by how close the set is to each finite union of rational intervals. The metric of "closeness" used is $d(A,B) = \mu (A \triangle B)$ where $\triangle$ is the symmetric difference.

Now define a sigma-algebra (up to a.e. equivalence) by the operator $f \mapsto \mathbb{E}[f\mid\mathcal{X}]$ which can be viewed as an operator from $L^2$ to $L^2$ for example (this can be made computable). While I don't want to go into the details, this has an advantage that one can ask if a set $A$ is an element of $\mathcal{X}$. While you can't get a perfect answer, you can get an approximation to a number between 0 and 1. Were $0$ is yes, and anything else is no.

If I really needed to compute with sigma-algebras in a probability theory context, I would do something like this.

Update: Here is an update to my answer based on the details that you gave about your project in your comment below. It looks like you would like to consider a space $X$, and then the space $\mathcal{M}_1(X)$ of probability measures on $X$, and then the space $\mathcal{M}_1(\mathcal{M}_1(X))$ and so on.

This is doable from a computational prospective assuming $X$ is a computable metric space and $\mathcal{M}_1(X)$ is the space of Borel probability measures on $X$. Examples of computable metric spaces include $\{0,1\}^\mathbb{N}$ (good for coin flipping), $C([0,1])$ (good for Brownian motion and continuous path processes), the RCCL functions on $[0,1]$ under the Stockenrod metic (good for RCLL processes), $R^\mathbb{N}$ (for real-valued discrete time Markov chains) and much more.

Given a computable metric space $X$, the space $\mathcal{M}_1(X)$ of Borel probability measures is also a computable metric space. The metric is the Levy-Prokohorov metric (which is a bit of a pain to work with). Also, one can represent the measures by their integrals, which are continuous linear operators on the bounded continuous functions. This represents the same topology. A good resource is "Computability of probability measures and Martin-Löf randomness over metric spaces" by Hoyrup and Rojas (you can skip the stuff about randomness for your needs) and "Representing Probability Measures using Probabilistic Processes" by Matthias Schröder and Alex Simpson (mentioned in another answer). The too papers have equivalent approaches.

Indeed, while I don't know if epistemic game theory has been looked at from a computational prospective, I know that related concepts like conditional probability, de Finetti's theorem, and nonparametric Bayesian statistics have been looked at using the theory of computable metric spaces and computable probability measures. Dan Roy's website is a good place to begin.

-
@Jason: thank you so much for the comprehensive answer. I want to be able to compute things in terms of probabilities. Obviously I won't be evaluating a measure on every possible measurable set, but I want to have a guarantee that I can at least measure a wide class of sets. Incidentally, neither approach you propose works in general, since both are rooted in topological measurable spaces. But there are plenty of reasonable spaces which do not admit topologically generated $\sigma$-algebras. e.g., $\{0,1\}^{\mathbb R}$, see this question: mathoverflow.net/questions/87838 – Tom LaGatta Jun 19 '13 at 4:56
Can you expand on this statement? "Given a type X, you can make a new type 𝚂𝚒𝚐𝚖𝚊𝙰𝚕𝚐𝚎𝚋𝚛𝚊(X) that depends on X, and can be understood as the sigma-algebras of X. Rather than going into the details, it is important to note that this is all a formalism. If I know nothing about X then I only know the most basic properties about 𝚂𝚒𝚐𝚖𝚊𝙰𝚕𝚐𝚎𝚋𝚛𝚊(X)." – Tom LaGatta Jun 19 '13 at 4:59
@Tom, while it is true that there are weird sigma-algebras and weird sets, I don't think they have any value in computation. Computation is actually a very topological thing. A computation in some sense has to be continuous. I admit, I still don't know what applications you are looking for. What could you reasonably compute about a sigma-algebra on ${0,1}^\mathbb{R}$? From a computational perspective, ${0,1}^\mathbb{R}$ is much too big, unless I am misunderstanding your applications. – Jason Rute Jun 19 '13 at 6:48
Moreover, I specialize in the computability of probability theory (at the most high level: what is and is not computable). Anything practical in probability seems to be doable on the Borel probability measure on a complete separable metric space. Everything else is just mathematical generalization that has little practical value. – Jason Rute Jun 19 '13 at 6:51
@Tom, I added an update after that paragraph you were interested in more. However, having said this, I really still have no idea what you are trying to do, so I can't give too much help. If you are able to get your project to work, I would be really curious how it goes. (You could contact me personally.) – Jason Rute Jun 19 '13 at 7:17

I am not exactly sure what you are looking for. There is this work in inductively generated sigma-algebras in type theory: http://link.springer.com/article/10.1007%2Fs001530100123

More generally, I would be inclined to an algebraic approach to measure theory.

For instance, using Riesz spaces (of real valued measurable functions modulo zero measure)

http://logicandanalysis.org/index.php/jla/article/view/14/12

or the related pointfree (localic) approach

http://www.cs.bham.ac.uk/~sjv/Riesz.pdf

http://homepages.inf.ed.ac.uk/als/Research/Sources/mrs.pdf

There is also these formalizations in type theory:

https://www.lri.fr/~paulin/ALEA/ (randomized algorithms)

http://www.cs.unibo.it/~sacerdot/PAPERS/jfr.pdf (Lebesgue’s Dominated Convergence Theorem in Matita).