Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||Probabilistic Non-Determinism|
|Authors: ||Jones, Claire|
|Supervisor(s): ||Plotkin, Gordon|
|Issue Date: ||Jul-1990|
|Publisher: ||University of Edinburgh. College of Science and Engineering. School of Informatics.|
|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.|
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.