Termination and completion modulo associativity, commutativity and identity
type: Item
instance of: scholarly article
title: Termination and completion modulo associativity, commutativity and identity
zbMATH Open document ID: 0759.68047
DOI: 10.1016/0304-3975(92)90165-C
author: Jean-Pierre Jouannaud
author: Claude Marché
published in: Theoretical Computer Science
publication date: 1993-01-17T00:00:00Z
review text: For rewriting modulo a set \(E\) of equational axioms one has to solve three problems: (1) Matching and unification modulo \(E\), (2) termination of the rewrite relation \(\to_{R/E}\) and (3) completion. For the most important case where \(E\) is a set or AC-axioms (associativity and commutativity) these problems are already solved. In practice one needs other cases too, e.g. AC1 (AC \(+\) identity) or ACI (AC \(+\) idempotency). In the present paper the problems (2) and (3) are studied for the case AC1. The usual way to solve problems (2) is to construct an \(E\)-compatible reduction ordering \(>\) such that \(R\subseteq>\). Then \(\to_{R/E}\) is terminating. Unfortunately, AC1-compatible reduction ordering are very weak. For example, if \(+\) is an AC1-symbol and \(f(x+y)\) is the left-hand side of a rule then \(f(s)\) is reducible for every term \(s\) since \(f(s)=_{\text{AC1}}f(s+0)\). To overcome this problem there is an idea of \textit{P. Baird}, \textit{S. Peterson} and \textit{R. W. Wilkerson} [RTA- Conference 1989, Lect. Notes Comput Sci., Vol. 355 (1989)] to apply constrained rewriting, i.e., to forbid instantiations of variables in a rule by 0 that may cause non-termination. For example, the rule \(- (x+y)\to(-x)+(-y)\) is replaced by \((x\neq 0\wedge y\neq 0)\mid -(x+y)\to(- x)+(-y)\). Using this idea of constrained rewriting the authors are able to extend (well-known) AC-simplification orderings to restricted AC1- simplification orderings and so to prove termination of the constrained rewrite relation. For doing AC1-completion the authors combine \(E\)-completion with constrained rewriting. From \(E\)-completion the techniques for proof transformations are used. To be more specific, the AC-completion of \textit{L. Bachmair} and \textit{N. Dershowitz} [Theor. Comput. Sci. 67, No. 2/3, 173-201 (1989; Zbl 0686.68021)] and their extended rules (to avoid critical pairs between a rule and an AC-axiom) are used. As far as constrained rewriting is concerned the…
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 96270
reviewed by: Jürgen Avenhaus
describes a project that uses: REVE
MaRDI profile type: MaRDI publication profile
cites work: Completion for rewriting modulo a congruence
cites work: Termination orderings for associative-commutative rewriting systems
cites work: Complete sets of reductions modulo associativity, commutativity and identity
cites work: Q3783523
cites work: Termination of rewriting
cites work: Q4385532
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Q5581665
cites work: New decision algorithms for finitely presented commutative semigroups
cites work: Complete Sets of Reductions for Some Equational Theories
Recommended article: AC-Termination of rewrite systems: A modified Knuth-Bendix ordering
Recommended article: On how to move mountains ‘associatively and commutatively’
Recommended article: Termination Modulo Combinations of Equational Theories
Recommended article: Complete sets of reductions modulo associativity, commutativity and identity
Recommended article: On ground AC-completion
description: scientific article; zbMATH DE number 96270