Com Sci 319
Lambda Calculus
Winter 2000

Department of Computer Science
The University of Chicago

Online discussion using HyperNews

• [8 Feb] Assignment #4 is due on Monday, 14 February, at the beginning of class. (O'D)



• [17 Jan] The HyperNews discussion is set up. Please read the instructions, and jump in. The system reports an error whenever you post, but the only error is the error report itself. I'm trying to get that fixed. In the meantime, please don't post the same message repeatedly in response to the erroneous error message. (O'D)



• [29 Dec 1999] The Web materials for ComSci 319 are under construction. Some links are broken. (O'D)

Logistics

• Venue: MW 9:00-10:20, Ryerson 257



• Instructor: Michael J. O'Donnell
  • Office: Ryerson 257A.
  • email: odonnell@cs.uchicago.edu
  • Office hours: by appointment. Contact me by email, phone at the office (312-702-1269), or phone at home (847-835-1837 between 9:30 and 5:30 on days that I work at home). You may drop in to the office any time, but you may find me out or busy if you haven't confirmed an appointment. Check my personal schedule before proposing an appointment.



• Teaching Assistant: Ilia Bisnovatyi.
  • Office: Ryerson 257C.
  • email: ilia@cs.uchicago.edu
  • Ilia will mostly work on logistics, rather than course content.

Copyright information

Last modified: Tue Feb 8 18:22:50 CST 2000

Catalog Description

The lambda calculus is a formal system for studying the definitions of functions, independently of the domains and ranges on which those functions operate. It was invented as a model of the lower-level mechanics of mathematical logic, but today it is mainly applied to the design of control structures for programming languages. Along the way, it provided the first characterization of the computable functions and the foundation for proof theory, and it showed the subtlety of the relation between parallelism and nondeterminism, which is still misunderstood today. This course covers the crucial properties of the lambda calculus and its variable-free cousin the combinator calculus, emphasizing the deep connections between various areas of logic and computation that arise from the ability to interpret a lambda term equally naturally as a program and as a proof. In particular, the pun by which A=>B may denote that A implies B, or the class of functions from A to B, turns out to have a deep significance, leading to intuitive foundations for intuitionism, and radically new and useful ideas of the power of a logical system.

The course is moderately challenging mathematically, at perhaps the level of introductory group theory, but it is especially demanding in the breadth of intuition required to see the fundamental unity of the very different sounding applications of the calculus. The material is very useful for all graduate students in computer science, and also valuable to college students who have the flexibility to connect mathematical theorems closely to practical and philosophical intuitions.

Texts

There will probably be 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. Amazon is engaged in a patent action against Barnes & Noble, claiming exclusive rights to use one-click shopping. Some people consider this an abuse of intellectual property law, and prefer not to do business with Amazon.

Class Resources

odonnell@cs.uchicago.edu