Skorohod’s Theorem is a fundamental result from stochastic process theory. It makes two assertions:
- Any Borel probability measure on a Polish space can be realized as for some random variable , where denotes Lebesgue measure and is the “law of ,” the push forward of under .
- Moreover, if is a weakly convergent sequence of probability measures on , then the associated random variables converge almost surely wrt .
Recently, the author devised a domain-theoretic proof of Skorohod’s Theorem. Since domain theory is a mainstay of denotational semantics, and since Probabilistic Programming concerns modeling probability measures and stochastic processes, it’s reasonable to look for connections between the domain-theoretic proof of Skorohod’s Theorem and the semantics of Probabilistic Programming languages. But there is a difference in how computability is realized in the domain-theoretic approach used to prove Skorohod’s Theorem, versus the standard approach to computable metric spaces and their probability measures:
- The domain-theoretic model used in the proof of Skorohod’s Theorem is built from topological subsets of the Polish space . For example, in the case of locally compact spaces, the domain is the family of compact subsets ordered by reverse inclusion. Computability is “implicit” in the domain model, but can be instantiated by an enumeration of a countable basis of the domain, i.e., of a countable neighborhood basis of that forms a basis for the domain model.
- In the standard approach, a computable metric space consists of a Polish space , a countable subset , with the assumption that is computable. The computable structure is then lifted to via simple measures with rational coefficients that are concentrated on finite subsets of .
This difference can be seen in how computable simple measures are represented. In contrast to the standard approach to computable metric spaces where computable simple measures are concentrated on finite subsets of , in the domain-theroetic model, each point mass arising in a computable simple measure has for its mass a subset of the Polish space. Devising an application of the domain-theoretic proof of Skorohod’s Theorem to Probabilistic Programming first requires an understanding of how the computable structure on and one on the domain model built from appropriate topological susbsets of are related.