text:
\section{Introduction}

\subsubsection*{Completion procedures}
The critical-pair completion (CPC) is an approach developed in the mid sixties that combines completion procedures and the notion of \emph{critical pair}, also called \emph{critical branching}~\cite{Shirshov62,Bergman78,Buchberger87}. It originates from theorem proving~\cite{Robinson65}, polynomial ideal theory~\cite{Janet20,Buchberger65}, and the word problem in usual algebras~\cite{KnuthBendix70,Nivat73,LeChenadec84}.
This approach has found many applications to solve algorithmic problems, see \cite{Buchberger87,IoharaMalbos20} for an historical account.
In the mid eighties CPC has found original and deep applications in algebra in order to solve coherence problems for monoids~\cite{Squier94,GuiraudMalbos18}, and monoidal categories~\cite{GuiraudMalbos12mscs, CurienMimram17}, or to compute homological invariants of associative algebras \cite{Anick86}, and monoids \cite{Squier87,Kobayashi90}. The CPC approach was extended to two-dimensional rewriting systems in \cite{Mimram10,GuiraudMalbos09}.
More recently, higher-dimensional extensions of the critical-pair completion approach were used for the computation of cofibrant replacements of algebraic and categorical structures~\cite{GuiraudMalbos12advances, GaussentGuiraudMalbos15, MimramMalbos16,GuiraudHoffbeckMalbos19}.
These constructions are actually higher-dimensional extensions of the critical-pair completion approach, where the obstructions in each dimension are formulated in terms of critical branchings. While generators and rules are in dimension $1$ and $2$ respectively, the critical branchings, and the critical triple branchings, that is overlappings of rules on critical branchings, describe $3$-dimensional and $4$-dimensional cocycles respectively. This generalizes in higher-dimensions, where for $n\geq 4$, the $n$-dimensional cocycles are described by overlappings of a rule on a critical $(n-1)$-branching. These constructions based on critical-pair completion are known for monoids, small categories, and algebras over a field. However, the extension of these methods to a wide range of algebraic structures is made difficult because of the interaction between the rewriting rules and the inherent axioms of the algebraic structure. For this reason, the higher-dimensional extensions of the critical-pair completion approach for a wide range of algebraic structures, including groups, Lie rings, is still an open problem.

\subsubsection*{Critical branching lemma}
One of the main tools to reach confluence in critical-pair completion procedures for algebraic rewriting systems is the \emph{critical branching lemma}, by Knuth-Bendix, \cite{KnuthBendix70}, and Nivat, \cite{Nivat73}. Nivat showed that the local confluence of a string rewriting system (SRS) is decidable, whether it is terminating or not.
The proof of this result is based on classification of the local branchings into \emph{orthogonal} branchings, that involve two rules that do not overlap, and \emph{overlapping} branchings. A \emph{critical branching} is a minimal overlapping application of two rules on the same redex.
When the orthogonal branchings are confluent, if all critical branchings are confluent, then local confluence holds.
Thus, the main argument to achieve critical branching lemma is to prove that orthogonal and overlapping branchings are confluent.
For SRS and term rewriting systems (TRS), orthogonal branchings are always confluent, and confluence of critical branchings implies confluence of overlapping branchings. The situation is more complicated for rewriting systems on a linear structure.

The well known approaches of rewriting in the linear context consist in orienting the rules with respect to an ambiant monomial order, and critical branching lemma is well known in this context. However,
some algebras do not admit any higher-dimensional finite convergent presentation on a fixed set of generators with respect to a monomial order, \cite{GuiraudHoffbeckMalbos19}.
Due to algebraic perspectives, an approach of linear rewriting where the orientation of rules does not depend of a monomial order was introduced in~\cite{GuiraudHoffbeckMalbos19}.
However, in that setting there are two conditions to guarantee a critical branching lemma, namely termination and positivity of reductions. A positive reduction for a linear rewriting system (LRS), as defined in~\cite{GuiraudHoffbeckMalbos19}, is the application of a reduction rule on a monomial that does not appear in the polynomial context.
For instance, consider the LRS on an associative algebra over a field $\mathbb{K}$ given in \cite{GuiraudHoffbeckMalbos19} defined by the following two rules
\[
\alpha: xy\rightarrow xz,
\qquad
\beta : zt \rightarrow 2yt.
\]
It has no critical branching, but it has the following non-confluent additive branching:

\vskip-10pt

\[
\xymatrix @R=0.18em {
&& 4xyt
	\ar [r] ^-*+{4\alpha t}
& 4xzt
	\ar [r] ^-*+{4x\beta}
& \cdots
\\
& 2xzt
	\ar@/^/ [ur] ^-*+{2x\beta}
	\ar@{.>} [dr] ^(0.55)*+{xzt + x\beta}
\\
xyt + xzt
	\ar@/^/ [ur] ^-*+{\alpha t + xzt}
	\ar@/_/ [dr] _-*+{xyt + x\beta}
	\ar@{} [rr] |-{ =}
&& xzt + 2xyt
\\
& 3xyt
	\ar@{.>} [ur] _(0.55)*+{\alpha t + 2xyt}
	\ar@/_/ [dr] _-*+{3\alpha t}
\\
&& 3xzt
	\ar [r] _-*+{3x\beta}
& 6xyt
	\ar [r] _-*+{6\alpha t}
& \cdots
}
\]
The dotted arrows correspond to non positive reductions. This example illustrates that the lack of termination is an obstruction to confluence of orthogonal branchings in a \emph{left-monomial LRS}, that is whose rules transform a monomial into a polynomial. Indeed, the critical branching lemma for linear $2$-dimensional polygraphs states that a terminating left-monomial linear polygraph is locally confluent if and only if all its critical branchings are confluent, {\cite[Theorem 4.2.1]{GuiraudHoffbeckMalbos19}}

\subsubsection*{Rewriting modulo}
Rewriting modulo appears naturally in algebraic rewriting when studied reductions are defined modulo the axioms of an ambiant algebraic or categorical structure, \emph{e.g.} rewriting in commutative, groupoidal, linear, pivotal, weak structures. Furthermore, rewriting modulo facilitates the analysis of confluence. In particular, rewriting modulo a set of relations makes the property of confluence easier to prove. Indeed, the family of critical branchings that should be considered in the analysis of confluence is reduced, and the non-orientation of a part of the relations allows more flexibility when reaching confluence.

The most naive approach of rewriting modulo is to consider the rewriting system $\ere{P}{R}$ consisting in rewriting on congruence classes modulo the axioms $P$. This approach works for some equational theories, such as associative and commutative theories. However, it appears inefficient in general for the analysis of confluence. Indeed, the reducibility of an equivalence class needs to explore all the class, hence it requires all equivalence classes to be finite.
Another approach of rewriting modulo has been considered by Huet in \cite{Huet80}, where rewriting sequences involve only oriented rules and no equivalence steps, and the confluence property is formulated modulo equivalence. However, for algebraic rewriting systems such rewriting modulo is  too restrictive for computations, see~\cite{JouannaudLi12}.
Peterson and Stickel introduced in~\cite{PetersonStickel81} an extension of Knuth-Bendix's completion procedure,~\cite{KnuthBendix70}, to reach confluence of a rewriting system modulo an equational theory, for which a finite, complete unification algorithm is known. They applied their procedure to rewriting systems modulo axioms of associativity and commutativity, in order to rewrite in free commutative groups, commutative unitary rings, and distributive lattices.
Jouannaud and Kirchner enlarged this approach in \cite{JouannaudKirchner84} with the definition of rewriting properties for any rewriting system modulo~$S$ such that $R\subseteq S \subseteq \ere{P}{R}$.
They also proved a critical branching lemma and developed a completion procedure for rewriting systems modulo $\er{P}{R}$, whose one-step reductions consist in application of a rule in $R$ using $P$-matching at the source. Their completion procedure is based on a finite $P$-unification algorithm. Bachmair and Dershowitz in \cite{BachmairDershowitz89} developed a generalisation of Jouannaud-Kirchner's completion procedure using inference rules. Several other approaches have also been studied for TRS modulo to deal with various equational theories, see \cite{Viry95, Marche96}.

\subsubsection*{Algebraic polygraphs}
In this article, we introduce a categorical model for rewriting in algebraic structures which formalizes the interaction between the rules of the rewriting system and the inherent axioms of the algebraic structure.
In Section~\ref{S:Preliminaries}, we recall the notion of cartesian $2$-dimensional polygraph introduced in \cite{MalbosMimram20}, corresponding to rewriting systems that present a Lawvere algebraic theory. A cartesian $2$-polygraph defines a categorical interpretation of TRS. It is defined by an equational signature $(P_0,P_1)$ and a cellular extension of the free algebraic theory $\freetha{P}_1$ on $(P_0,P_1)$. One defines in Section~\ref{S:AlgebraicPolygraphsModulo} the structure of \emph{algebraic polygraph} as a data made of a cartesian $2$-polygraph $P$ and a set $Q$ of generating ground $1$-cells and a cellular extension $R$ on the ground $1$-cells.

\subsubsection*{An algebraic critical branching lemma}
In this work we introduce an algebraic setting for the formulation of the critical branching lemma. We define the structure of algebraic polygraph modulo which formalizes the interaction between the rules of the rewriting system and the inherent axioms of the algebraic structure. Then we prove a formulation of the Newman lemma modulo, \cite{Newman42}, for quasi-terminating algebraic polygraphs modulo:

\begin{quote}
{\bf Theorem \ref{T:NewmanLemmaModulo}.}
\emph{
Let $\Pr$ be a quasi-terminating algebraic polygraph modulo, and $\sigma$ be a positive strategy on $\Pr$. If $\Pr$ is locally $\sigma$-confluent modulo, then it is $\sigma$-confluent modulo.
}
\end{quote}

We show a critical branching lemma for algebraic polygraphs modulo. We deduce from this result a critical branching lemma for rewriting systems on algebraic structures whose axioms are specified by TRS satisfying appropriate convergence relations modulo associativity and commutativity. Finally, we explicit our results in linear rewriting, and explain why termination is a necessary condition to characterize local confluence in that case.

\begin{quote}
{\bf Theorem \ref{T:AlgebraicCriticalBranchingTheorem}.}
\emph{
Let $\Pr=(P,Q,R,S)$ be an algebraic polygraph modulo having a positive confluent strategy $\sigma$. If $\ere{P}{R}$ is quasi-terminating, then an algebraic rewriting system on $\Pr$ is locally confluent if and only if its critical branchings are confluent.
}
\end{quote}

\subsubsection*{Organisation of the article}
In Section~\ref{S:Preliminaries}, we recall the categorical structure of cartesian polygraph introduced in \cite{MalbosMimram20}, and we define progressive examples of cartesian $2$-polygraphs presenting various algebraic theories, until the main cartesian $2$-polygraph presenting the theory of modules over a commutative ring. In Section~\ref{S:AlgebraicPolygraphs}, we introduce the notion of algebraic polygraph modulo, and their rewriting properties. We define the notion of positive reduction with respect to an algebraic polygraph in order to define algebraic rewriting systems, whose rules are induced by the positive reductions.
In Section~\ref{S:ConfluenceAlgebraicPolygraphsModulo}, we present the confluence property with respect to a positive strategy following \cite{DupontMalbos18b} and we prove the Newman confluence lemma and the critical branching lemma in this setting. Finally, last section states the algebraic critical branching lemma, that we apply to string, linear, and group rewriting.

\section{Preliminaries on algebraic theories}
\label{S:Preliminaries}

In this section we recall notions on algebraic theories from \cite{Lawvere63} and the structure of cartesian polygraph introduced in~\cite{MalbosMimram20}.

\subsection{Cartesian polygraphs and theories}

\subsubsection{Signature and terms}
\label{SSS:SignatureAndTerms}
A \emph{signature} is defined by a set $P_0$ of \emph{sorts} and a $1$-polygraph, \emph{i.e.} a directed graph,
\[
\xymatrix{
P_0^\ast
&
\ar@<+0.5ex>[l]^-{\partial_0^+}
\ar@<-0.5ex>[l]_-{\partial_0^-}
P_1
}
\]
on the free monoid $P_0^\ast$ over $P_0$. Elements of $P_1$ are called \emph{operations}. For an operation $\alpha$ in~$P_1$, its source $\partial_0^-(\alpha)$ is called its \emph{arity} and its target $\partial_0^+(\alpha)$ its \emph{coarity}. For sorts $s_1,\ldots,s_k$, we denote $\sort{s}=s_1\ldots s_k$ their product in the free monoid $P_0^\ast$. We denote $\size{\sort{s}}=k$ the \emph{length} of $\sort{s}$ and the sort $s_i$ in $\sort{s}$ will be denoted by $\sort{s}_i$.

