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 omega-1 continuous function-space constructor and are used in the denotational semantics of programming languages which feature unbounded choice constructs. Surprisingly, the category of cpo's and omega-1 continuous embeddings is not omega-0 cocomplete. Hence the standard technique for solving reflexive domain equations fails. We give two alternative methods. We discuss also the issue of completeness of the lambda-beta-eta-calculus w.r.t reflexive domain models. We show that among the reflexive domain models in the category of cpo's and omega-0 continuous functions there is one which has a minimal theory. We give a reflexive domain model in the category of cpo's and omega-1 continuous functions whose theory is precisely the lambda-beta-eta theory. So omega-1 continuous lambda-models are complete for the lambda-beta-eta calculus.