Lambda Calculus

Prof. Tobias Nipkow, Sommersemester 2015

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, alpha-conversion.
Beta-reduction
Definition of beta-reduction. Definition of parallel reduction >. Proof that > has the diamond property. Because >* = →β* this implies that β-reduction is confluent. (See confluence proof for orthogonal TRS)
Eta-reduction
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, fixed-point combinators.
Typed Lambda calculus
Simply typed lambda calculus
Simple types. Implicitly and explicitly typed terms. Type checking rules. Properties: 1. beta-reduction preserves types ("subject reduction") (w/o proof). 2. beta-reduction terminates on type-correct terms (w/o proof). Thus beta-equivalence is decidable for type-correct terms (but has non-elementary complexity). Corollary The simply-typed lambda-calculus can only represent total functions. Thm Every computable functions is representable as a closed type-correct lambda-term whose only contants are additional fixed-point combinators (proof only sketched).
Type inference
The rules. 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 isomorphism
Types = formulas, 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

Primary: Additional:
  • 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