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 rescheduled 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 firstorder logic. It combines the topics termrewriting and lambdacalculus with a logical view.
Part I: Term Rewriting
 Abstract reduction systems

 Abstract reduction systems
 Basic definitions Thm ChurchRosser iff confluent. Thm For convergent reductions, two elements are equivalent iff their normal forms are equal.
 Wellfounded Induction
 Thm Wellfounded 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_{1},...,s_{n}) ≈_{E} f(t_{1},...,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 1rule 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 righthand 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.
 KnuthBendix 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, leftlinear) are confluent.
Part II: Lambda Calculus
 Untyped Lambda calculus

 Syntax
 Terms, notational conventions, Currying, static binding, free and bound variables, substitution, alphaconversion.
 Betareduction
 Definition of betareduction. Definition of parallel reduction >. Proof that > has the diamond property. Because >^{*} = →_{β}^{*} this implies that βreduction is confluent. (See confluence proof for orthogonal TRS)
 Etareduction
 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, fixedpoint combinators.
 Typed Lambda calculus

 Simply typed lambda calculus
 Simple types. Implicitly and explicitly typed terms. Type checking rules. Properties: 1. betareduction preserves types ("subject reduction") (w/o proof). 2. betareduction terminates on typecorrect terms (w/o proof). Thus betaequivalence is decidable for typecorrect terms (but has nonelementary complexity). Corollary The simplytyped lambdacalculus can only represent total functions. Thm Every computable functions is representable as a closed typecorrect lambdaterm whose only contants are additional fixedpoint combinators (proof only sketched).
 Type inference
 The rules. Typecorrect terms no longer have a unique type but still a most general type. Proof by a concrete Prologlike interpretation of the typing rules as backward computation rules.
 Letpolymorphism
 Universally quantified type schemas. Typing rules for "let" and for type schemas. Syntaxdirected typing rules with builtin quantifier handling.
 CurryHoward isomorphism
 Types = formulas, lambdaterms = proofs, betareduction = proofreduction. 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, NorthHolland, 2nd edition, 1984
 JeanYves 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. LambdaCalculus and Combinators: An Introduction, Cambridge University Press, 2008