A representable approach to finite nondeterminism

Stuart Anderson, Anthony Power

Research output: Contribution to journalArticlepeer-review

Abstract

We reformulate denotational semantics for nondeterminism, taking a nondeterministic operation V on programs, and sequential composition, as primitive. This gives rise to binary trees. We analyse semantics for both type and program constructors such as products and exponential types, conditionals and recursion, in this setting. In doing so, we define new category-theoretic structures, in particular premonoidal categories. We also account for equivalences of programs such as those induced by associativity, symmetry and idempotence of V, and we study finite approximation by enrichment over the category of ?-cpos with least element. We also show how to recover the classical powerdomains, especially the convex powerdomain, as three instances of a general, computationally natural, construction.
Original languageEnglish
Pages (from-to)3 - 25
Number of pages23
JournalTheoretical Computer Science
Volume177
Issue number1
DOIs
Publication statusPublished - 30 Apr 1997

Fingerprint

Dive into the research topics of 'A representable approach to finite nondeterminism'. Together they form a unique fingerprint.

Cite this