Lambda-calcul, types et modèles. (Lambda calculus, types and models). (French) Zbl 0697.03004

Krivine, Jean-Louis

Études et Recherches en Informatique. Paris etc.: Masson. viii, 176 p. FF 198.00 (1990).

This course in \(\lambda\)-calculus is presented as an introduction to four aspects of the theory: pure \(\lambda\)-calculus, combinatory logic, models and type systems, with the intention of bringing to light their interdependency and the underlying unity of the subject.
All basic results in pure \(\lambda\)-calculus are proved (with streamlined or new proofs) including: the Church-Rosser, Böhm and normalization theorems, the representation of recursive functions and the equivalence of \(\lambda\)-calculus with combinatory logic. Substitution lemmas and variable capture are looked at with great care.
Types appear first in this book as a tool for studying normalization phenomena: left (strong, head, etc.) normalizable terms are characterized in terms of their typeability with respect to Coppo and Dezani’s intersection type systems. Types appear also for their own sake and their underlying foundational interest in functional programming “by proofs” (Curry-Howard isomorphism). There is a presentation of Girard’s system F and a new proof of the fact that a function f is representable in F iff it is provably total in second-order combinatory logic (named \(AF_ 2\) by the author). This result is proved here via: realizability in standard models of \(AF_ 2\), Gödel transformation, and simple abstract definitions of data-types. Part of the proof ensures the program correctness of \(AF_ 2\) viewed as a high level programming language: the \(\lambda\)-term extracted from any proof of the totality of f will really compute f.
Thus models of second-order combinatory logic appear as the natural semantic tool for studying F. But the “model” side of the book is also represented by a study of models of pure \(\lambda\)-calculus. First a general framework is given, stressing the functional aspects but without any use of category theory. Then the author, whose aim is to provide practical non-categorical tools for building models, concentrates on models S(D) which are the spaces of initial segments of preordered sets (D,\(\leq)\), equipped with an application i: \(D^ f\times D\to D\) suitable for coding in S(D) the space of its Scott-continuous functions \((D^ f\) is the set of finite subsets of D). Classical models of \(\lambda\)- calculus are reconstructed in that way and applications are given to the model-theory of \(\lambda\)-calculus, for example an elegant proof of the consistency of \(\lambda\)-calculus with (strong) surjective pairing.
No specific knowledge is required “but some practice in mathematical logic”; however a reader with no previous knowledge of the subject may want to combine the reading of this book, which I highly recommend, with that of a more classical book or paper since one finds here very few extra-mathematical comments and motivations outside the short introduction.

Reviewer: C.Berline

MSC:

03B40	Combinatory logic and lambda calculus
68N01	General topics in the theory of software
68Q60	Specification and verification (program logics, model checking, etc.)
03-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
68-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science
68Q65	Abstract data types; algebraic specification
03D60	Computability and recursion theory on ordinals, admissible sets, etc.

Keywords:

pure \(\lambda \) -calculus; combinatory logic; models; type systems