Syzygies among reduction operators

TL;DR

This paper introduces syzygies among reduction operators, relating them to algebra presentations, and develops a basis construction method to optimize rewriting procedures, exemplified by Gr{"o}bner basis computation.

Contribution

It defines syzygies for reduction operators, connects them to algebra presentations, and provides a basis construction method to improve confluence and reduction efficiency.

Findings

Constructed a basis for syzygies among reduction operators

Linked syzygies to confluence in rewriting systems

Optimized completion procedures for reduction operators

Abstract

We introduce the notion of syzygy for a set of reduction operators and relate it to the notion of syzygy for presentations of algebras. We give a method for constructing a linear basis of the space of syzygies for a set of reduction operators. We interpret these syzygies in terms of the confluence property from rewriting theory. This enables us to optimise the completion procedure for reduction operators based on a criterion for detecting useless reductions. We illustrate this criterion with an example of construction of commutative Gr{\"o}bner basis.