The convex powerdomain in a category of posets realized by cpos

Alexander Simpson

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We construct a powerdomain in a category whose objects are posets of data equipped with a cpo of “intensional” representations of the data, and whose morphisms are those monotonie functions between posets that are “realized” by continuous functions between the associated cpos. The category of cpos is contained as a full subcategory that is preserved by lifting, sums, products and function spaces. The construction of the powerdomain uses a cpo of binary trees, these being intensional representations of nondeterministic computation. The powerdomain is characterized as the free semilattice in the category. In contrast to the other type constructors, the powerdomain does not preserve the subcategory of cpos. Indeed we show that the powerdomain has interesting computational properties that differ from those of the usual convex powerdomain on cpos. We end by considering the solution of recursive domain equations. The surprise here is that the limit-colimit coincidence fails. Nevertheless, by moving to a setting in which one considers “realizability” at the level of functors, algebraic compactness is achieved.
Original languageEnglish
Title of host publicationCategory Theory and Computer Science
Subtitle of host publication6th International Conference, CTCS '95 Cambridge, United Kingdom, August 7–11, 1995 Proceedings
EditorsDavid Pitt, DavidE. Rydeheard, Peter Johnstone
PublisherSpringer-Verlag GmbH
Number of pages29
Publication statusPublished - 1995

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'The convex powerdomain in a category of posets realized by cpos'. Together they form a unique fingerprint.

Cite this