- 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.
- Untyped Lambda calculus
Terms, notational conventions, Currying, static binding, free and bound variables, substitution, alpha-conversion.
- 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)
- 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.
- 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.
- Hendrik Pieter Barendregt. The
its Syntax and Semantics, North-Holland, 2nd edition, 1984
- Jean-Yves Girard, Yves
and Paul Taylor. Proofs
and Types, Cambridge Tracts in Theoretical Computer Science,
University Press, 1989
- Chris Hankin. An
Introduction to Lambda Calculi for Computer Scientists, King's
College Publications, 2004
- J. Roger Hindley and
to Combinators and Lambda Calculus, Cambridge University Press, 1986
- J. Roger Hindley and
Seldin. Lambda-Calculus and Combinators: An Introduction, Cambridge University Press, 2008