1: \section*{Contents} To help readers find their way around the
2: inevitably complex structure of this paper,
3: we start with a brief description of each section.
4:
5: \noindent {\bf 1. Introduction.} This briefly sets some of
6: the background for the paper and describes the motivation for this work.
7:
8: \noindent{\bf 2. Our class of groups in context.}
9: We define the class of groups to which this paper is devoted and prove
10: various relations with related classes of groups.
11: Groups in our class satisfy our main theorem (\thref{main}), which
12: states that if the set of minimal \shl reducing rules is regular,
13: then our program succeeds in finding the finite state automaton which
14: accepts these rules.
15:
16: \noindent{\bf 3. Welding.} Here we describe one of the main new ideas in
17: this paper, namely welding. This process can be applied to any finite
18: state automaton. In our case it is the tool which enables us perform
19: the apparently impossible task of generating an infinite set of
20: Knuth--Bendix rules from a finite set. Welding has good properties
21: from the abstract language point of view (see \thref{welding unique}).
22: Welding has some important features.
23: Firstly, if an automaton starts by
24: accepting only pairs $(u,v)$ such that $\bar u = \bar v$ in $G$, then
25: the same is true after welding.
26: Secondly, the welded automaton can encode infinitely many distinct
27: equalities, even if the original only encoded a finite number.
28: Thirdly, the welded automaton is usually much smaller than the
29: original automaton.
30: At the end of this section we show that any
31: group determined by a regular set of rules is finitely presented.
32:
33: \noindent{\bf 4. Standard Knuth--Bendix.} In this section,
34: we describe the standard Knuth--Bendix process for
35: string rewriting, in the form in which it is normally used to analyze
36: finitely presented groups and monoids. We need this as a background against
37: which to describe our modifications.
38:
39: \noindent{\bf 5. Our version of Knuth--Bendix.}
40: We give a description of our Knuth--Bendix procedure.
41: We describe critical pair analysis, minimization of a rule and give
42: some brief details of our method of reduction using a two-variable
43: automaton which encodes the rules.
44:
45: \noindent{\bf 6. Correctness of our Knuth--Bendix Procedure.}
46: We prove that our Knuth--Bendix procedure does
47: what we want it to do. The proof is not at all easy. In part the
48: difficulty arises from the fact that we have to not only find new
49: rules, but also delete unwanted rules, the latter in the interests of
50: computational efficiency, or, indeed, computational feasibility.
51: Our main tool is the concept of a Thue path (see \thref{Thue path}).
52: Although it is hardly possible that this is a new concept, we have not
53: seen elsewhere its systematic use to understand the progress of
54: Knuth--Bendix with time.
55: One hazard in programming Knuth--Bendix is that some clever manoeuvre
56: changes the Thue equivalence relation.
57: The key result here is \thref{maintain congruence}, which carefully
58: analyzes the effect of various operations on Thue equivalence. In fact
59: it provides more precise control, enabling other hazards, such as
60: continual deletion and re-insertion of the same rule, to be avoided.
61: It is also the most important step in proving our main result,
62: \thref{main}. This says that if our program is applied to a group
63: defined by a regular set of minimal \shl rules, then, given sufficient time
64: and space, a finite state automaton accepting exactly these rules will
65: eventually be constructed by our program, after which it will loop
66: indefinitely, reproducing the same finite state automaton (but
67: requiring a steadily increasing amount of space for redundant information).
68:
69: \noindent{\bf 7. Fast reduction.}
70: We describe a surprisingly pleasant aspect
71: of our data structures and procedures, namely that reduction with
72: respect to our probably infinite set of rules can be carried out very
73: rapidly. Given a reducible word $w$, we can find a rule $(\lambda,\rho)$, such
74: that $w$ contains $\lambda$ as a subword, in a time which is linear in
75: the length of $w$.
76: Fast algorithms in computer science are often achieved by using finite
77: state automata, and the current situation is an example.
78: We explain how to construct the necessary automata and why they work.
79:
80: \noindent{\bf 8. A modified determinization algorithm.}
81: Here we describe a modification of the standard algorithm, to be
82: found in every book about computing algorithms, that
83: determinizes a non-deterministic finite state automaton. Our version
84: saves space as compared with the standard one. It is well suited
85: to our special situation. We give axioms which enable one to see when
86: this improved algorithm can be used.
87:
88: \noindent{\bf 9. Miscellaneous details.}
89: A number of miscellaneous points are discussed.
90: In particular, we compare our approach to that taken in
91: \textit{kbmag} (see \cite{Holt:KBMAG}).
92:
93: \section{Introduction}
94:
95: We give some background to our paper, and describe the class of groups
96: of interest to us here.
97:
98: A celebrated result of Novikov and Boone asserts that the word problem for
99: finitely presented groups is, in general, unsolvable. This means that
100: a finite presentation of a group is known and has been written down
101: explicitly, with the
102: property that there is no algorithm whose input is a word in the
103: generators, and whose output states whether or not the word is
104: trivial. Given a presentation of a group for which one is unable to
105: solve the word problem, can any help at all be given by a computer?
106:
107: The answer is that some help \textit{can} be given with the kind of
108: presentation that arises naturally in the work of many mathematicians,
109: even though one can formally prove that there is no procedure that
110: will \textit{always} help.
111:
112: There are two general techniques for trying to determine, with the help
113: of a computer, whether two words in a group are equal or not. One is
114: the Todd--Coxeter coset enumeration process and the other is the
115: Knuth--Bendix process. Todd-Coxeter is more adapted to finite groups
116: which are not too large. In this paper, we are motivated by groups which
117: arise in the study of low dimensional topology. In particular they are
118: usually infinite groups, and the number of words of length $n$ rises
119: exponentially with $n$. For this reason, Todd--Coxeter is not much use
120: in practice. Well before Todd--Coxeter has had time to work
121: out the structure of a large enough neighbourhood of the identity in the
122: Cayley graph to be
123: helpful, the computer is out of space.
124:
125: On the other hand, the Knuth--Bendix process is much better adapted to this
126: task, and it has been used quite extensively, particularly by Sims,
127: for example in connection with computer investigations into problems
128: related to the Burnside problem.
129: It has also been used to good effect by Holt and Rees in their automated
130: searching for isomorphisms and homomorphisms between two given
131: finitely presented groups (see \cite{HoltRees:Software}).
132: In connection with searching for a \shl-automatic structure on a group,
133: Holt was the first person to realize that the
134: Knuth--Bendix process might be the right direction to choose (see
135: \cite {EpsteinHoltRees}). Knuth--Bendix will run
136: for ever on even the most innocuous hyperbolic triangle groups, which are
137: perfectly easy to understand. Holt's successful plan was to use
138: Knuth--Bendix for a certain amount of time, decided heuristically, and
139: then to interrupt Knuth--Bendix and make a guess as to the automatic
140: structure. One then uses axiom-checking,
141: a part of automatic group theory (see
142: \cite[Chapter 6]{WPiG}), to see whether the guess is correct.
143: If it isn't correct, the checking process will produce suggestions as to how
144: to improve the guess.
145: Thus, using the concept of an automatic group as a mechanism for
146: bringing Knuth--Bendix to a halt has been one of the philosophical bases
147: for the work done at
148: Warwick in this field almost from the beginning.
149: In addition to the works already cited in this paragraph, the reader
150: may wish to look at \cite{HoltRees:Software} and \cite{Holt:WarwickSoftware}.
151:
152: For a \shl-automatic group, a minimal set of
153: Knuth--Bendix rules may be infinite, but it is always a regular
154: language (see \thref{automatic implies regular}),
155: and therefore can be encoded by a finite state machine.
156: In this paper, we carry this philosophical approach further,
157: attempting to compute this finite state machine directly, and to carry
158: out as much of the Knuth--Bendix process as possible using only
159: approximations to this machine.
160:
161: Thus, we describe a setup that can handle an infinite regular set of
162: Knuth--Bendix rewrite rules. For our setup to be effective, we need to
163: make several assumptions. Most important is the assumption that we
164: are dealing with a group, rather than with a monoid. Secondly, our
165: procedures are perhaps unlikely to be of much help unless the group actually
166: is \shl-automatic.
167: Our main theorem---see \thref{main}---is that our
168: Knuth--Bendix procedure succeeds in constructing the finite state
169: machine which accepts the (unique) confluent set of \shl minimal rules
170: describing a group, if and only if this set of rules is a regular
171: language.
172:
173: Previous computer implementations of the semi-decision procedure to
174: find the \shl-automatic structure on a group are
175: essentially specializations of the Knuth--Bendix procedure
176: \cite{KnuthBendix} to a
177: string rewriting context together with fast, but space-consuming,
178: automaton-based methods of performing word reduction relative to a finite set
179: of \shl-reducing rewrite rules. Since \shl-automaticity
180: of a given finite presentation is, in general, undecidable, space-efficient
181: approaches to the Knuth--Bendix procedure are desirable.
182: Our new algorithm performs a Knuth--Bendix type procedure relative
183: to a possibly infinite regular set of \shl-reducing rewrite rules,
184: together with a companion word reduction algorithm which has been designed with
185: space considerations in mind.
186:
187: In standard Knuth--Bendix, there is a tension between time and space
188: when reducing words. Looking for a left-hand side in a word can take a
189: long time, unless the left-hand sides are carefully arranged in a data
190: structure that traditionally
191: takes a lot of space. Our technique can do very rapid
192: reduction without using an inordinate amount of space (although, for
193: other reasons, we have not been able to save as much space as we
194: originally hoped).
195: This is explained in \thref{A modified determinization algorithm}.
196:
197:
198: We would like to thank Derek Holt for many conversations about this
199: project, both in general and in detail. His help has, as always, been generous
200: and useful.
201: