Reduction operators and completion of rewriting systems. (January 2018)

• Record Type: Journal Article
• Authors: Chenavier, Cyrille
• Is Part Of: Journal of symbolic computation. Volume 84(2018)
• Page Start: 57
• Page End: 83
• Publication Date: 2018-01
• Subjects: Reduction operators -- Completion -- Noncommutative Groebner bases; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2017.03.002
• Languages: English
• ISSNs: 0747-7171

Abstract

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 notions of confluence and of Church–Rosser property. We show that these notions are equivalent. We give an algebraic formulation of completion and show that such a completion exists using the lattice structure. We interpret the confluence for reduction operators in terms of Gröbner bases. Finally, we introduce generalised reduction operators relative to non totally ordered sets.