CMSC 31900
Lambda CalculusPrerequisites: Knowledge of algebra or equivalent level of math
Catalog Description: This course covers the crucial properties of the lambda calculus and its variant, the combinator calculus. We emphasize 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 of type A to B and as a proof that A implies B.
Long 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. Lambda and combinator calculi are studied as much by philosophers as by mathematicians and computer scientists.
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 crucial knowledge 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.
Instructors: M. O'DonnellQuarter offered: Winter. Not offered in 2009-2010; will be offered 2010-11.
Last Verified by Sharon Salveter on 8 April, 2003.