| Nordic Journal of Computing Uncountable Limits and the Lambda Calculus (2008) | |||||||||||||
Abstract | |||||||||||||
| 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 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. CR Classification: F.3.2, F.4.1, D.3.3 Key words: countable non-determinism, denotational semantics, domain equations, lambda-calculus. 1. | |||||||||||||
Publication details | |||||||||||||
| |||||||||||||