6th International School on Rewriting >> Introduction to Term Rewriting

6th International School on Rewriting

July 16th - 20th, 2012. Valencia, Spain

ITR: Introduction to Term Rewriting

Term rewriting is a very simple and general model of computation at the heart of Computer Science which:

  • Is an essential technique in equational logic and in rewriting logic, and also in concurrency.
  • Can be directly used to write declarative programs in both:
    • functional programming, and
    • concurrent and distributed programming.
  • Can give formal semantics to conventional programming languages.
  • Is at the heart of various theorem proving and model checking formal verification techniques.

The present Introduction to Term Rewriting course at ISR 2012 will cover the following topics:

  1. Equational logic, term rewriting systems, and functional programming in Maude.
  2. Rewriting modulo axioms.
  3. Confluence, termination, and sufficient completeness of term rewriting systems.
  4. Rewriting logic and declarative concurrent programming in Maude.
  5. Deductive and model checking verification of temporal logic properties of Maude concurrent programs and of imperative concurrent programs.

More in detail, the contents of the 17 lectures planned for the course is as follows:

  1. Lecture 1: Introduction to the course.
  2. Lecture 2: Unsorted, many-sorted and order-sorted signatures and algebras.
  3. Lecture 3: Term algebras. Substitutions. Equations and conditional equations. Conditional term rewriting and term rewriting systems. Confluence and (unconditional) termination. Canonical forms and the canonical term algebra. Operational and denotational semantics of equational programs. Sufficient completeness.
  4. Lecture 4: Order-sorted equational logic. Soundness of term rewriting as an equational deduction mecha- nism. Completeness of term rewriting under the confluence assumption. Semi-decidability and decidability of equational properties by rewriting.
  5. Lecture 5: Rewriting modulo axioms of associativity and/or commutativity and/or identity. The canonical term algebra modulo axioms. Sufficient completeness modulo axioms.
  6. Lecture 6: Confluence versus ground confluence. The Maude Church-Rosser Checker. Mathematical analysis of local confluence.
  7. Lecture 7: Syntactic unification and unification modulo axioms. Critical pairs and checking local confluence. Tree automata and checking sufficent completeness. The Maude Sufficient Completeness Checker.
  8. Lecture 8: Termination and reduction orderings. Polynomial orderings. The lexicographic path ordering. Termination modulo axioms. Operational termination of conditional term rewriting systems. The Maude Termination Tool.
  9. Lecture 9: Rewriting logic semantics of concurrent systems. Rewriting logic semantis of automata and Petri nets. Maude system modules and the rewrite and search commands.
  10. Lecture 10: Rewriting logic semantics of concurrent object systems. The inference rules of rewriting logic; their logical and computational meanings.
  11. Lecture 11: Reachability models of rewrite theories. Executability conditions and coherence. The canonical reachability model of a rewrite theory as its denotational semantics. Invariants.
  12. Lecture 12: Model checking invariants through search. Examples. Bounded model checking.
  13. Lecture 13: Deductive verification of safety properties for a rewrite theory. The Invariant Analyzer tool.
  14. Lecture 14: Linear Temporal Logic (LTL) and its Kripke sructure semantics. The Kripke structure associated to a rewrite theory.
  15. Lecture 15: Model checking verification of LTL formulas. The Maude LTL model checker. Examples.
  16. Lecture 16: Rewriting logic semantics of concurrent programming laguages and formal verification of imperative concurrent programs.
  17. Lecture 17: A survey of rewriting logic and its applications.

Readings. The primary readings are the lecture notes themselves. Additional readings are listed in the course web page and are available in the memory stick distributed to ISR 2012 participants.

Active Participation. Active participation is strongly encouraged.

Homework, Final, and Honor Code. There are two homework assignments that each participant is expected to complete. Solutions to these assignments will be explained in the Exercises in Term Rewriting lectures. Homeworks 2 and 3 are simultaneously the final exam for the course. Course participants are trusted on their honor to work exclusively by themselves in the solution of each homework assignments, which can be completed anywhere at each participant's convenience before the due dates and times. Violation of this trust is sufficient ground for not obtaining the final ISR 2012 certificate of studies for Track A.

<< Back to Previous Page.