Automatically proving confluence of non-terminating rewrite systems via a generalized Newman-style approach
Prof. Bernhard Gramlich
- School of Computer Science, TU Wien, Austria
- Data e ora
martedì 11 aprile 2006
- caffè, tè & C. ore 17.00
Ca' Vignal 3 - Piramide,
- Data pubblicazione
21 marzo 2006
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.