Knuth-Bendix for groups with infinitely many rules

TL;DR

This paper introduces a novel automaton-based method to efficiently perform the Knuth-Bendix rewriting process for groups with infinitely many rules, enabling fast reduction of words in shortlex order.

Contribution

It presents a new approach using a two-variable automaton and a welding operation to handle infinite rewriting rules in groups, improving determinization techniques.

Findings

Automaton can store infinite rewriting rules efficiently.

Welding operation enhances automaton determinization.

Method enables fast word reduction in groups with infinite rules.

Abstract

It is shown how to use a small finite state automaton in two variables in order to carry out the Knuth-Bendix process for rewriting words in a group in shortlex order. The two-variable automaton can be used to store an infinite set of rules and to carry out fast reduction of arbitrary words using this infinite set. We introduce a new operation, which we call welding, which applies to an arbitrary finite state automaton. We show how to improve on the standard subset construction to determinize a non-deterministic automaton under special conditions which hold in our situation.