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

Relatore
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

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

Referente
Maria Paola Bonacina

Referente esterno

Data pubblicazione
21 marzo 2006

Dipartimento
 

Riassunto

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.
ornamento
Inizio pagina