Algebraic critical pair lemma
Cyrille Chenavier, Benjamin Dupont, and Philippe Malbos
1
2,3

Johanes Kepler University, Linz, Austria, cyrille.chenavier@jku.atUniversité de Lyon, France, {bdupont,malbos}@math.univ-lyon1.fr
Abstract

Convergent rewriting systems on algebraic structures give methods to prove coherence
results and compute homological invariants of these structures. These methods are basedon higher-dimensional extensions of the critical pair lemma that characterizes local confluence from confluence of critical pairs. The analysis of local confluence of rewriting systems
on algebraic structures, such as groups or linear algebras, is complicated because of theunderlying algebraic axioms, and local confluence properties require additional termination conditions. In this work, we define the structure of algebraic polygraph modulo thatformalizes the interaction between the rules of the rewriting system and the inherent algebraic axioms, and we show a critical pair lemma algebraic polygraphs. We deduce fromthis result a critical pair lemma for rewriting systems on algebraic structures specified byrewriting systems convergent modulo AC. As an illustration, we explicit our constructions
on linear rewriting systems.

1

Introduction

The critical-pair completion (CPC) is an approach developed in the mid sixties that combinescompletion procedure and the notion of critical pair [2]. It originates from theorem proving [12],polynomial ideal theory [1], and the word problem [9, 11]. In the mid eighties, CPC has foundoriginal and deep applications in algebra to solve coherence problems [14], or to compute homological invariants [13]. More recently, higher-dimensional extensions of the CPC approach wereused for the computation of cofibrant replacements of algebraic and categorical structures [5, 6].
These constructions based on CPC are known for monoids, small categories, and algebras overa field. However, the extension of these methods to a wide range of algebraic structures is madedifficult because of the interaction between the rewriting rules and the inherent axioms of thealgebraic structure. For this reason, the higher-dimensional extensions of the CPC approach
for a wide range of algebraic structures, including groups, Lie algebras, is still an open problem.
One of the main tools to reach confluence in CPC procedure for algebraic rewriting systems isthe critical pair lemma, or critical branching lemma (CBL). Its proof is based on classification of
the local branchings into orthogonal branchings, that is involving two rules that do not overlap,
overlapping branchings involving two rules that overlap. A 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, themain argument to achieve CBL is to prove that orthogonal and overlapping branchings areconfluent. For string and term rewriting systems, 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 ruleswith respect to an ambient monomial order, and CBL is well known in this context. However,some algebras do not admit any higher-dimensional finite convergent presentation on a fixed setof generators with respect to a monomial order, [5]. However, when the orientation of rules does
not depend on a monomial order, as in [5], the CBL requires additional assumptions, namely

Algebraic critical pair lemma

Chenavier, Dupont, and Malbos

termination and positivity of reductions. A positive reduction for a linear rewriting system,as defined in [5], is the application of a reduction rule on a monomial that does not appear in
the polynomial context. For instance, consider the linear rewriting system on an associative
algebra over a field K given in [5] defined by rules α : xy → xz and β : zt → 2yt. It has no
critical branching, but it has a non-confluent additive branching:
2xβ
αt + xzt // 4xyt4αtxzt + xβ+=
xyt + xzt
3 xzt + 2xyt
. 3xyt αt + 2xyt
xyt + xβ
/ 3xzt3αt3xβ/ 4xzt

4xβ

/ ···

2xzt

/ 6xyt/ ···6αtThe dotted arrows correspond to non positive reductions. We note that the lack of termination
is an obstruction to confluence of orthogonal branchings.
In this work we introduce an algebraic setting for the formulation of the CBL. We define
the structure of algebraic polygraph modulo which formalizes the interaction between the rulesof the rewriting system and the inherent axioms of the algebraic structure. We show a CBL
for algebraic polygraphs modulo. We deduce from this result a CBL for rewriting systems on
algebraic structures whose axioms are specified by term rewriting systems that are convergent
modulo associativity and commutativity. Finally, we explicit our results in linear rewriting, andexplain why termination is a necessary condition to characterize local confluence in that case.
In Section 2, we recall the categorical structure of cartesian polygraph introduced in [10]. In
Section 3, we introduce the notion of algebraic polygraph modulo, and we refer the reader to [4]for a categorical interpretation of the given constructions. In Section 4, we present confluence
property of algebraic polygraphs modulo from [4] and algebraic polygraphs modulo with respect
a positive strategy σ. Finally, we state the algebraic critical branching lemma. This abstract
is a short version of the preprint [3], where more detailed constructions and examples can befound.

