Is there any known CCC closed under a probabilistic powerdomain operation?

Question

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

1. Regina Tix, Klaus Keimel, and Gordon Plotkin (2004) "Semantic domains for combining probability and non-determinism".
2. Michael Mislove (2013) "Anatomy of a domain of continuous random variables I"
3. Michael Mislove (2013) "Anatomy of a domain of continuous random variables II"
4. Jung, A. and R. Tix (1998) "The troublesome probabilistic powerdomain"

Answer 1

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.

Answer 2

The comment below is correct, but it's important to understand the meaning of "finite" or "compact" elements of a domain. These are the denotations of objects computable in finite time, so their appearance in a semantic model is not for proof-theoretic convenience - they represent the strong connection between the model and actual computation.

Answer 3

Well, Mislove's quote already contains a positive answer: the category of dcpos is carteisan closed and also closed under the probabilistic powerdomain. It can indeed be used to give a denotational semantics to higher-order probabilistic computation. However, dcpos fail to satisfy the "usual approximation assumptions" that every element can be approximated by "finite" elements in some sense, as is the case for algebraic and continuous cpos. These assumptions help with certain denotational arguments but are not needed to give a semantics per se.