Show simple item record

dc.contributor.authorDi Gianantonio, Pietro
dc.contributor.authorHonsell, Furio
dc.contributor.authorPlotkin, Gordon
dc.coverage.spatial20en
dc.date.accessioned2003-11-05T17:19:55Z
dc.date.available2003-11-05T17:19:55Z
dc.date.issued1995
dc.identifier.citationNordic Journal of Computing, 2(2):126-145, Summer 1995en
dc.identifier.urihttp://hdl.handle.net/1842/211
dc.description.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 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.en
dc.format.extent272833 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherPublishing Association Nordic Journal of Computingen
dc.subjectcountable non-determinismen
dc.subjectdenotational semanticsen
dc.subjectdomain equationsen
dc.subjectlambda-calculusen
dc.subjectLaboratory for Foundations of Computer Science
dc.titleUncountable Limits and the Lambda Calculusen
dc.typeArticleen


Files in this item

This item appears in the following Collection(s)

Show simple item record