## Probabilistic Non-Determinism

**Claire Jones**
*Abstract:* Much of theoretical computer science is based
on use of inductive complete partially ordered sets (or ipos). The
aim of this thesis is to extend this successful theory to make it
applicable to probabilistic computations. The method is to
construct a ``probabilistic powerdomain'' on any ipo to represent
the outcome of a probabilistic program which has outputs in the
original ipo. In this thesis it is shown that evaluations
(functions which assign a probability to open sets with various
conditions) form such a powerdomain. Further, the powerdomain is a
monadic functor on the categoy `Ipo`.

For restricted classes of ipos a powerdomain of probability
distributions, or measures which only take values less than one,
has been constructed (by Saheb-Djahromi). In the thesis we show
that this powerdomain may be constructed for continuous ipos where
it is isomorphic to that of evaluations.

The powerdomain of evaluations is shown to have a simple Stone
type duality between it and sets of upper continuous functions.
This is then used to give a Hoare style logic for an imperative
probabilistic language, which is the dual of the probabilistic
semantics.

Finally the powerdomain is used to give a denotational semantics
of a probabilistic metalanguage which is an extension of Moggi's
lambda-c-calculus for the powerdomain monad. This semantics is then
shown to be equivalent to an operational semantics.

**Ph.D Thesis - Price £8.00**

*LFCS report ECS-LFCS-90-105 (also published as
CST-63-90)*

This is a 197-page PhD thesis which is available as a gzipped PostScript file (309Kb) or
uncompressed PostScript file
(1Mb).

Previous |

Index |

Next