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

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.
Prof. Bernhard Gramlich - School of Computer Science, TU Wien, Austria

Data e ora
martedì 11 aprile 2006 alle ore 17.30 - caffè, tè & C. ore 17.00

Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Maria Paola Bonacina

Data pubblicazione
21 marzo 2006


Offerta formativa