Recall from \cite{Lawvere63} that an \emph{(multityped Lawvere algebraic) theory} for a given set of sorts $P_0$ is a category with finite products $\tha{T}$ together with a map $\iota$ from $P_0$ and with values in its set of $0$-cells $\tha{T}_0$, and such that every $0$-cell in $\tha{T}_0$ is isomorphic to a finite product of $0$-cells in $\iota(P_0)$.
We denote by $\freetha{P}_1$ the free theory generated by a signature $(P_0,P_1)$ whose  products on $0$-cells of $\freetha{P}_1$ are induced by products of sorts in $P_0^\ast$, and the $1$-cells of $\freetha{P}_1$ are \emph{terms} over $P_1$ defined by induction as follows:
\begin{enumerate}[{\bf i)}]
\item the canonical projections $x_i^{\sort{s}} : \sort{s} \rightarrow \sort{s}_i$, for $1\leq i \leq \size{\sort{s}}$ are terms, called \emph{variables},
\item for any terms $f:\sort{s} \rightarrow r$ and $f':\sort{s} \rightarrow r'$ in $\freetha{P}_1$, there exists a unique $1$-cell $\pair{f,f'} : \sort{s} \rightarrow rr'$, called \emph{pairing} of  terms $f,f'$, such that $x_1^{rr'}\pair{f,f'} = f$ and $x_2^{rr'}\pair{f,f'} = f'$,
\item for every operation $\varphi : \sort{r} \rightarrow s$ in $P_1$, $\sort{s}$ in $S_0^\ast$ and terms $f_i : \sort{s} \rightarrow \sort{r}_i$ in $\freetha{P}_1$ for $1\leq i \leq \size{\sort{r}}$, there is a term $\varphi\pair{f_1,\ldots,f_{\size{\sort{r}}}} : \sort{s} \rightarrow s$.
\end{enumerate}
We define the \emph{size} of a term $f$ as the minimal number, denoted by $\size{f}$, of operations used in its definition.

For any $0$-cells $\sort{s},\sort{s}'$ in $\freetha{P}_1$, we denote by $1_{\sort{s}}$ the identity $1$-cell on a $0$-cell $\sort{s}$, we denote by $\epsilon_{\sort{s}}$ the \emph{eraser} $1$-cell defined as the unique $1$-cell from $\sort{s}$ to the terminal $0$-cell $\ob{0}$, and we denote by $\delta_{\sort{s}}=\pair{1_{\sort{s}},1_{\sort{s}}} : \sort{s} \rightarrow \sort{s}\times\sort{s}$ the \emph{duplicator} $1$-cell.
We denote respectively by $x_{\sort{s}}^{\sort{s}\sort{s'}}:\sort{s}\sort{s}'\rightarrow \sort{s}$ (resp. $x_{\sort{s}'}^{\sort{s}\sort{s'}}:\sort{s}\sort{s}'\rightarrow \sort{s}'$) the canonical projections. Finally, we denote by $\tau_{\sort{s},\sort{s}'}:\sort{s}\sort{s}' \rightarrow \sort{s}'\sort{s}$ the \emph{exchange} $1$-cell defined by
$\tau_{\sort{s},\sort{s}'} = \pair{x_{\sort{s}'}^{\sort{s}\sort{s'}},x_{\sort{s}}^{\sort{s}\sort{s'}}
}$.

\subsubsection{Two-dimensional cartesian polygraph}
A \emph{cartesian $2$-polygraph} is a data $(P_0,P_1,P_2)$ made of
\begin{enumerate}[{\bf i)}]
\item a signature $(P_0,P_1)$,
\item a cellular extension of the free theory $\freetha{P}_1$, that is a set $P_2$ equipped with two maps
\[
\xymatrix{
\freetha{P}_1
&
\ar@<+0.5ex>[l]^-{\partial_1^+}
\ar@<-0.5ex>[l]_-{\partial_1^-}
P_2
}
\]
satisfying the following \emph{globular conditions} $\partial_0^\mu\circ \partial_1^- = \partial_0^\mu\circ \partial_1^+$, for $\mu\in\{-,+\}$.
\end{enumerate}

An element $\alpha$ of $P_2$ is called a \emph{rule} with \emph{source} $\partial_-(\alpha)$ and target $\partial_+(\alpha)$, that we denote respectively by $\alpha_-$ and $\alpha_+$, so that such a rule is denoted by $\alpha : \alpha_- \Rightarrow \alpha_+$. The globular conditions impose that such a rule $f\Rightarrow g$ relates terms of same arity $\sort{s}$ and same coarity $\ob{r}$, and it will be pictured as follows:
\[
\xymatrix@C=3em{
\sort{s}
	\ar@/^3ex/ [r] ^-{f} ^{}="src"
	\ar@/_3ex/ [r] _-{g} ^{}="tgt"
	\ar@2 "src"!<0pt,-10pt>;"tgt"!<0pt,10pt> ^-{\alpha}
&
\ob{r}
}
\]

\subsubsection{Two-dimensional theories}
Recall that a \emph{$2$-theory} on a set $P_0$ of sorts is a $2$-category with the additional following cartesian structure:
\begin{enumerate}[{\bf i)}]
\item it has a terminal $0$-cell \ob{0}, that is for every $0$-cell $\sort{s}$ there exists a unique $1$-cell $e_{\sort{s}} : \sort{s} \rightarrow \ob{0}$, called \emph{eraser}, and the identity $2$-cell is the unique endo-$2$-cell on an eraser,
\item it has products, that is for all $0$-cells $\sort{r},\sort{r}'$ there is a product $0$-cell $\sort{r}\sort{r}'$ and $1$-cells $x_{\sort{r}}^{\sort{r}\sort{r}'}: \sort{r}\sort{r}' \rightarrow \sort{r}$ and $x_{\sort{r}'}^{\sort{r}\sort{r}'} \rightarrow \sort{r}'$ satisfying the two following conditions:
\begin{itemize}
\item for any $1$-cells $f_1:\sort{s} \rightarrow \sort{r}$ and $f_2:\sort{s} \rightarrow \sort{r}'$, there exists a unique pairing $1$-cell $\pair{f_1,f_2} : \sort{s} \rightarrow \sort{r}\sort{r'}$, such that $x_{\sort{r}}^{\sort{r}\sort{r}'}\pair{f_1,f_2} =f_1$, and $x_{\sort{r}'}^{\sort{r}\sort{r}'}\pair{f_1,f_2} =f_2$,
\item for any $2$-cells $\alpha_i : f_i \Rightarrow f_i'$, $i=1,2$, there exists a unique $2$-cell $\pair{\alpha_1,\alpha_2} : \pair{f_1,f_2} \Rightarrow \pair{f_1',f_2'}$.
\end{itemize}
\end{enumerate}

We refer the reader to \cite{MalbosMimram20} for a detailed construction.

\subsubsection{Free $2$-theories}
\label{SS:Free2Theory}
We denote by $\freetha{P}_2$ the free $2$-theory generated by a cartesian $2$-polygraph $(P_0,P_1,P_2)$.
We briefly recall its construction and refer the reader to \cite{MalbosMimram20} for details.
The underlying $1$-category of $\freetha{P}_2$ is the free theory $\freetha{P}_1$ generated by the signature $(P_0,P_1)$.
Its $2$-cells are defined inductively as follows:
\begin{enumerate}[{\bf i)}]
\item for any $2$-cell $\alpha: u \Rightarrow v$ in $P_2$ and $1$-cell $w$ in $\freetha{P}_1$, there is a $2$-cell $\alpha w: u \star_0 w \Rightarrow v \star_0 w$ in $\freetha{P}_2$,
\item for any $2$-cells $\alpha$, $\beta$ in $\freetha{P}_2$, there is a $2$-cell $\pair{ \alpha, \beta} : \pair{\alpha_-, \beta_-} \Rightarrow \pair{\alpha_+,\beta_+}$ in $\freetha{P}_2$,
\item for any $2$-cell $\alpha$ in $\freetha{P}_2$, there are $2$-cells in $\freetha{P}_2$ of the form $A[\alpha] : A[\alpha_-] \Rightarrow A[\alpha_+]$ where $A[\boxempty]$ denotes an \emph{algebraic context} of the form:
\[
A[\boxempty] := f\pair{\id_{f_1},\ldots,\boxempty_i,\ldots,\id_{f_k}} : \sort{s} \rightarrow \ob{r},
\]
where $f_1,\ldots,f_k:\sort{s} \rightarrow \sort{r_i}$ and $f: \sort{r} \rightarrow \ob{r}$ are $1$-cells of $\freetha{P}_1$, and $\boxempty_i$ is the $i$-th element of the pairing.
\item these $2$-cells are submitted to the following exchange relations
\begin{equation*}
\label{E:exchangeRelation2cells}
 f \pair{f_1,...,\alpha,...,f_j,...,f_k} \star_1 f \pair{f_1,...,f_i,...,\beta,...,f_k} = f \pair{f_1,...,f_i,...,\beta,...,f_k}\star_1 f \pair{f_1,\alpha,...,f_j,...,f_k}
\end{equation*}
where $f_i: \sort{s} \rightarrow \sort{r_i}$ and $f: \sort{r} \rightarrow \ob{r}$ are $1$-cells in $\freetha{P}_1$, $\alpha$ and $\beta$ are $2$-cells in $P_2$.
We will denote by $\pair{f_1,...,\alpha,...,\beta,...,f_k}$ the $2$-cell defined above.
\item The $\star_1$-composition of $2$-cells in $P_2$ is given by sequential composition.
\end{enumerate}

The source and target maps $\partial^\pm_1$ extend to $\freetha{P}_2$ and we denote $a_-$ and $a_+$ for $\partial_1^-(a)$ and $\partial_1^+(a)$.

\subsubsection{Ground terms}
Let $(P_0,P_1,P_2)$ be a cartesian $2$-polygraph.
A \emph{ground term} in the free theory $\freetha{P}_1$ is a term with source $\ob{0}$.
A $2$-cell $a$ in the free theory $\freetha{P}_2$ is called \emph{ground} when $a_-$ is a ground term. Finally, an algebraic context
$A[\boxempty] = f\pair{f_1,\ldots,\boxempty_i,\ldots f_{\size{\sort{r}}}}$ is called \emph{ground} when the $f_i$ are ground terms.

\subsubsection{Free $(2,1)$-theory}
A \emph{free $(2,1)$-theory} is a theory $\tha{T}$ whose any $2$-cell is invertible with respect the $\star_1$-composition. That is, any $2$-cell $\alpha$ of $\tha{T}_2$ has an inverse
$\alpha^- : \alpha_+ \Rightarrow \alpha_-$
satisfying the relations $ \alpha \star_1 \alpha^- = 1_{\alpha_-}$ and~$\alpha^- \star_1 \alpha = 1_{\alpha_+}$.

We denote by $\tck{P}_2$ the free $(2,1)$-theory generated by a cartesian $2$-polygraph $(P_0,P_1,P_2)$. The $2$-cells of the $(2,1)$-theory $\tck{P}_2$ corresponds to elements of the equivalence relation generated by $P_2$.

\subsubsection{Rewriting properties of cartesian polygraphs}
Let $P$ be a cartesian $2$-polygraph.
The algebraic contexts of the cartesian $2$-polygraph $P$ can be composed, and we will denote by $AA'[\boxempty] := A[A'[\boxempty]]$. In the same way, one defines a \emph{multi-context} (of arity $2$) as
\[
B[\boxempty_i , \boxempty_j] := f \pair{\id_{f_1} , \ldots, \boxempty_i, \ldots, \boxempty_j, \ldots, \id_{f_k}},
\]
where the $f_k: \sort{s} \rightarrow \sort{r_k}$ and $f: \sort{r} \rightarrow \ob{r}$ are $1$-cells in $\freetha{P}_1(X)$, and $\boxempty_i$ (resp. $\boxempty_j$) has to be filled by a $1$-cell $g_i: \sort{s} \rightarrow \sort{r_i}$ (resp. $g_j: \sort{\ob{s}} \rightarrow \sort{\ob{r}_j}$).

A $2$-cell of the form $A[\alpha w]$ where $A$ is an algebraic context, $w$ is a $1$-cell in $\freetha{P}_1$ and $\alpha$ is a rule in $P_2$ is called a \emph{rewriting step of $P$}.
A \emph{rewriting path} is a non-identity $2$-cell of $\freetha{P}_2$. Such a $2$-cell can be decomposed as a $\star_1$-composition  of rewriting steps:
\[
\alpha=A_1[\alpha_1] \star_1 A_2[\alpha_2] \star_1 \ldots A_k[\alpha_k],
\]

The \emph{length} of a $2$-cell $\alpha$ in $\freetha{P}_1$, denoted by $\ell(f)$, is the minimal number of rewriting steps in any $\star_1$-decomposition of $\alpha$. In particular, a rewriting step is a $2$-cell of length $1$.

\subsubsection{Notations}
For the sake of readability, we will denote terms and rewriting rules of cartesian polygraphs as in term rewriting theory, \cite{Terese03}. The canonical projections $x_i^{\sort{s}} : \sort{s} \rightarrow \sort{s}_i$, for $1\leq i \leq |\sort{s}|$ are identified to "\emph{variables}" $x_1,\ldots,x_{|\sort{s}|}$. And a $1$-cell $f: \sort{s} \rightarrow \ob{r}$ is denoted by $f(x_1,\ldots,x_{|\sort{s}|})$, and a rule $\alpha : f \Rightarrow g$ with $f,g: \sort{s} \rightarrow {\ob r}$ will be denoted by
\[
\alpha_{x_1,\ldots,x_{|\sort{s}|}} : f(x_1,\ldots,x_{|\sort{s}|}) \Rightarrow g(x_1,\ldots,x_{|\sort{s}|}).
\]

\subsection{Algebraic examples}

\subsubsection{Associative and commutative magmas}
\label{SSS:AssociativeCommutativeMagmas}
Denote by $\poly{Mag}$ the cartesian $2$-polygraph whose signature has a unique sort denoted by $1$ and a unique generating $1$-cell $\mu : 2 \rightarrow 1$, and an empty set of generating $2$-cells.
Denote by $\poly{Ass}$ the cartesian $2$-polygraph such that $\poly{Ass}_1 = \poly{Mag}_1$ and with a unique generating $2$-cell:
\begin{eqn}{equation}
\label{E:AssociativityRule}
A_{x,y,z}^\mu \: : \: \mu (\mu (x,y) ,z ) \Rightarrow \mu (x, \mu(y,z))
\end{eqn}

Denote by $\poly{AC}^\mu$ (or simply $\poly{AC}$ when there is no ambiguity) the cartesian $2$-polygraph such that $\poly{AC}_1 = \poly{Mag}_1$, and $\poly{AC}_2 = \poly{Ass}_2 \cup \{ C \} $ with
\begin{eqn}{equation}
\label{E:CommutativityRule}
C^\mu \: : \: \mu (x,y) \Rightarrow \mu(y,x)
\end{eqn}
that corresponds to the rule $C^\mu :\mu \tau \Rightarrow \mu$, where $\tau$ is the exchanging operator defined in Section \ref{SSS:SignatureAndTerms}. Note that the cartesian $2$-polygraph $\poly{AC}$ is not terminating, and that the rule $C$ can not be oriented in a terminating way. As a consequence, in the sequel when $P_2$ is defined by a set of relations together with relations corresponding to commutativity and associativity axioms for some operation $\mu$, we will chose to work modulo the polygraphs $\poly{AC}^\mu$.

\subsubsection{Monoids}
\label{Ex:TheoryMonoids}
We define the cartesian polygraph $\poly{Mon}$ whose signature has a unique sort $1$, \linebreak $\poly{Mon}_1=\poly{Ass}_1 \cup \{e : 0 \rightarrow 1\}$, and $\poly{Mon}_2=\poly{Mag}_2\cup \{E_l^\mu,E_r^\mu\}$ with
\begin{eqn}{equation}
\label{E:NeutralElementMonoid}
E_l^\mu \: : \: \mu (e,x) \Rightarrow x \qquad E_r^\mu \: : \:  \mu(x,e) \Rightarrow x.
\end{eqn}
Then the theory $\cl{P}$ is the theory of monoids that we will denote by $\tha{M}$. We also define the cartesian polygraph $\poly{CMon}$ by $\poly{CMon}_i = \poly{Mon}_i$ for $0 \leq i \leq 1$ and $\poly{CMon}_2 = \poly{Mon}_2 \cup \{ C^\mu \}$ where $C^\mu$ is the commutativity $2$-cell defined in~\eqref{E:CommutativityRule}.

\subsubsection{Groups}
\label{SSS:PresentationOfGroups}
We define the cartesian polygraph $\poly{Grp}$ whose signature has a unique sort $1$, $\poly{Grp}_1 = \poly{Mon}_1 \cup \{ \iota : 1 \rightarrow 1 \}$, and $\poly{Grp}_2 = \poly{Mon}_2 \cup \{ I_l^\mu, I_r^\mu \}$ with
\begin{eqn}{equation}
\label{E:InverseRelGroup}
I_l^{\mu,\iota} \: : \: \mu ( \iota(x),x ) \Rightarrow e \qquad I_r^{\mu,\iota} \: : \: \mu( x, \iota(x)) \Rightarrow e
\end{eqn}

