Set-theoretical and other elementary models of the \(\lambda\)-calculus (Q1314361): Difference between revisions

The first part of this paper consists of the author's previously unpublished but seminal work, dating back to 1972, creating the first model of the lambda calculus. The paper is best summarised as in the abstract: The first part begins with an elementary set-theoretical model of the \(\lambda\beta\)-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 \(\lambda\beta\eta\)-calculus is constructed by means of a natural deduction method. Finally, a theorem is proved giving some general properties of those nontrivial models of the \(\lambda\beta\eta\)- calculus which are continuous complete lattices. The second part begins with a brief discussion of models of the \(\lambda\)-calculus in set theories with anti-foundation axioms. Next the model of the \(\lambda\beta\)-calculus of Part I and also the closely related -- but different! -- models of Scott (1976, 1980) and of Engeler (1981, 1988) are reviewed. Then general frameworks in which elementary constructions of models can be given are discussed. Following Longo (1982), one can employ certain Scott-Engeler algebras. Following Coppo et al (1983), one can obtain filter models from their extended applicative type structures. An extended discussion is given of various ways of construction models of the \(\lambda\beta\eta\)-calculus, and the connections between them. Finally an extension of the theorem to complete partial orders is given. The theme of the paper is the consideration of means of constructing models. There is hardly any analysis of their properties; there is no discussion of their application.