MPRI, 24 hours, 3 credits (1 homework + 1 exam) [serveur pédagogique]

**Schedule:** Thursday 8:30-12:45, from 16 November 2017 to 18 January 2018.

**Place:** ENS Cachan, Cournot building, room 321

**Staff:** Frédéric Blanqui (lectures, 8:30-10:30) and Alessio Mansutti (exercises, 10:45-12:45)

Rewriting theory is the study of relations and, in particular, relations on symbolic expressions (terms). Relations can for instance be used to model transition systems, operational semantics, computation rules, and decide equational theories.

Term rewriting is based on the notion of pattern matching. Programming languages like OCaml and Haskell, or proof assistants like Agda or Coq use a restricted form of pattern matching. Programming languages like Maude and proof assistants like Dedukti allow a more general form of pattern-matching.

Two properties will be of particular interest for us: termination (there is no infinite sequence of rewrite steps) and confluence (the order of rewrite steps does not matter).

This course aims at introducing the fundamentals of rewriting theory, and in particular term rewriting systems, and some basic termination and confluence results and techniques used in nowadays state-of-the-art termination and confluence automated provers.

**Planning:**

- 16 November: term rewriting, F-algebra, interpretation-based reduction orders [Lecture 1] [Exercises 1] [Solutions 1]
- 23 November: well-founded induction, lexicographic ordering, multiset ordering, RPO [Lecture 2] [Exercises 2] [Solutions 2]
- 30 November: dependency pairs, dependency graph [Lecture 3] [Exercises 3] [Solutions 3] [Homework] to be returned on
**21 December** - 7 December: unification, critical pairs, Knuth-Bendix completion [Lecture 4] [Exercises 4] [Solutions 4]
- 14 December: orthogonal systems, confluence by decreasing diagrams [Lecture 5] [Exercises 5] [Solutions 5]
- 21 December: non-modularity of termination, incremental termination proofs, well-quasi-orders, [Lecture 6] [Exercises 6] [Solutions 6]
**deadline to return homework** - 11 January: introduction to deduction modulo rewriting by
**invited speaker**Gilles Dowek, and demonstration of termination and confluence tools [Exercises 7] [Solutions 7] - 18 January:
**exam**(no TD) [Exam 2016]

**Online termination, confluence or completion tools:**

More tools are available on:

**Related lectures:** Well quasi-orders for algorithms, Gilles Dowek's lecture on proofs in theories (every two years, next in 2018-2019)

Last updated on 8 February 2018. Come back to main page.