Termination and completion modulo associativity, commutativity and identity (Q1199927)

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 there are two well-known problems: (a) If one wants to orient an equation \(s=t\) into a rule \(\phi\mid s\to t\), in general not all instances of \(s=t\) can be oriented. Those that cannot be oriented, i.e. those instantiations that do not satisfy \(\phi\), have to be kept as equations. (b) In the same way, if an equation \(s=t\) can be reduced to \(s=t'\) by \(\phi\mid\ell\to r\), then in general not all instances of \(t\) can be reduced to \(t'\). Some instances of \(s=t\) not reducible by the rule have to be kept as equations if \(s=t\) is replaced by \(s=t'\). Keeping these problems in mind the techniques of AC-completion carry over to constrained AC1-completion.