2

Cartesian polygraphs

A signature is defined by a set P0 of sorts and a set P1 of operations on the free monoid overP0 . We denote by s0 (α) and t0 (α) the arity and coarity of α ∈ P1 . When s1 , . . . , sk are sorts,
we denote s = s1 . . . sk their product in the free monoid over P0 . We denote by P1× the freetheory generated by a signature (P0 , P1 ). Its 1-cells, also called terms on the signature (P0 , P1 )s
are defined inductively. The canonical projections xi : s → si are variables, and for any terms
f : s → r and f 0 : s → r 0 in P1× , we denote by hf, f 0 i : s → rr 0 , the pairing of terms f, f 0 . A(cartesian) 2-polygraph is a data made of a signature (P0 , P1 ), and a set P2 equipped with twomaps t1 , s1 : P2 → P1× , satisfying the globular conditions s0 s1 = s0 t1 and t0 s1 = t0 t1 . Anelement α of P2 is called a rule, and relates terms of same arity and coarity.
2.1. Two-dimensional theories. Recall that a 2-theory is a 2-category with an additional
cartesian structure on its 1-cells and 2-cells [10]. We denote by P2× the free 2-theory generated
by a cartesian 2-polygraph (P0 , P1 , P2 ). Its underlying 1-category is the free theory P1× , andits 2-cells are defined inductively as follows. For α : f ⇒ f 0 in P2 and h ∈ P1× , there is a 2-cell
αh : f ? h ⇒ f 0 ? h in P2× , and for β : g ⇒ g 0 in P2× , there is a 2-cell hα, βi : hf, gi ⇒ hf 0 , g 0 i.
2

Algebraic critical pair lemma

Chenavier, Dupont, and Malbos

Finally, there are 2-cells in P2× of the form A[α] : A[f] ⇒ A[f 0 ] where A[] denotes an algebraic
context of the form: khidk1 , . . . , i , . . . , idkj i : s → r, where k1 , . . . , kj : s → ri and k : r → r
belong to P1× , and i is the i-th element of the pairing. These 2-cells are required to satisfy
exchange relations, see [10]. The source and target maps s1 , t1 extend to P2× and we denote a−
and a+ for s1 (a) and t1 (a). A ground term in P1× is a term with source 0. A 2-cell a in P2× isground when a− is a ground term. An algebraic context A[] = fhf1 , . . . , i , . . . f|r| i is called
ground when the fi are ground terms.
The free (2, 1)-theory generated by a cartesian 2-polygraph (P0 , P1 , P2 ), denoted by P2> , isthe free 2-theory P2× whose any 2-cell is invertible with respect the ?-composition. The 2-cellsof the (2, 1)-theory P2> corresponds to elements of the equivalence relation generated by P2 .
2.2. Rewriting properties of cartesian polygraphs. The algebraic contexts of a 2polygraph P can be composed as follows AA 0 [] := A[A 0 []]. One defines a bi-context as
B[i , j ] := fhidf1 , . . . , i , . . . , j , . . . , idfk i where the fk : s → rk and f : r → r are terms in
P1× , and i (resp. j ) has to be filled by a term gi : s → ri (resp. gj : s → rj ). A 2-cellof the form A[αw] where A is an algebraic context, w is a term in P1× and α ∈ P2 is calleda P-rewriting step. A P-rewriting path is a non-identity 2-cell of P2× . Such a 2-cell can be
decomposed as a ?-composition of rewriting steps α = A1 [α1 w1 ] ? . . . Ak [αk wk ].

3

Algebraic polygraphs modulo