Note that following \cite{Hullot1980ACO}, the following set of generating $2$-cells gives a cartesian polygrah, denoted by $\widetilde{\poly{Grp}}$, Tietze equivalent to $\poly{Grp}$, that is also presenting the theory $\cl{\poly{Grp}}$, and convergent modulo the cartesian polygraph $\poly{Ass}$:
\begin{eqn}{equation}
\label{E:PresentionGrpConvergentModuloA1}
 G_1^{\mu,\iota} \: : \: \iota (e) \Rightarrow e \quad G_2^{\mu,\iota} \: : \: \iota (\iota(x)) \Rightarrow x \quad G_3^{\mu,\iota} \: : \: \iota(\mu(x,y)) \Rightarrow \mu (\iota(y), \iota(x))
\end{eqn}
\begin{eqn}{equation}
\label{E:PresentionGrpConvergentModuloA2}
 \quad G_4^{\mu,\iota} \ : \: \mu(x,\mu(\iota(x),y)) \Rightarrow y \quad G_5^{\mu,\iota} \: : \: \mu ( \iota(x) , \mu (x,y)) \Rightarrow y
 \end{eqn}

\subsubsection{Abelian groups}
Consider the cartesian polygraph $\poly{Ab}$ whose signature has a unique sort $1$, $\poly{Ab}_1 = \poly{Grp}_1 $ and $\poly{Ab}_2 = \poly{Grp}_2 \cup \{ C \}$ where $C$ is the commutativity generating $2$-cell defined in~\eqref{E:CommutativityRule}.

\subsubsection{Rings}
Consider the cartesian polygraph $\poly{Ring}$ whose signature has a unique sort $1$, $ \poly{Ring}_1 = \poly{Ab}_1 \coprod \poly{Mon}_1$ with the following notations:
\[
\poly{Ab}_1 \:=\: \{+ : \ob{2}\rightarrow \ob{1},\; 0 : \ob{0} \rightarrow \ob{1}, \; - : \ob{1} \rightarrow \ob{1} \},
\qquad
\poly{Mon}_1 \:=\: \{\cdot : \ob{2} \rightarrow \ob{1},\; 1 : \ob{0} \rightarrow \ob{1}\},
\]
and $\poly{Ring}_2 = \poly{Ab}_2 \cup \poly{Mon}_2 \cup \{D_l,D_r\}$, where
\begin{eqn}{equation}
\label{E:Distributivity}
D_l : x \cdot (y+z) \Rightarrow x \cdot y + x \cdot z
\qquad
D_r : (y+z) \cdot x \Rightarrow y\cdot x + z \cdot x
\end{eqn}

The cartesian $2$-polygraph $\poly{CRing}$ (commutative rings) is the cartesian $2$-polygraph whose signature has a unique sort $1$, $\poly{CRing} = \poly{Ring}_1$ with the same notations as above, and $\poly{CRing}_2 = \poly{Ring}_2 \cup \{ C^{\cdot} \}$ where $C^{\cdot}$ is the commutativity generating $2$-cell
\begin{eqn}{equation}
\label{E:CommutativityRingProduct}
C^{\cdot} \: : \: \cdot (x,y) \Rightarrow \cdot (y,x)
\end{eqn}

Following \cite[Example 12.2]{PetersonStickel81}, the following set of generating $2$-cells gives a cartesian polygraph that is Tietze equivalent to $\poly{CRing}$, and is convergent modulo $\poly{AC}$:
\begin{eqn}{equation}
\label{E:ConvergentPresentationCRingModAC}
 E_r^+, \: I_r^{+,-}, \: G_1^{+,-}, \: G_2^{+,-}, \: G_3^{+,-}, \: D_r, \: R_1 \: : \: x \cdot 0 \Rightarrow 0, \: R_2 \: : \: x \cdot (-y) \Rightarrow - (x \cdot y), \: E_r^{\cdot}
 \end{eqn}

\subsubsection{Modules over a commutative ring}
\label{SS:ConvergentPresentationRModModuloAC}
The cartesian $2$-polygraph $\poly{Mod}$ with $\poly{Mod}_0 = \{\ob{m},\ob{r}\}$, and $\poly{Mod}_1 = \poly{CRing}_1 \cup \poly{Ab}_1 \cup \{ \eta : \ob{r}\ob{m} \rightarrow \ob{m}\}$ with the following notations
\begin{enumerate}[{\bf i)}]
\item $\poly{CRing}_0=\{\ob{r}\}$, $\poly{CRing}_1=\{+ : \ob{rr}\rightarrow \ob{r},\; 0 : \ob{0} \rightarrow \ob{r},\;- : \ob{r} \rightarrow \ob{r}, \; \cdot : \ob{rr} \rightarrow \ob{r},\; 1 : \ob{0} \rightarrow \ob{r}\}$;
\item $\poly{Ab}_0=\{\ob{m}\}$, $\poly{Ab}_1 = \{\oplus : \ob{mm} \rightarrow \ob{m}, 0^{\oplus}: \ob{0} \rightarrow \ob{m}, \; \iota : \ob{m} \rightarrow \ob{m} \}$;
\item If there is no possible confusion, we will denote $\eta(\lambda,x) = \lambda.x$ for $\lambda$ and $x$ of type $\ob{r}$ and $\ob{m}$ respectively.
\end{enumerate}
and $\poly{Mod}_2 = \poly{CRing}_2 \cup \poly{Ab}_2 \cup \{ M_1, M_2, M_3, M_4\}$ with
\begin{eqn}{equation}
\label{E:CompatibilityRulesModules}
M_1 :  \lambda . (\mu . x)\Rightarrow  (\lambda \cdot \mu).x
\qquad
M_2 : 1.x \Rightarrow x
\end{eqn}
\begin{eqn}{equation}
\label{E:DistributivityModules}
M_3 : \lambda . (x \oplus y) \Rightarrow (\lambda .x)\oplus (\lambda .y)
\qquad
M_4 : \lambda .x \oplus \mu .x \Rightarrow (\lambda + \mu).x
\end{eqn}

Following \cite{Hullot1980ACO}, the $2$-cells in~\eqref{E:ConvergentPresentationCRingModAC} together with the following set of $2$-cells
\begin{eqn}{equation}
\label{E:ConvergentPresentationRMod}
M_1, \quad M_2, \quad M_3, \quad M_4, \quad N_1 \: : \:  x \oplus 0^{\oplus} \Rightarrow x, \quad N_2 \: : \: x \oplus (\lambda.x) \Rightarrow (1+\lambda).x,
\end{eqn}
\begin{eqn}{equation}
\label{E:ConvergentPresentationRMod2}
N_3 \: : \: x \oplus x \Rightarrow (1 + 1).x, \quad N_4 \: : \: x . 0^\oplus \Rightarrow 0^\oplus, \quad N_5 \: : \: 0. x \Rightarrow 0^\oplus, \quad N_6 \: : \: \iota(x) \Rightarrow (- 1).x
\end{eqn}
give a convergent presentation of the theory of modules over a commutative ring modulo $\poly{AC}^\cdot \coprod \poly{AC}^{+}$, which contains all the associativity and commutativity relations for the operations $\cdot$ and $+$. This presentation can be summarized with the following set of generating $2$-cells:
\begin{align*}
& x + 0 \Rightarrow x & (\text{ring}_1) \qquad \qquad &  x + (-x) \Rightarrow 0 \qquad  & (\text{ring}_2) \\
& - 0 \Rightarrow 0 & (\text{ring}_3) \qquad \qquad &  - (-x) \Rightarrow x \qquad & (\text{ring}_4) \\
& - (x+y) \Rightarrow (-x) + (-y) & (\text{ring}_5) \qquad \qquad  & x \cdot (y + z) \Rightarrow x \cdot y + x \cdot z \ \qquad & (\text{ring}_6) \\
& x \cdot 0 \Rightarrow 0 & (\text{ring}_7) \qquad \qquad & x \cdot (-y) \Rightarrow - (x \cdot y) \qquad & (\text{ring}_8) \\
& 1 \cdot x \Rightarrow x & (\text{ring}_9) \qquad \qquad & a \oplus 0^{\oplus} \Rightarrow a \qquad & (\text{mod}_1) \\
& x . (y . a) \Rightarrow (x \cdot y) . a & (\text{mod}_2) \qquad \qquad & 1 . a \Rightarrow a \qquad & (\text{mod}_3) \\
& x . a \oplus y . a \Rightarrow (x + y) . a & (\text{mod}_4) \qquad \qquad & x . (a \oplus b) \Rightarrow (x . a) \oplus (y . b) \qquad & (\text{mod}_5) \\
& a \oplus (r . a) \Rightarrow (1+r) . a & (\text{mod}_6) \qquad \qquad & a \oplus a \Rightarrow (1+1) . a \qquad & (\text{mod}_7) \\
& x . 0^{\oplus} \Rightarrow 0^{\oplus} & (\text{mod}_8) \qquad \qquad & 0 . a \Rightarrow 0^{\oplus} \qquad & (\text{mod}_{9}) \\
& I(a) \Rightarrow (-1) . a  & (\text{mod}_{10}) \qquad \qquad & &
\end{align*}
Let us denote by $\poly{Mod}'_2$ the set containing the $2$-cells~\eqref{E:ConvergentPresentationCRingModAC}, \eqref{E:ConvergentPresentationRMod} and \eqref{E:ConvergentPresentationRMod2}, and denote by $\poly{Mod}^c$ the cartesian $2$-polygraph $(\poly{Mod}_0, \poly{Mod}_1, \poly{Mod}'_2 \cup \poly{AC}^\cdot \cup \poly{AC}^+)$. It also presents the theory of modules over a commutative ring.

\section{Algebraic polygraphs modulo}
\label{S:AlgebraicPolygraphsModulo}

In this section we introduce the notion of algebraic polygraph as a cellular extension on ground terms over a signature endowed with constants. In Subsection~\ref{SS:AlgebraicPolygraphModulo}, we introduce the notion of algebraic polygraph modulo and refer the reader to \cite{DupontMalbos18b} for a categorical interpretation of the constructions given in this section.

\subsection{Algebraic polygraphs}
\label{S:AlgebraicPolygraphs}

\subsubsection{Constants}
Let $(P_0,P_1)$ be a signature, and $Q$ be a set of \emph{generating $1$-cell (called constants)} with source $\ob{0}$ and target a sort in $P_0$. We denote by $P_1\langle Q \rangle$ the sub-theory of the free theory $\freetha{(P_1\cup Q)}$ made of all ground terms.

\subsubsection{Algebraic polygraph}
An \emph{algebraic polygraph} is a data $(P,Q,R)$ where,
\begin{enumerate}[{\bf i)}]
\item $P$ is a cartesian $2$-polygraph,
\item $Q$ is a family of sets of generating constants $(Q_{\ob{s}})_{\ob{s}\in P_0}$,
\item $R$ is a cellular extension of the theory $P_1\langle Q \rangle$.
\end{enumerate}
Note that the cellular extension $R$ is indexed by the sorts of $P_0$, that is it defines a
family $(F_{\ob{s}},R_{\ob{s}})_{\ob{s}\in P_0}$ of $1$-polygraphs, where
$F_{\ob{s}} = P_1\langle Q \rangle_{\ob{s}}$.

\subsubsection{Example}
Let $\poly{Mon}_2$ be the cartesian $2$-polygraph defined in~\eqref{Ex:TheoryMonoids}. One defines an algebraic polygraph by setting:
\begin{eqn}{equation}
\label{E:AlgebraicPolygraphB3+}
Q = \{s,t : \ob{0} \rightarrow \ob{1}\},
\qquad
R=\{\;\alpha \: : \:(s\cdot t)\cdot s \Rightarrow t\cdot (s\cdot t)\;\}.
\end{eqn}

\subsubsection{Rewriting in algebraic prolygraphs}
Let $\Pr = (P,Q,R)$ be an algebraic polygraph, and let
 $\alpha : f \Rightarrow g $ be a ground $2$-cell in $R$. A \emph{$R$-rewriting step} is a ground $2$-cell in the free $2$-theory $\freetha{R}$ on $(P_1\cup Q, R)$ of the form
