Remy Haemmerle, Post-doctoral Researcher, Technical University of Madrid (UPM), Spain
The standard method to prove confluence of term rewriting system (TRS) is based on the study of joinability of critical pairs. This notion of critical pairs obtained by superposing the left-hand sides of rewriting rules have been adapted to a wide variety of rewriting systems, ranging from conditional TRS, higher-order rewriting, graph rewriting and constraint handling rules. However, although there is no general definition of an abstract notion of critical pairs from which the concrete definition could be obtained as particular instances.
In this talk I will first recall some classical abstract properties about confluence. Then I will present an abstract notion of critical pair for arbitrary reduction relations provided with context operators and show how this notion applied to TRS and multiset rewriting.