mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...

, in the theory of

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 ...

systems, Newman's

lemma Lemma may refer to: Language and linguistics * Lemma (morphology), the canonical, dictionary or citation form of a word * Lemma (psycholinguistics), a mental abstraction of a word about to be uttered Science and mathematics * Lemma (botany), ...

, also commonly called the diamond lemma, states that a terminating (or strongly normalizing)

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 ...

(ARS), that is, one in which there are no infinite reduction sequences, is

confluent In geography, a confluence (also: ''conflux'') occurs where two or more flowing bodies of water join to form a single channel. A confluence can occur in several configurations: at the point where a tributary joins a larger river (main stem); o ...

if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent. Equivalently, for every

binary relation In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over sets and is a new set of ordered pairs consisting of elements in and in ...

with no decreasing infinite chains and satisfying a weak version of the diamond property, there is a unique

minimal element In mathematics, especially in order theory, a maximal element of a subset ''S'' of some preordered set is an element of ''S'' that is not smaller than any other element in ''S''. A minimal element of a subset ''S'' of some preordered set is defin ...

in every connected component of the relation considered as a

graph Graph may refer to: Mathematics *Graph (discrete mathematics), a structure made of vertices and edges **Graph theory, the study of such graphs and their properties *Graph (topology), a topological space resembling a graph in the sense of discre ...

. Today, this is seen as a purely combinatorial result based on

well-foundedness In mathematics, a binary relation ''R'' is called well-founded (or wellfounded) on a class ''X'' if every non-empty subset ''S'' ⊆ ''X'' has a minimal element with respect to ''R'', that is, an element ''m'' not related by ''s&nb ...

due to a proof of Gérard Huet in 1980. Newman's original proof was considerably more complicated.

Diamond lemma

In general, Newman's lemma can be seen as a

combinatorial Combinatorics is an area of mathematics primarily concerned with counting, both as a means and an end in obtaining results, and certain properties of finite structures. It is closely related to many other areas of mathematics and has many ap ...

result about binary relations → on a set ''A'' (written backwards, so that ''a'' → ''b'' means that ''b'' is below ''a'') with the following two properties: * → is a

well-founded relation In mathematics, a binary relation ''R'' is called well-founded (or wellfounded) on a class ''X'' if every non-empty subset ''S'' ⊆ ''X'' has a minimal element with respect to ''R'', that is, an element ''m'' not related by ''s& ...

: every non-empty subset ''X'' of ''A'' has a minimal element (an element ''a'' of ''X'' such that ''a'' → ''b'' for no ''b'' in ''X''). Equivalently, there is no infinite chain . In the terminology of rewriting systems, → is terminating. * Every covering is bounded below. That is, if an element ''a'' in ''A'' covers elements ''b'' and ''c'' in ''A'' in the sense that and , then there is an element ''d'' in ''A'' such that and , where denotes the reflexive

transitive closure In mathematics, the transitive closure of a binary relation on a set is the smallest relation on that contains and is transitive. For finite sets, "smallest" can be taken in its usual sense, of having the fewest related pairs; for infinite ...

of →. In the terminology of rewriting systems, → is locally confluent. The lemma states that if the above two conditions hold, then → is confluent: whenever and , there is an element ''d'' such that and . In view of the termination of →, this implies that every connected component of → as a graph contains a unique minimal element ''a'', moreover for every element ''b'' of the component. Paul M. Cohn, (1980) ''Universal Algebra'', D. Reidel Publishing, (''See pp. 25–26'')

Notes

References

* M. H. A. Newman. ''On theories with a combinatorial definition of "equivalence"''. Annals of Mathematics, 43, Number 2, pages 223–243, 1942. *

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, 199
(book weblink)
* John Harrison, ''Handbook of Practical Logic and Automated Reasoning'', Cambridge University Press, 2009, , chapter 4 "Equality".

External links

*
"Newman's Proof of Newman's Lemma", a PDF on the original proof
{{webarchive, url=https://web.archive.org/web/20170706084416/http://www.phil.uu.nl/~oostrom/publication/pdf/newmansproof.pdf , date=July 6, 2017 Wellfoundedness Lemmas Rewriting systems