A Set-Theoretical Definition of Application

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.