Com Sci 319
A course in the
Department of Computer Science
The University of Chicago
- [8 Feb] Assignment #4
is due on Monday, 14 February, at the beginning of class. (O'D)
- [17 Jan] The
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)
- Venue: MW 9:00-10:20, Ryerson 257
Michael J. O'Donnell
- Office: Ryerson 257A.
- email: firstname.lastname@example.org
- 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
before proposing an appointment.
- Teaching Assistant: Ilia Bisnovatyi.
- Office: Ryerson 257C.
- email: email@example.com
- Ilia will mostly work on logistics, rather than course
Last modified: Tue Feb 8 18:22:50 CST 2000
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
There will probably be no required text. Important books on the
- 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
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
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
Barnes & Noble online,
BigWords (use the B-CODE
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
intellectual property law, and prefer not to do business with
Students in the class
Collaborative book project
Lecture Notes and Schedule
Archive of Previous Quarters' Homeworks and Exams
Maintained by Michael J. O'Donnell, email: