1: \section{Our version of Knuth--Bendix.}
2: \label{our version}[Section]
3:
4: In this section we consider a
5: rewriting system which is the accepted language of a rule automaton for some
6: finitely presented group. We call the automaton \Rules.
7: We describe a Knuth--Bendix type algorithm for such
8: a system. In light of the undecidability results mentioned in
9: \ref{Objective.}, our algorithm
10: does not provide a test for confluence.
11: We can however use our procedure together with other procedures which
12: handle \shl-automatic groups,
13: to prove confluence by an indirect
14: route, provided the group is \shl-automatic.
15: Details of the theory of how this is done can be found in
16: \cite{WPiG}. The practical details are carried out in
17: programs by Derek Holt---see \cite{Holt:KBMAG}.
18:
19: We will introduce the concept of \RR-reduction, that is, reduction
20: using a two-variable automaton, which we call \Rules, encoding our
21: possibly infinite set of rules.
22: We prove some results about how reducibility may change with time.
23:
24: \subsection{Properties of the rule automaton.}
25: \label{properties of Rules}
26: The most important data structure is a small two-variable PDFA
27: which we call \Rules. Roughly speaking, this accepts all the rules
28: found so far. It has the following properties.
29: \begin{enumerate}
30: \item $\Rules$ is a trim rule automaton.
31: \item $\Rules$ has one initial state and one final state and they are
32: equal.
33: \item $\Rules$ and its reversal
34: $\Rev \Rules$ are both partially
35: deterministic.
36: \item Any arrow labelled $(x,x)$, with either source or target
37: the initial state, has source equal to target.
38: has source the initial state. If this condition is not fulfilled, we can
39: identify the source and target of the appropriate $(x,x)$-arrows,
40: and then weld. We will still have a rule automaton.
41: Later on (see Lemmas~\ref{arrows removed 1} and \ref{arrows removed 2}) we
42: will show that (after any necessary identifications and welding)
43: we can omit such arrows without loss, and, in fact, with a gain
44: given by improved computational efficiency.
45: Apart from the passages proving these lemmas,
46: we will assume from now on that there are no arrows
47: labelled $(x,x)$ with source or target the initial state of $\Rules$.
48: \end{enumerate}
49:
50: The first three conditions imply that $\Rules$ is welded.
51: Since $\Rules$ is a rule automaton,
52: Proposition~\ref{validrules} shows that
53: each accepted pair $(u,v)\in L(\Rules)$ gives a valid identity $\bar u = \bar v$
54: in $G$.
55:
56: \subsection{The automaton $\SLtwo$.}\label{SLtwo definition}
57: The automaton $\Rules$ may accept pairs $(u,v)$ such that $u$ is shorter
58: than $v$. We cannot consider such a pair as a rule and so we want to
59: exclude it. To this end we introduce the automaton $\SLtwo$. This is a five
60: state automaton, depicted in Figure~\ref{SL2}, which accepts pairs $(u,v)
61: \in \Astar\times\Astar$, such that $u$ and $v$ have no common prefix, $u$ is
62: \shl-greater than $v$ and $|v|
63: \le |u| \le |v|+2$. By combining $\SLtwo$ with $\Rules$, we obtain a regular
64: set of rules
65: $\SetOfRules \Rules$, which is possibly infinite, namely
66: $L(\Rules)\cap L(\SLtwo)$. An automaton accepting this set can be constructed
67: as follows. Its states are pairs $(s,t)$, where $s$ is a state of $\Rules$ and
68: $t$ is a state of $\SLtwo$. Its unique initial state is the pair of initial
69: states in $\Rules$ and $\SLtwo$. A final state is any state $(s,t)$ such that
70: both $s$ and $t$ are final states. Its arrows are labelled by $(x,y)$, where
71: $x\in A$ and $y\in A^+$. Such an arrow corresponds to a pair of arrows, each
72: labelled with $(x,y)$, the first from $\Rules$ and the second from $\SLtwo$.
73:
74: \begin{figure}[htbp]
75: \begin{center}
76: {\fontsize{10}{12pt}\selectfont
77: \begin{picture}(100,140)(0,-20)
78: \put(0,50){\circle{5}}
79: \put(-2,39){$1$}
80: \put(-12.5,50){\vector(1,0){10}}
81: \put(1.7,51.7){\vector(1,1){30}}
82: \put(-6,74){$(x,y),$}
83: \put(-14,64){$x>y$}
84: \put(1.7,48.3){\vector(1,-1){30}}
85: \put(-10,27){$(x,y),$}
86: \put(-2,17){$x<y$}
87: \put(33.5,83.5){\circle*{5}}
88: \put(31.5,73){$2$}
89: \put(33.5,96){\circle{20}}
90: \put(29.8,103){$<$}
91: \put(23,112){$(x,y)$}
92: \put(33.5,16.5){\circle{5}}
93: \put(31.5,21){$3$}
94: \put(33.5,4){\circle{20}}
95: \put(29.8,-8){$<$}
96: \put(23,-17){$(x,y)$}
97: \put(67,50){\circle*{5}}
98: \put(65,39){$4$}
99: \put(2.5,50){\vector(1,0){62}}
100: \put(22,54){$(x,\$)$}
101: \put(35.2,81.8){\vector(1,-1){30}}
102: \put(52,70){$(x,\$)$}
103: \put(35.2,18.2){\vector(1,1){30}}
104: \put(53,25){$(x,\$)$}
105: \put(67,50){\vector(1,0){62}}
106: \put(89,54){$(x,\$)$}
107: \put(131.5,50){\circle*{5}}
108: \put(129.5,39){$5$}
109: \end{picture}
110: }
111: \end{center}
112: \caption{\sf The automaton $\SLtwo$. Solid dots represent final states.
113: Roman letters represent arbitrary
114: letters from the alphabet $A$ and the labels on the arrows indicate multiple
115: arrows.
116: For example, from state $2$ to itself there is one arrow for each pair in
117: $A\times A$.}
118:
119: \label{SL2}
120: \end{figure}
121:
122: \subsection{Restrictions on relative lengths.}
123: \label{right-hand sides at most two shorter}
124: The following discussion is closely connected with
125: \thref{conditions and minimals}.
126: The restriction $|u| \le |v| +2$ needs some explanation. The point is that if
127: we have a rule with $|u| > |v| +2$, then we have an equality $\bar u = \bar v$
128: in $G$. We write $u = u'x$, where $x\in A$. The formal inverse $X$ of $x$
129: is also an element of $A$. We therefore have a pair of words
130: $(u', vX)$ which represent equal elements in $G$. If our set of rules were
131: to contain such a rule, then $u=u'x$ would reduce to $vXx$, and this reduces
132: to $v$, making the rule $(u,v)$ redundant. This leads to an obvious technique
133: for transforming any rule we find into a new and better
134: rule with $|v| \le |u| \le |v|+2$. Since we take this into account when
135: constructing the automaton $\Rules$, we are justified in making the
136: restriction.
137:
138: This analysis can be carried further. Let
139: $u=u_1\cdots u_{r+2}=u'u_{r+2} = u_1 u''$ and
140: let $v=v_1\cdots v_r$. If $u_1>v_1$, then the rule $(u,v)$ can be
141: replaced by the better rule $(u',vu_{r+2}^{-1})$.
142: If $u_2 > u_1^{-1}$, then $(u,v)$ can be replaced by $(u'',u_1^{-1}v)$.
143: We do in fact carry out these steps when installing new rules.
144: The extra information could have been included in the FSA $\SLtwo$. However,
145: it seems that this would involve more complicated coding at various
146: points, probably without any gain in efficiency.
147:
148: We could consider the steps just
149: described as an attempt to force our structures to define a set of
150: rules which conforms to known properties (see \thref{conditions and
151: minimals}) of the set of
152: $U$-minimal rules (see \ref{U} for the definition of $U$).
153: The most important reason for insisting on these additional
154: restrictions on our rules is to keep down the size of our data
155: structures.
156:
157: \subsection{The basic structures.}
158: The basic structures used in our procedure are:
159: \begin{enumerate}
160: \item A two-variable automaton $\Rules$ satisfying the conditions
161: laid down in \ref{properties of Rules}.
162: When we want to
163: specify that we are working with the $\Rules$ automaton during the $n$th
164: Knuth--Bendix pass (see \ref{Knuth--Bendix pass} for the definition of a
165: Knuth--Bendix pass), we will use the notation $\Rules[n]$. We extract
166: explicit rules from $\Rules[n]$ by taking elements of the intersection
167: $\SetOfRules{\Rules[n]} = L(\Rules[n]) \cap L(\SLtwo)$. The two-variable
168: automaton $\SLtwo$ was defined in Section~\ref {SLtwo definition} and
169: is depicted in Figure~\ref{SL2}.
170:
171: \item A finite set \Store of rules, which is the disjoint union of
172: several subsets of rules : \Considered, \This, \New and \Delete.
173: One point of the separate subsets is to avoid constantly doing the
174: same critical pair analyses. Another point is to ensure that our
175: Knuth--Bendix process is fair (see \thref{fair}). The reason for
176: holding some rules in a \Delete list, rather than delete them
177: immediately, is to make reduction more efficient.
178: This will be explained further in \ref{deletion delay}.
179:
180: \Store will continually change, while $Rules$ is constant during a
181: Knuth--Bendix pass. We change $\Rules$
182: at the end of each Knuth--Bendix pass.
183: We will perform the Knuth--Bendix process, using the rules in \Store
184: for critical pair analysis, as described in \ref{Critical pair analysis.}.
185: \item \Considered is a subset of \Store such that each rule
186: has already been compared with each other rule in \Considered,
187: including with itself,
188: to see whether left-hand sides overlap.
189: The consequent critical pair
190: analysis has also been carried out for pairs of rules in \Considered.
191: Such rules do not need to be compared with
192: each other again.
193: \item \This is a subset of \Store (empty at the beginning of each
194: Knuth--Bendix pass) containing rules which we plan to use
195: during this pass to compare for overlaps with the rules in \Considered, as in
196: \ref{first case}. These rules are minimal for
197: the current pass (see \ref{minimization}) and so should not be minimized again.
198: \item \New is a subset of \Store containing new rules which have
199: been found during the current pass, other than those which are output
200: by the minimization routine (see \ref{minimization} for the meaning of
201: ``minimization''). Rules which are
202: output by the minimization routine are added to \This.
203: \item \Delete is a subset of \Store containing rules which are to be
204: deleted at the end of this pass.
205: \item The two-variable automaton \WDiff contains
206: all the states and arrows of $\Rules[n]$, and possibly other states and
207: arrows. It satisfies the conditions of \ref{properties of Rules}.
208: This automaton is used to accumulate appropriate new rules which are
209: output by the minimization routine. As rules are considered during the
210: Knuth--Bendix pass, states and arrows of \WDiff are marked as \needed.
211: At the end of the pass, other states and arrows are removed, and
212: \WDiff becomes the new \Rules automaton $\Rules[n+1]$.
213: \item A PDFA $P(\Rules)$ formed from
214: \Rules by a certain subset construction.
215: This automaton accepts words which are \RR-reducible, that is,
216: words which contain a left-hand side of a rule in
217: $\SetOfRules\Rules$. The automaton is used as part of
218: our rapid reduction procedure (see \thref{Fast reduction}).
219: More details of $P(\Rules)$ are provided in \ref{P}.
220: \item A PDFA $Q(\Rules)$ which accepts the reversals of left-hand sides
221: of rules in $\SetOfRules\Rules$. This is also formed from \Rules by
222: a subset construction and is also used for rapid reduction.
223: More details of $Q(\Rules)$ are
224: provided in \ref{Q}.
225: \end{enumerate}
226:
227: \subsection{Initial arrangements.}
228: Before describing the main Knuth--Bendix process, we explain how the
229: data structures are initially set up. Let $R$ be the original set of
230: defining relations together with special
231: rules of the form $(x.\inverse(x),\epsilon)$ which
232: make the formal inverse $\inverse(x)$ into the actual inverse of $x$.
233:
234: We rewrite each relation of $R$ in the form
235: of a relator, which we cyclically reduce in the free group.
236: We assume that each relator has the form
237: $l.\inverse(r)$, where $l$ and $r$ are elements of $\Astar$ and $(l,r)$ is
238: accepted by $\SLtwo$.
239:
240: For each rule $(l,r)$, including the special rules
241: $(x.\inverse(x),\epsilon)$, we form a rule
242: automaton, as explained in \ref{ruleworddiff}. These automata are then welded
243: together to form the two-variable rule automaton \WDiff satisfying the
244: conditions of \ref{properties of Rules}. Each state and arrow
245: of \WDiff is marked as \needed.
246: Each of these rules is inserted into \New. \Considered, \This and
247: \Delete are initially empty. Set $\Rules[1]=\WDiff$.
248:
249: \subsection{The main loop---a Knuth--Bendix pass.}
250: \label{main loop}
251: We now describe the procedure followed during the course of a single
252: Knuth--Bendix pass.
253:
254: A significant proportion of the time in a Knuth--Bendix pass is spent in
255: applying a procedure which we term {\it minimization}. Each rule encountered
256: during the pass is input (often after a delay)
257: to this procedure and the output is called a
258: {\it minimal rule}.
259: The details of this process are given in sections~\ref{minimization}
260: and \ref{handling minimization output}.
261:
262: \begin{enumerate}
263: \item\label{start main loop}
264: At the beginning of a Knuth--Bendix pass, \This is empty.
265: If $n>0$, save space by deleting previously defined automata $P(\Rules[n])$,
266: $Q(\Rules[n])$ and $\Rules[n]$. Increment $n$.
267: The integer $n$ records which Knuth--Bendix pass we are currently working on.
268: \item\label{process Considered}[Step]
269: For each rule $(\lambda,\rho)$ in \Considered,
270: minimize $(\lambda,\rho)$ as in \ref{minimization} and handle the output rule
271: $(\lambda_1,\rho_1)$ as in \ref{handling minimization output}.
272: This may affect \Store and \WDiff.
273: \item \label{process New}[Step]
274: For each rule $(\lambda,\rho)$ in \New,
275: minimize $(\lambda,\rho)$ as in \ref{minimization} and handle the output as in
276: \ref{handling minimization output}.
277: This may affect \Store and \WDiff.
278:
279: Since rules added to \New during minimization are always strictly smaller than
280: the rule being minimized (see \ref{inserting}), it follows that
281: the process of examining rules in \New does not continue indefinitely.
282: As a result, we can be sure that our process is fair (see \ref{fair}).
283: \item\label{process This}
284: For each rule $(\lambda,\rho)$ in \This:
285: \begin{enumerate}
286: \item Delete the rule from \This and add it to \Considered.
287: \item\label{compare for overlaps}[Step]
288: For each rule $(\lambda_1,\rho_1)$ in \Considered:
289: \begin{quote} Look for overlaps between $\lambda$ and
290: $\lambda_1$. That is we have to find each
291: suffix of $\lambda$ which is a prefix
292: of $\lambda_1$ and
293: each suffix of $\lambda_1$ which is a
294: prefix of $\lambda$.
295: Then \RR-reduce in two different ways as in
296: \ref{first case}, obtaining a pair of words $(u,v)$
297: with $u\ge v$. (Roughly speaking, \RR-reduction means
298: the use of rules in $\SetOfRules{\Rules}$. More
299: precision is provided in \ref{inserting}.)
300: If $u>v$, $(u,v)$ is inserted into \New,
301: unless it is already in \Store.
302:
303: Note that we may have to allow $\lambda=\lambda_1$ in order to
304: deal with the case where two different rules have the
305: same left-hand side. In this case, both the prefix and suffix
306: of both left-hand sides is equal to $\lambda=\lambda_1$.
307: \end{quote}
308: \end{enumerate}
309: \item\label{using WDiff}
310: \WDiff was possibly affected in \thref{process Considered} and
311: \thref{process New}.
312: With \WDiff in its present form,
313: delete from \WDiff all arrows and states which are not marked as
314: \needed. Copy \WDiff into $\Rules[n+1]$
315: and mark all arrows and states of \WDiff as not \needed.
316: %The details of this step are given in \ref{WDiffdetails}.
317: \item \label{process Delete}
318: Delete the rules in \Delete.
319: \item This ends the description of a Knuth--Bendix pass.
320: Now we decide whether to terminate the Knuth--Bendix process. Since we know of
321: no procedure to decide confluence of an infinite system of rules (indeed, it is
322: probably undecidable), this decision is taken on heuristic grounds. In our
323: context, a decision to terminate could be taken simply on the grounds that
324: \WDiff and $\Rules[n]$ have the same states and arrows. In other words, no new
325: word-differences or arrows between word-differences have been found or
326: deleted during this pass.
327: If the Knuth--Bendix process is not terminated, go to \ref{start main loop}.
328: \end{enumerate}
329:
330: \begin{definition}
331: \label{minimization}[Definition]
332: We now provide the details of the minimization routine.
333: This processes a rule so as to create from it a minimal rule
334: (see \thref{minimal}), where, roughly speaking, minimality is defined using
335: the current set of rules.
336: Since the set of rules is changing, this is a bit difficult to pin
337: down. So instead we make the following definition, which is more
338: precise, though the underlying concept is the same.
339: Let $(u,v)\in \Astar\times\Astar$ and let $u=u_1\cdots u_p$
340: and $v=v_1\cdots v_q$, where $u_i, v_j \in A$.
341: We say that $(u,v)$ is a \textit{minimal rule} if $u\neq v$,
342: $\bar u = \bar v$ in $G$
343: and the following procedure does not change $(u,v)$. The procedure is
344: called the \textit{minimization routine}.
345: We always start the minimization routine with $u>v$, though this
346: condition is not necessarily maintained as $u$ and $v$ change during the
347: routine.
348: Here the meaning of a ``minimal rule'' changes with time: a rule may
349: be minimal at one time and no longer minimal at a later time.
350:
351: \begin{enumerate}
352: \item\label{reduce prefix}
353: \RR-reduce (that is, reduce using the rules of \Rules)
354: the maximal proper prefix $u_1\cdots u_{p-1}$
355: of $u$ obtaining $u'$.
356: Reduction may result in rules being added to \New as described in
357: \ref{reduction gives new rule}.
358: If $u\neq u'u_p$, change $u$ to $u'u_p$ and go to
359: Step~\ref{reduce u}.
360: \item\label{reduce suffix}
361: \RR-reduce the maximal proper suffix $u_2\cdots u_p$
362: of $u$ obtaining $u''$.
363: Reduction may result in new rules being added to \New.
364: Replace $u$ by $u_1u''$.
365: \item\label{reduce u}
366: If $u$ has changed since the original input to the minimization routine,
367: then \RR-reduce $u$ as explained in \ref{history stack}.
368: This may result in rules being added to \New as described in
369: \ref{reduction gives new rule}.
370: \item\label{reduce v}[Step]
371: \label{minimization loop}[Step]
372: \RR-reduce $v$.
373: \item If $v > u$, interchange $u$ and $v$.
374: \item If (a) $p >q+2$ or (b) if $p = q+2$, $q>0$
375: and $u_1 > v_1$ or (c) if $p=2$, $q=0$ and
376: $u_1>\inverse(u_2)$, replace $(u,v)$ by
377: $(u_1\cdots u_{p-1}, v_1\cdots v_q \inverse(u_p))$ and repeat this step until
378: we can go no further.
379: \item If $p=q+2$ and $u_2 > \inverse(u_1)$, replace $(u,v)$ by
380: $(u_2\cdots u_p,\inverse(u_1)v_1\cdots v_q)$.
381: \item If $q>0$ and $u_1 = v_1$, cancel the first letter
382: from $u$ and from $v$ and repeat this step.
383: \item If $q>0$ and $u_p =v_q$, cancel the last letter from $u$ and
384: from $v$ and repeat this step.
385: \item If $(u,v)$ has changed since the last time Step~\ref{minimization
386: loop} was executed, go to Step~\ref{minimization loop}.
387: \item Output $(u,v)$ and stop.
388: \end{enumerate}
389: \end{definition}
390:
391: Note that the output could be $(\epsilon,\epsilon)$, which means
392: that the rule is redundant. Otherwise we have output $(u,v)$ with $u>v$.
393: Note that the minimization procedure keeps on decreasing $(u,v)$ in the
394: ordering given by using first the \shl-ordering on $u$ and then, in
395: case of a tie, the \shl-ordering on $v$.
396: Since this is a well-ordering, the minimization
397: procedure has to stop.
398:
399: \subsection{Handling minimization output.}
400: \label{handling minimization output}
401: Suppose the input to minimization is $(\lambda,\rho)$ and its output
402: is $(\lambda_1,\rho_1)$.
403: \begin{enumerate}
404: \item If $(\lambda_1,\rho_1) \neq (\epsilon,\epsilon)$,
405: incorporate (by welding) $(\lambda_1,\rho_1)$ into the language accepted
406: by \WDiff.
407: Insert $(\lambda_1,\rho_1)$ into \This if it was not already in \This
408: or \Considered. Remove it from \New, if it was there previously.
409: \item\label{deletion: proper subword}
410: If some proper subword of $\lambda$ is \RR-reducible, then this will
411: be discovered during the first few steps of minimization.
412: ($(\lambda_1,\rho_1) = (\epsilon,\epsilon)$ turns out to be
413: a special case of this,
414: as we will see in \ref{deleting rules irred}.)
415: In this case, delete $(\lambda,\rho)$ from \Store immediately the
416: minimization procedure is otherwise complete.
417: \item\label{deletion delay}
418: If, at the time of minimization,
419: all proper subwords of $\lambda$ were \RR-irreducible and
420: if $(\lambda,\rho)$ was not minimal, move
421: $(\lambda,\rho)$ to the \Delete list. The reason for this possibly
422: surprising policy of not deleting immediately is that further
423: reduction during this pass may once again
424: produce $\lambda$ as a left-hand side by the
425: methods of \ref{Fast reduction} and
426: \ref{finding the left-hand side}. We want to avoid the work involved in
427: finding the right-hand side by the method which will be explained in
428: \ref{finding the right-hand side}. For this, we need to have a rule
429: in \Store with left-hand side equal to $\lambda$---see \ref{reduction
430: gives new rule}.
431: \end{enumerate}
432:
433: \subsection{Details on the structure of \WDiff.}
434: \label{WDiffdetails}
435: At the beginning of Step~\ref{using WDiff}, each state $s$ of $\WDiff$
436: is associated to a word $w_s \in A\uast$ which is irreducible with respect
437: to $\SetOfRules{\Rules[n]}$. $\WDiff$ is a rule automaton: the rule
438: automaton structure is given by associating the
439: element $\overline{w_s}\in G$ to the state $s$.
440: Whenever a minimal rule $r$ is encountered during the $n$th pass, it
441: is adjoined to the accepted language of \WDiff by welding and the
442: corresponding states and arrows are marked as \needed.
443: State labels are calculated as and when new states and arrows are added
444: to $\WDiff$.
445:
446: At the end of the $n$th Knuth--Bendix pass,
447: \WDiff is an automaton which represents the
448: word-differences and arrows between them encountered during that pass.
449: At this stage the word
450: attached to each state is irreducible with respect to the rules in
451: $\SetOfRules{\Rules[n]}$ but not necessarily
452: with respect to the rules implicitly contained in \WDiff. Before starting the
453: next pass, we \RR-reduce the state labels of \WDiff with respect to
454: $\SetOfRules{\WDiff}$. If \WDiff now contains distinct states labelled by the
455: same word we connect them by epsilon arrows and replace \WDiff by
456: $\Weld \WDiff$. We then repeat this procedure until
457: all states are labelled
458: by distinct words which are irreducible with respect to
459: $\SetOfRules{\WDiff}$. If during this procedure a state or arrow marked
460: as \needed is identified with another which may or may not be marked
461: as \needed, the resulting state or arrow is marked as \needed.
462:
463:
464: \subsection{\RR-reduction and inserting rules.}\label{inserting}
465: Given a word $w$, we look for an \RR-reducible subword $\lambda$ such
466: that all proper subwords of $\lambda$ are \RR-irreducible,
467: by looking in $\SetOfRules{\Rules}$.
468: Later (\thref{Fast reduction})
469: we will describe how to
470: do this quickly, but, at the moment, the reader can just think of a
471: non-deterministic search in the automaton giving the \shl rules
472: recognized by $\Rules$. Having found a reducible subword
473: $\lambda$ of $w$, with no reducible subword,
474: we do not automatically use the corresponding right-hand
475: side $\rho$, found from the exploration of \Rules,
476: because this naive approach is computationally inefficient.
477: Instead we look in \Store to see if there is a rule
478: $(\lambda,\rho)$. If there is such a rule, then we can find it
479: quickly given $\lambda$,
480: and we proceed with our reduction, replacing the subword
481: $\lambda$ in $w$ with $\rho$.
482:
483: It may however turn out that
484: we can find an \RR-reducible subword $\lambda$ of $w$, with no
485: \RR-reducible subwords, and yet
486: there is no rule of the form $(\lambda,\rho)$ in \Store.
487: In this case, we have to spend time
488: finding such a rule in $\SetOfRules\Rules$.
489: Once found, we immediately insert it into \Store,
490: otherwise the logic of the Knuth--Bendix procedure can go wrong.
491:
492: In this way, reduction of a single word can result in the insertion of
493: several new rules into \Store.
494:
495: It follows from the above description
496: that the \RR-reducibility of a word $w$ depends only on \Rules.
497: Since \Rules does not change during a Knuth--Bendix pass,
498: exactly the same subset of $\Astar$ will be \RR-reducible throughout
499: such a pass. However, because we may use rules in the changing set \Store,
500: the \textit{result} of \RR-reduction may change during a pass.
501:
502: Another, more conventional, source of rules to insert into \Store come
503: from critical pair analysis in \thref{compare for overlaps}.
504:
505: Minimization also results in rules being added to \Store, both
506: directly, as the output of the minimization procedure, but also
507: indirectly because minimization uses reduction, and, as we will see in
508: \ref{finding the right-hand side}. reduction can add rules to \Store.
509: It is important to note that any rules
510: added to \Store during the minimization of a rule $(\lambda,\rho)$ are
511: strictly smaller than $(\lambda,\rho)$, if we order such pairs by
512: using $\lambda$ first and then $\rho$ in case of a tie.
513: We used this fact when discussing \thref{process New}.
514:
515: \subsection{Deleting rules.}\label{deleting rules}
516: Deletion of rules happens only at the end of each minimization step, and at the
517: end of each pass, when rules marked for deletion are actually deleted.
518: During a Knuth--Bendix pass, deletion
519: does not occur after the beginning of Step~\ref{process This}.
520: Suppose that the output from minimization of $(\lambda,\rho) \in
521: \Store$ is $(\lambda_1,\rho_1)$.
522:
523: \begin{enumerate}
524: \item\label{deleting rules irred}[Case]
525: If every proper subword of $\lambda$ is \RR-irreducible, then
526: $\lambda_1$ is a non-trivial subword of $\lambda$.
527: This follows by going through the successive steps of
528: minimization (\thref{minimization}).
529: These change $\lambda$ and $\rho$, while maintaining
530: the inequality $\lambda > \rho$.
531: In particular $\lambda_1 > \rho_1$, so that $\lambda_1 \neq \epsilon$.
532: If $(\lambda_1,\rho_1) \neq (\lambda,\rho)$, then we delete
533: $(\lambda,\rho)$ after a delay.
534: The mechanism is to mark it for
535: deletion by moving it to the \Delete list and actually delete it only
536: at the end of the current Knuth--Bendix pass (Step~\ref{process Delete}).
537:
538: \item\label{deleting rules red}[Case]
539: If some proper subword of $\lambda$ is reducible,
540: then $(\lambda,\rho)$ is immediately deleted from \Store
541: at Step \ref{deletion: proper subword} at the end of the
542: minimization procedure. (\RR-reducibility of some proper subword of
543: $\lambda$ is discovered
544: at Step~\ref{reduce prefix} or \ref{reduce suffix}.)
545: \end{enumerate}
546:
547: \begin{lemma}\label{before This}
548: Suppose that, for some $n\in\naturals$,
549: there is a rule $(\alpha,\beta)\in\Store$
550: during the $n$-th Knuth--Bendix pass,
551: {\em before} the beginning of Step~\ref{process This}.
552: Then there is a non-trivial subword $\lambda$ of
553: $\alpha$ such that some rule
554: $(\lambda,\rho)$ is output from some instance of the minimization
555: procedure during the $n$-th pass.
556: If $\lambda=\alpha$, then $\rho \le \beta$.
557: The rule $(\lambda,\rho)$ is a rule in \Store at the
558: beginning of the $(n+1)$-st pass and is accepted by $\Rules[n+1]$.
559: \end{lemma}
560: \begin{proof}
561: By examining \ref{main loop}, we see that
562: $(\alpha,\beta)$ must be the input to the minimization routine
563: at some time during the $n$-th
564: pass. (We check the four possibilities, namely that it is in
565: \Considered, \This, \New or \Delete, one by one. If it is in \Delete,
566: it must have been the input to the minimization procedure at some
567: earlier stage during the $n$-th pass.)
568:
569: We first deal with the case where
570: some proper subword of $\alpha$ is \RR-reducible during the
571: $n$-th pass.
572: During the first three steps of minimization (\thref{minimization}),
573: an \RR-reducible subword $\lambda$ of $\alpha$ is found, with the
574: property that all the proper subwords of $\lambda$ are \RR-irreducible.
575: Minimization then either finds a rule of the form
576: $(\lambda,\rho)$ already in \Store, or such a rule is
577: added to \New by the reduction process---see \ref{reduction gives new
578: rule}.
579: In any case, it will either be minimized during this pass, or it has
580: already been minimized (and possibly moved to the \Delete list.
581:
582: At the moment when $(\lambda,\rho)$ is minimized during the $n$-th pass,
583: we must be in Case~\ref{deleting rules irred}.
584: So the output $(\lambda_1,\rho_1)$ from the minimization
585: procedure with input $(\lambda,\rho)$ gives the required rule.
586: $\lambda_1$ is a subword of $\lambda$ and $\lambda$ is a proper
587: subword of $\alpha$.
588:
589: Alternatively, all proper subwords of $\alpha$ are \RR-irreducible
590: during the $n$-th pass,
591: in which case we set $(\lambda,\rho)$ to be the output from
592: minimization of $(\alpha,\beta)$.
593: By \ref{deleting rules irred}, $\lambda$ is a non-trivial subword
594: of $\alpha$. If $\lambda=\alpha$, then $\rho\le \beta$.
595: \end{proof}
596:
597: \begin{lemma}\label{after This}
598: Suppose that, for some $n\in\naturals$,
599: there is a rule $(\alpha,\beta)\in\Store$
600: during the $n$-th Knuth--Bendix pass, {\em after} the beginning of
601: Step~\ref{process This}.
602: Then there is a non-trivial subword $\lambda$ of $\alpha$ such that some rule
603: $(\lambda,\rho)$ is output from some instance of the minimization
604: procedure during the $(n+1)$-st pass.
605: If $\lambda=\alpha$, then $\rho \le \beta$.
606: \end{lemma}
607:
608: \begin{proof}
609: If $(\alpha,\beta)$ is in the \Delete list, then it must have been
610: input to the minimization procedure at some earlier time during the
611: $n$-th pass. By \thref{deleting rules red}, every proper subword of
612: $\alpha$ must have been found to be \RR-irreducible during the $n$-th pass.
613: Let $(\alpha',\beta')$ be the output from minimization.
614: By \thref{deleting rules irred}, $\alpha'$ is a non-trivial subword
615: of $\alpha$, and, if $\alpha'=\alpha$, then $\beta'<\beta$.
616: Now $(\alpha',\beta')$ is in \Store at the beginning of the $(n+1)$-st
617: pass. We apply \thref{before This} to $(\alpha',\beta')$ at the
618: $(n+1)$-st pass.
619:
620: If $(\alpha,\beta)$ is not on the \Delete list, then it must be in \Store
621: at the beginning of the $(n+1)$-st pass.
622: Once again, we can apply \thref{before This}.
623: \end{proof}
624:
625: The following result is often applied with $w=\alpha$.
626: \begin{proposition}\label{stays RR reducible}
627: Let $w\in \Astar$ be a word which contains the left-hand side $\alpha$ of a
628: rule $(\alpha,\beta)$ input to the minimization routine during the
629: $n$-th Knuth--Bendix pass.
630: Then, for $m\ge n$, $w$ contains the left-hand side of a rule which is
631: input to the minimization procedure during the $m$-th Knuth--Bendix pass.
632: Moreover $w$ is \RR-reducible for $m>n$.
633: \end{proposition}
634: \begin{proof}
635: We assume inductively that if $m>n$ then
636: $w$ contains a subword $\alpha$, such that a rule of the form $(\alpha,\beta)$
637: is input to the minimization procedure during the $(m-1)$-st pass.
638: Since minimization happens only
639: before the beginning of Step~\ref{process
640: This}, \thref{before This} gives a rule $(\lambda,\rho)$, such that
641: $\lambda$ is a non-trivial subword of $\alpha$.
642: Moreover, $(\lambda,\rho)$ is
643: minimal during the $(m-1)$-st pass and is contained in \Store at the
644: beginning of the $m$-th pass. Therefore $(\lambda,\rho)$ is input to the
645: minimization procedure during the $m$-th pass, as required.
646:
647: The rule $(\lambda,\rho)$ is welded into \WDiff during the $(m-1)$-st
648: pass and is therefore accepted by $\Rules[m]$.
649: It follows that $w$ is \RR-reducible during the $m$-th pass.
650: Inductively this is true for all $m>n$.
651: \end{proof}
652: