Reduction Operators and Completion of Rewriting Systems

TL;DR

This paper introduces a lattice-based algebraic framework for rewriting systems using reduction operators, establishing their properties, confluence, and connections to Gr"obner bases, including generalizations to non-total orders.

Contribution

It provides a novel algebraic and lattice-theoretic formulation of rewriting systems and completion, linking reduction operators with Gr"obner bases and extending to non-total orders.

Findings

Reduction operators form a lattice structure.

Confluence is equivalent to the Church-Rosser property.

Algebraic formulation of completion and relation to Gr"obner bases.

Abstract

We propose a functional description of rewriting systems where reduction rules are represented by linear maps called reduction operators. We show that reduction operators admit a lattice structure. Using this structure we define the notion of confluence and we show that this notion is equivalent to the Church-Rosser property of reduction operators. In this paper we give an algebraic formulation of completion using the lattice structure. We relate reduction operators and Gr\"obner bases. Finally, we introduce generalised reduction operators relative to non total ordered sets.