Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Newman's lemma
Summary
In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond 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 is confluent precisely when it is locally confluent.
Equivalently, for every binary relation with no decreasing infinite chains and satisfying a weak version of the diamond property, there is a unique minimal element in every connected component of the relation considered as a graph.
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.
In general, Newman's lemma can be seen as a combinatorial 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: 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 a0 → a1 → a2 → a3 → .... 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 a → b and a → c, then there is an element d in A such that b d and c d, where denotes the reflexive transitive closure of →. In the terminology of rewriting systems, → is locally confluent.
The lemma states that if the above two conditions hold, then → is confluent: whenever a b and a c, there is an element d such that b d and c d. In view of the termination of →, this implies that every connected component of → as a graph contains a unique minimal element a, moreover b a for every element b of the component.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.