Let (P0 , P1 ) be a signature, and Q be a set of generating ground terms whose target is a sort×in P0 . We denote by P1 hQi the set of ground terms of the free theory (P1 ∪ Q) . An algebraic
polygraph is a data made of a 2-polygraph P, a family of set of constant 1-cells Q, and a cellularextension R of the set of ground terms P1 hQi, that is a set equipped with two source andtarget maps R → P1 hQi. A R-rewriting step is a ground 2-cell in the free 2-theory R× of theform A[α] : A[f] → A[g], where A[] is a ground context. A R-rewriting path is a finite or
infinite sequence a1 ? . . . ? ak ? . . . of R-rewriting steps ai . The size of a R-rewriting path a,denoted by |a|, is the number of rewriting steps needed to write a as a composition as above.
The cellular extension P2 defined on P1× extends to a cellular extension on the free 1-theory×b2 . We denote by P2 hQi the set of ground 2-cells in the free 2-theory(P1 ∪ Q) denoted by P×b(P2 ) . The algebraic polygraph (P, Q, P2 hQi) is called the algebraic polygraph of axioms. We
denote by PhQi the quotient of P1 hQi by the congruence generated by relations in P2 hQi.
3.1. Positive strategies. Denote by f the image of a ground term f by the canonical projection π : P1 hQi → PhQi. Let σ : PhQi → Set be a map such that for any f ∈ PhQi, σ(f) isa chosen non-empty subset of π−1 (f). Such a map is called a positive strategy with respect to(P, Q). A R-rewriting step a is called σ-positive if a− belongs to σ(a− ), and a R-rewriting patha1 ? . . . ? ak is called σ-positive if any of its rewriting steps is positive.
We will use positive strategies wrt a 2-polygraph P such that P2 = P20 ∪P200 , with P20 confluent
modulo P200 . For every 1-cell f in PhQi, we set σ(f) = NF(f, P20 mod P200 ), where f ∈ π−1 (f),the set of normal forms of f for P20 modulo P200 . This is well-defined following [7], since if
f, f 0 ∈ π−1 (f), then NF(f, P20 mod P"2 ) ≡P"2 NF(f 0 , P20 mod P"2 ).
3.2. Algebraic polygraphs modulo. Given an algebraic polygraph P = (P, Q, R) and apositive strategy σ on P, one denotes by P RP the cellular extension of P1 hQi whose elements
are of the form e ? a ? e 0 , where e and e 0 are 2-cells in P2 hQi> and a is a R-rewriting step such3

Algebraic critical pair lemma

Chenavier, Dupont, and Malbos

0that e+ = a− and a+ = e−
, see [4] for a detailed construction. A 2-cell e ? a ? e 0 in P RP iscalled σ-positive if a is a σ-positive R-rewriting step. An algebraic polygraph modulo, APM forshort, is a data (P, Q, R, S) made of an algebraic polygraph (P, Q, R), and a cellular extension S
of P1 hQi such that R ⊆ S ⊆ P RP .
An algebraic polygraph (P, Q, R) is called quasi-terminating if for each sequence (fn )∈N of
1-cells of P1 hQi such that for each n ∈ N, there is a rewriting step fn → fn+1 , the sequence(fn )∈N contains an infinite number of occurrences of same 1-cell. An APM (P, Q, R, S) is called
quasi-terminating if the algebraic polygraph (P, Q, S) is quasi-terminating. A 1-cell f of P1 hQi
is quasi-irreducible if for any S-rewriting step f → g, there exists a S-rewriting sequence from g
to f. A quasi-normal form of a 1-cell f in P1 hQi is a quasi-irreducible 1-cell fe of P1 hQi such thate For a quasi-terminating APM, any 1-cell f ofthere exists a S-rewriting sequence from f to f.
P1 hQi admits at least a quasi-normal. A quasi-normal form strategy is a map s : P1 hQi → P1 hQiesending a 1-cell f on a chosen quasi-normal f.
An algebraic rewriting system on (P, Q, R, S, σ) is a cellular extension S of PhQi defined byσσ
S = {a : a− ⇒ a+ | a ∈ S}. Let us consider the subset S of S defined by S = {a : a− ⇒σ
×a+ | a is a σ-positive S-rule}. A S-rewriting step (resp. a S -rewriting step) is a 2-cell in S
σ×

(resp. S ) of the form C[a] : C[a− ] ⇒ C[a+ ] , where C is a ground context of P1 hQi and C[a]is a S-rewriting step (resp. σ-positive S-rewriting step). A S-rewriting path is a sequence of
S-rewriting steps.

4

Confluence in algebraic polygraphs modulo

Let P = (P, Q, R, S) be an APM with a positivity strategy σ. A σ-branching of P is a triple(a, e, b) where a, b are σ-positive 2-cells of S× and e is a 1-cell of P2 hQi> such that e− =a− and e+ = b− . It is local if a is a S-rewriting step, b is a 2-cell of S× and e a 2-cellof P2 hQi> such that |e| + |b| = 1. Note that the 2-cell b (resp. e) can be an identity 2cell of S× (resp of P2 hQi> ), and in that case the σ-branching is of the form (a, e) (resp.
(a, b)). Such a σ-branching is σ-confluent modulo if there exist σ-positive 2-cells a 0 and b 0
0
in S× and a 2-cell e 0 of P2 hQi> as depicted on the right. We say that f a / f 0 a / h
the APM P is confluent modulo (resp. locally confluent modulo) if any e
 e0

0
/
/
σ-branching modulo (resp. local branching modulo) is confluent modulo. g
g
h0
0
b

b

4.1. Theorem (Newman lemma modulo for algebraic polygraphs modulo). Let P bea quasi-terminating APM, and σ be a positive strategy on P. If P is locally σ-confluent modulo,
then it is σ-confluent modulo.
The proof of this result, and of Thm. 4.4 are based on the principle of double induction
on the distance to the quasi-normal form, and are extensions to quasi-terminating setting of
Huet’s constructions based on double induction principle [7] in the terminating setting. Let
d : P1 hQi → N maping a 1-cell f to the length d(f) of the shortest P RP -rewriting path from fe that we extend to a map on σ-branchings (a, e, b) by setting d(a, e, b) := d(a− ) + d(b− ).
to f,
We define a well-founded order ≺ on the set of σ-branchings of P by (a, e, b) ≺ (a 0 , e 0 , b 0 ) ifd(a, e, b) < d(a 0 , e 0 , b 0 ).
4.2. Classification of local σ-branchings modulo. The local σ-branchings modulo of S
can be classified in the following families:
A[a+ ] o4aA[a− ]
Triviala/ A[a+ ]A[a+ ] oabA[a− ] = A[A 0 [b− ]]Inclusion independant/ A[A 0 [b+ ]]Algebraic critical pair lemma

B[a,b− ]/ B[a+ , b− ]=B[a− , b− ]Chenavier, Dupont, and Malbos

B[a− , b− ]B[a− ,b]/ B[a− , b+ ]Orthogonal

B[a− , e− ]B[a,e− ]/ B[a+ , e− ]B[a− ,e]
B[a− , t1 (e)]Orthogonal modulo

together with symmetries on orthogonal σ-branchings modulo, for some σ-positive S-rewriting
steps a, b, 2-cell e in P2 hQi> , ground contexts A, A 0 , and ground bi-contexts B, B 0 . The
remaining local σ-branchings modulo are called non-orthogonal σ-branchings modulo.
We define an order relation on σ-branchings modulo of P = (P, Q, R, S) by setting (a, e, b) v
(A[a], A[e], A[b]) for a ground context A. A critical σ-branching modulo is a local σ-branchingmodulo P which is non trivial, non orthogonal and minimal wrt the order relation v.
4.3. Positive confluence. An APM (P, Q, R, S) with a positive strategy σ is called σ-positively
confluent if, for any S-rewriting step f, there exists a representing
a0
/
af
−
0
0
af
− ∈ σ(a− ) of a− and two σ-positive S-reductions a and b ofe e 00size at most 1 as in the following on the right.
/
/
/
a
−

a

e0

b0

4.4. Theorem (Terminating critical branching theorem modulo). Let (P, Q, R, S) be aquasi-terminating and positively σ-confluent APM with a positive strategy σ. Then it is locally
σ-confluent modulo if and only if the two following properties hold:a0 ) any critical σ-branching modulo (a, b) made of S-rewriting steps is σ-confluent modulo.
b0 ) any critical σ-branching modulo (a, e), with a S-rewriting step and e is a 2-cell in P2 hQi>
of length 1, is σ-confluent modulo.
When all the reductions are positive, that is S(u) = π−1 (u) for any u, the quasi-termination
assumption in Prop. 4.4 are not needed. In that case, the positive confluence is always satisfied.
4.5. Algebraic critical branching lemma. Let A be an algebraic rewriting system on an
APM P = (P, Q, R, S). The critical branchings of A are the projections of the critical σσbranchings modulo of P of the form a0 ), that is pairs (a, b) of S -rewriting steps such thatfthere is a σ-branching modulo in P with source (af− , b− ). From Prop. 4.4, we deduce our main
result.
4.6. Theorem. Let P = (P, Q, R, S) be an APM such that P RP is quasi-terminating and positively confluent. Let A be an algebraic rewriting system on P. Then A is locally confluent if
and only if its critical branchings are confluent.
4.7. CBL for linear rewriting. Suppose that P contains the convergent 2-polygraph modulo
AC that presents the theory of modules over commutative rings given in [8], denoted by RMod.
If P200 is the 2-polygraph of associativity and commutativity relations, and P20 is RMod, thenThm. 4.6 corresponds to CBL for linear rewriting systems proved in [5]. Indeed, given an APM(P, Q, R, S) with the σ-strategy defined in 3.1, one proves that the positivity confluence of S withrespect to σ implies the factorization property of [5]. This property means that any rewritingσstep a of S can be decomposed as a = b ? c−1 where b and c are either rewriting steps of S or
identities. Finally, the quasi-termination assumption of P RP is equivalent to the termination
assumption in [5].

