3rd International School on Rewriting
21 – 26 July 2008, Obergurgl, Austria
Program – Track B – Abstract Rewriting
LecturerVincent van Oostrom
Termination of term rewriting systems can (always) be shown by interpreting them into so-called monotone algebras. While abstracting from the terms (into objects) these provide (well-founded order) structure to the steps. Many heuristics for finding interpretations have been developed.
In these lectures we focus on the analog abstract structures for properties other than termination, e.g. confluence, orthogonality, standardization, ... In particular, confluence of term rewriting systems can (always) be shown by interpreting them into so-called decreasing diagrams. While abstracting from the terms (into objects) these provide (decreasing diagram) structure to the steps. We give heuristics for finding appropriate interpretations to deal with concrete confluence problems.