Lambda Calculus

Chair for Logic and Verification

Overview

Professor Prof. Tobias Nipkow
Time and Place Monday 16:15 ‐ 17:45 in MI Hörsaal 2
Live stream TUM-Live
First Lecture
Language English
TUMonline Lambda Calculus (IN2358)
Moodle Course Übung zu Lambda Calculus (IN2358)
Discussion Forum Zulip
Lecture Notes Lecture Notes on Lambda Calculus

News

General notice

Exam

Previous exams

Endterm

The endterm exam will take place in the Hans Fischer lecture hall on from 11:00 ‐ 12:30.

The exam will be a standard pen-and-paper exam. You are allowed to bring one DIN A4 sheet with hand-written notes on both sides.

Exam (Solution, Correction notes)

Grading

Grade Min Points
1 36.5
1.3 34
1.7 31.5
2 29
2.3 26.5
2.7 24
3 21.5
3.3 19
3.7 16.5
4 14
4.3 11.5
4.7 9
5 0

Post-Exam Review

You have received a link for the online review together with the grade published on TUMonline. The exam review runs until Tuesday midnight, i.e. 2023-02-28 00:15.

Retake

The retake exam will take place in the Walter Hieber lecture hall on from 17:00 ‐ 18:30.

The exam will be a standard pen-and-paper exam. You are allowed to bring one DIN A4 sheet with hand-written notes on both sides.

Exam (Solution, Correction notes)

Grading

Unfortunately, the points for the exercises in the exam were not distributed properly. Thus, some exercises yield significantly fewer points than intended and the exam in total only has 30 instead of 40 points. In order to bring the grading scheme closer to the intended grading scheme, we introduce virtual points as shown in the table below.

Exercise Actual Virtual
1a) 4 2
1b) 4 3
1c) 4 4
2 8 8
3a) 1 3
3b) 1 2
3c) 1 3
4a) 2 2
4b) 3 5
5a) 1 4
5b) 1 4
Sum 30 40

Using the virtual points, the exam is graded according to the following grading scheme.

Grade Min Points
1 36.5
1.3 34
1.7 31.5
2 29
2.3 26.5
2.7 24
3 21.5
3.3 19
3.7 16.5
4 14
4.3 11.5
4.7 9
5 0

The introduction of virtual points changes the relation between the exercises. As is, this may lead to a worse grade when compared to the actual points printed on the exam. We prevent this by scaling down the virtual points for each exercise to the actual points (no rounding) and apply the following grading scheme.

Grade Min Points
1 27.5
1.3 26
1.7 24.5
2 22.5
2.3 21
2.7 19
3 17.5
3.3 15.5
3.7 14
4 12
4.3 10.5
4.7 9
5 0

The better one of the two grades is the final grade. Please note that the points that you see in TUMexam are not necessarily correct because they are rounded.

Post-Exam Review

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. 2023-04-21 00:15.

Exercises

Organiser Lukas Stevens
TUMonline Übungen zu Lambda Calculus (IN2358)
Time and Place Thursday 10:00 ‐ 12:00 in Taurus 1, Galileo
First Tutorial

Exercise Sheets

The submission of the homework exercises as well as their solutions are available on Moodle.

Exercise Sheet For Digital Editing Tutorial Solution
Exercise 01 Exercise 01 Tutorial Solution 01
Exercise 02 Exercise 02 Tutorial Solution 02
Exercise 03 Exercise 03 Tutorial Solution 03
Exercise 04 Exercise 04 Tutorial Solution 04
Exercise 05 Exercise 05 Tutorial Solution 05
Exercise 06 Exercise 06 Tutorial Solution 06
Exercise 07 Exercise 07 Tutorial Solution 07
Exercise 08 Exercise 08 Tutorial Solution 08
Exercise 09 Exercise 09 Tutorial Solution 09
Exercise 10 Exercise 10 Tutorial Solution 10
Exercise 11 Exercise 11 Tutorial Solution 11
Exercise 12 Exercise 12 Tutorial Solution 12
Exercise 13 Exercise 13 Tutorial Solution 13

Contents

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:

Syntax Name Description
\(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:

  1. Untyped Lambda calculus

    1. Syntax: Terms, notational conventions, Currying, static binding, free and bound variables, substitution, alpha-conversion.

    2. Beta-reduction: Definition of \(\beta\)-reduction. Proof that \(\beta\)-reduction is confluent.

    3. Eta-reduction: Motivation, definition and basic properties: termination and (local) confluence.

    4. Reduction strategies: Without proof: contraction of leftmost \(\beta\)-redexes leads to a normal form if one exists.

    5. Lambda calculus as a programming language: Booleans, pairs, Church numerals, fixed-point combinators.

  2. Typed Lambda calculus

    1. Simply typed lambda calculus: Simple types. Implicitly and explicitly typed terms. Type checking rules.

    2. 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.

    3. Let-polymorphism: Universally quantified type schemas. Typing rules for “let” and for type schemas. Syntax-directed typing rules with built-in quantifier handling.

    4. 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.

Literature