Term rewriting and the word problem for certain infinite presentations of groups.
Roger Eric Needham · Deep Blue (University of Michigan) · 1992
A Knuth-Bendix procedure for string rewriting, when applied to a presentation for a group G in an attempt to solve the word problem, often diverges. In this thesis we develop a Knuth-Bendix procedure for equational term rewriting which can find an infinite, confluent presentation for G in certain cases where previous procedures fail. As do finite ones, these presentations yield an efficient solution of the word problem for G. Our procedure requires the presentations to be parameterized, in the sense that they can be expressed as finitely many rules between terms, the latter being products of words and words with syntactic variables as formal exponents. The exponents are quantified over the positive integers. We introduce restricted equational rewriting, a generalization of rewriting modulo a congruence, in which one seeks to transform a rewrite system into one which computes unique normal forms, up to congruence, only for terms from a distinguished subset of the set of all terms. We express the completion procedure in terms of an equational inference system a la Bachmair and Dershowitz. We generalize the technique of equational narrowing so as to make use of such rewrite systems, and construct a unification algorithm modulo the usual properties of positive integer exponents. We give applications of the procedure to various Coxeter groups, including ones which fall outside the scope of a theorem of Le Chenadec, which characterizes confluent presentations for Coxeter groups of large type.