Affordable Access

Publisher Website

Semantic Domains for Combining Probability and Non-Determinism

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
222
Identifiers
DOI: 10.1016/j.entcs.2009.01.002
Keywords
  • Semantic Domains
  • Nondeterminism
  • Probabilistic Nondeterminism
  • Directed Complete Partially Ordered Cones
  • Hahn-Banach Theorems
  • Denotational Semantics
Disciplines
  • Linguistics
  • Mathematics

Abstract

Abstract We present domain-theoretic models that support both probabilistic and nondeterministic choice. In [A. McIver and C. Morgan. Partial correctness for probablistic demonic programs. Theoretical Computer Science, 266:513–541, 2001], Morgan and McIver developed an ad hoc semantics for a simple imperative language with both probabilistic and nondeterministic choice operators over a discrete state space, using domain-theoretic tools. We present a model also using domain theory in the sense of D.S. Scott (see e.g. [G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove, and D. S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 2003]), but built over quite general continuous domains instead of discrete state spaces. Our construction combines the well-known domains modelling nondeterminism – the lower, upper and convex powerdomains, with the probabilistic powerdomain of Jones and Plotkin [C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 186–195. IEEE Computer Society Press, 1989] modelling probabilistic choice. The results are variants of the upper, lower and convex powerdomains over the probabilistic powerdomain (see Chapter 4). In order to prove the desired universal equational properties of these combined powerdomains, we develop sandwich and separation theorems of Hahn-Banach type for Scott-continuous linear, sub- and superlinear functionals on continuous directed complete partially ordered cones, endowed with their Scott topologies, in analogy to the corresponding theorems for topological vector spaces in functional analysis (see Chapter 3). In the end, we show that our semantic domains work well for the language used by Morgan and McIver.

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments

More articles like this

Topological Cones: Foundations for a Domain Theore...

on Electronic Notes in Theoretica... Jan 01, 2006

On Combining Probability and Nondeterminism

on Electronic Notes in Theoretica... Jan 01, 2006

A relational semantics for parallelism and non-det...

on Annals of Pure and Applied Log...

Determinism and non-determinism in PDL

on Theoretical Computer Science Jan 01, 1991
More articles like this..