AbstractIn this paper we address the problem of solving recursive domain equations using uncountable limits of domains. These arise for instance, when dealing with the omega1-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 omega1-continuous embeddings is not omega0-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 omega0-continuous functions there is one which has a minimal theory. We give a reflexive domain model in the category of cpo's and omega1-continuous functions whose theory is precisely the lambda beta eta theory. So omega1-continuous lambda-models are complete for the lambda beta eta-calculus.
Categories and Subject Descriptors: F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic; D.3.3 [Programming Languages]: Language Constructs and Features
Additional Key Words and Phrases: countable non-determinism, denotational semantics, domain equations, lambda-calculus
Selected papers that cite this one
- Chantal Berline and Klaus Grue. A kappa-denotational semantics for map theory in ZFC + SI. Theoretical Computer Science, 179(1-2):137-202, 1 June 1997. Fundamental Study.
- Peter Selinger. Order-incompleteness and finite lambda models (extended abstract). In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 432-439, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.
Selected references
- K. R. Apt and G. D. Plotkin. Countable nondeterminism and random assignment. Journal of the ACM, 33(4):724-767, October 1986.