diamond lemma

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

1 Newman’s Diamond Lemma

The basic diamond lemma, that of Newman [Newman], is today mosteasily presented in of binary relations.

Theorem 1.

Let $X$ be a set and let $\mathrm{\to }$ be a binary relation on $X$.If $\mathrm{\to }$ is terminating, then the following conditions are equivalent:

1. For all $a,b,c\in X$ such that $a\to b$ and $a\to c$, then $b$ and $c$ are joinable.

2. Every $a\in X$ has a unique normal form.

Condition 1 can be graphically drawn as