Newman's Lemma
   HOME

TheInfoList



OR:

In
theoretical computer science Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation. It is difficult to circumscribe the theoretical areas precisely. The Associati ...
, specifically in
term rewriting In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduc ...
, Newman's lemma, also commonly called the diamond lemma, is a criterion to prove that an
abstract rewriting system In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting ...
is
confluent Confluent, Inc. is an American technology company headquartered in Mountain View, California. Confluent was founded by Jay Kreps, Jun Rao and Neha Narkhede on September 23, 2014, in order to commercialize an open-source streaming platform Apa ...
. It states that local confluence is a sufficient condition for confluence, provided that the system is also terminating. This is useful since local confluence is usually easier to verify than confluence. The lemma was originally proved by
Max Newman Maxwell Herman Alexander Newman, FRS (7 February 1897 – 22 February 1984), generally known as Max Newman, was a British mathematician and codebreaker. His work in World War II led to the construction of Colossus, the world's first operatio ...
in 1942. A considerably simpler proof (given below) was proposed by
Gérard Huet Gérard Pierre Huet (; born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and ...
. A number of other proofs exist.


Statement and proof

The lemma is purely combinatorial and applies to any relation. Owing to the context where it is commonly applied, it is stated below in the terminology of
abstract rewriting system In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting ...
s (this is simply a set whose elements are called terms, equipped with a relation \to called reduction, and see the corresponding article for definitions of termination, confluence, local confluence and normal forms). Newman's lemma: If an abstract rewriting system is terminating and locally confluent, then it is confluent. As a corollary, every term has a ''unique'' normal form. Proof: We prove by
well-founded induction In mathematics, a binary relation is called well-founded (or wellfounded or foundational) on a set or, more generally, a class if every non-empty subset has a minimal element with respect to ; that is, there exists an such that, for every , ...
on u along \to that every diagram can be extended to a diagram where the dotted arrows represent sequences of arbitrarily many reductions by \to. If u = v or u = w, this is trivial. Otherwise, we have at least one reduction on each side: By local confluence, this diagram can be extended to: then by induction hypothesis on v_0: and finally, by induction hypothesis on w_0:


Eriksson's polygon property lemma

A related result was shown by Kimmo Eriksson in 1993. Recall that an abstract rewriting system is locally confluent if for any two reductions a \to b and a \to c, there exists d such that b \to^* d and c \to^* d. If additionally it is required that the reduction chains b \to^* d and c \to^* d have the same length, then the system is said to have the polygon property. Examples of rewriting systems with the polygon property include
bubble sort Bubble sort, sometimes referred to as sinking sort, is a simple sorting algorithm that repeatedly steps through the input list element by element, comparing the current element with the one after it, Swap (computer science), swapping their values ...
and the
chip-firing game The chip-firing game is a one-player game on a graph which was invented around 1983 and since has become an important part of the study of structural combinatorics. Each vertex has the number of "chips" indicated by its state variable. On each f ...
. Eriksson's polygon property lemma shows that if an abstract rewriting system is terminating and has the polygon property, then not only is it confluent (according to Newman's lemma), but additionally every terminating chain of reductions from a given state has the same length.


References

* * * * * * * * * *


External links

* {{planetmath, urlname=diamondlemma, title=Diamond lemma Wellfoundedness Lemmas Rewriting systems