1: \section{Standard Knuth--Bendix.}
2: \label{Standard Knuth--Bendix}[Section]
3:
4: We recall the classical Knuth--Bendix procedure. Later we will explain
5: how our procedure differs from it.
6: We continue to restrict to the \shl case and to groups.
7: Suppose $G$ is a group given by a finite set of generators and
8: relators. We define $A$ to be the set of generators together with
9: their formal inverses. Our initial set of rules
10: consists of all rules of the
11: form $(x.\inverse(x),\epsilon)$ for $x\in A$, together with
12: all rules of the form $(r,\epsilon)$, where $r$ varies over the
13: finite set of defining relators for $G$.
14:
15: After running the Knuth--Bendix procedure (which we are about to
16: describe) for some time, we will still have a finite set $R$ of rules.
17: As always, we assume that $R$ satisfies
18: Conditions~\ref{Standard assumptions about rules.}.
19:
20: To test for confluence of a finite set of rules, we need only do critical pair
21: analysis, as explained in \ref{Critical pair analysis.}, \ref{first
22: case} and \ref{second case}. The proof of this is as follows.
23:
24: Suppose $R$ is not confluent.
25: Let $w$ be the \shl least word over $A$ for which there are two
26: different chains of elementary reductions giving rise to distinct
27: irreducibles.
28: Since $w$ is shortest, it is easy to see that the first elementary
29: reductions in the two chains must overlap.
30:
31: \subsection{Critical pair analysis.}
32: \label{Critical pair analysis.}
33: A pair of rules
34: $(\lambda_1,\rho_1)$ and $(\lambda_2,\rho_2)$ can overlap
35: in two possible ways.
36: First, a non-empty word $z$ may be a suffix of $\lambda_1=s_1z$
37: and a prefix of
38: $\lambda_2=zs_2$ (or vice versa).
39: Second, $\lambda_2$ may be a subword of
40: $\lambda_1$ (or vice versa) and we write $\lambda_1=s_1\lambda_2s_2$.
41:
42: These cases are not disjoint. In particular, if one of $s_1$
43: and $s_2$ is trivial in the second case, it can equally well be
44: treated under the first case with $z$ equal either to $\lambda_1$ or
45: to $\lambda_2$.
46:
47: \subsection{First case of critical pair analysis.}
48: \label{first case}
49: In the first case, there are two elementary reductions of
50: $u=s_1zs_2$, namely to $\rho_1s_2$ and to $s_1\rho_2$.
51: Further reduction to irreducibles either gives the same irreducible
52: for each of the two computations, or else
53: gives us distinct irreducibles $v$ and $w$.
54: From Conditions~\ref{Standard assumptions about rules.} we deduce that
55: $v$ and $w$ represent the same element of $G$.
56: So, if $v$ and $w$ are distinct, we augment $R$ with the
57: rule $(v,w)$ if $w < v$ or
58: with $(w,v)$ if $v < w$.
59: Clearly Conditions~\ref{Standard assumptions about rules.} are
60: maintained.
61:
62: Note that it is important to allow $(\lambda_1,\rho_1) = (\lambda_2,\rho_2)$
63: in the case just discussed,
64: provided there is a $z$ which is both a proper suffix and
65: a proper prefix of $\lambda_1=\lambda_2$.
66:
67: \subsection{Second case of critical pair analysis.}
68: \label{second case}
69: In the second case, there are two elementary reductions of
70: $u=\lambda_1=s_1\lambda_2 s_2$, namely to $\rho_1$ and to $s_1\rho_2s_2$.
71: If $\rho_1$ and $s_1\rho_2s_2$ reduce to distinct irreducibles
72: $v$ and $w$, we augment $R$
73: with either $(v,w)$ or with $(w,v)$, depending on whether $v>w$ or
74: $w>v$.
75:
76: \subsection{Omitting rules.}
77: \label{omitting rules}
78: In practice, it is important to remove rules which are redundant, as
79: well as to add rules which are essential. Omitting rules is
80: unnecessary in theory, provided that we have unlimited time and space at our
81: disposal. In practice, if we don't omit rules, we are liable to be
82: overwhelmed by unnecessary computation. Moreover, nearly all programs
83: in computational group theory suffer from excessive demands for space.
84: Indeed this is one of the reasons for developing the algorithms and
85: programs discussed in this paper. So it is important to throw away
86: information that is not needed and doesn't help.
87:
88: For this reason, in Knuth--Bendix programs one looks from
89: time to time at each rule $(\lambda,\rho)$ to see if it can be
90: omitted. If a proper subword of
91: the left-hand side can be reduced, then we
92: are in the situation of \ref{second case}. If the two reductions
93: mentioned in \ref{second case}
94: lead to the same irreducible, we omit $(\lambda,\rho)$ from the
95: set of rules. If the two reductions lead to different irreducibles,
96: then we augment the set of rules as described in \ref{second case} and
97: again omit $(\lambda,\rho)$.
98: We also investigate whether the right-hand
99: side $\rho$ of a rule $(\lambda,\rho)$ is reducible to $\rho'$.
100: If so, we can omit $(\lambda,\rho)$ from $R$ and replace
101: it with the rule $(\lambda,\rho')$.
102:
103: It is easy to see that such omissions do not change the Thue
104: equivalence classes.
105: The process of analyzing critical pairs and augmenting or diminishing
106: the rule set while maintaining the conditions of \ref{Standard
107: assumptions about rules.} is called the {\it Knuth--Bendix Process}.
108:
109: If the Knuth--Bendix process terminates, every left-hand side having
110: been checked against every left-hand side in critical pair analysis
111: without any new rule being added, we know that we have a finite
112: confluent system of rules.
113: Usually it
114: does not terminate and it produces new rules {\it ad infinitum}.
115:
116: \begin{definition}\label{fair}[Definition]
117: It is important that the process be \textit{fair}.
118: By this we mean
119: that if you fix your attention on two rules at any one time, then
120: either their left-hand sides must have already been, or must
121: eventually be, checked for overlaps; or one
122: or both of them must eventually be omitted.
123: If the process is not fair, it might concentrate exclusively on one
124: part of the group: for example, in the case of the product of two
125: groups, the process might pay attention only to one of the factors.
126: \end{definition}
127:
128: \subsection{The limit of the process.}\label{limit}
129: As the Knuth--Bendix process proceeds, $R$ changes and the set of
130: $R$-reducibles steadily increases. This is obvious when we add a rule
131: as in \ref{first case} and \ref{second case}. It is also easy to see
132: when we omit a rule---we need only check that if we omit
133: $(\lambda,\rho)$ from $R$ as in \ref{omitting rules},
134: then $\lambda$ remains reducible.
135:
136: Now let us fix a positive integer $n$.
137: Eventually the set of reducibles of length at most $n$ stops increasing
138: with time, and the set of irreducibles of length at most $n$ stops
139: decreasing.
140: Since the word problem is in general insoluble, we will in general not know for
141: sure at any one time or for any fixed $n$ whether the set of
142: reducibles has stopped increasing. It may look as though it has
143: permanently stabilized and then suddenly start increasing again.
144:
145: Once stabilized, we know by \thref{fair}
146: that any two reductions of a given word of
147: length at most $n$ will give the same irreducible (otherwise a new
148: rule would be added at some time, creating one of more new reducibles
149: of length at most $n$).
150: It follows that if
151: we take the limit of the set of rules (the set of rules which appear
152: at some time and are never subsequently omitted),
153: then we have a confluent set of rules. We deduce from
154: \thref{properties imply group} that, after stabilization of the set of
155: reducibles of length at most $n$,
156: any irreducible of length at most $n$ is in \shl normal form.
157: In fact, at this point, the set of rules with left-hand side of length at most
158: $n$ coincides with the set of $U$-minimal rules in $U$ (defined in
159: \ref{U} and \ref{minimal}).
160:
161: \subsection{Knuth--Bendix pass.}
162: \label{Knuth--Bendix pass}
163: One procedure for carrying out the Knuth--Bendix process is to divide the
164: finite set \Store of rules found so far into three disjoint subsets.
165: The first subset,
166: called {\Considered}, is the set of rules whose left-hand sides have been
167: compared with each other and with themselves for overlaps.
168: The second set of rules, called {\This}, is the set of rules waiting to
169: be compared with those in {\Considered}. The third set, called {\New},
170: consists of those rules most recently found.
171: Here we only sketch the process. Fuller details of our more elaborate
172: form of Knuth--Bendix are provided in \thref{our version}.
173:
174: The Knuth--Bendix process proceeds in phases, each of which is
175: called a \textit{Knuth--Bendix pass}. Each pass starts by looking at each
176: rule in {\Considered} and seeing whether it can be deleted as in
177: \ref{omitting rules}.
178: Consideration of an existing rule in {\Considered} can lead to a
179: new rule, in which case the new rule is added to {\New}.
180:
181: Next, we look at each rule $r$ in \New to see if it is can be omitted
182: or replaced by a better rule, a process which we call
183: \textit{minimization}.
184: The details of our minimization procedure
185: will be given in \ref{minimization}.
186: If the minimization procedure changes a rule, the old rule is either
187: deleted or marked for future deletion. The new rule is added to \This.
188: Eventually \New is emptied.
189:
190: We then look at each rule in \This.
191: Its left-hand side is compared with
192: itself and with all the left-hand sides of rules in
193: {\Considered}, looking for overlaps as in \ref{first case}.
194: Any new rules found are added to {\New}.
195: Then $r$ is moved into {\Considered}.
196: Eventually \This becomes empty.
197:
198: We then proceed to the next pass.
199: