A probabilistic powerdomain of evaluations.

*(English)*Zbl 0716.06003
Logic in computer science, Proc. 4th Annual Symp., Pacific Grove/CA (USA) 1989, 186-195 (1989).

Summary: [For the entire collection see Zbl 0713.00018.]

We give a probabilistic powerdomain construction on the category of inductively complete partial orders; it is the partial order of continuous [0,1]-valued evaluations on the Scott topology. By means of a theory of integration with respect to such evaluations, the power-domain is shown to be a monad, and indeed one gets a model for Moggi’s computational lambda-calculus. One can also solve recursive domain equations involving the powerdomain, and all this gives a meta-language for programming languages with probabilistic features. This is used to give the semantics of a language with a probabilistic parallel construct. We show the construction generalises previous work on partial orders of measures, and indeed restricts to the category of continuous partial orders, where it can be characterised as a free continuous finitary algebra.

We give a probabilistic powerdomain construction on the category of inductively complete partial orders; it is the partial order of continuous [0,1]-valued evaluations on the Scott topology. By means of a theory of integration with respect to such evaluations, the power-domain is shown to be a monad, and indeed one gets a model for Moggi’s computational lambda-calculus. One can also solve recursive domain equations involving the powerdomain, and all this gives a meta-language for programming languages with probabilistic features. This is used to give the semantics of a language with a probabilistic parallel construct. We show the construction generalises previous work on partial orders of measures, and indeed restricts to the category of continuous partial orders, where it can be characterised as a free continuous finitary algebra.

##### MSC:

06B35 | Continuous lattices and posets, applications |

68Q55 | Semantics in the theory of computing |

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

03B40 | Combinatory logic and lambda calculus |