Back to the index. Or to the chambers

This article has 54 links. View as Cloud or List.

Commutative Diagram Division Ring Expression Infinite Associative Equivalence Relation Reflexive Non Degenerate Sesquilinear Distributive Group Action Strict Relation Theory Closed Operator Proof Riemann Multiple Integral Converse Theorem Group Implication Structures And Satisfaction Equivalence Class Function Logical Implication Property Basic Polygon Generating Set Of A Group Algebraic System Relation Axiom Bijection Number Necessary And Sufficient Multivalued Function Terms And Formulas Elementarily Equivalent Ordered Tuplet Sequence Classes Of Algebras Algorithm Satisfaction Relation Transitive Deck Transformation Special Elements In A Relation Algebra Primary Ideal Complete Sound Normalizing Reduction Polyadic Algebra With Equality Well Founded Relation Terminating Reduction Closure Of A Relation With Respect To A Property Well Founded Induction Diamond Grobner Basis Congruence On A Partial Algebra Confluence

1	Commutative Diagram
1	Equivalence Relation
1	Distributive
1	Riemann Multiple Integral
1	Basic Polygon
1	Reflexive Non Degenerate Sesquilinear
1	Algebraic System
1	Closed Operator
1	Expression
1	Division
1	Property
1	Proof
1	Strict
1	Sequence
1	Equivalence Class
1	Structures And Satisfaction
1	Relation
1	Function
1	Terms And Formulas
1	Infinite
1	Ordered Tuplet
1	Elementarily Equivalent
1	Axiom
1	Converse Theorem
1	Relation Theory
1	Multivalued Function
1	Necessary And Sufficient
1	Number
1	Bijection
1	Logical Implication
1	Implication
1	Ring
1	Associative
1	Group Action
1	Generating Set Of A Group
1	Group
2	Algorithm
2	Deck Transformation
2	Classes Of Algebras
2	Satisfaction Relation
2	Transitive
3	Special Elements In A Relation Algebra
3	Complete Sound
3	Primary Ideal
6	Normalizing Reduction
6	Polyadic Algebra With Equality
7	Closure Of A Relation With Respect To A Property
9	Terminating Reduction
9	Well Founded Relation
9	Well Founded Induction
11	Congruence On A Partial Algebra
12	Confluence
13	Diamond
18	Grobner Basis

Loading ...

Planetmath Browser (2008—2009)

BSD licence | A django site

All articles taken from PlanetMath.org snapshot under CC-BY-SA licence.

→ The original article on PlanetMath.org

Other Formats: LaTeX

New! You can click on formulas to copy the LaTeX source to your clipboard. | Math Videos

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.

Theorem 1 Let be a set and let $\rightarrow$ be a binary relation on . If $\rightarrow$ is terminating, then the following conditions are equivalent:

For all $a,b,c \in X$ such that $a \rightarrow b$ and $a \rightarrow c$ , then and are joinable.
Every $a \in X$ has a unique normal form.

Condition 1 can be graphically drawn as

$\displaystyle \xymatrix @-2ex{ & a \ar[dl] \ar[dr] \\ b \ar[dr]^>>>>{*} & & c \ar[dl]_>>>>{*} \\ & d }$

where $\stackrel{*}{\rightarrow}$ denotes the reflexive transitive closure of $\rightarrow$ . 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 $a,b,c \in X$ forming the top two sides of such a diagram, there is a fourth corner $d \in X$ 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 $\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 to . 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.

Lemma 1 Let be a set and $\rightarrow$ a binary relation on such that all elements of has a unique normal form with respect to $\rightarrow$ . Denote by $\sim$ the reflexive transitive symmetric closure of $\rightarrow$ and denote by the function $X \longrightarrow X$ which sends every element to its normal form with respect to $\rightarrow$ . Then for all $x,y \in X$ ,

$\displaystyle x \sim y$ if and only if $\displaystyle \quad N(x)=N(y)$ .

(1)

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

$\displaystyle X_{\mathrm{nf}} = \left\{ \, x \in X \,\,\vrule\,\, \text{$x$ is on normal form} \, \right\}$

to $X/{\sim}$ given by $x \mapsto [x]_\sim$ , and its inverse can thanks to Lemma 1 be defined in terms of the normal form map

as $[x]_\sim \mapsto N(x)$ .

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”.

Algorithm 1 (Normal form) Let be a set and $\rightarrow$ a strict binary relation on which satisfies the descending chain condition.

Input: An element $x \in X$ .
Output: A normal form of .
Procedure: If is on normal form with respect to $\rightarrow$ then return . Otherwise there is some $y \in X$ such that $x \rightarrow y$ ; pick one such . Set and repeat the procedure from start.

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.

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.]

Bibliography

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.