All of us are, in the course of lifelong learning, invariably dropped into the middle of an infinite ocean, where any point is the center. So, it may be quite unproductive for someone such as myself, a working stiff with a day job, to muse: “What if I had learned lambda calculus first?” (or similarly, other permutations among set theory, category theory, and lambda calculus). One could further multiply the possibilities to 24 by separating combinatory logic (CL), the coequal subject of this book, from lambda calculus, a separation that is often done. And the three or four subjects are, of course, interconnected; there is, for example, a category-theoretic object [1].

Without challenging the authors’ characterization of this substantive and authoritative book as “an introduction,” I must say that although of moderate length, the book is deeper and more detailed (per page) than any introductory book that I have read. The symbols are dense and intense, so the book must be “worked through” using twice the effort needed for most introductions--an effort well worth expending. My first attempt at lambda calculus constituted the desultory reading of Alonzo Church’s seminal book [2]. Although I am not saying “Don’t read Church’s book,” I am suggesting that you do try Hindley and Seldin’s, without implying that the book is easy going.

There remain the cognitive challenges to, first, “forget” what you know (for example, about axiomatic set theory) and, second, to keep in mind that lambda calculus and CL are dominant, while selected set concepts, as distinct from Zermelo-Fraenkel set theory, are incidental and subordinate. E.W. Dijkstra’s complementary maxim to the effect that it is harder to unlearn--here, for example, out-of-context meanings of familiar symbols--than it is to learn also comes into play. As a case in point, the book begins with a clear example of lambda notation for function application, followed by a rigorous inductive definition of lambda terms, the definition including, “If M and N are any λ-terms, then (MN) is a λ-term.” There shortly ensues introduction of the symbol ≡ for syntactic identity, with both the symbol and its extralinguistic meaning ostensibly carried over intact from propositional logic. However, the early location (page 4) and wording of this statement--“It will be assumed of course that if MN ≡ PQ, then M ≡ P and N ≡ Q”--may be puzzling to the beginner, over and above the “of course.” An assumption plays a formal role in, for example, the natural deduction proof steps that involve material implication (in propositional logic); it is there that a working hypothesis is eventually discharged. So the predicate-logic-trained λ-calculus beginner may next guess that the (M ≡ P and N ≡ Q) consequence of MN ≡ PQ is a defined property of ≡. The point of this lengthy nitpick is twofold: to validate the reader’s possible discomfort at this early stage, and to encourage reading on as, generally, clarity will ensue. The connection with Gentzen’s natural deduction system is in fact made in, among other places, chapter 13, where the notion of propositions-as-types is treated. The authors’ treatment of the lambda/CL theory underlying the Curry-Howard isomorphism between constructive logic and type theory alone--itself the basis of at least one excellent book [3]--is worth the price of this book. It is not negative to characterize both lambda calculus and CL as being “all about syntax,” but the syntax will be treacherous to those who remain engaged only superficially. So I encourage the reader to get exercises 1.4* and 1.8* right--the answers to starred problems are in the back--before proceeding further.

The 16 chapters and five appendices comprise a highly synergistic interleaving of lambda calculus and CL, and thus display the significant advantage of concurrent treatment of these “equivalent” theories. Among the highlights are: term-structure; beta-reduction; weak reduction and abstraction in CL; the fixed-point, Church-Rosser, and Böhm theorems; (primitive) recursive and computable functions; undecidability; formal theories of beta-equality in lambda and of weak equality in CL; extensionality in lambda and in CL; simple typing, Church-style, and Curry-style, including the aforementioned marvelous treatment of propositions-as-types that lends depth and rationale to this powerful contemporary formal method, which is so “important in the theoretical foundations of computing”; and models of CL and lambda calculus.

Although there will never be a royal road to mastering the intrinsically intricate subjects of this excellent book, this is definitely one road to take.