Newman's lemma
Encyclopedia
In the theory of rewriting
systems, Newman's lemma
states that a terminating (or strongly normalizing) abstract rewriting system
(ARS), that is, one in which there are no infinite reduction sequences, is confluent
if it is locally confluent. In fact a terminating ARS it is confluent precisely when it is locally confluent.
Today, this is seen as a purely combinatorial result based on well-foundedness due to a proof of Gérard Huet
in 1980. Newman's original proof was considerably more complicated.
An earlier proof of the theorem was given by Church and Rosser.
Rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
systems, Newman's lemma
Lemma (mathematics)
In mathematics, a lemma is a proven proposition which is used as a stepping stone to a larger result rather than as a statement in-and-of itself...
states that a terminating (or strongly normalizing) abstract rewriting system
Abstract rewriting system
In mathematical logic and theoretical computer science, an abstract rewriting system is a formalism that captures the quintessential notion and properties of rewriting systems...
(ARS), that is, one in which there are no infinite reduction sequences, is confluent
Confluence (term rewriting)
In computer science, confluence is a property of rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.- Motivating example :Consider...
if it is locally confluent. In fact a terminating ARS it is confluent precisely when it is locally confluent.
Today, this is seen as a purely combinatorial result based on well-foundedness due to a proof of Gérard Huet
Gérard Huet
Gérard Pierre Huet is a French computer scientist.- Biography :Gérard Huet graduated from the Université Denis Diderot , Case Western Reserve University, and the Université de Paris....
in 1980. Newman's original proof was considerably more complicated.
An earlier proof of the theorem was given by Church and Rosser.
Textbooks
- Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink)
- Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998 (book weblink)
- John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, ISBN 9780521899574, chapter 4 "Equality".