Skip to main content
MathOverflow

Return to Question

replaced http://stackoverflow.com/ with https://stackoverflow.com/
Source Link
Community Bot
Community Bot
  • 1
  • 2
  • 3

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 Haskellincluding 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?

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?

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?

edited tags
Link
Asaf Karagila ♦
Asaf Karagila ♦
  • 39.7k
  • 8
  • 134
  • 282
Source Link
Tom LaGatta
Tom LaGatta
  • 8.5k
  • 1
  • 43
  • 82

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?