Models of the lambda calculus
C.P.J. Koymans · Data Archiving and Networked Services (DANS) · 1984
In 1969 Scott constructed mathematical models for the it-calculus; see Scott (1972). It took some time, however, before a general definition of the notion of a it-calculus model was given. This was done independently in Barendregt (1977, 1981), Berry (1981), Hindley and Longo (1980), Meyer (1980), Obtulowicz (1979), and Scott (1980). All of these definitions except Berry's are reviewed in Cooperstock (1981). There seemed to be some disagreement on the notion of a it-calculus model. Barendregt introduced two classes of models, viz. the ),-algebras and the it-models. Berry's models coincide essentially with the ).-algebras, whereas the models of Hindley-Longo, Meyer, Obtulowicz, and Scott all coincide with the it-models. Barendregt was inspired by proof theoretic considerations (coincompleteness, see Plotkin, 1974) for introducing both ),-algebras and itmodels. He did this both in a syntactical and a first order way. We will replace his syntactical method by the so-called environment models. (These are in fact also syntactical but somewhat easier to handle.) Moreover, inspired by Berry (1981) and Meyers (1974) (for the typed it-calculus) we give a unified categorical description of both it-algebras and ),-models. By methods taken from Scott (1980), it will be proved that the structures thus obtained consist of all it-algebras and it-models. The categorical description gives a convincing argument that the two kinds of models form a natural class of interpretations of the it-calculus. In the meantime there seemed to have formed a consensus about the need for both it-algebras and it-models. The revised version Meyer (1981) includes also ),-algebras. Scott (1980) constructs Cartesian closed categories (ccc's) from it-theories; but this construction essentially goes via a it-algebra (ittheory-~ term model (which is a it-algebra)~ ccc). We prefer this way of describing Scott's construction, because different it-algebras may have the same theory, but yet different ccc's. Now we will give a short description of the three ways of introducing the 3O6 0019-9958/82 $2.00