\[
A[\alpha] : A[f] \Rightarrow A[g],
\]
where $A[\boxempty]$ is a ground context. It can be depicted by the following diagram:
\[
\begin{tikzpicture}[baseline = 0,scale=0.871]
	\draw[-,thick,black] (-1.5,0.5) -- (1.5,0.5);
	\draw[-,thick,black] (-1.5,0.5) -- (0,-1.5);
	\draw[-,thick,black] (1.5,0.5) -- (0,-1.5);
	\draw[-,thick,black] (-0.7,0.5) --  (0,-0.5) -- (0.7,0.5) -- (-0.7,0.5);
	\fill[color=gray!20] (-0.7,0.5) --  (0,-0.5) -- (0.7,0.5) -- (-0.7,0.5);
	\draw[-,thick,black] (0,-1.5) -- (0,-1.8);
	\draw[-,thick,black] (-0.7,0.5) -- (-0.7,0.7);
		\draw[-,thick,black] (0.7,0.5) -- (0.7,0.7);
	\draw[-,thick,black] (-1.5,0.5) -- (-1.5,0.7);
		\draw[-,thick,black] (1.5,0.5) -- (1.5,0.7);
	\node at (0,-0.65) {$\ob{r}$};
    \node at (0,0.8) {$\ob{0}$};
    \node at (0,0) {$f$};
    \node at (-1.1,0.7) {$\ldots$};
    \node at (1.1,0.7) {$\ldots$};
    \node at (0,1.3) {};
    \node at (0,-1.15) {$A$};
\end{tikzpicture}  \quad  \raisebox{-0.2cm}{$\overset{a}{\Rightarrow}$}
\qquad \begin{tikzpicture}[baseline = 0,scale=0.871]
	\draw[-,thick,black] (-1.5,0.5) -- (1.5,0.5);
	\draw[-,thick,black] (-1.5,0.5) -- (0,-1.5);
	\draw[-,thick,black] (1.5,0.5) -- (0,-1.5);
	\draw[-,thick,black] (-0.7,0.5) --  (0,-0.5) -- (0.7,0.5) -- (-0.7,0.5);
	\fill[color=gray!20] (-0.7,0.5) --  (0,-0.5) -- (0.7,0.5) -- (-0.7,0.5);
	\draw[-,thick,black] (0,-1.5) -- (0,-1.8);
	\draw[-,thick,black] (-0.7,0.5) -- (-0.7,0.7);
		\draw[-,thick,black] (0.7,0.5) -- (0.7,0.7);
	\draw[-,thick,black] (-1.5,0.5) -- (-1.5,0.7);
		\draw[-,thick,black] (1.5,0.5) -- (1.5,0.7);
	\node at (0,-0.65) {$\ob{r}$};
    \node at (0,0.8) {$\ob{0}$};
    \node at (0,0) {$g$};
    \node at (-1.1,0.7) {$\ldots$};
    \node at (1.1,0.7) {$\ldots$};
    \node at (0,1.3) {};
    \node at (0,-1.15) {$A$};
\end{tikzpicture}
\]
A \emph{$R$-rewriting path} is a finite or infinite sequence $\underline{a} = a_1\star_1 a_2  \star_1 \ldots \star_1 a_k \star_1 \ldots$ of $R$-rewriting steps $a_i$.
The \emph{length} of $2$-cell $\underline{a}$ in $\freetha{R}$, denoted by $\ell(a)$, is the minimal number of $R$-rewriting steps needed to write $\underline{a}$ as a composition as above
\subsubsection{Example}
Consider the rule $\alpha$ defined in~\eqref{E:AlgebraicPolygraphB3+}, and the algebraic context $A[\boxempty] = (s\cdot \boxempty) \cdot t$, we have the rewriting step
\[
A[\alpha] : (s\cdot ((s\cdot t)\cdot s)) \cdot t \Rightarrow (s\cdot (t \cdot (s\cdot t)) \cdot t.
\]

\subsubsection{Algebraic polygraph of axioms}
The cellular extension $P_2$ defined on $\freetha{P}_1$ extends to a cellular extension on the free $1$-theory $\freetha{(P_1 \cup Q)}$ denoted by $\widehat{P}_2$, whose source and target maps are defined in such a way that the following diagram commutes
\[
\xymatrix@C=3.5em@R=1em{
P_2 \ar@{_{(}->}[dd] \langle Q \rangle \ar [ddrr] <0.6ex>^-{}  \ar [ddrr] <-0.6ex>_-{} & &  \\ & & \\
P_2 \ar [r] <0.6ex> ^-{\partial_1^-} \ar [r] <-0.6ex> _-{\partial_1^+}  & \freetha{P}_1 \ar@{^{(}->}[r] & \freetha{(P_1 \cup Q)} }
\]
and denote by $P_2 \langle Q \rangle$ (resp $\tck{P_2 \langle Q \rangle}$) the set of ground $2$-cells in $\freetha{\widehat{P}_2}$ (resp. $\tck{\widehat{P}}_2$). The set $P_2 \langle Q \rangle$ thus contains the groundified $2$-cells of $P_2$. The data $(P,Q,P_2 \langle Q \rangle)$ defines an algebraic polygraph, that we call the \emph{algebraic polygraph of axioms}. We say that two terms $f$ and $g$ in $P_1 \langle Q \rangle$ are \emph{algebraically equivalent} with respect to $P$, denoted by $f \equiv_{P_2} g$, if there exists a ground $2$-cell in $\tck{P_2 \langle Q \rangle}$ from $f$ to $g$.

We will denote by $\cl{P\langle Q \rangle}$ the quotient of the full sub-category $ P_1\langle Q \rangle$ of $\freetha{(P_1 \cup Q)}$ by the congruence generated by the $2$-cells in $P_2 \langle Q \rangle$. Namely, two terms $f$ and $g$ that are related by a $2$-cell in $\tck{P_2 \langle Q \rangle}$ are identified in the quotient.

Note that the algebraic polygraph $(P,Q,P_2 \langle Q \rangle)$ shares the rewriting properties of the cartesian $2$-polygraph $P$. In particular, if $P$ is terminating (resp. quasi-terminating, confluent, confluent modulo $P'$), then $(P,Q,P_2 \langle Q \rangle)$ is terminating (resp. quasi-terminating, confluent, confluent modulo $(P',Q,P'_2 \langle Q \rangle)$).

\subsubsection{Example}
In the example of the algebraic polygraph defined in~\eqref{E:AlgebraicPolygraphB3+}, the set $P_2 \langle Q \rangle$ is defined by the associativity relations on ground terms on the constants $s$ and $t$. For instance, $P_2 \langle Q \rangle$ contains the following ground $2$-cell:
\[ A_{s,t,s}: (s \cdot t) \cdot s \Rightarrow s \cdot (t \cdot s). \]

\subsubsection{Positivity}
Denote $
\pi : P_1\langle Q \rangle \rightarrow \cl{P\langle Q\rangle}
$ the canonical projection, and let $\sigma : \cl{P \langle Q \rangle} \rightarrow \catego{Set}$ be a map such that for any $\cl{f} \in\cl{P \langle Q \rangle}$, $\sigma(\cl{f})$ is a chosen non-empty subset of $\pi^{-1}(\cl{f})$. Such a map is called a \emph{positive strategy} with respect to $(P,Q)$. A rewriting step $a$ in $\freetha{R}$ is called \emph{$\sigma$-positive} if $a_-$ belongs to $\sigma(\cl{a_-})$.
A rewriting path $a_1\star_1 \ldots \star_1 a_k$ in $\freetha{R}$ is called \emph{$\sigma$-positive} if any of its rewriting steps is positive.

\subsubsection{Positivity from confluence modulo}
\label{SS:StrategiesPositivity}
We introduce positive strategies that depend on the inherent cartesian $2$-polygraph $P$. Suppose that $P$ admits a decomposition $P_2 = P'_2 \cup P''_2$, where
$P'_2$ is confluent modulo $P''_2$. For every $1$-cell $\cl{f}$ in $\cl{P\langle Q \rangle}$, we set
\[
\sigma(\cl{f}) = NF(f,P'_2 \; mod\; P''_2),\quad \text{where $f \in \pi^{-1}(\cl{f})$,}
\]
the set of normal forms of $f$ with respect to $P'_2$ modulo $P_2''$.
Note that the strategy $\sigma$ is well-defined. Indeed, following \cite[Lemma 2.6]{Huet80}, for any $f,f'\in \pi^{-1}(\cl{f})$, we have $NF(f,P'_2\; mod\; P"_2) \equiv_{P"_2} NF(f',P'_2\;mod\; P"_2)$.

\subsubsection{Remark}
Note that in many algebraic situations, we have $\poly{Ass} \subseteq P''_2$. In particular, in the case of SRS, $P'_2$ will be empty and $P''_2 = \poly{Ass}$. In that case, any term in $P_1 \langle Q \rangle$ is a normal form for the empty polygraph modulo $\poly{Ass}$, and thus the positive strategy consists in taking all the fiber. In the case of LRS, $P''_2$ will be $AC$, the algebraic polygraph corresponding to associativity and commutativity relations of the operations, and $P'_2$ will be the convergent presentation of $\poly{RMod}$ modulo $AC$ given in Section \ref{SS:ConvergentPresentationRModModuloAC}.

\subsection{Algebraic polygraphs modulo}
\label{SS:AlgebraicPolygraphModulo}

\subsubsection{Algebraic polygraph modulo}
Given an algebraic polygraph $\Pr=(P,Q,R)$ and a positive strategy $\sigma$ on $\Pr$, one denotes by $\ere{P}{R}$ the cellular extension
\[
\xymatrix{
P_1 \langle Q \rangle
&
\ar@<+0.5ex>[l]
\ar@<-0.5ex>[l]
\ere{P}{R}
}
\]
made of triple $(e,a,e')$, where $e$ and $e'$ are ground $2$-cells in $P_2\langle Q\rangle^\top$ and $a$ is a $R$-rewriting step. Such a triple will be denoted by $e \star a \star e'$, called a \emph{$\ere{P}{R}$-rule}, and pictured by
\[
\xymatrix@R=5em@C=7em{
\ob{0}
  \ar@/^9ex/[r] ^-{e_-} _-{}="1"
  \ar@/^3ex/[r] |-{e_+} ^-{}="2"
  \ar@/_3ex/[r] |-{e'_-} ^-{}="3"
  \ar@/_9ex/[r] _-{e'_+} _-{}="4"
&
s
	\ar@2 "1"!<0pt,-8pt>;"2"!<0pt,8pt> ^-{e}
	\ar@2 "2"!<0pt,-8pt>;"3"!<0pt,8pt> ^-{a}
	\ar@2 "3"!<0pt,-8pt>;"4"!<0pt,8pt> ^-{e'}
}
\]

We refer the reader to \cite{DupontMalbos18b} for a detailed construction of the cellular extension $\ere{P}{R}$. Such a rule is called $\sigma$-positive if $a$ is a $\sigma$-positive $R$-rewriting step.
An \emph{algebraic polygraph modulo} is a data $(P,Q,R,S)$ made of
\begin{enumerate}[{\bf i)}]
\item an algebraic polygraph $(P,Q,R)$,
\item a cellular extension $S$ of $P_1\langle Q \rangle$ such that $R \subseteq S \subseteq \ere{P}{R}$.
\end{enumerate}
Note that the data $(P,Q,S)$ defines an algebraic polygraph modulo.

\subsubsection{Example}
Let us consider the algebraic polygraph $(P,Q,R)$ defined in~\eqref{E:AlgebraicPolygraphB3+}, then the following composition gives a rewriting step in $\ere{P}{R}$:
\[
(s \cdot (s \cdot (t \cdot s))) \cdot t \equiv_{P_2} (s\cdot ((s\cdot t)\cdot s)) \cdot t \overset{A[\alpha]}{\Rightarrow} (s\cdot (t \cdot (s\cdot t)) \cdot t \equiv_{P_2} ((s \cdot t) \cdot (s \cdot t)) \cdot t.
\]

\subsubsection{Termination properties}
\label{SSS:Termination}
An algebraic polygraph $\Pr=(P,Q,R)$ is called
\begin{enumerate}[{\bf i)}]
\item \emph{terminating} if there is no infinite rewriting sequence for $\Pr$, that is there is no sequence $(f_n)_{\in \mathbb{N}}$ of $1$-cells of $P_1\langle Q\rangle$ such that for each $n\in \mathbb{N}$, there is a rewriting step $f_n \rightarrow f_{n+1}$,
\item \emph{quasi-terminating} if for each sequence $(f_n)_{\in \mathbb{N}}$ of $1$-cells of $P_1\langle Q\rangle$ such that for each $n\in \mathbb{N}$, there is a rewriting step $f_n \rightarrow f_{n+1}$, the sequence $(f_n)_{\in \mathbb{N}}$ contains an infinite number of occurrences of same $1$-cell,
\item \emph{algebraically terminating} if for each sequence $(f_n)_{\in \mathbb{N}}$ of $1$-cells of $P_1\langle Q\rangle$ such that for each $n\in \mathbb{N}$, there is a rewriting step $f_n \rightarrow f_{n+1}$, the sequence $(f_n)_{\in \mathbb{N}}$ contains an infinite number of occurrences of same $1$-cell in context, that is, there exist $k,l\in \mathbb{N}$, such that $f_{k+l}=A[f_k]$ where $A$ is a possibly empty ground context of $\Pr$,
\item \emph{exponentiation free} if there is no rewriting path with source a $1$-cell $f$ of $P_1\langle Q \rangle$ and target $C[f]$, where $A$ is a nontrivial ground context of $\Pr$.
\end{enumerate}

We refer to \cite{Dershowitz87} for weakened notions of termination. Note that any quasi-terminating polygraph is algebraically terminating. But the converse implication is false in general, indeed the rewriting system $a \rightarrow a\cdot a$ is algebraically terminating, but not quasi-terminating. In fact, it is not exponentiation free either. One proves that both properties algebraically terminating and exponentiation free implies the quasi-terminating property.

An algebraic polygraph modulo $(P,Q,R,S)$ is called \emph{terminating} (resp. \emph{quasi-terminating}) if the algebraic polygraph $(P,Q,S)$ is terminating (resp. quasi-terminating). Note that an algebraic polygraph is a special case of algebraic polygraph modulo when $S=R$. In the sequel we will only consider algebraic polygraphs modulo.

\subsubsection{Quasi-normal forms}
\label{SSS:QuasiNormalForms}
Let $\Pr=(P,Q,R,S)$ be an algebraic polygraph modulo. A $1$-cell $f$ of $P_1\langle Q \rangle$ is called a \emph{quasi-irreducible} if for any $S$-rewriting step $f \rightarrow g$, there exists a $S$-rewriting sequence from $g$ to $f$.
A \emph{quasi-normal form (with respect to $\Pr$)} of a $1$-cell $f$ in $P_1\langle Q \rangle$ is a quasi-irreducible $1$-cell $\widetilde{f}$ of $P_1\langle Q\rangle$ such that there exists a $S$-rewriting sequence from $f$ to $\widetilde{f}$.

When the algebraic polygraph modulo $\Pr$ is quasi-terminating, any $1$-cell $f$ of $P_1\langle Q \rangle$ admits at least a quasi-normal. Such a quasi-normal is neither $S$-irreducible nor unique in general. A \emph{quasi-normal form strategy} is a map
\[
s: P_1\langle Q \rangle \rightarrow P_1\langle Q \rangle
\]
sending a $1$-cell $f$ on a chosen quasi-normal $\widetilde{f}$. Let us define a map
$d : P_1\langle Q \rangle \rightarrow \mathbb{N}$ sending a $1$-cell $f$ to
\[
d(f) = \min\{\;l(\underline{a}) \;|\; \underline{a}\;\text{is a $\ere{P}{R}$-rewriting path from $f$ to $\widetilde{f}$ }\},
\]
counting the distance from $f$ to $\widetilde{f}$.

\subsection{Algebraic rewriting systems}

\subsubsection{Algebraic rewriting system}
Note that the cellular extension $S$ defined on $P_1 \langle Q\rangle$ extends to a cellular extension of the cartesian $1$-category $\cl{P \langle Q \rangle}$, with source and target maps defined respectively by $\cl{\partial}_1^- := \pi \circ \partial_1^-$ and $\cl{\partial}_1^+ := \pi \circ \partial_1^+$.
An \emph{algebraic rewriting system} on an algebraic polygraph modulo $(P,Q,R,S)$ with a positive strategy $\sigma$ is a cellular extension $\cl{S}$ of $\cl{P\langle Q\rangle}$ defined in such a way that the following diagram commutes
\[
\xymatrix@C=5em@R=2.5em{
&
S
\ar@<+0.5ex>[dl] ^-{\cl{\partial}_1^-}
\ar@<-0.5ex>[dl] _-{\cl{\partial}_1^+}
\ar[d] ^-{\pi'}
\\
\cl{P\langle Q \rangle}
&
\cl{S}
\ar@<+0.5ex>[l] ^-{}
\ar@<-0.5ex>[l] _-{}
}
\]
where the map $\pi '$ assigns to a $S$-rule $e \star a \star e'$ an element $\cl{a}$ in $\cl{S}$ with source $\cl{a_-}$ and target $\cl{a_+}$.
Explicitly,
\[
\cl{S} \: = \: \{ \cl{a} : \cl{a_-} \Rightarrow \cl{a_+} \: | \: e \star a \star e' \in S \}.
\]
Note that $\cl{S} = \cl{R}$ for any $R \subseteq S \subseteq \ere{P}{R}$. Let us consider the subset $\cl{S}^\sigma$ of $\cl{S}$ defined by  $
\cl{S}^\sigma \: = \: \{ \cl{a} : \cl{a_-} \Rightarrow \cl{a_+} \: | \: \text{$a$ is a $\sigma$-positive $S$-rule} \}
$.

A \emph{$\cl{S}$-rewriting step} (resp. a $\cl{S}^\sigma$-rewriting step) is the quotient of a $S$-rewriting step (resp. $\sigma$-positive rewriting step) by the canonical projection $\pi$, that is a $2$-cell of the form $
\cl{C}[\cl{a}] : \cl{C}[\cl{a_-}] \Rightarrow \cl{C}[\cl{a_+}]$,
where $C$ is a ground context of $P_1\langle Q \rangle$ and $C[a]$ is a $S$-rewriting step (resp. $\sigma$-positive $S$-rewriting step). A \emph{$S$-rewriting path}  is a sequence of $\cl{S}$-rewriting steps.

\subsubsection{Example: string rewriting systems}
Recall that a SRS is defined as a set $Q$ of letters and a binary relation $\rightarrow$ on the free monoid $Q^\ast$.
Such a SRS can be interpreted as a quotient algebraic polygraph as follows. Indeed, consider an algebraic polygraph modulo $(\poly{Mon},Q,R,S)$, where $\poly{Mon}$ is the cartesian polygraph defined in~\eqref{Ex:TheoryMonoids}, the set of constants $Q$ is the set of letters of the SRS, and the cellular extension $R$ corresponds to a fibration of the binary relation $\rightarrow$ modulo associativity.

For instance, consider the algebraic polygraph defined in~\eqref{E:AlgebraicPolygraphB3+}. Then by quotient, we obtain the SRS
\[ \langle s,t \: | \: sts \Rightarrow tst \: \rangle \]
that presents the monoid $B_3^+$ of braids on $3$ strands.

\subsubsection{Example: linear rewriting systems}
A LRS is an algebraic rewriting system on an algebraic polygraph modulo $(P,Q,R,S)$ such that $\poly{Mod}^c \subseteq P$, where $\poly{Mod}^c$ is the cartesian $2$-polygraph presenting the theory of modules over a commutative ring defined in Section \ref{SS:ConvergentPresentationRModModuloAC}.

\section{Confluence in algebraic polygraphs modulo}
\label{S:ConfluenceAlgebraicPolygraphsModulo}

In this section we present confluence properties of algebraic polygraphs modulo with fixed positive strategies.

\subsection{Confluence modulo with respect to a positive strategy}

\subsubsection{Branchings in algebraic polygraphs modulo}
Let $\Pr=(P,Q,R,S)$ be an algebraic polygraph modulo and $\sigma$ a positive strategy on $\Pr$. A \emph{$\sigma$-branching} of $(P,Q,R,S)$ is a triple $(a,e,b)$ where $f$ and $g$ are $\sigma$-positive $2$-cells of $\freetha{S}$ and $e$ is a $1$-cell of
$\tck{P_2 \langle Q \rangle}$ such that $e_- = a_-$ and $e_+ = b_-$. Such a $\sigma$-branching is depicted as follows
\[
\xymatrix @R=1.25em @C=2.75em{
u
  \ar[r] ^-{a}
  \ar[d] _-{e}
&
u'
\\
v
  \ar[r] _-{b}
&
v'
} \: \raisebox{-6mm}{$.$}
\]
Note that the $2$-cells are represented by simple arrows in confluence diagrams for better readability in the diagrams in the sequel. The $2$-cell $b$ (resp. $a$) can be an identity $2$-cell of $\freetha{S}$, and in that case the $\sigma$-branching is of the form $(a,e)$ (resp. $(e,b)$). The source of such a $\sigma$-branching is the pair $(f,f)$ where $f= a_- = e_-$ (resp. $f = b_- = e_+$). The $2$-cell $e$ in $\tck{P_2 \langle Q \rangle}$ can also be trivial, and in that case the $\sigma$-branching modulo is a regular $\sigma$-branching $(a,b)$. We denote by $(u,u)$ its source, where $u = a_- = b_-$.

Such a $\sigma$-branching is \emph{$\sigma$-confluent modulo} if there exist $\sigma$-positive $2$-cells $a'$ and $b'$ in $\freetha{S}$ and a $2$-cell $e'$ of $\tck{P_2 \langle Q \rangle}$ as follows:
\[
\xymatrix @R=1.25em @C=2.75em{
f
  \ar[r] ^-{a}
  \ar[d] _-{e}
&
f'
  \ar@{.>}[r] ^-{a'}
&
h
  \ar[d] ^-{e'}
\\
g
  \ar[r] _-{b}
&
g'
  \ar@{.>}[r] _-{b'}
&
h'
}
\]

We say that the triple $(a',e',b')$ is \emph{a $\sigma$-confluence modulo} of the $\sigma$-branching modulo $(a,e,b)$, and that the pair of terms $(f,g)$ is the \emph{source} of the $\sigma$-branching $(a,e,b)$. Such a $\sigma$-branching is \emph{local} if $a$ is a rewriting step of $S$, $b$ is $\ell(e) + \ell(b) = 1$. Namely, it is either of the form $(a,e)$ or $(a,b)$.

We say that the algebraic polygraph modulo $(P,Q,R,S)$ is \emph{confluent modulo} (resp. \emph{locally confluent modulo}) if any $\sigma$-branching modulo (resp. local $\sigma$-branching modulo) is confluent modulo.

\begin{remark}
As noted in \cite[Section 2]{BachmairDershowitz89}, the algebraic polygraph $R$ is the polygraph for which is the most difficult to reach $\sigma$-confluence modulo. Indeed, if $R$ is confluent modulo $P$, then any algebraic polygraph modulo $(P,Q,R,S)$ is confluent modulo $P$. For this reason, in many situation we relax by proving $\sigma$-confluence of $\er{P}{R}$ or $\ere{P}{R}$ modulo $P$. They also noticed that when $\ere{P}{R}$ is terminating, $\re{P}{R}$ is confluent modulo $P$ if and only if $\ere{P}{R}$ is confluent modulo $P$, and in that case $\re{P}{R}$ defines the same set of normal forms than $\ere{P}{R}$. As a consequence, we will either prove $\sigma$-confluence of $\re{P}{R}$ and $\ere{P}{R}$ in the sequel, leading to the same quotient algebraic rewriting system. Note finally that when $\er{P}{R} \subseteq S \subseteq \ere{P}{R}$, any local $\sigma$-branching modulo of the form $(a,e)$ is trivially confluent modulo $P$ via the $\sigma$-confluence modulo $(1_{a_-}, e^- \star_1 a,1_{a_+})$.
\end{remark}

\subsubsection{Double induction on the distance to the quasi-normal form}
\label{SSS:InductionQNFModulo}
Consider the distance map $d: P_1 \langle Q \rangle \rightarrow \mathbb{N}$ defined in Section \ref{SSS:QuasiNormalForms}. We extend this distance on $1$-cells of $P_1 \langle Q \rangle$ to a distance on $\sigma$-branchings modulo $(a,e,b)$ by defining
\[
d(a,e,b) := d(a_-) + d(a_+).
\]

We then define a well-founded order $\prec$ on the set of $\sigma$-branchings of $S$ modulo $P$ by:
\[
(a,e,b) \prec (a',e',b') \: \text{if} \: d(a,e,b) < d(a',e',b').
\]
The confluence proofs in the sequel will be made using induction on this order. Note that this corresponds to a process of induction on sources of $\sigma$-branchings modulo, that is pairs of $1$-cells in $P_1 \langle Q \rangle$, with respect to distance of the quasi-normal form with respect to $\ere{P}{R}$. This follows Huet's double induction principle in the terminating setting, based on induction on an auxiliary rewriting system constructed on pairs of terms.

In this way, one proves for quasi-terminating algebraic polygraphs modulo the Newman lemma, using Huet's proof in the terminating setting, \cite{Huet80}.

\begin{theorem}[Newman lemma modulo for algebraic polygraphs modulo]
\label{T:NewmanLemmaModulo}
Let $\Pr$ be a quasi-terminating algebraic polygraph modulo, and $\sigma$ be a positive strategy on $\Pr$. If $\Pr$ is locally $\sigma$-confluent modulo, then it is $\sigma$-confluent modulo.
\end{theorem}
\begin{proof}
Assume that $\Pr$ is locally $\sigma$-confluent modulo $P$. We prove this result by induction on the well-founded order $\prec$ on $\sigma$-branchings modulo defined in~\eqref{SSS:InductionQNFModulo}. Let us pick a $\sigma$-branching modulo $(a,e,b)$ of $\Pr$, and assume that for any $\sigma$-branching modulo $(a',e',b')$ such that
$ (a,e,b) \prec (a',e',b')$,
the $\sigma$-branching modulo $(a',e',b')$ is confluent modulo $P$. Let us prove this results in two steps.

\textbf{Step 1:} We prove that any $\sigma$-branching modulo $(a,e)$,  where $a$ is a $S$-rewriting step and $e$ is a $2$-cell in $\tck{P_2 \langle Q \rangle}$ is $\sigma$-confluent modulo. Let us denote by $u$ the $1$-cell $a_-$, so that $(a,e)$ is a $\sigma$-branching modulo of source $(f,f)$. If $f$ is $S$-irreducible, then $a$ is an identity $2$-cell, and the $\sigma$-branching is trivially confluent. We then suppose that $a$ is not an identity,
and proceed by induction on $\ell(e) \geq 1$. If $\ell(e) = 1$, $(a,e)$ is a local $\sigma$-branching of $S$ modulo $P$ and it is confluent modulo by local $\sigma$-confluence.
Now, let us assume that for $k \geq 1$, any $\sigma$-branching $(a'',e'')$ of $S$ modulo $P$ such that $\ell(e'') = k$ is confluent modulo $E$, and let us consider a $\sigma$-branching $(a,e)$ of $S$ modulo $P$ such that $\ell(e) = k+1$. We choose a decomposition $e = e_1 \star e_2$ with $e_1$ of length $1$. Using local $\sigma$-confluence on the $\sigma$-branching $(a,e_1)$, there exists a $\sigma$-confluence modulo $(a',e'_1,a_1)$ modulo $P$ of this $\sigma$-branching. Then, we choose a decomposition $a_1 = a_1^1 \star a_1^2$ with $a_1^1$ of length $1$. By induction hypothesis on the $\sigma$-branching modulo $(a_1^1,e_2)$, there exists a $\sigma$-confluence modulo $(a'_1,e'_2,b)$ of this $\sigma$-branching, as in the following diagram:
\[
\xymatrix@R=2.25em @C=4em{
f \ar [d] _-{e_1} \ar [r] ^-{a} & f' \ar [r] ^-{a'} & f'' \ar [d] ^-{e'_1} \\
f_1 \ar [d] _-{\rotatebox{90}{=}} \ar [r] |-{a_1^1} ^-{}="2" & f'_1 \ar [d] ^-{\rotatebox{90}{=}} \ar [r] |-{a_1^2} & f''_1  \\
f_1 \ar [r] |-{a_1^1} _-{}="3" \ar [d] _ -{e_2} & f'_1 \ar [r] |-{a'_1} & f'_2 \ar [d] ^-{e'_2} \\
g \ar [rr] _-{b} ^-{}="1" & & g'
\ar@2{} "1,2";"2,2" |{\text{Local conf mod $E$}}
\ar@2{} "3,2";"1" |{\text{Induction on $\ell(e)$}}
\ar@2{} "2";"3" |{=}
}
\]
Now, since $f \equiv f_1 \overset{a_1^1}{\Rightarrow} f'_1$, we have $d(f'_1) = d(f) -1$, and thus $(a_1^2,a'_1) \prec (a,e)$ so that we can use induction on the $\sigma$-branching $(a_1^2, a_1')$ of $S$ modulo $P$ of source $(f'_1,f'_1)$ to prove that there exists a $\sigma$-confluence modulo $(a_2,e_3,a'_2)$ of this $\sigma$-branching. By a similar argument, we have $d(f''_1) < d(f)$ and $d(f'_2) < d(f)$ and we can apply induction on the $\sigma$-branchings modulo $(a_2,(e'_1)^-)$ and $(a'_2, e'_2)$ respectively. Therefore, there exist $2$-cells $a''$,$a_3$, $a'_3$ and $b'$ in $\freetha{S}$ and $2$-cells $e''_1$ and $e''_2$ in $\tck{P_2 \langle Q \rangle}$ as in the following diagram:
\[
\xymatrix@R=2.25em@C=4em{
f \ar [d] _-{e_1} \ar [r] ^-{a} & f' \ar [r] ^-{a'} & f'' \ar [d] ^-{e'_1} \ar [rr]^-{a''} ^-{}="4" & & f''' \ar [d] ^-{e''_1} \\
f_1 \ar [d] _-{\rotatebox{90}{=}} \ar [r] |-{a_1^1} ^-{}="2" & f'_1 \ar [d] ^-{\rotatebox{90}{=}} \ar [r] |-{a_1^2} & f''_1 \ar [r] |-{a_2}  & h_1 \ar [r] |-{a_3} \ar [d] ^-{e_3} & h'_1  \\
f_1 \ar [r] |-{a_1^1} _ -{}="3" \ar [d] _ -{e_2} & f'_1 \ar [r] |-{a'_1} & f'_2 \ar [d] ^-{e'_2} \ar [r] |-{a'_2}  & h_2 \ar [r] |-{a'_3} & h'_2  \ar [d] ^-{e''_2} \\
g \ar [rr] _-{b} ^-{}="1" & & g' \ar [rr] _ -{b'} _-{}="5" & & g''
\ar@2{} "1,2";"2,2" |{\text{Local conf mod $E$}}
\ar@2{} "3,2";"1" |{\text{Induction on $\ell(e)$}}
\ar@2{} "2";"3" |{=}
\ar@2{} "2,3";"3,3" |{\text{Ind.}}
\ar@2{}  "4";"2,4" |{\text{Ind.}}
\ar@2{}   "3,4";"5" |{\text{Ind.}}
}
\]
We can then use once again induction on the $\sigma$-branching $(a_3,e_3,a'_3)$ of $S$ modulo $P$ of source $(h_1,h_2)$, and so on. Since the order $\prec$ is well-founded, this process terminates in finitely many steps until we reach the quasi-normal form $\widetilde{f}$. This yields the $\sigma$-confluence of the $\sigma$-branching $(a,e)$.

\textbf{Step 2:}
Now, let us prove that any $\sigma$-branching modulo $(a,e,b)$ is confluent modulo $P$. Let us choose such a $\sigma$-branching and denote by $(f,g)$ its source. We assume that  any $\sigma$-branching $(a',e',b')$ of $S$ modulo $P$ with $(a',e',b') \prec (a,e,b)$ is confluent modulo $P$. We follow the proof scheme used by Huet in \cite[Lemma 2.7]{Huet80}. Let us denote by $n := \ell(a)$ and $m:= \ell(b)$. We assume without loss of generality that $n > 0$ and we fix a decomposition $a = a_1 \star_{1} a_2$ with $a_1$ of length $1$.
If $m = 0$, by Step 1 on the $\sigma$-branching $(a_1,e)$ of $S$ modulo $P$, there exists a $\sigma$-confluence modulo $(a'_1,e',b')$ of this $\sigma$-branching. Then, since $d(f_1) = d(f)-1$, we have $(a_2,a'_1) \prec (a,e)$ and we can apply double induction on the $\sigma$-branching modulo $(a_2,a'_1)$, as pictured in the following diagram:
\[
\xymatrix@R=2.25em @C=4em{
f \ar [r] ^-{a_1} ^-{}="2" \ar [d] _-{\rotatebox{90}{=}} & f_1 \ar [r] ^-{a_2} \ar [d] ^-{\rotatebox{90}{=}} & f_2 \ar [r]^-{a'_2} & f'_2 \ar [d] ^-{}\\
f \ar [d] _ -{e} \ar [r] |-{a_1} _ -{}="3" & f_1 \ar [r] |-{a'_1} & f_2 \ar [r] |-{a''_1} \ar [d] ^-{e'} & f'_2 \\
g \ar [rr] _ -{b'} ^-{}="1" & & g' &
\ar@2{} "2,2";"1" |{\text{Step 1}} \ar@2{} "2";"3" |{=}
\ar@2{} "1,3";"2,3" |{\text{Ind.}} } \]
We finish the proof of this case with a similar argument as in Step 1, using repeated inductions that terminate after a finite number of steps because the order $\prec$ is well-founded.

Now, assume that $m > 0$ and fix a decomposition $b = b_1 \star_{1} b_2$ of $b$ with $b_1$ of length $1$. Using Step 1 on the $\sigma$-branching modulo $(a_1,e)$, there exists a $\sigma$-confluence modulo $(a'_1,e_1,c_1)$ of this $\sigma$-branching. We distinguish two cases whether $c_1$ is trivial or not.

\medskip

If $c_1$ is trivial, the $\sigma$-confluence of the $\sigma$-branching modulo $(a,e,b)$ is given by the following diagram
\[
\xymatrix@R=2.25em@C=4em {
f \ar [d] _ -{\rotatebox{90}{=}} \ar [r] ^-{a_1} ^-{}="11" & f_1 \ar [d] ^-{\rotatebox{90}{=}} \ar [r] ^-{a_2} & f_2 \ar [rrr] ^-{a'_2} & & & f'_2 \ar [d] ^-{}    & \\
f \ar [r] |-{a_1} _-{}="12" \ar [d] _ -{e} & f_1 \ar [r] |-{a'_1} & f'_1 \ar [rr] |-{a_3} ^-{}="1" \ar [d] ^-{e'}  &  & f_3 \ar [d] ^-{e_1} \ar [r] ^-{a_4} ^-{}="8" & f_4 \ar [r] |-{a_5} & f_5 \ar [d] ^-{} \\
g \ar [d] _ -{\rotatebox{90}{=}} \ar [rr] |-{1_g} ^-{}="2" & & g \ar [d] _-{\rotatebox{90}{=}} \ar [r] |-{b_1} ^-{}="5" & g'_1 \ar [d] ^-{\rotatebox{90}{=}} \ar [r] |-{b'_1} & g''_1 \ar [r] |-{b''_1} & h_1 \ar [d] ^-{} \ar [r] ^{b_3} & h_3 \\
g \ar [rr] _-{1_g} _-{}="3" & & g \ar[r] |-{b_1} _-{}="6" & g'_1 \ar [r] _-{b_2} & g_2 \ar [r] _ -{b'_2} & h_2 &
\ar@2{} "3,4";"2,4" |{\text{Step 1}}
\ar@2{} "2";"2,2" |{\text{Step 1}}
\ar@2{} "11";"12" |{=}
\ar@2{} "2";"3" |{=}
\ar@2{} "5";"6" |{=}
\ar@2{} "1,3";"2,3"!<75pt,0pt> |{\text{Ind.}}
\ar@2{} "2,6";"3,6" |{\text{Ind.}}
\ar@2{} "3,5";"4,5" |{\text{Ind.}}
} \]

where the $\sigma$-branchings modulo $(a_1,e)$ and $(b_1,e')$ are confluent modulo $P$ by Step 1, and induction applies on the $\sigma$-branchings $(a_2,a'_1 \star_{1} a_3)$, $(b'_1,b_2)$ and $(a_4,e_1,b''_1)$ since $d(f_1) < d(f)$, $d(f_1) < d(g)$, $d(g'_1) < d(g)$, $d(g'_1) < d(f)$ and $d(f_3) < d(f)$ respectively. We then reach a $\sigma$-confluence modulo of the $\sigma$-branching modulo $(a,e,b)$ similarly.

\medskip

If $c_1$ is not trivial, let us fix a decomposition $c_1 = c_1^1 \star_{1} c_1^2$ with $c_1^1$ of length $1$. The $\sigma$-confluence of the $\sigma$-branching modulo $(a,e,b)$ is given by the following diagram:

\[ \xymatrix@R=2.25em@C=5em {
f \ar [d] _-{\rotatebox{90}{=}} \ar [r] ^-{a_1} ^-{}="1" & f_1 \ar [d] ^-{\rotatebox{90}{=}}  \ar [r] ^-{a_2} & f_2 \ar [r] ^-{a'_2} & f'_2 \ar [d] ^-{} & \\
f \ar [d] _ -{e} \ar [r] |-{a_1} _-{}="2" & f_1 \ar [r] |-{a'_1} & f'_1 \ar [d] ^-{} \ar [r]|-{a_3} & f_3 \ar [r] |-{a_4} & f_4 \ar [d] ^-{} \\
g \ar [d] _-{\rotatebox{90}{=}} \ar [r] |-{c_1^1} ^-{}="5" & g_1 \ar [d] ^-{\rotatebox{90}{=}} \ar [r] |-{c_1^2} & h_1 \ar [r] |-{c_2} & h_2 \ar [d] ^-{} \ar [r] |-{c'_2} & h'_2 \\
g \ar [d] _-{\rotatebox{90}{=}} \ar [r] |-{c_1^1} _-{}="6" &  g_1 \ar [r] |-{c'_1} & h'_1 \ar [d] ^-{} \ar [r] |-{c_3} & h_3 \ar [r]  |-{c'_3} & h'_3 \ar [d] ^-{} \\
g  \ar [d] _-{\rotatebox{90}{=}} \ar [r] |-{b_1} ^-{}="3" & g' \ar [d] ^-{\rotatebox{90}{=}} \ar [r] |-{b'_1} & g'_1 \ar [r] |-{b'_2} & g'_2 \ar [r] |-{b'_3} \ar [d] ^-{} & g'_3 \\
g \ar [r] _-{b_1} _-{}="4" & g' \ar [r] _-{b_2} & g_2 \ar [r] _-{b_3} & g_3 &
\ar@2{} "1";"2" |{=}
\ar@2{} "3";"4" |{=}
\ar@2{} "5";"6" |{=}
\ar@2{} "2,2";"3,2" |{\text{Step 1}}
\ar@2{} "4,2";"5,2" |{\text{Local conf mod $E$}}
\ar@2{} "1,3";"2,3" |{\text{Ind.}}
\ar@2{} "2,4";"3,4" |{\text{Ind.}}
\ar@2{} "3,3";"4,3" |{\text{Ind.}}
\ar@2{} "5,4";"4,4" |{\text{Ind.}}
\ar@2{} "5,3";"6,3" |{\text{Ind.}}
 }
 \]
where the $\sigma$-branching modulo $(a_1,e)$ is confluent modulo by Step 1, the $\sigma$-branching modulo $(c_1^1,b_1)$ is $\sigma$-confluent by local $\sigma$-confluence modulo, and one checks that induction applies on the $\sigma$-branchings $(a_2,a'_1)$, $(c_1^2,c'_1)$, $(b'_1,b_2)$, $(a_3,c_2)$ and $(c_3,b'_2)$. Similarly, we can repeat inductions to reach a $\sigma$-confluence modulo of $(a,e,b)$.
\end{proof}

\subsection{Critical $\sigma$-branchings modulo}

\subsubsection{Classification of local $\sigma$-branchings}
\label{SSS:ConfluenceTerminationAlgebraicPolygraphsModulo}
The local $\sigma$-branchings modulo of $\Pr$ can be classified in the following families:
\begin{enumerate}[{\bf i)}]
\item \emph{trivial} $\sigma$-branchings of the form
\begin{equation*}
\xymatrix@R=1.25em @C=3.5em{
A[a_-] \ar[d] _-{\rotatebox{90}{=}}
                \ar[r] ^-{A[a]} & A[a_+] \\
               A[a_-]
                \ar[r] _-{A[a]} & A[a_+]}
\end{equation*}
for some ground context context $A$ and $\sigma$-positive $S$-rewriting step $a$.
\item \emph{inclusion independant} $\sigma$-branchings modulo of the form
\begin{equation*}
\label{E:InclusionIndependantbranchingsModulo}
\xymatrix@R=1.25em@C=4em{
A[a_-] \ar[d] _-{\rotatebox{90}{=}}
                \ar[r] ^-{A[a]}
                & A[a_+] \\
 A[A'[b_-]]
                 \ar[r] _-{A[A'[b]]}
                  & A[A'[b_+]]}
\end{equation*}
for some ground contexts context $A$ and $A'$, and $\sigma$-positive $S$-rewriting steps $a$ and $b$.
\item \emph{orthogonal} $\sigma$-branchings modulo of the form
\[
\xymatrix@R=1.25em@C=4em{
B[a_-,b_-] \ar[d] _-{\rotatebox{90}{=}}
                \ar[r] ^-{B[a, b_-]} & B[a_+,b_-] \\
              B[a_-,b_-]
                 \ar[r] _-{B[a_-, b]} & B[a_-,b_+] }
\]
\[
\xymatrix@R=1.5em@C=4em{
B[a_-,e_-]
                 \ar[d] _-{B[a_-, e]}
                \ar[r] ^-{B[a, e_-]} & B[a_+,e_-] \\
B[a_-,e_+]  & }
\qquad
 \xymatrix@R=1.5em@C=3.5em{
B[e'_-,b_-]
                 \ar[d] _-{B'[e', b_-]}
                \ar[r] ^-{B'[e'_-, b]} & B'[e'_-,b_+] \\
B'[e'_+,b_-]  & }
\]
for some ground multi-contexts $B$ and $B'$ of arity $2$, $S$-rewriting steps $a$,$b$ and $c$ of $S$, and $2$-cells $e$ and $e'$ in $\tck{P_2 \langle Q \rangle}$.
\item \emph{non orthogonal} $\sigma$-branchings are the remaining local $\sigma$-branchings, that is nor inclusion independant nor orthogonal.
\end{enumerate}

\subsubsection{Critical $\sigma$-branchings}
We define an order relation on $\sigma$-branchings modulo of an algebraic polygraph modulo $(P,Q,R,S)$ by setting $(a,e,b)\sqsubseteq (a',e',b')$ if there exists a ground context $A$ of $P_1 \langle Q \rangle$ such that $a' = A[a]$, $e' = A[e]$ and $b' = A[b]$. A \emph{critical $\sigma$-branching modulo} is a local $\sigma$-branching modulo $P$ which is non trivial, non orthogonal and minimal for the order relation $\sqsubseteq$.

\subsubsection{Positively confluence}
An algebraic polygraph modulo $\Pr=(P,Q,R,S)$ with a positive strategy~$\sigma$ is called \emph{positively $\sigma$-confluent} if, for any $S$-rewriting step $a$, there exists a representing $\widetilde{a}_- \in \sigma(a_-)$ of $a_-$ and two $\sigma$-positive $S$-reductions $a'$ and $b'$ of length at most $1$ as in the following diagram
\[
\xymatrix@R=1.5em @C=2.25em{
\widetilde{a}_-
  \ar[rrr] ^-{a'}
  \ar[d] _-{e}
&&&
 \ar[d] ^-{e''}
\\
a_-
  \ar[r] _-{a}
&
  \ar[r] _-{e'}
&
  \ar[r] _-{b'}
&
}
\]
In that case, we say that $\sigma$ is a \emph{positive confluent strategy} for $\Pr$.

\begin{proposition}[Terminating critical branching theorem modulo]
\label{P:TerminatingCriticalBranchingTheoremModulo}
Let $(P,Q,R,S)$ be a quasi-terminating algebraic polygraph modulo with a positive strategy $\sigma$. If $(P,Q,R,S)$ is positively $\sigma$-confluent, then it is locally $\sigma$-confluent modulo if and only if the two following properties hold:
\begin{description}
\item[$\mathbf{a_0)}$] any critical $\sigma$-branching modulo $(a,b)$, where $a$ and $b$ are $S$-rewriting steps, is $\sigma$-confluent modulo.
\item[$\mathbf{b_0)}$] any critical $\sigma$-branching modulo $(a,e)$, where $a$ is an $S$-rewriting step and $e$ is a $2$-cell in $\tck{P_2 \langle Q \rangle}$ of length $1$, is $\sigma$-confluent modulo.
\end{description}
\end{proposition}
\begin{proof}
The left to right implication is trivial. Let us prove the converse.
Suppose that condition $\mathbf{a_0)}$ holds and prove condition {\bf a)}. The proof of the other implication is similar.
We prove this by analyzing all the possible cases of local $\sigma$-branchings modulo given in~\eqref{SSS:ConfluenceTerminationAlgebraicPolygraphsModulo}. Local aspherical $\sigma$-branchings are always $\sigma$-confluent modulo. Let us consider a local orthogonal $\sigma$-branching modulo of the form
\[
\xymatrix@R=1.7em@C=4em{
B[a_-,b_-]
                 \ar[d] _-{\rotatebox{90}{=}}
                \ar[r] ^-{B[a,b_-]} & B[a_+,b_-]
               \\
 B[a_-,b_-] \ar[r] _-{B[a_-,b]}  &  B[a_-,b_+] }
 \]
 where $B[a,b_-]$ and $B[a_-,b]$ are $\sigma$-positive $S$-reductions. There are natural $2$-cells in $\freetha{S}$ that give a $\sigma$-confluence modulo of this diagram:
 \[
\xymatrix@R=1.7em@C=4em{
B[a_-,b_-]
                 \ar[d] _-{\rotatebox{90}{=}}
                \ar[r] ^-{B[a,b_-]} & B[a_+,b_-] \ar@{.>} [r] ^-{B[a_+,b]} & B[a_+,b_+] \ar [d] ^-{\rotatebox{90}{=}}
               \\
 B[a_-,b_-] \ar[r] _-{B[a_-,b]}  &  B[a_-,b_+]  \ar@{.>} [r] _-{B[a,b_+]} & B[a_+,b_+] }
 \]
 However, it may happen that these reductions are not $\sigma$-positive. Without loss of generality, let us assume that they are both not $\sigma$-positive. By positive $\sigma$-confluence assumption, there exists a representative $\widetilde{B[a_+,b_-]}$ (resp. $\widetilde{B[a_-,b_+]}$) of $B[a_+,b_-]$ (resp. $B[a_-,b_+]$) in $P_1 \langle Q \rangle$, $\sigma$-positive $S$-rewriting sequences $h_1$ and $h_2$, and $2$-cells $e_1$,$e_2$ in $\tck{P_2 \langle Q \rangle}$ as in the following diagram:
 \[
\xymatrix@R=1.7em@C=4em{ & \widetilde{B[a_+,b_-]} \ar [dd] ^-{} \ar [rr] ^-{} & & \ar [d] ^-{} & \\
& & f_1 \ar [d] ^-{e_1} \ar [r] |-{c_1}  & & \\
B[a_-,b_-]
                 \ar[d] _-{\rotatebox{90}{=}}
                \ar[r] ^-{B[a,b_-]} & B[a_+,b_-] \ar@{.>} [r] ^-{B[a_+,b]} & B[a_+,b_+] \ar [d] ^-{\rotatebox{90}{=}}
               \\
 B[a_-,b_-] \ar[r] _-{B[a_-,b]}  &  B[a_-,b_+] \ar@{.>} [r] _-{B[a,b_+]} \ar [dd] _-{} & B[a_+,b_+] \ar [d] ^-{e_2}  \\
 & & f_2 \ar [r] |-{c_2}  & \ar [d] ^-{} & \\
 &  \ar [rr] _-{} & & &}
 \]
Then, we have $d(f_1) < d(B[a_-,b_-])$ and $d(f_2) < d(B[a_-,b_-])$ so that we can use induction of the $\sigma$-branching modulo $(c_1, e_1 \star e_2, c_2)$ of source $(f_1,f_2)$. As a consequence, there exists a $\sigma$-confluence modulo $(c'_1,e,c'_2)$ of this $\sigma$-branching modulo, and we then construct a $\sigma$-confluence modulo of $(B[a,b_-], B[a_-,b])$ by successive applications of induction as in the proof of Theorem \ref{T:NewmanLemmaModulo}. This process terminates since $\ere{P}{R}$ is quasi-terminating, and thus the order $\prec$ on $\sigma$-branchings modulo defined in~\eqref{SSS:InductionQNFModulo} is well-founded.
Let us now consider an overlapping $\sigma$-branching modulo of the form $(a,b)$ where $a$ and $b$ are $\sigma$-positive $S$-rewriting steps. By definition, there exists a ground context $A$ of $P_1 \langle Q \rangle$ and a critical $\sigma$-branching modulo $(a',b')$ such that $(a,b) = (A[a'], A[b'])$. Following condition $\mathbf{a_0)}$, the critical $\sigma$-branching $(a',b')$ is $\sigma$-confluent modulo, and there exists a $\sigma$-confluence modulo $(a'',e',b'')$ of this $\sigma$-branching. However, the reductions $A[a'']$ and $A[b'']$ that would give a confluence modulo of $(a,b)$ are not necessarily $\sigma$-positive:
\[
\xymatrix@R=2em @C=3.5em{
u  \ar [d] _-{\rotatebox{90}{=}} \ar [r] ^-{a} & \ar@{.>} [r] ^-{A[a'']} & \ar [d] ^-{A[e']} \\
u \ar [r] _-{b} & \ar@{.>} [r] _-{A[b'']} & } \]
However, using positive $\sigma$-confluence of $S$, we are able to construct a $\sigma$-confluence modulo of the $\sigma$-branching modulo $(a,b)$ as in the previous case.
\end{proof}

\subsubsection{Full positive strategy}
\label{R:NoTermination}
When all reductions are positive, that is when $\sigma(\cl{f})= \pi^{-1} (\cl{f})$ for any $1$-cell $\cl{f}$, we say that $\sigma$ is a \emph{full positive strategy}. In that case, the quasi-termination assumption in Proposition~\ref{P:TerminatingCriticalBranchingTheoremModulo} is not needed, since the natural confluences represented by dotted arrows are $\sigma$-positive. Moreover, the positive $\sigma$-confluence is always satisfied, by considering $a' = a$ and $b' = 1_{t_1(a)}$.

\subsection{Algebraic critical branching lemma}

By taking the quotient of the $S$-rewriting paths in Proposition \ref{P:TerminatingCriticalBranchingTheoremModulo}, in this section we obtain an algebraic critical branching lemma.

\subsubsection{Critical branchings of algebraic polygraph}
Let $\Pr=(P,Q,R,S)$ be an algebraic polygraph modulo with a positive strategy $\sigma$ and let $\mathcal{A}$ be an algebraic rewriting system on $\Pr$.
The \emph{critical branchings} of $\mathcal{A}$ are the projections of the critical $\sigma$-branchings modulo of $\Pr$ of the form $\mathbf{a}_0)$, that is pairs $(\cl{a},\cl{b})$ of $\cl{S}^\sigma$-rewriting steps such that there is a $\sigma$-branching modulo in $\Pr$ with source $(\widetilde{a_-},\widetilde{b_-})$. As a consequence of Proposition~\ref{P:TerminatingCriticalBranchingTheoremModulo}, we deduce the following result.

\begin{theorem}
\label{T:AlgebraicCriticalBranchingTheorem}
Let $\Pr=(P,Q,R,S)$ be an algebraic polygraph modulo having a positive confluent strategy $\sigma$. If $\ere{P}{R}$ is quasi-terminating, then an algebraic rewriting system on $\Pr$ is locally confluent if and only if its critical branchings are confluent.
\end{theorem}

As an immediate consequence, we deduce the following usual critical branching lemma.
\begin{corollary}
\label{C:ClassicalCriticalBranchingTheorem}
Let $\Pr$ be an algebraic polygraph modulo with a full positive strategy. Any algebraic rewriting system on $\Pr$ is locally confluent if and only if all its critical branchings are confluent.
\end{corollary}

\section{Examples of algebraic rewriting systems}

We apply the algebraic critical branching lemma to SRS and LRS, and we discuss the case of rewriting in groups.

\subsection{Critical branching for string rewriting systems}
\label{SS:CriticalBranchingSRS}

\subsubsection{Critical branching lemma for string rewriting systems}
When $\poly{Mon}$ is the cartesian $2$-polygraph presenting the theory $\tha{M}$ of monoids given in~\eqref{Ex:TheoryMonoids}, Theorem~\ref{T:AlgebraicCriticalBranchingTheorem} corresponds to critical branching lemma for SRS as proved by Nivat, \cite{Nivat73}.

\begin{theorem}
\label{T:CBSRS}
Let $\Pr$ be an algebraic polygraph modulo on the cartesian $2$-polygraph $\poly{Mon}$. Then any algebraic rewriting system on $\Pr$ is locally confluent if and only if its critical branchings are confluent.
\end{theorem}

In that case, the choice of positive strategy $\sigma$ making all the $2$-cells in $\freetha{S}$ be $\sigma$-positive implies that the positive $\sigma$-confluence is obvious. Moreover the quasi-terminating hypothesis is not required as explained in Remark \ref{R:NoTermination}.

\subsection{Critical branching for linear rewriting systems}
\label{SS:CriticalBranchingLinearRewriting}

\subsubsection{Critical branching lemma for linear rewriting systems}
Consider a cartesian $2$-polygraph $P$ having an underlying linear structure, that is $P$
contains the cartesian $2$-polygraph $\poly{Mod}^c$ presenting the theory of modules over a commutative ring as defined in Section \ref{SS:ConvergentPresentationRModModuloAC}.
Consider a decomposition of the polygraph $P$ as in~Section \ref{SS:StrategiesPositivity},
with $P''_2$ being the $2$-polygraph $\poly{AC}^+ \cup \poly{AC}^{\cdot}$, and $P'_2$ being $\poly{Mod}^c$ and $\sigma$ the associated strategy. Note that in that case, $\ere{P}{R}$ can never be terminating: indeed, because of the linear context, for any $R$-rule $a: f \Rightarrow g$, we have a $\ere{P}{R}$-rewriting step given by
\begin{eqn}{equation}
\label{E:LinearCycle}
\xymatrix{g \equiv_P -f + (g+f) \ar@2 [rrr] ^-{-a + (g+f)} & & & -g + (g+f) \equiv_P f}
\end{eqn}
However, if the rewriting system  $\cl{S}^\sigma$ is terminating, then $\ere{P}{R}$ is quasi-terminating, then as a consequence of Theorem~\ref{T:AlgebraicCriticalBranchingTheorem} we have

\begin{theorem}
\label{T:CBLlinear1}
Let $\Pr$ be a terminating algebraic polygraph modulo on a cartesian $2$-polygraph $P$ having an underlying linear structure and a positive confluent strategy $\sigma$.
Then any algebraic rewriting system on $\Pr$ is locally confluent if and only if its critical branchings are confluent.
\end{theorem}

Given an algebraic polygraph modulo $(P,Q,R,S)$ having an underlying linear structure with the $\sigma$-strategy of normal forms modulo \poly{AC} defined in~Section \ref{SS:StrategiesPositivity}.
Consider an algebraic rewriting system $\cl{S}$ on $(P,Q,R,S)$.
The positivity confluence of $S$ with respect to $\sigma$ implies the factorisation property of \cite[Lemma 3.1.3]{GuiraudHoffbeckMalbos19}, stating that any rewriting step $\cl{a}$ of $\cl{S}$ can be decomposed in the free $(2,1)$-theory on $\cl{S}$ as $\cl{a} = \cl{b} \star \cl{c}^{-1}$, where $\cl{b}$ and $\cl{c}$ are either positive rewriting steps of $\cl{S}^\sigma$ or identities, as pictured in the following diagram:
\begin{eqn}{equation}
\label{E:FactorisationProperty}
\raisebox{0.8cm}{
\xymatrix@R=2em@C=2em{
& h & \\
f \ar@2@{.>}@/_1.5ex/ [rr] _-{\cl{a}} \ar@2@/^1.5ex/ [ur] ^-{\cl{b}}  & & g \ar@2@/_1.5ex/ [ul] _-{\cl{c}}
}}
\end{eqn}
Note that if $\cl{a}$ is already a rewriting step of $\cl{S}^\sigma$, this factorisation is trivial. When $\cl{a}$ is in $\cl{S}$ but not in $\cl{S}^\sigma$, that is $\cl{a}$ is a quotient of a non-$\sigma$-positive $S$-rewriting sequence, it states that $\cl{a}$ can be factorised using positive reductions. In this way, we have the following critical branching criterion for linear algebraic rewriting systems.

\begin{theorem}
\label{T:CBLlinear2}
Let $\Pr$ be a terminating algebraic polygraph modulo on a cartesian $2$-polygraph $P$ having an underlying linear structure satisfying the factorisation property~\eqref{E:FactorisationProperty}.
Then any algebraic rewriting system on $\Pr$ is locally confluent if and only if its critical branchings are confluent.
\end{theorem}

\subsubsection{Left-monomial rewriting systems}
Consider an algebraic rewriting system on an algebraic polygraph modulo $(P,Q,R,S)$, where $P$ has an underlying linear structure. Its rules transform linear combinations of terms into linear combinations of terms. The system is called \emph{left-monomial} when the source of any rule of $R$ is an element of $P_1\langle Q \rangle$ that does not contain neither the operation $\oplus : {\bf m}{\bf m} \rightarrow {\bf m}$ nor $\eta : {\bf r}{\bf m} \rightarrow {\bf m}$ defined in Section~\ref{SS:ConvergentPresentationRModModuloAC}. Equivalently, the source of any rule of the algebraic rewriting system is a \emph{monomial}.

For terminating left-monomial LRS local confluence is equivalent to the confluence of critical branchings, \cite[Theorem 4.3.2]{GuiraudHoffbeckMalbos19}. The proof of this criterion requires the factorisation property~\eqref{E:FactorisationProperty} that always holds in this context.
We expect that in the left-monomial linear setting the positive confluence is equivalent to this property. It is still an open question in order to explain the criterion for local confluence of LRS as a rewriting modulo result.

\subsection{Rewriting with inverses}
\label{SS:RewritingInverse}

We conclude these algebraic examples by presenting a notion of group rewriting system defined as an algebraic rewriting system.

\subsubsection{Rewriting in groups}
Rewriting is used in group theory to give algorithmic methods for decision problems, such as the word/conjugacy/geodesic problems, \cite{LeChenadec84,LeChenadec86, DiekertDuncanMyasnikov10, DiekertDuncanMyasnikov12, Chouraqui09, Chouraqui11}. In most cases, the method consists in constructing a convergent presentation of the considered group. Note also that homological finiteness conditions for finite convergence for groups were introduced, \cite{CremannsOtto96}. Finally, algorithms to compute relations among relations (syzygies) for groups given by generators and relations were developed in \cite{HeyworthWendsley03}.
However, in all these works the presentations of the groups are interpreted by SRS, or by Gröbner bases, that present groups, or group rings, as monoids, or monoid rings, with axioms of inverses given explicitly in the set of rules. Namely, for a group $G$ presented by a set of generators $X$ and a set of relations $\mathcal{R}$, it is associated the following SRS:
\[
\langle \, Q \;|\; \, \eta_x : xx^- \rightarrow 1,\; \eta^-_x : x^-x\rightarrow 1, \rho_r : r \rightarrow 1, \;\text{for $r\in \mathcal{R}$} \rangle.
\]

When solving decision problems, or computing homological invariants for groups, the rules $\eta_x$ and $\eta^-_x$ that present invertibility axioms, make the problem more complicated uselessly. Indeed, these rules should not be considered as those defining the group. In this way, the notion of rewriting in groups is not algebraically well considered yet.

\subsubsection{Group rewriting systems}
Consider an algebraic polygraph $(P,Q,R)$, where $P=\widetilde{\poly{Grp}}$ is the convergent cartesian $2$-polygraph presenting the algebraic theory of groups defined in \eqref{SSS:PresentationOfGroups}. We denote by $P_1 \langle Q \rangle_{\text{red}}$ the set of reduced ground terms of $P_1 \langle Q \rangle$ with respect to $P_2 \langle Q \rangle$. By definition, the operations of the signature $P$ induce on the set of ground terms $\cl{P\langle Q \rangle}$ a structure of group isomorphic to the free group $F(Q)$ generated by $Q$.

A cellular extension of the theory $P_1\langle Q \rangle$ is called \emph{reduced} if for any of its ground $2$-cell $\alpha$, the ground terms $s(\alpha)$ and $t(\alpha)$ belong to $P_1 \langle Q \rangle_{red}$.

\begin{lemma}
There exists a unique reduced cellular extension $R_{red}$ of the theory $P_1\langle Q \rangle$ such that the algebraic rewriting systems $\cl{R}$ and $\cl{R}_{red}$ on $\cl{P\langle Q \rangle}$ coincide.
\end{lemma}
\begin{proof}
The ground $2$-cells of $R_{red}$ are obtained by reducing the sources and targets of ground $2$-cells of~$R$ with respect to $P_2\langle Q \rangle$.
\end{proof}

From now on, we assume that the cellular extension $R$ is reduced.

\subsubsection{Positive strategies for reductions in groups}
\label{SSS:PositiveStrategiesGroups}
The free group $\cl{P\langle Q \rangle}$ can be constructed as a quotient monoid. Indeed, consider the free monoid $(Q \sqcup Q^-)^\ast$ over the set $Q \sqcup Q^-$ of constants and their formal inverses, with $Q^-=\{ x^- \: \mid \: x \in Q \}$. Then, the group $\cl{P\langle Q \rangle}$ is isomorphic as a monoid to the free monoid $(Q \sqcup Q^-)^\ast$ subject to the relations
\begin{eqn}{equation}
\label{E:InverseRelations}
x x^- \to 1, \quad\text{and}\quad  x^- x \to 1, \quad\text{for any $x \in Q$}.
\end{eqn}
Note that the set of relations \eqref{E:InverseRelations} is convergent, and thus the elements of the group $\cl{P\langle Q \rangle}$ are identified with normal forms of elements of $(Q \sqcup Q^-)^\ast$ with respect to these relations

Let us fix a total order $\prec$ over $Q \sqcup Q^-$ such that for all $x,y\in Q$, $x\prec y$ implies $x^-\prec y^-$. Denote by $\prec_{\text{deglex}}$ the deglex order on the free monoid $(Q \sqcup Q^-)^\ast$ induced by the order $\prec$.

Any ground term in the theory $P_1\langle Q \rangle$ can be written $f(\iota^{n_1}(x_1),\ldots,\iota^{n_k}(x_k))$ for $n_1, \dots, n_k \in \mathbb{N}$, where $\iota$ is the inverse operation defined in \eqref{SSS:PresentationOfGroups}, and $\iota^0$ denotes the identity $1$-cell of the theory $\freetha{P}_1$. Moreover, if each $n_i$ is chosen to be maximal, then $f$ is uniquely determined, and does not contain the operation $\iota$ in its leafs.
One defines a map
\[
\llbracket \, \rrbracket : P_1 \langle Q \rangle \to (Q \sqcup Q^-)^\ast
\]
that associates to any ground term $f(\iota^{n_1}(x_1),\ldots,\iota^{n_k}(x_k))$ in $P_1 \langle Q \rangle$, where the $n_i$'s are maximal as above, the word $x_1^{\varepsilon_1}\ldots x_k^{\varepsilon_k}$, where $\varepsilon_i=+$ if $n_i$ is even, and $\varepsilon=-$ if $n_i$ is odd.

Let us denote by $red(u)$ the normal form in $(Q \sqcup Q^-)^\ast$ of $\llbracket u \rrbracket$ with respect to relations of \eqref{E:InverseRelations}. Let $\models$ be the order on $P_1\langle Q\rangle$ defined by $u \models v$ if $red(u) \prec_{\text{deglex}} red(v)$.

We define a positive strategy for the algebraic polygraph $(P,Q,R)$, by setting, for any $\cl{w} \in \cl{P\langle Q \rangle}$, the set $\sigma(\cl{w})$ to be the subset of $\pi^{-1}(\cl{w})$ whose elements are of the form
\[
\mu(\mu(u,r_1^\varepsilon), v),
\quad\text{and}\quad
\mu(u,\mu(r_1^\varepsilon, v)),
\]
where
$u,v\in P_1\langle Q\rangle_{\text{red}}$, $r_1 \to r_2 \in R$, $\varepsilon=\pm 1$, and such that
\[
\mu(\mu(u,r_2^\varepsilon), v) \models \mu(\mu(u,r_1^\varepsilon), v),
\]
where, for $i=1,2$, we let $r_i^\varepsilon:=r_i$ if $\varepsilon=1$, and $r_i^\varepsilon:=\iota(r_i)$ otherwise.

\begin{proposition}
For the positive strategy $\sigma$ defined above, the algebraic polygraph $(P,Q,R)$ is positively $\sigma$-confluent.
\end{proposition}
\begin{proof}
Let us introduce an auxiliary strategy $\sigma'$ for $(P,Q,R)$ by setting
  \begin{eqn}{equation}
    \label{E:InterPositiveStrategyGroups}
    \sigma'(\cl{w})=\left\{C[r_1]\in\pi^{-1}(\cl{w})\mid
    \text{$C$ is a context of $P_1 \langle Q \rangle$}, \: r_1 \to r_2 \in R, \: \text{s.t.} \:
    C[r_2] \models C[r_1] \right\},
  \end{eqn}
for any $\cl{w} \in \cl{P\langle Q \rangle}$.
Prove that $(P,Q,R)$ is positively $\sigma'$-confluent.
For any rule $r_1\rightarrow r_2\in R$ and any ground context $C$ of $P_1\langle Q \rangle$ such that
$C[r_2]\models C[r_1]$, the reduction $C[r_1]\rightarrow C[r_2]$ is $\sigma'$-positive. Otherwise, if
$C[r_1] \models C[r_2]$, then the reduction
  $C[\mu(\mu(r_2,r_1^{-1}),r_1)]\to C[\mu(\mu(r_2,r_2^{-1}),r_1)]$ is $\sigma'$-positive and
  $C[\mu(\mu(r_2,r_1^{-1}),r_1)]$ and $C[\mu(\mu(r_2,r_2^{-1}),r_1)]$ are equivalent with respect to $P_2 \langle Q \rangle$ to
  $C[r_2]$ and $C[r_1]$, respectively. Now, it is sufficient to show that any $\sigma'$-positive
  reduction is also $\sigma$-positive.

Let us consider a $\sigma'$-positive reduction $C[r]: C[r_1] \to C[r_2]$,
let $n$ be the largest integer such that $C[r_1] = C_1 [\iota^n(r_1)]$ and $C_1$ is a (possibly empty) context. Denote by $\varepsilon := n \: \text{mod} \: 2$, then $\iota^n(r_1)$ is equivalent to $r_1^\varepsilon$  modulo $P_2\langle Q\rangle$.

If $C_1$ is empty, then the reduction is of the form $r_1^{\varepsilon} \to r_2^{\varepsilon}$. Since $C[r_2] \models C[r_1]$, then $r_2^{\varepsilon} \models r_1^{\varepsilon}$ and thus it is $\sigma$-positive.

Otherwise, $C_1 [r_1^\varepsilon]$ may be written either as $\mu(\mu(u', r_1^\varepsilon), v')$
or $\mu(u', \mu(r_1^\varepsilon, v'))$, where $u'$ and $v'$ are ground terms in $P_1\langle Q\rangle$. Denote by $u:= \widehat{u'}$ and $v := \widehat{v'}$ be the normal forms of $u'$ and $v'$
with respect to $P_2 \langle Q \rangle$.
Then $C_1 [r_1^\varepsilon]$ is equivalent modulo $P_2 \langle Q \rangle$ to
$\mu(\mu(u, r_1^\varepsilon), v)$ or $\mu(u, \mu(r_1^\varepsilon, v))$. Moreover, since $ red(u r_2^\varepsilon v) = red (C[r_2]) \prec_{\text{deglex}} red(C[r_1]) = red(u r_1^\varepsilon v)$,
the reduction $u r_1^\varepsilon v \to u r_2^\varepsilon v$ is $\sigma$-positive, where $ur_i^\varepsilon v$ denotes either
$\mu(\mu(u, r_i^\varepsilon), v)$ or $\mu(u, \mu(r_i^\varepsilon, v))$.
\end{proof}

\subsubsection{Example}
Let us consider the algebraic polygraph modulo $(P,Q,R, \ere{P}{R})$, where $P=\widetilde{\poly{Grp}}$, $Q = \{ s, \: t \}$ and $R = \{ \mu ( \mu(s,t),s) \Rightarrow \mu (t, \mu(s,t))\}$.
We consider the deglex order induced by the ordering $s>t>s^->t^-$.
The positive $\ere{P}{R}$-rewriting steps are of the form
\[
u \mu ( \mu(s,t),s) v \Rightarrow u \mu (t, \mu(s,t)) v \quad \text{or} \quad u \mu( \mu(s^-,t^-),s^-) v \Rightarrow u \mu (t^-, \mu(s^-,t^-)) v,
\]
where $u,v$ are reduced elements of $P_1 \langle Q \rangle_{\text{red}}$, and the orientation is compatible with the order $\models$ as defined in~\eqref{SSS:PositiveStrategiesGroups}. For instance, there is a positive $\ere{P}{R}$-rewriting step
\[ \mu ( \mu (\mu(s,t),s),t) \Rightarrow \mu ( \mu (t, \mu(s,t)), t) \]
yielding a reduction $stst \Rightarrow tstt$ in the free group $F(Q)$.

Let us give another example. Consider $u= tst$, $v = st$ and $\varepsilon = -1$, there is a $\sigma$-positive $\ere{P}{R}$-reduction as follows:
\[ tst \mu(\mu(s^-,t^-),s^-) st \equiv_P tst \mu(\mu(s^-,t^-),s^-) sts s^- \Rightarrow tst \mu(t^-, \mu(s^-,t^-)) stss^- \equiv_P \mu(s,t) \]
that gives a rewriting step $tsts^- \Rightarrow st$ in the quotient.

There is a critical branching of $\ere{P}{R}$ as follows:
\[
\xymatrix{
\mu(\mu(\mu(s,t),s), \mu(t,s)) \ar [r] \ar [d] & \mu(\mu(t,\mu(s,t)), \mu(t,s))
\\
\mu (\mu(s,t), \mu(\mu(s,t),s)) \ar [r] & \mu (\mu(s,t), \mu(t,\mu(s,t)))
}
\]
that is not confluent modulo. It induces the following non confluent algebraic critical branching in the free group $F(Q)$
\[
\xymatrix@R=0.8em{
& tstts \\
ststs \ar@/^2ex/ [ur]
\ar@/_2ex/ [dr] & \\
& sttst }
\]

\section{Conclusion and perspectives}

In this article, we have introduced the structure of algebraic rewriting system. We have instantiated this structure in various contexts widely used in computer algebra, such as string, linear, and group rewriting. We have formulated sufficient conditions to prove the critical branching lemma for algebraic rewriting systems. Our results lead us to formulate several perspectives.

In Section~\ref{SS:CriticalBranchingSRS}, we recovered the critical branching lemma for SRS with respect to a convergent presentation of the algebraic theory of monoids and a positive strategy making all the reductions positive, formalizing the classical setting of string rewriting. One may wonder what happens if we consider another presentation of the algebraic theory of monoids and another positive strategy. The choices of the presentation of the algebraic theory and the positive strategy define a paradigm of string rewriting. This raises the question to formalise a notion of Tietze equivalence between paradigms of string rewriting.

For left-monomial LRS and Gröbner bases the critical branching lemma only requires termination. Theorem~\ref{T:CBLlinear2} proves that the factorisation property is also required. Note that this property is always satisfied when we rewrite in left-monomial linear structures such as commutative or associative algebras. We expect that for left-monomial LRS, the factorisation property is equivalent to the positive confluence, and is always satisfied.

In the situation of group rewriting presented in Section~\ref{SS:RewritingInverse} we have defined a positive strategy to rewrite in a free group. We prove a critical branching lemma with respect to this strategy. However, we don't know an algorithm to compute the exhaustive list of critical branching with respect to this strategy yet, this is a work in progress. The same algorithmic problem occurs for the computation of the critical branchings for LRS that are not left-monomial.

Another issue is to extend the algebraic critical branching proved in this article to higher-structures such as linear operads. Rewriting was defined on linear operads in terms of shuffle Gröbner bases by Dotsenko and Khoroshkin in  \cite{DotsenkoKhoroshkin10} and shuffle linear polygraphs by Malbos and Ren in \cite{MalbosRen20}.
The structure of algebraic polygraph introduced in this article formalizes one-dimensional algebraic rewriting, that is rewriting in one-dimensional algebraic structures such as monoids, groups, modules, etc. We expect that our constructions can be extended to the setting of linear operads by considering algebraic polygraphs defined over a structure of cartesian $2$-polygraphs on shuffle trees.

Finally, another outlook is to extend our algebraic critical branching lemma to conditional rewriting systems in order to formalise the critical branching lemma for LRS defined over a field. The conditional rules are used to specify the rules depending on the invertibility of scalars in the field.

\begin{small}
  \renewcommand{\refname}{\Large\textsc{References}}
  \bibliographystyle{plain}

redpajama_set_name: RedPajamaArXiv


text:
1. mistrovství světa  v házené žen o jedenácti hráčích proběhlo ve dnech 25. – 28. září v Maďarsku.

Mistrovství se zúčastnila čtyři mužstva. Hrálo se v jedné skupině systémem každý s každým. Mistrem světa se stal tým Maďarska.

Výsledky a tabulka

 Maďarsko –  7:2

25. září 1949 – Budapešť

 Československo –  4:2

25. září 1949 – Budapešť

 Maďarsko –  Československo 4:1

26. září 1949 – Budapešť

 –  8:1

26. září 1949 – Budapešť

 Maďarsko –  7:3

28. září 1949 – Budapešť

 –  Československo 3:2

28. září 1949 – Budapešť

Soupisky

1.  Maďarsko

2.  Rakousko

Reference

Externí odkazy
 (en) IHF-Archív
 (en) Sportovní statistiky

Údržba:Články s referencemi v nadpisech
Mistrovství světa v házené žen
Házená v roce 1949
Házená v Maďarsku
Sport v Maďarsku v roce 1949
Sportovní události v Budapešti

redpajama_set_name: RedPajamaWikipedia


The GOP organized cigarette smuggling into Russia through Poland in late 1990 and early 1991, paying of KGB operatives in Russia. Cigarette sales in Russia were a method then of supplying income for disabled veterans, as cigarette kiosks were a "perk" of military service and a method of survival for many.
The KGB, in turn, arranged for Soviet bankers to tour the US, with Republican Party hosts and CIA security. Arrangements were made to set up a worldwide money laundering operation, I think we know who runs that.
Word was already out that the Soviet Union was down to its last days. The commercial banks of Leningrad, Moscow, the Ukraine, Belarus, Latvia and Estonia made deals with members of the GOP to split their assets, money removed from Russia, half to go to the Bush family and party leaders, the other half to be kept for the KBG who would be invited into the United States to run the Russian mafia and take over heroin distribution through the communities they would establish in Brighton Beach/Little Odessa.
Money laundering began through Cyprus, where organized crime had taken a strong foothold, and moved through accounts in Switzerland and the Caymans to selected banks in the US, some in Denver, some in Detroit and the major one in Astoria, New York, the former home of the Steinway Piano Company.
The first cigarette deals were negotiated by old line CIA accompanied by national leaders of the GOP. Just by accident, I attended more than one of those meetings and I don't even smoke.
I remember that thousands of cigarette machines were to be offered also but were refused. Russians felt they could never be secured.
Meetings were also held between the GOP, CIA and Diebold, the company accused of aiding in the rigging of voting machines. Diebold wanted a foothold in Soviet/Russian banking.
I remember Diebold talking about ATM machines and the Soviets responding that they had only recently decided to start using teller windows. You just don't forget that level of irony.
As I remember, I may have sat through those also.
The bank deals were cemented during a private fundraiser at the Pierre hotel in New York. I remember sitting between a key US senator responsible for overseeing banking issues and a lobbyist for this new partnership.
The evening was an interesting mix of major corporations and "made guys" filling the room. There are photos, nobody was careful.
The critical issue to be clear on is that the cigarette deal had little to do with cigarette companies and much to do with enriching GOP leaders who financed their retirement, huge homes, boats, all of it with laundered stolen cash from Russia, profits from cigarette deals and cemented a partnership with the Russian mafia which would later be supplanted with deals run through Kosovo and Albania, more vicious criminals, less cultured and more conveniently located for managing the world's heroin business.
This is why Camp Bondsteel was built, one of America's largest overseas bases, to channel heroin from, at that time, Turkey, today from Afghanistan, into Western Europe and the US.
The question being asked is how a Mormon can represent "big tobacco" when the real question is why would a Mormon open hundreds or thousands of numbered bank accounts in "safe havens" and work with organized crime.
Then again, a study of both the CIA and FBI lends itself to tales of the "Mormon Mafia," and their stranglehold on those organizations.
Anyone who comes against the Mormons and lives in the Western United States knows what real terrorism is like.