Equational Logic
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
 
News
- 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.
 
Excercises
- 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)
 
Contents
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). - Semantics
 - 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
 - 
  
- 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
 
 - Confluence
 - 
  
- 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
 - 
 
- 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:- 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