Generalizing Newman's Lemma for Left-Linear Rewrite Systems
Authors
Bernhard Gramlich and Salvador Lucas
Abstract
Confluence criteria for non-terminating rewrite systems are
known to be rare and notoriously difficult to obtain. Here we prove a
new result in this direction. Our main result is a generalized version
of Newman's Lemma for left-linear term rewriting 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.