@inbook{f247f28492c24f4bacf99b996c5850e4,

title = "Countable Non-Determinism and Uncountable Limits",

abstract = "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{\textquoteright}s and ω 1-continuous embeddings is not ω 0-cocomplete. Hence the standard technique of Ad{\'a}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{\'a}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.",

author = "Pietro Gianantonio and Furio Honsell and Silvia Liani and Plotkin, {Gordon D.}",

year = "1994",

doi = "10.1007/978-3-540-48654-1_12",

language = "English",

isbn = "978-3-540-58329-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "130--145",

editor = "Bengt Jonsson and Joachim Parrow",

booktitle = "CONCUR {\textquoteright}94: Concurrency Theory",

}