Di Gianantonio, Pietro

Honsell, Furio

Plotkin, Gordon

20

2003-11-05T17:19:55Z

2003-11-05T17:19:55Z

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 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.

272833 bytes

application/pdf

Nordic Journal of Computing, 2(2):126-145, Summer 1995

http://hdl.handle.net/1842/211

en

Publishing Association Nordic Journal of Computing

countable non-determinism

denotational semantics

domain equations

lambda-calculus

Laboratory for Foundations of Computer Science

Uncountable Limits and the Lambda Calculus

Article