A probabilistic powerdomain of evaluations. (English) Zbl 0716.06003

Jones, C.; Plotkin, G. D.

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.

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

Keywords:

probabilistic powerdomain construction on the category of inductively complete partial orders; partial order of continuous [0,1]-valued evaluations on the Scott topology; monad; model for Moggi’s computational lambda-calculus; recursive domain equations; meta-language for programming languages with probabilistic features; semantics of a language with a probabilistic parallel construct; category of continuous partial orders