|
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.
The basic diamond lemma, that of Newman [3], is today most easily presented in terms of binary relations.
Theorem 1 Let be a set and let
be a binary relation on . If
is terminating, then the following conditions are equivalent:
- For all
such that
and
, then and are joinable.
- Every
has a unique normal form.
Condition 1 can be graphically drawn as
where
denotes the reflexive transitive closure of
. This is the “diamond” from which the result derives its name -- not crystallised carbon, but merely a square standing on one corner. In relation to this picture, what the condition says is that whenever one has
forming the top two sides of such a diagram, there is a fourth corner which completes the diamond.
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 . The
relation encodes a set of “elementary” equivalences -- an example in standard algebra of such an elementary equivalence might be the instance
of the distributivity axiom -- that generate the wanted . It is techincally possible to define the equivalence as the reflexive-transitive-symmetric closure of
, but since is typically infinite that definition does not lead to an effective method for determining whether . However when the relation
satisfies the conditions in Theorem 1, there does exist an algorithm which given
determines whether two arbitrary elements are related by .
In a computational setting, the interpretation of
is usually that there exists a “one-step simplification” that converts the expression to the expression . The corresponding interpretation of
is thus that there exists a finite sequence of “simplifications” that converts to . The formal term used for “simplifications” in this sense is reductions, so
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
which sends arbitrary elements of to their normal forms -- and this leads to a test for whether arbitrary elements are equivalent.
Lemma 1 Let be a set and
a binary relation on such that all elements of has a unique normal form with respect to
. Denote by the reflexive transitive symmetric closure of
and denote by the function
which sends every element to its normal form with respect to
. Then for all ,
if and only if . |
(1) |
Proof. Denote by
 the reflexive-transitive closure of
 and denote by
 the symmetrisation of
 . If  then obviously
 and thus
 as claimed. If conversely  then there must exist some sequence
where
 ,  , and  . For every  one of
 and
 must hold. In the former case
 and thus by transitivity
 , but this means
 is a normal form also of  . In the latter case one similarly shows that  is a normal form of  . Either way it follows from the uniqueness of the normal form that
 . Thus
 and hence  as claimed. 
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 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
to given by
, and its inverse can thanks to Lemma 1 be defined in terms of the normal form map as
.
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
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
which satisfy the descending chain condition and have unique normal forms, Algorithm 1 and Lemma 1 combine to an algorithm for deciding the relation . 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.
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
. This does not imply
, or even
, 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. “
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
also that
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
, it is necessary to verify that condition 1 holds for every concrete triple of elements of such that
. 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 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.
The most familiar such result is probably the diamond lemma for ring theory of Bergman [1], also known as the composition lemma for associative algebras [2].
[Give full statement of theorem? It's quite a mouthful.]
[Write about relation to Gröbner basis theory.]
- 1
- G. M. BERGMAN: The Diamond Lemma for Ring Theory, Adv. Math. 29 (1978), 178-218.
- 2
- L. A. BOKUT: Embeddings into simple associative algebras (Russian), Algebra i Logika 15, no. 2 (1976), pp. 117-142 and 245. English translation in Algebra and Logic, pp. 73-90.
- 3
- M. H. A. NEWMAN: On theories with a combinatorial definition of ``equivalence'', Ann. of Math. 43 (1942), 223-243.
|