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.

Diamond lemma

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: a0 → a1 → a2 → a3 → ... . In the terminology of rewriting systems, → is terminating. 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.

Textbooks