Lambda Calculus
General Notice

Exam: The oral exam will be held on February 8, 2018.

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.
 There will be weekly homework sheets, which will be graded. Students who achieve 50% of the homework points will
receive a bonus mark of 0.3, provided that they also pass the final exam.
Excercises
Contents
Lambda Calculus
 Untyped Lambda calculus

 Syntax

Terms, notational conventions, Currying, static binding, free and bound variables, substitution, alphaconversion.
 Betareduction
 Definition of betareduction. Definition of parallel reduction >. Proof that > has the diamond property. Because
>
^{*} = →
_{β}
^{*}
this implies that βreduction is confluent. (See confluence proof for orthogonal TRS)
 Etareduction
 Motivation, definition and basic properties: termination and (local) confluence. No proofs.
 Reduction strategies
 Without proof: contraction of leftmost βredexes leads to a normal form if one exists.
 Lambda calculus as a programming language
 Booleans, pairs, Church numerals, fixedpoint combinators.
 Typed Lambda calculus

 Simply typed lambda calculus
 Simple types. Implicitly and explicitly typed terms. Type checking rules. Properties: 1. betareduction preserves
types ("subject reduction") (w/o proof). 2. betareduction terminates on typecorrect terms (w/o proof).
Thus betaequivalence is decidable for typecorrect terms (but has nonelementary complexity).
Corollary The simplytyped lambdacalculus can only represent total functions.
Thm Every computable functions is representable as a closed typecorrect lambdaterm whose only contants
are additional fixedpoint combinators (proof only sketched).
 Type inference
 The rules. Typecorrect terms no longer have a unique type but still a most general type. Proof by a concrete
Prologlike interpretation of the typing rules as backward computation rules.
 Letpolymorphism
 Universally quantified type schemas. Typing rules for "let" and for type schemas. Syntaxdirected typing rules
with builtin quantifier handling.
 CurryHoward isomorphism
 Types = formulas, lambdaterms = proofs, betareduction = proofreduction. Proof of the subterm property of
proofs in normal form. Proof of decidability of intuitionistic propositional logic via proofs in normal form.
Literature
Primary:
Additional:

Hendrik Pieter Barendregt.
The Lambda Calculus, its Syntax and Semantics, NorthHolland, 2nd edition, 1984

JeanYves 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.
LambdaCalculus and Combinators: An Introduction, Cambridge University Press, 2008