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 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).
• 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.