A Set-Theoretical Definition of Application
View/ Open
Date
05/11/2003Author
Plotkin, Gordon
Metadata
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.