Edinburgh Research Archive logo

Edinburgh Research Archive

University of Edinburgh homecrest
View Item 
  •   ERA Home
  • Informatics, School of
  • Informatics Publications
  • View Item
  •   ERA Home
  • Informatics, School of
  • Informatics Publications
  • View Item
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.

A Set-Theoretical Definition of Application

View/Open
Set_Mod_lambda.pdf (378.4Kb)
Date
05/11/2003
Author
Plotkin, Gordon
Metadata
Show full item record
Abstract
This paper is in two parts. Part 1 is the previously unpublished 1972 memorandum [41], with editorial changes and some minor corrections. Part 2 presents what happened next, together with some further development of the material. The first part begins with an elementary set-theoretical model of the λβ-calculus. Functions are modelled in a similar way to that normally employed in set theory, by their graphs; difficulties are caused in this enterprise by the axiom of foundation. Next, based on that model, a model of the λβη-calculus is constructed by means of a natural deduction method. Finally, a theorem is proved giving some general properties of those non-trivial models of the λβη-calculus which are continuous complete lattices. In the second part we begin with a brief discussion of models of the λ-calculus in set theories with anti-foundation axioms. Next we review the model of the λβ-calculus of Part 1 and also the closely related- but different!- models of Scott [51, 52] and of Engeler [19, 20]. Then we discuss general frameworks in which elementary constructions of models can be given. Following Longo [36], one can employ certain Scott-Engeler algebras. Following Coppo, Dezani-Ciancaglini, Honsell and Longo [13], one can obtain filter models from their Extended Applicative Type Structures. We give an extended discussion of various ways of constructing models of the λβη-calculus, and the connections between them. Finally we give extensions of the theorem to complete partial orders. Throughout we concentrate on means of constructing models. We hardly consider any analysis of their properties; we do not at all consider their application.
URI
http://hdl.handle.net/1842/206
Collections
  • Informatics Publications

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page

 

 

All of ERACommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisorsThis CollectionBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisors
LoginRegister

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page