Uncountable limits and the lambda calculus
Pietro Di Gianantonio, Furio Honsell, Gordon D. Plotkin · ERA · 1995
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 denotational semantics of programming languages which feature unbounded choice constructs. Surprisingly, the category of cpo’s and ω1-continuous embeddings is not ω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 λβη-calculus w.r.t reflexive domain models. We show that among the reflexive domain models in the category of cpo’s and ω0-continuous functions there is one which has a minimal theory. We give a reflexive domain model in the category of cpo’s and ω1-continuous functions whose theory is precisely the λβη theory. So ω1-continuous λ-models are complete for the λβη-calculus.