Free constructions of powerdomains

  • Michael G. Main
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 239)


A powerdomain is a CPO together with extra algebraic structure for handling nondeterministic values. In the first powerdomains, the algebraic structure was a continuous binary operation or, which met certain axioms. Plotkin [9] and Smyth [14] showed how such a structure could be added to certain kinds of CPOs in a free or universal manner. This paper extends the work of Plotkin and Smyth by giving free constructions of powerdomains for a more adaptable algebraic structure: semiring modules. Prior to the constructions, three detailed examples are given, showing how the semiring module structure can capture information about nondeterministic behavior. By putting the available information in an algebraic framework, the algebraic properties can supplement the usual order-theoretic properties in program proofs.


Algebraic Structure Total Element Denotational Semantic Deterministic State Commutative Monoid 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. (1).
    S. Abramsky. Experiments, powerdomains and fully abstract models for applicative multiprogramming, in: Foundations of Computation Theory, LNCS 158, (Springer-Verlag, 1983), 1–13.Google Scholar
  2. (2).
    E.W. Dijkstra. A Discipline of Programming, (Prentice-Hall, 1976).Google Scholar
  3. (3).
    M.C.B. Hennessy and G.D. Plotkin. Full abstraction for a simple parallel programming language, in: Mathematical Foundations of Computer Science 79, LNCS 74, (Springer-Verlag, 1979), 108–120.Google Scholar
  4. (4).
    D. Kozen. Semantics of probabilistic programs, Journal of Computer and System Sciences 22 (1981), 328–350.Google Scholar
  5. (5).
    D. Lehmann, A. Pnueli and J. Stavi. Impartiality, justice and fairness: the ethics of concurrent computation, in: Automata, Languages and Programming, 8th Colloquium, LNCS 115, (Springer-Verlag, 1981), 264–277.Google Scholar
  6. (6).
    M.G. Main, Semiring Module Powerdomains, Technical Report Number CU-CS-286-84, Department of Computer Science, University of Colorado at Boulder, Boulder, CO 80309 (1984).Google Scholar
  7. (7).
    R. de Nicola and M.C.B. Hennessy. Testing equivalences for processes, in: Automata, Languages and Programming, 10th Colloquium, LNCS 154, (Springer-Verlag, 1983), 548–560.Google Scholar
  8. (8).
    D. Park. On the semantics of fair parallelism, in: Abstract Software Specifications LNCS 86 (Springer-Verlag, 1980), 504–526.Google Scholar
  9. (9).
    G.D. Plotkin. A powerdomain construction, SIAM J. Computing 5 (1976), 452–487.Google Scholar
  10. (10).
    G.D. Plotkin. Computer Science Postgraduate Course Notes, University of Edinburgh, 1980–81.Google Scholar
  11. (11).
    A. Pnueli. On the extremely fair treatment of probabilistic algorithms, in: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, (1983), 278–290.Google Scholar
  12. (12).
    A. Poigne. Using least fixed points to characterize formal computations of nondeterminate equations, in: Formalizations of Programming Concepts (J. Diaz and I. Ramos, Eds.), LNCS 107, (Springer-Verlag, 1981), 447–459.Google Scholar
  13. (13).
    A. Poigne. On effective computations of nondeterministic schemes, in: 5th International Symposium on Programming, LNCS 137, (Springer-Verlag, 1982), 323–336.Google Scholar
  14. (14).
    M. Smyth. Powerdomains, Journal of Computer and System Sciences 16 (1978), 23–36.Google Scholar
  15. (15).
    G. Winskel. Synchronisation trees, in: Automata, Languages and Programming, 10th Colloquium, LNCS 154, (Springer-Verlag, 1983), 696–711.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1986

Authors and Affiliations

  • Michael G. Main
    • 1
  1. 1.Department of Computer ScienceUniversity of ColoradoBoulderUSA

Personalised recommendations