Introduction to combinators and $$\lambda$$-calculus.(English)Zbl 0614.03014

London Mathematical Society Student Texts, 1. Cambridge etc.: Cambridge University Press. VIII, 360 p. (1986).
The lambda calculus and the theory of combinators are closely related theories developed by Church and Curry, respectively, as foundations for (higher order) logic and function theory. These theories were the source of the first uncomputability results and are now also of great interest to Computing Scientists as bases for functional programming languages, verification of programs as well as in more theoretical areas.
The present book, by two of the top workers in the field, is a wholly rewritten and greatly expanded version of ”Introduction to combinatory logic”, by the same authors and B. Lercher (1972; Zbl 0269.02005). Its aim is to introduce readers, with some knowledge of predicate calculus and recursive functions, to the basic techniques and results of the lambda calculus and the theory of combinators. This it does, but because of the, in itself, laudatory effort that has been made, in the early chapters, to make definitions more precise and theorems a little more general, less expert readers may find difficulties with some rather technical definitions and lemmas.
New material on the definition of models has been added to the earlier volume as well as a careful construction of Scott’s $$D_{\infty}$$ model. There is a wealth of extra material on type assignment and some more on logic based on combinators.
The volume contains many good exercises and has solutions to some at the back. At appropriate points throughout there are interesting historical notes and many useful references.
Reviewer: M.W.Bunder

MSC:

 03B40 Combinatory logic and lambda calculus 03-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations 03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations

Zbl 0269.02005