Prof. Tobias Nipkow, Sommersemester 2015
- TUM Online: Equational Logic and Lambda Calculus (IN2048)
- Lectures: Tuesday, 12:15 - 13:45 in HS3 00.06.011, and Wednesday, 8:30 - 10:00 in HS2 00.04.011
- Exercises: Wednesday, 10:15 - 11:45 in Konrad Zuse (MI 01.11.018),
- Start: 21.04.2015. First exercise: 22.4.2015
- Tutors: Lars Hupel, Johannes Hölzl
- 10.07.: The slots for the oral exam have been allocated. Please find them in TUMonline. The exam will take place in Prof. Nipkow's office: MI 00.09.055.
- 10.06.: The oral exam will take place on July 21st, between 09:00 and 12:00. Slots will be allocated as soon as registration for the exams is closed.
- 24.04.: The exercise session on April 29th has been re-scheduled to start 14:15 in room MI 00.09.038.
- 15.04.: The first exercise sheet will be published in week 2 and is due in week 3.
- There are no lectures in week 1. To compensate for that, the lectures in week 2 jump right in, without lengthy motivation. Read these 4 pages and the Wikipedia pages on Rewriting and Lambda Calculus for some motivation.
- 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.
- Excercise sheet 1 (tutorial solutions)
- Excercise sheet 2 (tutorial solutions)
- Excercise sheet 3 (tutorial solutions)
- Excercise sheet 4 (Templates for Homework 22: [hs] [ml], tutorial solutions)
- Excercise sheet 5 (Templates for Homework 27: [hs] [ml], tutorial solutions)
- Excercise sheet 6 (Template for Homework 33: [hs], tutorial solutions)
- Excercise sheet 7 (tutorial solutions)
- Excercise sheet 8 (tutorial solutions)
- Excercise sheet 9 (tutorial solutions)
- Excercise sheet 10 (tutorial solutions, Template for Homework 45: [hs])
- Excercise sheet 11 (tutorial solutions, Solution for Exercise 57: [thy])
- Excercise sheet 12 (tutorial solutions)
This course exclusively treats equational logic instead of the usual first-order logic. It combines the topics term-rewriting and lambda-calculus with a logical view.
Part I: Term Rewriting
- Abstract reduction systems
- Abstract reduction systems
- Basic definitions Thm Church-Rosser iff confluent. Thm For convergent reductions, two elements are equivalent iff their normal forms are equal.
- Well-founded Induction
- Thm Well-founded induction is valid iff the reduction terminates. Application: König's Lemma.
- Termination proofs
- Thm A finitely branching relation terminates iff it can be embedded into (N,>).
- Lexicographic orders
- Thm The lexicographic order on AxB terminates if the order on A and B terminate. Thm The lexicographic order on A* terminates if the order on A terminates.
- Multiset order
- Thm (Dershowitz and Manna) The multiset order terminates if the underlying order terminates.
- Equational Logic
- Terms and Substitutions
- Signature, term, position in term, subterm at position, replacement at position, substitution, composition of substitutions.
- Term Rewriting and Equational Logic
Identities, term rewriting (→E), equational logic (s ≈E t and E |- s ≈ t). Thm s ↔*E t iff s ≈E t.
Note that I defined equational logic with rule K (if s ≈E t then u[s]p ≈E u[t]p) but the book uses a different rule: if si ≈E ti for i=1,...,n then f(s1,...,sn) ≈E f(t1,...,tn). It can be shown easily that both rules are equivalent (in the presence of the other rules).
- Algebra. Validity and semantic consequence (|=). Thm (Birkhoff) E |- s ≈ t iff E |= s ≈ t.
- Equational Problems
Definition of word problem, unification problem and matching problem modulo E
- Word problems
- Undecidable for arbitrary E (Example: undecidable semigroup). Decidable for finite and convergent E.
- Congruence closure
Thm If E is finite and ground and
s ≈E t, then there is a proof of this fact that
involves only subterms of E, s, t.
Hence the word problem is decidable (in polynomial time) if E is finite and ground.
- Syntactic unification
- Basic definitions: the "more general" quasiorder on substitutions, most general unifier, idempotent substitution.
- Unification by transformation
- Transformation rules, soundness and completeness. Exponential worst case complexity.
- Termination is undecidable because TRS can simulate Turing machines and the Halting Problem for Turing machines is undecidable. Still undecidable for 1-rule TRS, and for TRS of 3 or more rules if all function symbols are unary. Open problem: is it decidable for 1 or 2 rules if all function symbols are unary?
- Termination is decidable for finite TRS where all right-hand sides are ground.
- Reduction orders, the interpretation method and polynomial interpretations.
- There is an annual Termination Competition
- Thm Confluence is undecidable for arbitrary finite TRSs.
- Newman's Lemma A terminating and localy confluent reduction is confluent.
- Critical Pair Lemma If all critical pairs of a TRS are joinable, the TRS is locally confluent.
- Knuth-Bendix Completion The completion algorithm. Example (groups): completion of (x.y).z → x.(y.z), 1.x → x, i(x).x → 1 generates the additional rules x.1 → x, i(1) → 1, x.i(x) → 1, i(x).(x.y) → y, x.(i(x).y) → y, i(i(x)) → x, i(x.y) → i(y).i(x).
- Thm Orthogonal TRSs (no critical pairs, left-linear) are confluent.
Part II: 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.
- Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press.
- Lecture notes on Lambda Calculus
- Jürgen Avenhaus. Reduktionssyteme, Springer, 1995
- 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