This book is a second edition of the Introduction to Combinators and λ-Calculus by the same authors. As its name suggests, it is an introduction to two closely related systems: λ-calculus and combinatory logic (CL). The description of these systems goes hand in hand, starting from the basics (β- and weak reductions, the fixed-point theorem and Böhm's theorem, and undecidability results), through proof theory of λβ and CLw and questions of extensionality, to an introduction of several approaches to typing in the two systems. The final chapters of the book introduce the semantics and model theory of λ-calculus and CL, paying special attention to the model D∞ discovered by Dana S. Scott, touching lightly the relation of weak normalisation, confluence and consistency theorems for the arithmetical version of CL to the consistency of Peano Arithmetic. The book's 345 pages are organised into 16 chapters and five appendices. The text is interleaved with instructive exercises, the harder of which are solved in the last appendix. The book is well-written and offers a broad coverage backed by an extensive list of references. It could serve as an excellent study material for classes on λ-calculus and CL as well as a reference for logicians and computer scientists interested in the formal background for functional programming and related areas.

Reviewer:

ppaj