ISR 2008

3rd International School on Rewriting

21 – 26 July 2008, Obergurgl, Austria

Program – Track B – Abstract Rewriting

Lecturer

Vincent van Oostrom

Introduction

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.

Material