Equivalently, is there a known denotational semantics for probabilistic higher-order functional programming languages? Specifically, is there a domain model of pure untyped $\lambda$-calculus extended by a symmetric random binary choice operation.
Motivation
Cartesian closed categories provide a semantics to higher-order $\lambda$-calculi. Probabilistic powerdomains provide semantics to stochastic programs. A CCC closed under a probabilistic powerdomain operation would provide a semantics to a stochastic higher-order functional programming language.
Related Work
Tix, Keimel, and Plotkin (2004) [1] give modern constructions of the lower-, upper-, and convex- powerdomain operations, but remark that
It still is an open problem whether there is a cartesian closed category of continuous domains which is closed under the construction of probabilistic powerdomains.
Mislove (2013) [2,3] gives semantics for continuous random variables in a first-order language, but remarks that
Even though the probabilistic power domain leaves the CCC of directed complete posets (dcpos, for short) and Scott-continuous maps invariant, there is no Cartesian closed category of domains – dcpos that satisfy the usual approximation assumption – that is known to be invariant under this construct. The best that is known is that the category of coherent domains is invariant under the probabilistic choice monad [4], but this category is not Cartesian closed.
References
- Regina Tix, Klaus Keimel, and Gordon Plotkin (2004) "Semantic domains for combining probability and non-determinism".
- Michael Mislove (2013) "Anatomy of a domain of continuous random variables I"
- Michael Mislove (2013) "Anatomy of a domain of continuous random variables II"
- Jung, A. and R. Tix (1998) "The troublesome probabilistic powerdomain"