Countable Non-Determinism and Uncountable Limits

Pietro Gianantonio, Furio Honsell, Silvia Liani, Gordon D. Plotkin

Research output: Chapter in Book/Report/Conference proceedingChapter


In this paper we address the problem of solving recursive domain equations using uncountable limits of domains. These arise for instance, when dealing with the ω 1-continuous function-space constructor and are used in the (generative) denotational semantics of programming languages which feature non-deterministic fair constructs implemented with unbounded choice. It is well known that such features cannot be modeled using just Scott-continuous functions; they can be modeled conveniently, instead, using functions which satisfy the weaker continuity property of ω 1-continuity. Surprisingly, the category of cpo’s and ω 1-continuous embeddings is not ω 0-cocomplete. Hence the standard technique of Adámek and Koubek for solving reflexive domain equations involving these constructs fails. This phenomenon was not noticed before in the literature. We discuss two alternative methods that can be used to solve the required domain equations. The first one is an application of the method of Adámek and Koubek to a different category. The second one, instead, is a genuine extension of their method and amounts to considering cones instead of limits. We put both methods on solid categorical grounds and discuss some applications. Finally we utilise the second method in order to give a model for the untyped λ-calculus whose theory is precisely the λβη theory. Thus we show that ω 1-lambda models are complete for the λβη-calculus.
Original languageEnglish
Title of host publicationCONCUR ’94: Concurrency Theory
Subtitle of host publication5th International Conference, Uppsala, Sweden, August 22–25, 1994, Proceedings
EditorsBengt Jonsson, Joachim Parrow
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-48654-1
ISBN (Print)978-3-540-58329-5
Publication statusPublished - 1994

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Countable Non-Determinism and Uncountable Limits'. Together they form a unique fingerprint.

Cite this