Lambda Calculus
News
 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