Equational Logic

Prof. Tobias Nipkow, Sommersemester 2012

• Lectures: Monday and Tuesday, 14:15 - 15:45 in HS2 (00.04.011) HS2 00.04.011
• Exercises: Friday 11:00 - 13:00 in Alonzo Church (MI 01.09.014)
  
  Exceptions: 11 May and 6 July in 00.09.055 Alan Turing (MI 00.09.055)
• Start: 16.04.2012. First exercise: 20.4.2012
• Tutors: Brian Huffman Peter Lammich

News

• Sept 24: Timetable for repetition exam available
• July 19: More information on exam available
• July 16: Bugfix in solution to exercise 10.1 (lambda calculus interpreter)
• July 13: Exercise sheet 12 is now online
• The written exam is on 8.8.2012 - register now
• July 9: Example solutions for sheets 2,4,6,8,10 will be distributed in the lecture today and tomorrow. The other sheets are to follow soon.
• July 9: Solution for exercise 10.1 is online
• July 9: Exercise sheet 11 is now online
• June 29: Exercise sheet 10 is out
• June 21: Exercise sheet 9 is out
• June 8: Exercise sheet 7 is out
• The tutorial for the logics lecture on June, 1st is canceled. The deadline for the homework is extended to the next tutorial on June, 8th.
• May 10: Exercise sheet 4 is out
• May 4: Exercise sheet 3 is out
• We changed the room for exercises! From Friday, 27th April, exercises will be in Alonzo Church (MI 01.09.014)
• April 25: Exercise sheet 2 is out
• April 20: Exercise sheet 1 is out
• First exercise is on April 20, 2012

Contents

This lecture 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 s_i ≈_E t_i for i=1,...,n then f(s₁,...,s_n) ≈_E f(t₁,...,t_n). 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).
• 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.

Material

Exercises Exercise 1 Exercise 2 Exercise 3 Exercise 4 Exercise 5 Exercise 6 No sheet for June, 1st Exercise 7 Exercise 8 Exercise 9 Exercise 10    Exercise 11 Exercise 12

If you use the Mercurial version control system, you can synchronize these files automatically: hg clone https://www4.in.tum.de/~lammich/hg/logics_website
[ view changelog ]

Exam

 

Timetable for repetition exam (Wiederholunsgprüfung) for Equational Logic and Lambda Calculus on 2. October 2012 in Prof. Nipkow's office (01.11.058):

9:00 Guni
9:30 Grebenshchikov
10:00 Wermser
10:30 Kastenmayer
11:00 Gaina

On 8.8.2012 there will be a written exam. It will last 120 minutes. You are allowed to bring one A4 sheet with your notes into the exam, books are not allowed.

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.

Literature

Primary:

• Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press.
• Skript zur Vorlesung Lambda Kalkül
• Lecture notes on Lambda Calculus

Additional:

• 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