Automatically proving confluence of non-terminating rewrite systems via a generalized Newman-style approach

Supervisor
Prof. Bernhard Gramlich - School of Computer Science, TU Wien, Austria
Date and time
Tuesday, April 11, 2006 at 5:30 PM - caffè, tè & C. ore 17.00
Place
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
Maria Paola Bonacina
External reference
Publication date
March 21, 2006
Department
 

Summary

Confluence is, besides termination, the most fundamental property of (term) rewrite systems. For a long time it is well-known how to prove confluence of terminating systems via Newman's Lemma. Yet, for non-terminating rewrite systems confluence criteria and proof techniques are very rare and notoriously difficult to obtain. Here we present a new approach in this direction. Our main result is a generalized version of Newman's Lemma for left-linear rewrite systems that does not need a full termination assumption. We discuss its relationships to previous confluence criteria, its restrictions,examples of application as well as open problems. The whole approach is developed in the (more general) framework of context-sensitive rewriting which thus turns out to be useful also for ordinary (context-free) rewriting.
In the talk, which is based on recent joint work with Salvador Lucas (Valencia, Spain), we will start with an overview of known confluence criteria for (possibly) non-terminating rewrite systems.





© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234