|Professor||Prof. Tobias Nipkow|
|Time and Place||Monday 16:15 ‐ 17:45 in MI Hörsaal 2|
|Live stream||RBG Live|
- 2021-01-26: The exam will take place on 2022-02-23 8:00 - 9:30 in MW 2001. Due to the relatively high number of registrations, the exam will be a written exam.
- 2021-12-23: Merry Christmas and a happy New Year! See you again in January.
- 2021-12-1: Due to the Dies Academicus, the tutorial will not take place tomorrow.
- 2021-11-23: Entered the correct starting time for the tutorial: 10:05.
- 2021-11-18: Homework solutions are now also published but only on Moodle.
- 2021-10-28: Homework submissions are managed with Moodle. The homework submissions will be marked but there won’t be a grade bonus.
- 2021-10-25: Added information about hygiene provisions.
- 2021-10-11: The lecture hall as well as the time and date of the lecture were changed. The date of the first tutorial was changed.
- Questions regarding the lecture and exercises can be discussed on Zulip. You can subscribe to all
Lambda-*streams by visiting this stream and clicking the curry emoji.
- This course overlaps with the second half of the course Equational Logic and Lambda Calculus (IN2048). Only one of the two courses can be credited towards your degree.
- The weekly homework sheets will be marked but there won’t be a grade bonus.
- In accordance with the rules set by the TUM, we will check your 2G status (recovered, vaccinated) before you enter the lecture hall. Additionally, you must check in when entering the room using the QRONITON contact tracing system. Masks are mandatory both when entering the room and when seated.
The exam will be in written form and take place on 2022-02-23 08:00 - 09:30 in MW 2001. In accordance with the hygiene provisions for exams, the 3G rule applies which means that unvaccinated people need to provide an official rapid certificate not older than 24 hours or PCR test certificate not older than 48 hours. Additionally, students are required to wear an FFP2 mask that they can take off while seated. You may bring an A4 sheet with hand-written notes on both sides.
You have received a link for the online review together with the grade published on TUMonline. The exam review runs until Sunday midnight, i.e. 2022-03-14 00:15.
|Time and Place||Thursday 10:05 ‐ 11:35 in seminar room 00.08.038|
The \(\lambda\)-calculus is a universal model of computation, i.e. it can simulate any Turing machine, that was introduced by Alonzo Church in the 1930s. Today it forms the basis of many functional programming languages such as Haskell or Idris. Due to the Curry-Howard correspondence terms of the \(\lambda\)-calculus can not only be interpreted as programs but also as proofs. In its simplest form, the \(\lambda\)-calculus only has three rules that dictate how a term can be constructed:
|\(x\)||Variable||A name representing a parameter or mathematical value.|
|\((\lambda x.\ t)\)||Abstraction||Function definition where \(t\) is a \(\lambda\)-term. The variable \(x\) becomes bound in the expression.|
|\((f\ t)\)||Application||Applying the function \(f\) to the argument \(t\). Both \(f\) and \(t\) are \(\lambda\)-terms.|
In order to compute with \(\lambda\)-terms we define \(\beta\)-reduction: the term \((\lambda x.\ t)\ s\) reduces to \(t[s / x]\) which means that any occurence of the variable \(x\) in \(t\) is replaced by \(s\). The above rules formalise the basic untyped \(\lambda\)-calculus. In the lecture, we will discuss the theoretical properties of both untyped and (simply) typed lambda calculus. In particular, we will investigate the correspondence of programs and proofs in the second part of the lecture:
Untyped Lambda calculus
Syntax: Terms, notational conventions, Currying, static binding, free and bound variables, substitution, alpha-conversion.
Beta-reduction: Definition of \(\beta\)-reduction. Proof that \(\beta\)-reduction is confluent.
Eta-reduction: Motivation, definition and basic properties: termination and (local) confluence.
Reduction strategies: Without proof: contraction of leftmost \(\beta\)-redexes leads to a normal form if one exists.
Lambda calculus as a programming language: Booleans, pairs, Church numerals, fixed-point combinators.
Typed Lambda calculus
Simply typed lambda calculus: Simple types. Implicitly and explicitly typed terms. Type checking rules.
Type inference: Type-correct terms no longer have a unique type but still a most general type. Proof by a concrete Prolog-like interpretation of the typing rules as backward computation rules.
Let-polymorphism: Universally quantified type schemas. Typing rules for “let” and for type schemas. Syntax-directed typing rules with built-in quantifier handling.
Curry-Howard correspondence: Types = propositions, lambda-terms = proofs, beta-reduction = proof-reduction. Proof of the subterm property of proofs in normal form. Proof of decidability of intuitionistic propositional logic via proofs in normal form.
- Hendrik Pieter Barendregt. The Lambda Calculus, its Syntax and Semantics, North-Holland, 2nd edition, 1984
- Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989
- Chris Hankin. An Introduction to Lambda Calculi for Computer Scientists, King’s College Publications, 2004
- J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and Lambda Calculus, Cambridge University Press, 1986
- J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators: An Introduction, Cambridge University Press, 2008