diamond lemma (original) (raw)

The diamond lemmas constitute a of results about the existenceof 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 relations.

Theorem 1.

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

1. 1. For all a,b,c∈X such that a→b and a→c, then b and c are joinable.
2. 1. Every a∈X has a unique normal form.

Condition 1 can be graphically drawn as