This review was restarted on Thu 15Aug13 during actual reading of this book.
I am somehow quite motivated to learn lambda calculus, since it is so historically important and also closely related to functional programming languages. Plus it is interesting for its own sake.
THIS BOOK VS. OTHER BOOKS ON LAMBDA CALCULUS
Other textbooks on the subject, of which I own several, never get around to helping us learn what lambda expressions are actually telling us. Those expressions remain pure gobbledegook. I am well into reading chapter 2 of this reprinted famous 1984 edition by Henk Barendregt and the fog is already starting to clear. In many places, the author didn't write a lot of descriptive prose, but when he did, there always seemed to be a great insight in it. So be aware of that good bang for the buck.
Another thing I like about the approach here is that combinators mostly flow out of lambda calculus instead of being a fully separate subject of equal status to lambda as in the other good standard text by Hindley and Seldin, which I read into chapter 10 in fall of 2011. Lambda-Calculus and Combinators: An Introduction ((Historically, lambda calculus and combinatory logic WERE invented and developed separately, starting in the 1930s. Lambda by Alonzo Church and his illustrious students at Princeton / combinatory by Haskell Curry and colleagues, some of them during his sojourns in Holland and Gottingen.)) By the way, Haskell Curry is still noteworthy, as the Haskell functional programming language is named after him, and there is another computation method referred to as 'currying', again after his last name.
READING THIS BOOK
PART I AND READING PLANS
Finished great chapter 2 on conversion on Sun 18Aug13 / barely started chapter 3 on reduction. Chapter 3 is as well-written and clear as chapter 2 was. Finished short and great chapter 4 about theories on Tue 3Sep13. Chapter 5 on lambda models is the last one in Part I, is over 30 pages long, and is fundamentally more difficult than any of chapters 1-4, so since I don't plan to read the Part V chapters of 18-21, I am skipping chapter 5 to start Part II with chapter 6 on classic lambda calculus. I did read the survey of Part V at end of chap5 on Thu 5Sep13 afternoon, however. I hope to continue understanding this book at least thru chapter 9 of its 21 chapters.
Chapter 6 on classic lambda is a gem of mainstream lambda calculus including a little bit of abstraction. Finished chap 6 on Fri 13Sep13. On Sun 15Sep13 afternoon, I well started short chapter 7 on combinators. Rather unusual, and stripped down to a tedious definition/theorem/proof bare bones approach. By section 7.2 though more clear and helpful writing returned to moderate extent. Did push thru the last 5 pages of chapter 7 on Wed 18Sep13 afternoon. Chapter 8 on more of classical lambda calculus soon, as I am a bit focussed on finishing final chapter IV of The Foundations of Mathematics (Logic). Enthusiastically got started on terrific chapter 8 on Wed 25Sep13 evening, so more later. Sections 8.1 and 8.2 were well written and quite interesting. Section 8.3 though is one of those fully Definition/Theorem/Proof (DTP) shuffles, a student-unfriendly type of writing. Difficult section 8.4, not just DTP all read, completing chapter 8 on Tue 8Oct13 evening. Chapter 9 on lambda-I calculus is completely DTP and the proofs tend to be getting longer, so my reading of this book unfortunately ended at end of chapter 8.
It really is great to be able to purchase this thorough and legendary book for a reasonable College Publications price, and I have found that CP makes rather durable paperbacks, i.e., more durable than similarly priced Dover books.
Since atypically for books on the CP roster, the Amazon page for this book is somewhat open in their 'Look Inside' utility, I shall not type in a version of the complicated table of contents as I often do in my reviews. Please check that 'look inside' for the full TOC. There are five 'Parts' of this book, each containing at least two chapters. Chapters 2-5 in part I introduce the main subjects of parts II thru V, and they each end with a small survey of the corresponding main Roman numeraled 'part' of the book.
Here is the list of the five parts: I Towards the Theory-1 (chaps 1-5) / II Conversion-129 (chaps 6-10) / III Reduction-273 (chaps 11-15) / IV Theories-409 (chaps 16-17) / V Models-467 (chaps 18-21) / Appendices-557 (A-C) / Full set of references and of indices.
THE NEW BOOK
On Thu 19Sep13 late afternoon, I received the new 2013 Lambda Calculus with Types (Perspectives in Logic) from Amazon. I am a member of the Association for Symbolic Logic (ASL), the co-publisher of this 850 page volume. Barendregt, Dekkers, and Statman are the main authors, but quite a few other experts also contributed. It combines familiar notation from the present book with some nice type tables similar to those in Benjamin Pierce's great 2002 type theory book, quite a bit of which I have read. The Amazon 'Look Inside' utility for the new book is notably open for large examination of it.