Texts

There is no required text. Important books on the topic include

• The Lambda Calculus: Its Syntax and Semantics, H. P. Barendregt, North-Holland, New York, volume 103 of Studies in Logic and the Foundations of Mathematics, J. Barwise, D. Kaplan, H. J. Keisler, P. Suppes, A. S. Troelstra editors, revised edition 1984, 621 pages, ISBN: 0 44487508 5 (paperback).
  
  This is an encyclopedic book, terse rather than easy to read, mathematically deep. As most North-Holland books, it is horrifically overpriced. The paperback edition is still quite expensive, and shoddily constructed with a glue-on binding. My copy started to lose pages in a few weeks. The hardback edition is probably more durable, but even more expensive. Nonetheless, the content is crucial, and everyone who is serious about the whole of theoretical computer science should own a copy.
  
  
• Introduction to Combinators and Lambda Calculus by J. Roger Hindley and Jonathan P. Seldin, Cambridge University Press, New York, volume 1 of London Mathematical Society Texts, E. B. Davies editor, 1986, 360 pages, ISBN: 0 521 31839 4 (paperback) 0 521 26896 6 (hardcover).
  
  This is a very accessible textbook, reasonably priced, but too elementary to satisfy a Ph.D. student in theoretical computer science. A handy supplement to get the easier parts quickly.
  
  
• Lambda Calculi: a Guide for Computer Scientists by Chris Hankin, Clarendon Press, Oxford, volume 3 of Graduate Texts in Computer Science, D. M. Gabbay, C. L. Hankin, T. S. E. Maibaum editors, 1994, 162 pages, ISBN: 0 19 853849 5 (paperback) 0 19 853841 (hardcover).
  
  I haven't read this one thoroughly yet. It appears to be a reasonably accessible textbook, at a somewhat higher level of mathematical difficulty than Hindley/Seldin, but covering topics in an order that I am not accustomed to.
  
  
• Combinators, Lambda Terms, and Proof Theory by Sören Stenlund, D. Reidel, Dordrecht Holland, Synthese Library, Donald Davidson, Jaakko Hintikka, Gabriël Nuchelmans, Wesley C. Salmon editors, 1972, 184 pages, ISBN: 90-277-0305-1.
  
  This is a wonderfully terse, clear reference to the basic definitions and theorems, presented for mathematicians. It includes the proof theoretic definitions, which many leave out. Alas, it is out of print.
  
  
• Combinatory Logic volume I by Haskell B. Curry and Robert Feys with two sections by William Craig, North-Holland, Amsterdam, Studies in Logic and the Foundations of Mathematics, L. E. J. Brouwer, E. W. Beth, A. Heyting editors, 1958, 417 pages.
  
  
• Combinatory Logic volume II by Haskell B. Curry, J. Roger Hindley, and Jonathan P. Seldin, North-Holland, Amsterdam, Studies in Logic and the Foundations of Mathematics, A. Heyting, H. J. Keisler, A. Mostowski, A. Robinson, P. Suppes editors, 1972, 520 pages, ISBN: 0 7204 2208 6.
  
  This is the bible for combinatory logic, including lambda calculus and proof-theoretic applications. It is hard to read, and only fluent mathematicians should try it. But, anyone who wants to do resarch in combinatory logic or lambda calculus must study this book. It lacks recent work of course, but it discusses many issues that are often neglected in more modern texts, including connections to the foundations of mathematics.
  
  
• The Combinatory Programme by Erwin Engeler in collaboration with K. Aberer, B. Amrhein, O. Gloor, M. von Mohrenschildt, D. Otth, G. Schwärzer, and T. Weibel, Birkhäuser, Boston, 1995, Progress in Theoretical Computer Science, Ronald V. Book editor, 142 pages, ISBN: 0 8176 3801 6, 3 7643 3801 6.
  
  This book is difficult to read unless you already know the basic definitions of the lambda and combinatory calculi. It is self-contained in principle, but definitions are presented in the style of reminders more than explanations. Once you know the basics, read this book for a detailed discussion of the relevance of combinatory logic to algebra and the foundations of mathematics.
  
  
• The Calculi of Lambda-Conversion by Alonzo Church, Princeton University Press, Princeton, volume 6 of Annals of Mathematical Studies, 1941, 77 pages.
  
  A historical classic, also short and fairly accessible. All of the material is covered elsewhere, but this book shows how Church was thinking at the time. His attitude toward the undefined is particularly interesting: the "lambda calculus" in this book describes only strict functions, and is now called the "lambda-I calculus". Today's "lambda calculus" is the "lambda-K calculus" to Church, and he considers it pathological. I think that Church restates his famous thesis here (participation credit to anyone who checks this out and posts the right quote), but he first stated it in 1935 in "An unsolvable problem of elementary number theory." I go along with Martin Davis in crediting Church with a lucky guess, and Turing with making that guess into a credible thesis.
  
  
• Outline of a Formalist Philosophy of Mathematics by Haskell B. Curry, Studies in Logic and the Foundations of Mathematics, L. E. J. Brouwer, E. W. Beth, A. Heyting editors, North-Holland, Amsterdam, 1951.
  
  This is a bit off the center of our topic, but I find it fascinating. Along with the introductory material in the two volumes of Combinatory Logic, this explains Curry's idea that ``Mathematics is the science of formal systems,'' which are objective things. It's a lot less clear than Saunders Mac Lane's ideas on ``functional formalism,'' but might be regarded as a precursor.

You may wish to order texts online from Amazon, Barnes & Noble online, BigWords (use the B-CODE B-2BFQA5), Bookpool, or other book vendors.

Copyright Michael J. O'Donnell <michael_odonnell@acm.org>. Licensed for free use.
This page is generated from PHP source code, with supporting files.