5Algebraic critical pair lemma

Chenavier, Dupont, and Malbos

References[1] B. Buchberger. An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo
a Zero Dimensional Polynomial Ideal. PhD thesis, University of Innsbruck, Austria, 1965.
[2] B. Buchberger. History and basic features of the critical-pair/completion procedure. J. Symbolic
Comput., 3(1-2):3–38, 1987. Rewriting techniques and applications (Dijon, 1985).
[3] Cyrille Chenavier, Benjamin Dupont, and Philippe Malbos. Algebraic polygraphs modulo andlinear rewriting. preprint, arXiv:2004.14361, 2020.
[4] B. Dupont and P. Malbos. Coherent confluence modulo relations and double groupoids.
arXiv:1810.08184, Hal-01898868, 2018.
[5] Y. Guiraud, E. Hoffbeck, and P. Malbos. Convergent presentations and polygraphic resolutions ofassociative algebras. Math. Z., 2019.
[6] Y. Guiraud and P. Malbos. Higher-dimensional normalisation strategies for acyclicity. Adv. Math.,
231(3-4):2294–2351, 2012.
[7] G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. J.
Assoc. Comput. Mach., 27(4):797–821, 1980.
[8] J.-M. Hullot. A catalogue of canonical term rewriting systems. 1980. SRI International, Technical
Report CSL 113.
[9] D. Knuth and P. Bendix. Simple word problems in universal algebras. In Computational Problems
in Abstract Algebra (Proc. Conf., Oxford, 1967), pages 263–297. Pergamon, Oxford, 1970.
[10] P. Malbos and S. Mimram. Cartesian polygraphic resolutions. in progress, 2020.
[11] M. Nivat. Congruences parfaites et quasi-parfaites. In Séminaire P. Dubreil, 25e année (1971/72),
Algèbre, Fasc. 1, Exp. No. 7, page 9. Secrétariat Mathématique, Paris, 1973.
[12] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12:23–41,
1965.
[13] C. Squier and F. Otto. The word problem for finitely presented monoids and finite canonicalrewriting systems. In RTA, 1987, volume 256 of LNCS, pages 74–82. 1987.
[14] C. C. Squier, F. Otto, and Y. Kobayashi. A finiteness condition for rewriting systems. TCS,
131(2):271–294, 1994.

6