Is there any known CCC closed under a probabilistic powerdomain operation? 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"
The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest.

In the past few years there has been a very active line of research around so-called quantitative denotational semantics of linear logic, based on the idea (originally due to Girard [1]) that higher-order programs may be modeled by power series.  In the probabilistic case, this takes the form of so-called probabilistic coherence spaces (PCS), also introduced by Girard [2] and studied in depth by Danos and Ehrhard [3].  PCS yield models of both typed and untyped probabilistic calculi which are of a very different nature than power domains and other monad-related models.  In particular, PCS give what is thus far the only known fully abstract model of probabilistic PCF [4], which is notoriously difficult and seemingly impossible to achieve with power domains (cf. the work of Jean Goubault-Larrecq).

Apart from Ehrhard, quantitative semantics is now actively developed by Michele Pagani and coauthors, I suggest you look at his web page for additional references.

[1] Jean-Yves Girard, Normal functors, power series and $\lambda$-calculus. Annals of Pure and Applied Logic 37 (2):129-177, 1988.

[2] Jean-Yves Girard, Between logic and quantic: a tract. In Linear logic in computer science, CUP, 2004.

[3] Vincent Danos and Thomas Ehrhard, Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209(6): 966-991, 2011.

[4] Thomas Ehrhard, Michele Pagani and Christine Tasson, Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proceedings of POPL, pp. 309-320, 2014.