IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2008 > Critical Pairs and Confluence of Arbitrary Reduction Relations

Remy Haemmerle

Tuesday, May 13, 2008

11:00am Meeting room 302 (Mountain View), level 3

Remy Haemmerle, Post-doctoral Researcher, Technical University of Madrid (UPM), Spain

Critical Pairs and Confluence of Arbitrary Reduction Relations

Abstract:

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.