Systems of reductions (Q1098283)

The volume presents an exposition of basic concepts and techniques from the area of systems of reductions (or term-rewriting systems). The notion of reduction is conceptually a simplification of the notion of equality: if reflexivity is given up, one is only allowed to use equations (between terms in a universal algebra) as directed rewriting rules, i.e. reductions. Generally, given a set of equations defining a universal algebra, it is not sufficient just to orient the equations into reductions, but some transformation of the system is necessary (the completion of the system of reductions). To be of some practical use, a term-rewriting system is required to satisfy certain essential properties, especially that of confluency (also called Church-Rosser property), and finite termination. As far as these important properties are undecidable in the general case, a detailed study of sufficient conditions applicable when building a term-rewriting system is needed. The book consists of five chapters. The first of them introduces general concepts from universal algebras, unification, theory of formal languages, and presents basic undecidable problems in general algebras. Chapters 2 is devoted to finite sets of reductions. Basic properties of reduction systems are defined and their properties proved, completion algorithm (the Knuth-Bendix algorithm) is introduced, and several sections are devoted to the analysis of this algorithm for various classes of algebras. Chapter 3 studies infinite sets of reductions, i.e. the case when the completion algorithm does not terminate. Two classes of infinite systems are studied: regular systems and forward-backward systems. For each of them undecidability of the confluence property is shown, and possible sufficient conditions for confluence are formulated. Chapter 4 is devoted to the study of automata accepting reducible words, and the complexity of the reduction algorithm is analyzed. Chapter 5, written by F. Otto, investigates decision problems concerning finitely presented monoids. Also in this case all the problems of interest are undecidable, and restricted classes allowing decidability are studied. The exposition of the material in the book is self-contained. Besides of original results obtained by the authors, parts of it present an introduction into the area of algebraic term-rewriting systems.