Normalized Rewriting -- Application to Ground Completion and Standard Bases

Abstract

We define a new kind of rewriting which is a variant of the usual notion of rewriting modulo an equational theory. This rewrite relation allows us to rewrite modulo theories for which the previous notion was not applicable, including identity, idempotency, Abelian group theory and commutative ring theory. We obtain a new completion algorithm which contains as instances many completion-like algorithms, for example AC (associative-commutative) completion algorithm, constrained AC1-completion, Buchberger's algorithm for computing standard bases of polynomial ideals over a commutative ring.

We investigate then the particular case of completion of ground equations, and we prove by a uniform method the termination of the completion process for a interesting class of equational theories, generalising the result of Narendran and Rusinowitch for ground equations modulo AC, and the result of Buchberger for polynomial ideals, which is the case of ground equations modulo the theory of commutative rings. We obtain also new decidability results on the word problem in ground theories modulo AC and identity, idempotency, nilpotency (new results to our knowledge), and the cases of ground theories modulo the theory of Abelian groups and commutative rings, which is already known in the case when the signature contains only constants, but is new for extended signatures.

full paper