Lambda Calculus

Prof. Tobias Nipkow, Winter semester 2017/18

General Notice



Lambda Calculus

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.


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