diamond lemma


The diamond lemmas constitute a of results about the existence of a unique normal form. Diamond lemmas exist in many diverse areas of mathematics, and as a result their technical contents can be quite different, but they are easily recognisable from their overall and basic idea — the “diamond” condition from which they inherit their name.

1 Newman’s Diamond Lemma

The basic diamond lemma, that of Newman [Newman], is today most easily presented in of binary relationsMathworldPlanetmath.

Theorem 1.

Let X be a set and let be a binary relation on X. If is terminating, then the following conditions are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath:

  1. 1.

    For all a,b,cX such that ab and ac, then b and c are joinable.

  2. 2.

    Every aX has a unique normal form.

Condition 1 can be graphically drawn as

\xymatrix@-2ex&a\xy@@ix@