PlanetMath: diamond lemma

The diamond lemmas constitute a class 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 structure and basic idea -- the “diamond” condition from which they inherit their name.

Newman's Diamond Lemma

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

The typical case to which one applies this theorem is that

is a set of formal terms on which one wishes to define an equivalence relation $\sim$ . The $\rightarrow$ relation encodes a set of “elementary” equivalences -- an example in standard algebra of such an elementary equivalence might be the instance $a(b +\nobreak c) \rightarrow ab + ac$ of the distributivity axiom -- that generate the wanted $\sim$ . It is techincally possible to define the equivalence $\sim$ as the reflexive-transitive-symmetric closure of $\rightarrow$ , but since

is typically infinite that definition does not lead to an effective method for determining whether $x \sim y$ . However when the relation $\rightarrow$ satisfies the conditions in Theorem 1, there does exist an algorithm which given $\rightarrow$ determines whether two arbitrary elements are related by $\sim$ .

In a computational setting, the interpretation of $x \rightarrow y$ is usually that there exists a “one-step simplification” that converts the expression

to the expression

. The corresponding interpretation of $x \stackrel{*}{\rightarrow} y$ is thus that there exists a finite sequence of “simplifications” that converts

. The formal term used for “simplifications” in this sense is reductions, so $x \stackrel{*}{\rightarrow} y$ is read as “

reduces to

” or “

can be reduced to

”.

The theorem has several immediate applications -- first of all that there is a unique function $N\colon X \longrightarrow X$ which sends arbitrary elements of

to their normal forms -- and this leads to a test for whether arbitrary elements are equivalent.

Proof. Denote by $\stackrel{*}{\rightarrow}$ the reflexive-transitive closure of $\rightarrow$ and denote by $\leftrightarrow$ the symmetrisation of $\rightarrow$ . If

then obviously $x \stackrel{*}{\rightarrow} N(x) = N(y) \stackrel{*}{\leftarrow} y$ and thus $x \sim N(x) \sim y$ as claimed. If conversely $x \sim y$ then there must exist some sequence

$\displaystyle z_0 \leftrightarrow z_1 \leftrightarrow \dotsb \leftrightarrow z_{n-1} \leftrightarrow z_n$

where $z_0,\dotsc,z_n \in X$ ,

, and

. For every

one of $z_k \rightarrow z_{k+1}$ and $z_k \leftarrow z_{k+1}$ must hold. In the former case $z_k \stackrel{*}{\rightarrow} z_{k+1} \stackrel{*}{\rightarrow} N(z_{k+1})$ and thus by transitivity $z_k \stackrel{*}{\rightarrow} N(z_{k+1})$ , but this means $N(z_{k+1})$ is a normal form also of

. In the latter case one similarly shows that

is a normal form of $z_{k+1}$ . Either way it follows from the uniqueness of the normal form that $N(z_k) = N(z_{k+1})$ . Thus $N(z_0) = N(z_1) = \dotsb = N(z_{n-1}) = N(z_n)$ and hence

as claimed. $\qedsymbol$

Another application of normal forms is to serve as representatives of the equivalence classes of

. Many mathematical constructions of algebraic structures (e.g. that of a quotient of a group) end up producing a set $X/{\sim}$ of equivalence classes of some given set

, but these are as a rule unfeasible for computational purposes. What one can do instead is to choose an element from each equivalence class and use these as representatives of their equivalence classes. When normal forms are known to be unique, there trivially exists a bijection from

How does one know that the normal form map

is effective, though? This is because of the terminating property on the binary relation in Theorem 1.

The primary consequence of being terminating is that $\stackrel{*}{\rightarrow}$ is well-founded, and it is no surprise that Theorem 1 is proved using well-founded induction. Being terminating is also what guarantees that the following algorithm “terminates”.

For relations $\rightarrow$ which satisfy the descending chain condition and have unique normal forms, Algorithm 1 and Lemma 1 combine to an algorithm for deciding the relation $\sim$ . A typical problem is however that uniqueness of the normal form is a global condition that is very hard to establish using elementary methods. Theorem 1 offers an equivalent local condition that often is straightforward to verify in each particular case by explicit calculations.

Diamond lemmas for algebraic structures

One disadvantage of the basic diamond lemma (Theorem 1) is that it requires all reductions to be explicit, whereas the average mathematician probably expects it to handle reduction schemas transparently. To illustate the difference, consider again the reduction $a(b +\nobreak c) \rightarrow ab+ac$ . This does not imply $(d +\nobreak e)(b +\nobreak c) \rightarrow (d +\nobreak e)b + (d +\nobreak e)c$ , or even $2(b +\nobreak c) \rightarrow 2b + 2c$ , because all three left hand sides are distinct as formulae (i.e., as elements of

). In order to let

, and

be arbitrary, one need to explicitly state that e.g. “ $a(b +\nobreak c) \rightarrow ab+ac$ for all well-formed formulae

, and

”. Even this may be less than what was intended, since it is often the case that one wants it to follow from $a(b +\nobreak c) \rightarrow ab+ac$ also that $f\bigl( a(b +\nobreak c) \bigr) \rightarrow f(ab +\nobreak ac)$ for arbitrary functionalised expressions

. Theorem 1 requires its user to take care of such details explicitly.

Moreover, the conditions in Theorem 1 are stated about arbitrary elements of

, so even if one employs schemas in the definition of $\rightarrow$ , it is necessary to verify that condition 1 holds for every concrete triple

of elements of

such that $b \leftarrow a \rightarrow c$ . This too can be done collectively using proof schemas, but the situation is complicated enough that it is often far from clear whether all cases have been checked. It is furthermore common that trivial verifications of a syntactic origin outnumber the verifications that have interesting mathematical content. This makes it less likely that mathematicians will actually bother to produce a complete proof, and more likely that they will skip it altogether by resorting to the notorious “It is easy to see that ...”

Finally, it is not always the case than one just wants an equivalence relation. When the base set

has an established algebraic structure one typically rather wants $\sim$ to be a congruence relation, but the basic diamond lemma can of course not take such sophistications into account. Therefore there exist also a number of specialised diamond lemmas which are tailored to particular algebraic structures and can make do with verifications of significantly fewer cases than the basic diamond lemma.

Newman's Diamond Lemma

Diamond lemmas for algebraic structures

Bibliography