Uncountable Limits and the Lambda Calculus

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.