## Uncountable Limits and the Lambda Calculus

##### Download

##### Date

1995##### Author

Di Gianantonio, Pietro

Honsell, Furio

Plotkin, Gordon

##### Metadata

Show full item record##### 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.