Clément Alleaume

Alleaume -Philippe Clément

Malbos

COHERENCE OF STRING REWRITING SYSTEMS BY DECREASINGNESS

Keywords: string rewriting systems, coherence, termination, decreasingness

come

INTRODUCTION

At the end of the eighties, using a homological argument, Squier showed that there are finitely presented monoids with a decidable word problem that cannot be presented by a finite convergent (i.e., confluent and terminating) string rewriting system, [START_REF] Squier | The word problem for finitely presented monoids and finite canonical rewriting systems[END_REF][START_REF] Craig | Word problems and a homological finiteness condition for monoids[END_REF]. He linked the existence of a finite convergent presentation for a finitely presented monoid to a homological property by showing that the critical branchings of a convergent string rewriting system generate the module of the 2-homological syzygies of the presentation. A purely combinatorial approach is then presented in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] to the question of whether or not a finitely presented monoid admits a finite convergent presentation. The existence of such a presentation is linked to a finiteness condition of finitely presented monoids, called finite derivation type, that extends the properties of being finitely generated and finitely presented.

Beyond the questions of decidability of the word problem and of the existence of finite convergent presentations, the graph-theoretical tools associated to convergent presentations of monoids developped in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] were applied to question of coherence problems for monoids (e.g., Artin monoids [START_REF] Gaussent | Coherent presentations of Artin monoids[END_REF] or plactic monoids [START_REF] Hage | Knuth's Coherent Presentations of Plactic Monoids of Type A[END_REF]) and monoidal categories [START_REF] Guiraud | Coherence in monoidal track categories[END_REF]. In particular, one of the problems is to compute a coherent presentation of a monoid presented by a string rewriting system. Such a presentation extends the generators and the rules by homotopy generators taking into account all the relations amongst the rewriting sequences. A method is given in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] to solve this problem from a convergent string rewriting system. However, in some situations it is difficult to get both confluence and termination on a finite set of generators and a finite set of rules.

In this article, using decreasingness methods from [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams[END_REF], we show how to weaken the termination hypothesis in the construction of coherent presentations. As an application we show how to extend a confluent and quasi-terminating string rewriting system into a coherent presentation.

Squier's two-dimensional complex. To a string rewriting system Σ 2 on an alphabet Σ 1 Squier, Otto and Kobayashi associated in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] a 2-dimensional cellular complex SpΣq, defined independently by Kilibarda [START_REF] Kilibarda | On the algebra of semigroup diagrams[END_REF] and Pride [START_REF] Stephen | Low-dimensional homotopy theory for monoids[END_REF]. The complex SpΣq has only one 0-cell, its 1-cells are the strings in the free monoid Σ 1 generated by the alphabet Σ 1 and its 2-cells are induced by the rewriting rules α : u ñ v in Σ 2 and the set Σ 2 of their inverses α ´: v ñ u. That is, there is a 2-cell in SpΣq between each pair of strings with shape wuw 1 and wvw 1 such that Σ 2 \ Σ 2 contains the relation u ñ v. This 2-dimensional complex is extended with 3-cells, called Peiffer confluences, filling all the 2-spheres of the following form wv 1 w 1 u 2 w 2 wv 1 w 1 α 2 w 2 2 R wu 1 w 1 u 2 w 2 wα 1 w 1 u 2 w 2 9 Y wu 1 w 1 α 2 w 2 5 U wv 1 w 1 v 2 w 2 wu 1 w 1 v 2 w 2 wα 1 w

1 v 2 w 2 C c Õ %
where α 1 : u 1 ñ v 1 and α 2 : u 2 ñ v 2 are in Σ 2 \ Σ 2 and w, w 1 and w 2 are strings in Σ 1 . The Peiffer confluences make homotopic the 2-cells corresponding to the application of rewriting steps on non-overlapping strings.

A homotopy basis of the complex SpΣq is defined as a set Σ 3 of additional 3-cells that makes SpΣq aspherical, that is any 2-dimensional sphere can be "filled up" by the 3-cells of Σ 3 . The presentation Σ is called of finite derivation type (FDT) if it is finite and it admits a finite homotopy basis. The FDT property is an invariant property for finitely presented monoids, that is, if Σ and Υ are two finite string rewriting systems that present the same monoid, then Σ has FDT if and only if Υ has FDT, [START_REF] Squier | A finiteness condition for rewriting systems[END_REF].

Squier's completion. Given a convergent string rewriting system Σ, the set made of one 3-cell filling a confluence diagram induced by each critical branching forms a homotopy basis of SpΣq, [START_REF] Squier | A finiteness condition for rewriting systems[END_REF]. Such a set of 3-cells is called a family of generating confluences of Σ. In others words, any diagram defined by two parallel rewriting sequences can be filled up by confluence diagrams induced by the critical branchings and by the Peiffer confluences. This result corresponds to a homotopical version of Newman's Lemma, [START_REF] Newman | On theories with a combinatorial definition of "equivalence[END_REF]. In particular, when the presentation is finite, it has finitely many critical branchings, hence a finite family of generating confluences. This is a way to prove that finite convergent presentations have FDT, [START_REF] Squier | A finiteness condition for rewriting systems[END_REF].

Squier's completion without termination. The above result starts from a convergent presentation and the construction of homotopy bases is made by Noetherian induction. In some situations, it is difficult to get both confluence and termination without adding new generators, as in the case of plactic monoids [START_REF] Hage | Knuth's Coherent Presentations of Plactic Monoids of Type A[END_REF] or Artin monoids [START_REF] Gaussent | Coherent presentations of Artin monoids[END_REF]. Moreover, the addition of new generators implies as much new relations and thus new potentially non confluent critical branchings. For instance, the Artin monoid on the symmetric group S 2 is the monoid of braids on three strands B 3 generated by two elements s and t and one relation sts " tst. Kapur and Narendran proved that this monoid does not admit a finite convergent presentation with only two generators, [START_REF] Kapur | A finite Thue system with decidable word problem and without equivalent finite canonical system[END_REF]. Note that a finite convergent presentation can be obtained by Knuth-Bendix completion on the presentation with three generators s, t, a and the two rules sts ñ tst and st ñ a, where a is a redundant generator.

Coherence for quasi-terminating polygraphs. In this article, we weaken the termination hypothesis and we give a construction of homotopy bases for decreasing and quasi-terminating string rewriting systems. The notion of quasi-termination weakens termination in the sense that if there is an infinite rewriting sequence it must contain infinitely many occurrences of the same 1-cell. In that case, Noetherian induction cannot be used to construct a coherent presentation. For this reason we proceed by using a well-founded labelling on the rewriting system, called the labelling to the quasi-normal form. For example, the monoid B 3 admits the following confluent and quasi-terminating presentation @ s, t ˇˇsts ñ tst, tst ñ sts D .

We obtain a homotopy basis of the monoid B 3 containing five 3-cells. This presentation can be homotopically reduced to obtain an empty homotopy basis.

Summary of results.

In this work, we use the categorical description of string rewriting systems by 2-polygraphs, that are recalled in Section 2. We introduce the notion of decreasing 2-polygraph from the corresponding one introduced by van Oostrom for abstract rewriting systems in [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams[END_REF]. We will use van Oostrom's decreasingness techniques to prove our main result. However, decreasingness for string rewriting systems needs to take into account the structure of rewriting on strings. In particular, we introduce the notion of Peiffer decreasingness in order to take into account the confluence diagrams induced by application of rewriting steps on non-overlapping strings and the notion of compatibility with contexts for taking into account the contexts of the rules.

In Section 3, we extend Squier's completion known on convergent 2-polygraphs to decreasing 2polygraphs. We define a Squier's decreasing completion of a decreasing 2-polygraph Σ as an extension of Σ by the globular extension of loops, containing one 3-cell for each equivalence class of elementary 2loop and the globular extension of generating decreasing confluences, containing a decreasing confluence diagram for each critical branching of Σ.

Our main result states that a strictly decreasing 2-polygraph whose labelling is compatible with contexts and Peiffer decreasing can be extended into a coherent presentation, Theorem 3.2.1. As a consequence of this result, we show how to compute a coherent presentation from a confluent and quasiterminating 2-polygraph. Finally, we show how our construction generalizes the one given in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] for convergent rewriting systems and we deduce some homological and homotopical consequences.

DECREASING POLYGRAPHS

In this section, we recall categorical notions used in this work to describe string rewriting systems and relations between rewriting sequences. We refer the reader to [START_REF] Guiraud | Polygraphs of finite derivation type[END_REF] for a deeper presentation of these notions. Then we introduce decreasing 2-polygraphs from the corresponding notion for abstract rewriting systems introduced by van Oostrom in [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams[END_REF].

2.1. Two-dimensional polygraphs and extended presentations 2.1.1. Two-dimensional polygraphs. A 1-polygraph Σ is a directed graph made of a set of 0-cells Σ 0 , a set of 1-cells Σ 1 and source and target maps s 0 , t 0 : Σ 1 Ñ Σ 0 . We denote by Σ 1 the free category generated by Σ 1 . A globular extension of the free category Σ 1 is a set Σ 2 equipped with two maps s 1 , t 1 : Σ 2 Ñ Σ 1 such that, for every α in Σ 2 , the pair ps 1 pαq, t 1 pαqq is a 1-sphere in the category Σ 1 , that is, s 0 s 1 pαq " s 0 t 1 pαq and t 0 s 1 pαq " t 0 t 1 pαq. A 2-polygraph is a triple Σ " pΣ 0 , Σ 1 , Σ 2 q, where pΣ 0 , Σ 1 q is a 1-polygraph and Σ 2 is a globular extension of Σ 1 , whose elements are called the 2-cells of the 2-polygraph. A presentation of a category C is a 2-polygraph such that the quotient of the free category Σ 1 by the congruence generated by Σ 2 is isomorphic to C. Note that a monoid being a category with a single object, is presented in the same way by a 2-polygraph with only one 0-cell.

2.1.2. Free 2-categories. Recall that a 2-category (resp. p2, 1q-category) C is a category enriched in category (resp. groupoid). Equivalently, a p2, 1q-category is a 2-category in which all 2-cells are invertible for the 1-composition. We denote by C 2 the set of 2-cells of C and the 0-composition (resp. 1-composition) of two 2-cells f and g in C is denoted by f ‹ 0 g, or by fg (resp. f ‹ 1 g) . We will denote by s i (resp. t i ) the i-source map (resp. i-target map) defined on 1-cells and 2-cells of a 2-category. A 2-sphere in C is a pair pf, gq of 2-cells of C such that s 1 pfq " s 1 pgq and t 1 pfq " t 1 pgq.

Given a 2-polygraph Σ, we will denote by Σ 2 the free 2-category generated by Σ and by Σ J 2 the free p2, 1q-category generated by Σ, that is the free 2-category generated by Σ in which all the 2-cells are invertible.

Rewriting sequences.

A rewriting step with respect to a 2-polygraph Σ is a 2-cell of Σ 2 of the form uϕv where u and v are 1-cells in Σ 1 and ϕ is a 2-cell of Σ 2 . We denote Σ stp the set of rewriting steps of Σ. A rewriting sequence with respect to Σ is a finite or infinite sequence f 0 ¨f1 ¨. . . ¨fi ¨¨¨¨, where the f i are rewriting steps such that t 1 pf i q " s 1 pf i`1 q for all i ě 0. A 1-cell u rewrites into a 1-cell v if there is a rewriting sequence f 0 ¨. . . ¨fn such that s 1 pf 0 q " u and t 1 pf n q " v.

For any rewriting sequence f 0 ¨f1 ¨. . .¨f n from u to v there is a corresponding 2-cell f 0 ‹ 1 f 1 ‹ 1 . . .‹ 1 f n in the 2-category Σ 2 with source s 1 pf 0 q " u and target t 1 pf n q " v. Conversely, any 2-cell f in the 2-category Σ 2 can be decomposed as a composite f 0 ‹ 1 . . . ‹ 1 f n of rewriting steps. Note that, this decomposition is unique up to Peiffer relations.

The length of a finite rewriting sequence f is the number, denoted by pfq, of rewriting steps occurring in the sequence. Given two 1-cells u and v such that u can be reduced to v, the distance from u to v, denoted by dpu, vq, is the length of the shortest rewriting sequence from u to v.

2.1.4. Support of a 2-cell. Let Σ be a 2-polygraph. Any 2-cell f in Σ 2 can be written as a 1-composite of finitely many rewriting steps u 1 ϕ 1 v 1 , . . . , u k ϕ k v k , where the u i and v i are 1-cells in Σ 1 and ϕ i is a 2-cell in Σ 2 . We define the support of the 2-cell f as the multiset, denoted by Supppfq, consisting of the 2-cells ϕ i occurring in this decomposition. The support is well-defined because any decomposition of f in Σ 2 into a 1-composite of rewriting steps involves the same rewriting steps. Note also that any such a decomposition is finite and thus the support of a 2-cell is a finite multiset. As a consequence, the multiset inclusion is a well-founded order on supports, allowing us to prove some properties by induction on the support of 2-cells.

2.1.5. Branchings. A (finite) branching of a 2-polygraph Σ is a pair pf, gq of (finite) rewriting sequences of Σ with a common source u " s 1 pfq " s 1 pgq. Such a branching will be denoted by pf, gq : u ñ pt 1 pfq, t 1 pgqq. A confluence of a 2-polygraph Σ is a pair pf 1 , g 1 q of rewriting sequences of Σ with a common target v " t 1 pf 1 q " t 1 pg 1 q. Such a confluence will be denoted by pf 1 , g 1 q : pt 1 pfq, t 1 pgqq ñ v.

A branching pf, gq is local (resp. aspherical) if f and g are in Σ stp (resp. f " g). A Peiffer branching

Two-dimensional polygraphs and extended presentations

of Σ is a local branching pfv, ugq with source uv where u, v are composable 1-cells and f, g are in Σ stp . An overlapping branching of Σ is a local branching that is not aspherical or Peiffer. An overlapping branching is called a critical branching if it is minimal for the order Ď on local branchings generated by pf, gq Ď pwfw 1 , wgw 1 q, for any local branching pf, gq composable with 1-cells w and w 1 in Σ 1 .

2.1.6. Termination and quasi-termination. A 2-polygraph Σ is terminating if it has no infinite rewriting sequence, that is there is no sequence pu n q nPN of 1-cells such that for each n in N, there is a rewriting step from u n to u n`1 . In that case, every 1-cell u of Σ 1 has at least one normal form p u, that is, there is no rewriting step with source p u. Following [START_REF] Dershowitz | Termination of rewriting[END_REF], we say that a 2-polygraph Σ is quasi-terminating if for each sequence pu n q nPN of 1-cells such that for each n in N there is a rewriting step from u n to u n`1 , the sequence pu n q nPN contains an infinite number of occurrences of the same 1-cell.

Let Σ be a 2-polygraph. A 1-cell u of Σ 1 is called a quasi-normal form if for any rewriting step with source u leading to a 1-cell v, there exists a rewriting sequence from v to u. A quasi-normal form of a 1-cell u is a quasi-normal form r u such that there exists a rewriting sequence from u to r u. If Σ is quasi-terminating, any 1-cell u of Σ 1 admits a quasi-normal form. Note that, this quasi-normal form is neither irreducible nor unique in general.

Example. Let us consider the 2-polygraph defined by the following 2-graph c

H h % E d 7 W p Ô b H h a p Ô
The 1-cell d has two quasi-normal forms which are a and b. The 1-cell c is not a quasi-normal form because there is a rewriting step from c to a and a cannot be rewritten into c.

Confluence and convergence.

A 2-polygraph Σ is confluent (resp. locally confluent) if every branching (resp. local branching) pf, gq of Σ can be completed by a confluence pf 1 , g 1 q : pt 1 pfq, t 1 pgqq ñ v. We say that Σ is convergent (resp. quasi-convergent) if it is confluent and it terminates (resp. quasi-terminates).

2.1.9. Example. The 2-polygraph ΣpB 3 q " @ s, t ˇˇα : sts ñ tst, β : tst ñ sts D presents the monoid B 3 . This polygraph is not terminating but it is quasi-terminating. It has four critical branchings pαt, sβq, pβs, tαq, pαts, stαq and pβst, tsβq. These four branchings are confluent as follows is a set Γ together with two maps s 2 , t 2 : Γ Ñ Σ J 2 satisfying the globular relations s 1 s 2 " s 1 t 2 and t 1 s 2 " t 1 t 2 . Two 2-cells f and g in Σ J

tst 2 βt $ D stst αt 9 Y
2 are equal with respect to Γ , and we denote f " Γ g, if f and g are equal in the quotient 2-category Σ J 2 {Γ of the 2-category Σ J 2 by the congruence on 2-cells generated by Γ .

Relations between rewriting sequences can be described using the notion of extended presentation. Recall from [START_REF] Guiraud | Higher-dimensional normalisation strategies for acyclicity[END_REF] that a p3, 1q-polygraph is a pair pΣ, Σ 3 q made of a 2-polygraph Σ and a globular extension Σ 3 of the free p2, 1q-category Σ J 2 , that is a set together with two maps s 2 , t 2 : Σ 3 Ñ Σ J 2 satisfying the globular relations s 1 s 2 " s 1 t 2 and t 1 s 2 " t 1 t 2 . We will denote by Σ J 3 the free p3, 1q-category generated by the p3, 1q-polygraph pΣ, Σ 3 q. An extended presentation of a category C is a p3, 1q-polygraph whose underlying 2-polygraph is a presentation of C.

Coherent presentations.

A coherent presentation of a category C is an extended presentation pΣ, Σ 3 q, such that the globular extension Σ 3 is a homotopy basis of the p2, 1q-category Σ J 2 . That is, for every 2-sphere pf, gq of Σ J 2 , there exists a 3-cell from f to g in the free p3, 1q-category generated by the p3, 1q-polygraph pΣ 2 , Σ 3 q.

Rewriting loops

In this part, Σ denotes a 2-polygraph.

2.2.1. Equivalent loops. A 2-loop in the 2-category Σ 2 is a 2-cell f of Σ 2 such that s 1 pfq " t 1 pfq. Two 2-loops f and g in Σ 2 are equivalent if there exist a decomposition f " f 1 ‹ 1 . . . ‹ 1 f p ,
where f i is a rewriting step of Σ for any 1 ď i ď p, and a circular permutation σ such that g " f σp1q ‹ 1 . . . ‹ 1 f σppq . This defines an equivalence relation on 2-cells of Σ 2 . We will denote by Lpfq the equivalence class of a 2-loop f in Σ 2 for this relation.

Lemma.

For any equivalent 2-loops f and g in Σ 2 , there exist 2-cells h and k of Σ J 2 such that f " h ‹ 1 g ‹ 1 k.

Proof. Let us decompose f into a sequence f " f 1 ‹ 1 . . . ‹ 1 f p of rewriting steps and let σ be a circular permutation such that g " f σp1q ‹ 1 . . . ‹ 1 f σppq . Let i be the integer such that σpiq " 1. Let k be the 2-cell f σp1q ‹ 1 . . . ‹ 1 f σpi´1q . Let h " k ´be the inverse of k for the 1-composition. Then, we have f " h ‹ 1 g ‹ 1 k.

Minimal and elementary loops. We say that a

2-loop f in Σ 2 is i) minimal with respect to 1-composition, if any decomposition f " g ‹ 1 h ‹ 1 k in Σ 2 with h a 2-loop
implies that h is either an identity or equal to f, ii) minimal by context, if there is no decomposition f " ugv, where u and v are nonidentity 1-cells in Σ 1 and g is a loop in Σ 2 .

A 2-loop f in Σ 2 is elementary if it is minimal both with respect to 1-composition and by context. As an immediate consequence of these definitions, any 2-loop f minimal for 1-composition can be written f " ugv, where g is an elementary loop and u, v are 1-cells in Σ 1 .

Lemma.

Let f be a nonidentity 2-loop in Σ 2 . Then, there exists a decomposition f "

f 1 ‹ 1 f 1 ‹ 1 f 2 in Σ 2 , where f 1 is a 2-loop minimal with respect to 1-composition and f 1 , f 2 are 2-cells such that f 1 ‹ 1 f 2 is a 2-loop.

Labelled polygraphs

Proof. Let f be a nonidentity 2-loop in Σ 2 . The proof is by induction on the support Supppfq. If the 2-loop f is minimal for 1-composition, we can write f " 1 s 1 pfq ‹ 1 f ‹ 1 1 s 1 pfq . If f is not minimal for 1composition, there exists a decomposition f " g ‹ 1 h ‹ 1 k, where h is a 2-loop that is neither an identity nor equal to f. Hence, Suppphq is strictly included in Supppfq that proves the decomposition.

2.2.5. Globular extensions of loops. We will denote by EpΣq the set of equivalence classes of elementary 2-loops of Σ 2 . A loop extension of Σ is a globular extension of the p2, 1q-category Σ J 2 made of a family of 3-cells A α : α 1 s 1 pαq indexed by exactly one α for each equivalence class in EpΣq.

2.2.6. Lemma. Let LpΣq be a loop extension of Σ. For any 2-loop f in Σ 2 , there exists a 3-cell from f to 1 s 1 pfq in the free p3, 1q-category LpΣq J generated by the p3, 1q-polygraph pΣ, LpΣqq.

Proof. Let us fix a loop extension LpΣq. Let f be 2-loop in Σ 2 . We proceed by induction on the support Supppfq.

Step 1. Suppose that f is elementary. By definition of LpΣq, the equivalence class Lpfq contains an elementary 2-loop e such that LpΣq contains a 3-cell A e from e to 1 s 1 peq . The 2-loop e being equivalent to f, by Lemma 2.2.2 there exist two 2-cells h and

k of Σ J 2 such that f " h ‹ 1 e ‹ 1 k. Thus, the 3-cell h ‹ 1 A e ‹ 1 k in LpΣq J goes from f to h ‹ 1 k. By construction the 2-cell h ‹ 1 k is equal 1 s 1 pfq .
In this way we construct a 3-cell in LpΣq J from f to 1 s 1 pfq .

Step 2. Suppose that f is minimal with respect to 1-composition. Then, there is a decomposition f " ugv, where u and v are 1-cells in Σ 1 and g is an elementary 2-loop in Σ 2 . By Step 1, there exists a 3-cell A g from g to 1 s 1 pgq in LpΣq J . Thus uA g v is a 3-cell in LpΣq J from f to 1 s 1 pfq .

Step 3. Suppose that f is a nonidentity 2-loop. By Lemma 2.2.4, the 2-loop f can be written as

f 1 ‹ 1 f 1 ‹ 1 f 2
where f 1 is a 2-loop minimal for 1-composition and f 1 and f 2 are 2-cells such that f 1 ‹ 1 f 2 is a 2-loop. By Step 2, there exists a 3-cell A f 1 in LpΣq J from f 1 to 1 s 1 pf 1 q . Hence, the

1-composite f 1 ‹ 1 A f 1 ‹ 1 f 2 is a 3-cell from f to f 1 ‹ 1 f 2 in LpΣq J .
The support of f 1 ‹ 1 f 2 being strictly included in the support of f, this proves the lemma by induction on the support of f.

Labelled polygraphs

2.3.1. Labelled 2-polygraphs. A well-founded labelled 2-polygraph is a data pΣ, W, ă, ψq made of a 2-polygraph Σ, a set W, a well-founded order ă on W and a map ψ : Σ stp ÝÑ W. The map ψ is called a well-founded labelling of Σ and associates to a rewriting step f a label ψpfq.

Given a rewriting sequence f " f 1 ¨. . . ¨fk , we denote by L W pfq " tψpf 1 q, . . . , ψpf k qu the set of labels of rewriting steps in f. Note that two distinct rewriting sequences f and g can correspond to a same 2-cell in the free 2-category Σ 2 despite L W pfq and L W pgq being distinct.

2.3.2.

Labelling to the quasi-normal form. Consider a quasi-convergent 2-polygraph Σ. By quasitermination, any 1-cell u admits a quasi-normal form, not unique in general. For every 1-cell u in Σ 1 , let us fix a quasi-normal form r u. Note that by confluence hypothesis, any two congruent 1-cells of Σ 1 have the same quasi-normal form. This defines a quasi-normal form map s : Σ 1 Ñ Σ 1 sending a 1-cell u on r u. The labelling to the quasi-normal form, labelling QNF for short, associates to the map s the labelling ψ QNF : Σ stp ÝÑ N defined by ψ QNF pfq " dpt 1 pfq, Ć t 1 pfqq,

Decreasing polygraphs

for any rewriting step f of Σ.

2.3.3. Lexicographic maximum measure, [START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams[END_REF]Definition 3.1]. Let pΣ, W, ă, ψq be a well-founded labelled 2-polygraph. Let w " w 1 . . . w n and w 1 " w 1 1 . . . w 1 m be 1-cells in the free monoid W ˚with w i and w 1 j in W. We denote by w pw 1 q the 1-cell w 1 . . . w n such that for every 0 ď k ď n, the 1-cell w k is defined by with f " f 1 ¨. . . ¨fn and g " g 1 ¨. . . ¨gm and f i labelled by l i and g j labelled by k j .

w k " # 1 if w k ă w 1 j for some 1 ď j ď m, w k otherwise.

Decreasing two-dimensional polygraphs

f 7 W g Õ % f 1 Õ % g 2 Õ % h 1 Õ % g 1 7 W f 2 7 W h 2 7 W (resp. f 7 W g Õ % f 1 Õ % g 1 7 W
).

and such that the following properties hold

i) k ă ψpfq, for all k in L W pf 1 q, ii) k ă ψpgq, for all k in L W pg 1 q,
iii) f 2 is an identity or a rewriting step labelled by ψpfq, iv) g 2 is an identity or a rewriting step labelled by ψpgq,

v) k ă ψpfq or k ă ψpgq, for all k in L W ph 1 q Y L W ph 2 q.
Such a diagram is then called a decreasing confluence diagram (resp. strictly decreasing confluence diagram) of the branching pf, gq.

A 2-polygraph Σ is decreasing (resp. strictly decreasing) if there exists a well-founded labelling pW, ă, ψq of Σ making all its local branching decreasing (resp. strictly decreasing).

As in the case of abstract rewriting systems, [18, Corollary 3.9.], we prove that any decreasing 2polygraph is confluent.

Strictly decreasing branching.

We extend the notion of strict decreasingness on local branchings to branchings as follows. A branching pf, gq is strictly decreasing is there is a confluence diagram pf ¨f1 , g ¨g1 q such that the two following properties hold i) for each k 1 in L W pf 1 q, we have k 1 ă k for any k in L W pfq, ii) for each l 1 in L W pg 1 q, we have l 1 ă l for any l in L W pgq.

Decreasingness from quasi-termination.

Any quasi-convergent 2-polygraph Σ is strictly decreasing with respect to any quasi-normal form labelling ψ QNF . Indeed, for any local branching u ñ pv, wq there exists a quasi-normal form r u and a confluence pf 1 , g 1 q : pv, wq ñ r u. The rewriting sequences f 1 and g 1 can be chosen of minimal length, thus making this confluence diagram strictly decreasing with respect the labelling ψ QNF .

2.4.4. Decreasingness of Peiffer branchings. For a Peiffer branching pfv, ugq : uv ñ pu 1 v, uv 1 q of a 2-polygraph Σ, the confluence pu 1 g, fv 1 q : pu 1 v, uv 1 q ñ u 1 v 1 is called the Peiffer confluence of the branching pfv, ugq. In a decreasing 2-polygraph pΣ, ψq every Peiffer branching can be completed into a decreasing confluence diagram. However, the confluence diagram obtained with the Peiffer confluence is not always decreasing as in the case of the following example. This Peiffer diagram is not decreasing with respect to ψ QNF . Indeed, we have ψ QNF pαaq " ψ QNF paαq " 1 and ψ QNF pαbq " ψ QNF pbαq " 2. However, this Peiffer branching is decreasing by using the following confluence paβ, βaq : pab, baq ñ a 2 , since ψ QNF paβq " ψ QNF pβaq " 0.

2.4.6. Peiffer decreasingness. A decreasing (resp. strictly decreasing) 2-polygraph pΣ, ψq is Peiffer decreasing with respect to a globular extension Γ of the p2, 1q-category Σ J 2 if, for any Peiffer branching pfv, ugq : uv ñ pu 1 v, uv 1 q, there exists a decreasing (resp. strictly decreasing) confluence diagram pfv ¨f1 , ug ¨g1 q:

u 1 v u 1 g ( H f 1 @ uv fv 8 X ug 6 V u 1 v 1 u 2 uv 1 fv 1 H h g 1 U u such that u 1 g ‹ 1 pfv 1 q ´"Γ f 1 ‹ 1 pg 1 q
´.

2.4.7. Example. Any 2-polygraph Σ such that any non trivial local branching pf, gq is confluent using two rewriting steps f 1 : t 1 pfq ñ v and g 1 : t 1 pgq ñ v is Peiffer decreasing. Indeed, a labelling such that all rewriting steps have the same label makes any local branching pf, gq decreasing. Moreover, with such a labelling, any Peiffer confluence is decreasing. In particular, the 2-polygraph ΣpB 3 q is decreasing for a singleton labelling.

2.4.8. Compatibility with contexts. Let pΣ, ψq be a well-founded labelled 2-polygraph. The labelling ψ is compatible with contexts if for any decreasing (resp. strictly decreasing) confluence diagram pf ¨f1 , g ¨g1 q, where pf, gq is a local branching, and for any composable 1-cells u 1 and u 2 in Σ 1 , the following confluence diagram is decreasing (resp. strictly decreasing):

u 1 vu 2 u 1 f 1 u 2 0 P u 1 uu 2 u 1 fu 2 8 X u 1 gu 2 6 V u 1 u 1 u 2 u 1 wu 2 u 1 g 1 u 2 E e
Note that a labelling QNF is not compatible with contexts in general.

2.4.9. ‹ 0 -compatibility. A well-founded labelling pW, ψ, ăq is ‹ 0 -compatible if for any rewriting steps f and g such that ψpfq ă ψpgq, we have ψpu 1 fu 2 q ă ψpu 1 gu 2 q for any composable 1-cells u 1 and u 2 in Σ 1 . Note that the ‹ 0 -compatibility does not implies the compatibility with contexts. Indeed, if pf, gq is a local branching that can be completed into a diagram

b f 1 $ D a f 7 W g 8 X d c g 1 P p
2.4.12. Multiset order. Given a well-founded set of labels pW, ăq, we consider the partial order ă mul on the multisets over W defined in [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF][START_REF] Vincent Van Oostrom | Confluence by decreasing diagrams[END_REF] as follows. For any multisets M and N over W, we set M ă mul N if there exist multisets X, Y and Z such that:

i) M " Z Y X, N " Z Y Y and Y is not empty,
ii) for every i in W such that Xpiq ‰ 0, there exists j in W such that Ypjq ‰ 0 and i ă j.

The order ă mul is well-founded because ă is. We call ď mul the symmetric closure of ă mul .

Let us mention a particular case of [18, Lemma 3.6.], that will be used in the proof of our main result.

2.4.13. Lemma. Let Σ be a decreasing 2-polygraph. For every diagram in Σ 2 of the following form

f 1 1 ! A f 2 ' G f 1 6 V g 1 8 X g 1 1 R r
where f 1 is a non empty rewriting sequences, f 2 and g 1 are rewriting sequence and the confluence diagram pf 1 ¨f1 1 , g 1 ¨g1 1 q is strictly decreasing, the inequality |pf 1 1 , f 2 q| ă mul |pg 1 , f 1 ¨f2 q| holds.

2.4.14. Proposition. Let pΣ, ψq be a well-founded labelled 2-polygraph. Then Σ is strictly decreasing if and only if any branching of Σ is strictly decreasing.

Proof. One implication is obvious. Let us assume that Σ is strictly decreasing and let pf, gq be a branching of Σ. We prove by induction on |pf, gq| that pf, gq is strictly decreasing. If f or g is an empty rewriting sequence, the strict decreasingness of pf, gq is trivial. Else, we can write

f 1 2 R f 2 $ D f 1 B b g 1 2 R g 2 P p g 1 2 R
such that the confluence diagram pf 1 ¨f2 , g 1 ¨g2 q is strictly decreasing. By Lemma 2.4.13, we have |pf 1 , f 2 q| ă mul |pf 1 , gq|. Thus, we have |pf 1 , f 2 q| ă mul |pf, gq| and we can use the induction hypothesis to construct a strictly decreasing confluence diagram pf 1 ¨k1 , f 2 ¨k2 q. By using again Lemma 2.4.13, we have |pg 2 ¨k2 , g 1 q| ă mul |pf, gq|. Thus, by applying again the induction hypothesis, we have a diagram

f 1 2 R f 2 $ D k 1 4 f 1 B b g 1 2 R k 2 7 W l 1 Ñ ! g 2 P p g 1 2 R l 2 B b
where the diagram pf ¨k1 ¨l1 , g ¨l2 q is strictly decreasing.

COHERENCE BY DECREASINGNESS

In this section, we extend to decreasing 2-polygraphs the notion of Squier's completion known for convergent 2-polygraphs. We give sufficient conditions on the labelling of a decreasing 2-polygraph making the Squier's decreasing completion a coherent presentation. In particular, we show how to extend a quasi-convergent 2-polygraph into a coherent presentation.

Squier's decreasing completion

Squier's completion provides a way to extend a convergent 2-polygraph into a coherent presentation, see [START_REF] Guiraud | Polygraphs of finite derivation type[END_REF][START_REF] Squier | A finiteness condition for rewriting systems[END_REF].

Squier's completion.

A family of generating confluences of a 2-polygraph Σ is a globular extension of the p2, 1q-category Σ J 2 that contains exactly one 3-cell of the following form

v f 1 & F u f 6 V g 7 W u 1 w g 1 I i Õ %
for each critical branching pf, gq of Σ. If Σ is confluent, it always admits such a family A Squier's completion of a convergent 2-polygraph Σ is a p3, 1q-polygraph that extends Σ by a chosen family of generating confluences. Any Squier's completion of a convergent 2-polygraph Σ is a coherent presentation of the category presented by Σ, [START_REF] Squier | A finiteness condition for rewriting systems[END_REF], see also [START_REF] Guiraud | Polygraphs of finite derivation type[END_REF].

3.1.2. Generating decreasing confluences. Let pΣ, ψq be a decreasing 2-polygraph. A family of generating decreasing confluences of Σ with respect to ψ is a globular extension of the p2, 1q-category Σ J 2 that contains, for every critical branching pf, gq : u ñ pv, wq of Σ, exactly one 3-cell D ψ f,g of the following form

v f 1 & F u f 6 V g 7 W u 1 w g 1 I i D ψ f,g Õ %
and where the confluence diagram pf ¨f1 , g ¨g1 q is decreasing with respect to ψ. Any decreasing 2polygraph admits such a family of generating decreasing confluences. Indeed, any critical branching is local and thus confluent by decreasingness hypothesis. However, note that such a family is not unique in general.

For a strictly decreasing 2-polygraph Σ, we define in the same way a family of generating strictly decreasing confluences of Σ, but where the confluence diagrams are strictly decreasing with respect to ψ. where OpΣ, ψq is a chosen family of generating decreasing confluences with respect to ψ and LpΣq is a loop extension of Σ defined in 2.2.5. If pΣ, ψq is a strictly decreasing 2-polygraph, a strictly decreasing Squier's completion is a Squier's decreasing completion, whose the generating decreasing confluences are required strict.

3.1.4. Lemma. Let pΣ, ψq be a strictly decreasing 2-polygraph. Let S sd pΣ, ψq be a strictly decreasing Squier's completion of Σ. Suppose that ψ is compatible with contexts and that pΣ, ψq is Peiffer decreasing with respect to the extension S sd pΣ, ψq. Then, for any 2-sphere pf, gq in Σ 2 , there exists a 3-cell from f to g in the p3, 1q-category S sd pΣ, ψq J .

Proof. We proceed in two steps.

Step 1. We prove that, for every local branching pf, gq : u ñ pv, wq of Σ, there exists a confluence pf 1 , g 1 q : pv, wq ñ u 1 of Σ and a 3-cell A : f ‹ 1 f 1 g ‹ 1 g 1 in S sd pΣ, ψq J such that the confluence diagram pf ¨f1 , g ¨g1 q is strictly decreasing.

In the case of an aspherical branching, we can choose f 1 and g 1 to be identity 2-cells, A to be an identity 3-cell and the confluence diagram pf, fq is trivially strictly decreasing.

Suppose that pf, gq is a Peiffer branching

pf 1 v 1 , u 1 g 1 q : u 1 v 1 ñ pu 1 1 v 1 , u 1 v 1 1 q. By hypothesis, the Peiffer confluence pf 1 v 1 ¨u1 1 g 1 , u 1 g 1 ¨f1 v 1 1 q is equivalent to a strictly decreasing confluence diagram pf 1 v 1 ¨f1 1 , u 1 g 1 ¨g1 1 q.
Hence, there exists a 3-cell A :

f 1 v 1 ‹ 1 f 1 1 u 1 g 1 ‹ 1 g 1 1 in the p3, 1q-category S sd pΣ, ψq J .
If pf, gq is an overlapping branching, we have pf, gq " pwhw 1 , wkw 1 q with ph, kq a critical branching. We consider the 3-cell D ψ h,k : h ‹ 1 h 1 k ‹ 1 k 1 of OpΣ, ψq corresponding to the strict generating decreasing confluence of the critical branching ph, kq with respect to the labelling ψ, or its inverse. Let us define the 2-cells f 1 " wh 1 w 1 and g 1 " wk 1 w 1 and the 3-cell A " wD ψ h,k w 1 . The labelling ψ being compatible with contexts, the confluence diagram corresponding to the 3-cell A is strictly decreasing.

Step 2. Let pf, gq be a 2-sphere in Σ 2 . This 2-sphere defines a branching with source s 1 pfq " s 1 pgq. The 2-polygraph Σ being strictly decreasing, we prove the lemma by well-founded induction on the measure 3.1. Squier's decreasing completion |pf, gq| of the branching pf, gq. If f or g is an identity 2-cell, say g " 1, the 2-cell f is a 2-loop. By Lemma 2.2.6, there exists a 3-cell E : f 1 s 1 pfq in the p3, 1q-category LpΣq J . Else, we have decompositions f " f 1 ‹ 1 f 2 and g " g 1 ‹ 1 g 2 in Σ 2 where pf 1 , g 1 q is a local branching. Note that f 2 or g 2 can be equal to an identity 2-cell. The local branching pf 1 , g 1 q is confluent by decreasingness. Moreover, by Step 1, there exists a 3-cell A :

f 1 ‹ 1 f 1 1 g 1 ‹ 1 g 1
1 in the p3, 1q-category S sd pΣ, ψq J , where the confluence diagram pf 1 ¨f1 1 , g 1 ¨g1 1 q is strictly decreasing. The branchings pf 1 1 , f 2 q is confluent by decreasingness. Moreover, the 2-polygraph Σ being strictly decreasing, by Lemma 2.4.14, there exist rewriting sequences h and k as indicated in the following diagram:

u 1 f 1 1 ' G f 2 # C A Õ % u f 1 9 Y g 1 5 U u 1 h 7 W p u k e y v 1 g 1 1 G g g 2 Q q B x C 7
such that the confluence diagrams pf 1 1 ¨h, f 2 ¨kq is strictly decreasing. Consider the multiset order ă mul associated to the order ă. The confluence diagram pf 1 ¨f1 1 , g 1 ¨g1 1 q being strictly decreasing, for any k in L W pf 1 1 q and any l in L W pg 1 1 q, we have k ă ψpf 1 q and l ă ψpg 1 q.

Thus |f 1 ¨f1 1 | " |f 1 | and |g 1 ¨g1 1 | " |g 1 |.
This implies the following equality |pf 1 , g 1 q| " |pf, gq|.

The confluence diagram pf 1 1 ¨h, f 2 ¨kq being strictly decreasing, by the same argument, we have

|pf 1 1 ¨h, f 2 ¨kq| " |pf 1 1 , f 2 q|.
Moreover, by Lemma 2.4.13, we have |pf 1 1 , f 2 q| ă mul |pf, g 1 q|. It follows that

|pf 1 1 ¨h, f 2 ¨kq| ă mul |pf, gq|.
By induction hypothesis, we deduce that there exists a 3-cell B :

f 2 ‹ 1 k f 1 1 ‹ 1 h in S sd
pΣ, ψq J . Finally, let us prove that there exists a 3-cell C :

g 1 1 ‹ 1 h g 2 ‹ 1 k in S sd pΣ, ψq J . We have |pg 1 1 ¨h, g 2 ¨kq| " |g 1 1 | Y |h pg 1 1 q | Y |g 2 | Y |k pg 2 q |.
On the other hand, we have

|pf, gq| " |f| Y |g| " |f| Y |g 1 | Y |g pg 1 q 2 |.
Furthermore, there exists a multiset R, possibly empty, such that |g 2 | " |g

pg 1 q 2 | Y R. Hence |pg 1 1 ¨h, g 2 ¨kq| " |g pg 1 q 2 | Y X and |pf, gq| " |g pg 1 q 2 | Y Y.
where

X " |g 1 1 | Y |h pg 1 1 q | Y R Y |k pg 2 q | and Y " |f| Y |g 1 |.
Moreover, we check that for every i in W such that Xpiq ‰ 0, there exists j in W such that Ypjq ‰ 0 and i ă j. Hence, we have |pg 1 1 ¨h, g 2 ¨kq| ă mul |pf, gq|. The existence of the 3-cell C follows by induction hypothesis. In this way, we have constructed a 3-cell in S sd pΣ, ψq J from f to g obtained by composition of the 3-cells A, B and C.

3.1.5. Example. The 2-polygraph ΣpB 3 q given in 2.1.9 is strictly decreasing for the labelling QNF ψ QNF defined in 2.4.11. It has four confluent critical branchings. Thus, a strictly decreasing Squier's completion of the 2-polygraph ΣpB 3 q is given by the following 3-cells: tst 2 βt

% E stst αt
H h D ψ QNF βst,tsβ Õ % tst β $ D sts α 9 Y 1 sts B b sts E α,β Õ %
where D ψ QNF tα,βs , D ψ QNF βs,tα , D ψ QNF αts,stα and D ψ QNF βst,tsα are the generating decreasing confluences and E α‹ 1 β is an elementary 2-loop of Σ. Each of these confluences is decreasing because: ψ QNF pαtq " ψ QNF psβq " 1 and ψ QNF pβtq " ψ QNF psαq " 0, ψ QNF pβsq " 0, ψ QNF ptαq " 2 and ψ QNF ptβq " 1, ψ QNF pβsq " 0, ψ QNF pαtsq " ψ QNF pstαq " 1 and ψ QNF pβtsq " ψ QNF pstβq " 0, ψ QNF pβstq " 0, ψ QNF ptsβq " 2 and ψ QNF ptsαq " 1, ψ QNF pβstq " 0.

Coherence by decreasingness

The following theorem is the main result of this article.

3.2.1. Theorem. Let pΣ, ψq be a strictly decreasing 2-polygraph. Let S sd pΣ, ψq be a strictly decreasing Squier's completion of Σ. If ψ is compatible with contexts and pΣ, ψq is Peiffer decreasing with respect to the extension S sd pΣ, ψq, then S sd pΣ, ψq is a coherent presentation of the category presented by Σ.

Proof. Let pf, gq be a 2-sphere of the p2, 1q-category Σ J 2 . By definition of Σ J 2 , the 2-cell f ‹ 1 g ´can be decomposed into a zigzag where the 2-cells f 0 , . . . , f k and g 0 , . . . , g l are 2-cells of the 2-category Σ 2 . Note that some of those 2-cells can be identities. By confluence of the 2-polygraph Σ, there exist families of 2-spheres of

Σ 2 f 1 i 9 f i 6 V f i´1 8 X f 1 i´1 T t g 1 j 9 g j 6 V g j´1 8 X g 1 j´1 T t f 1 1 9 f 0 6 V g 0 8 X g 1 1 T t f 1 k´1 9 f k 6 V g l 8 X g 1 l´1 T t
with same 1-target, for all 2 ď i ď k ´1 and 2 ď j ď l ´1. Note that some of these 2-spheres can be trivial. Then the 2-sphere pf, gq can be filled up by these 2-spheres as follows:

f 1 1 3 S f 1 e y f 2 7 W ¨¨f 1 2 % E f 1 k´2 q Õ f k´2 e y f k´1 7 W f 1 k´1 i } g 0 3 S f 0 A a g l i } f k u g 1 1 A a g 1 e y g 2 7 W ¨¨g 1 2 I i g 1 l´2 m g l´2 e y g l´1 7 W g 1 l´1 u
By Lemma 3.1.4, these 2-spheres can be filled up by 3-cells of the p3, 1q-category S sd pΣ, ψq J . Finally, the composition of these 3-cells gives a 3-cell of S sd pΣ, ψq J from f to g.

Strict decreasingness is a required condition in Theorem 3.2.1 as shown by the following example.

Example.

Consider the 2-polygraph Σ without 2-loop and containing two families pf i j q i,jPN,ij"0 and pg i j q i,jPN,ij"0 of 2-cells satisfying the following conditions:

i) the sequences pf 0 n q nPN , pf n 0 q nPN , pg 0 n q nPN and pg n 0 q nPN are infinite rewriting paths, ii) for any odd integer n, we have t 1 pf n 0 q " t 1 pg n 0 q and t 1 pf 0 n q " t 1 pg 0 n q, iii) for any even integer n, we have t 1 pf n 0 q " t 1 pf 0 n q and t 1 pg n 0 q " t 1 pg 0 n q, as indicated in the following diagram

f 0 0 6 V g 0 0 8 X } f 1 0 w g 1 0 f 2 0 7 W g 2 0 7 W z f 3 0 e g 3 0 ¨¨¨ 6 f 0 3 X x g 0 3 3 f 0 1 a g 0 1 f 0 2 e y g 0 2 e y
and such that the only critical branchings of Σ are of one of the following forms:

pf n 0 , g n 0 q, pf 0 n , g 0 n q, for n even, and pf 0 n , f n 0 q, pg 0 n , g n 0 q, for n odd. Let us consider the globular extension Γ of the free p2, 1q-polygraph Σ J 2 , defined by the following infinite family of 2-spheres:

pf n 0 ‹ 1 f n`1 0 , f 0 n ‹ 1 f 0 n`1 q and pg n 0 ‹ 1 g n`1 0
, g 0 n ‹ 1 g 0 n`1 q for n odd, and

pf n 0 ‹ 1 f n`1 0 , g n 0 ‹ 1 g n`1 0
q and pf 0 n ‹ 1 f 0 n`1 , g 0 n ‹ 1 g 0 n`1 q for n even. The globular extension Γ contains one generating confluence for each critical branching of Σ. However, we cannot define a 3-cell in the free p3, 1q-category generated by pΣ, Γ q with 2-source f 0 0 ‹ 1 f 0 1 and 2-target g 0 0 ‹ 1 g 0 1 . As a consequence, Γ does not form a homotopy basis of the p2, 1q-category Σ J 2 . In fact, we note that the 2-polygraph Σ is not strictly decreasing, because no labelling of Σ is well-founded, but decreasing with the singleton labelling.

Following 2.4.3, any quasi-convergent 2-polygraph Σ is strictly decreasing with respect to any quasinormal form labelling ψ QNF . The following result is a consequence of Theorem 3.2.1.

Corollary.

Let Σ be a quasi-convergent 2-polygraph and let ψ QNF be a quasi-normal form labelling of Σ. Let S sd pΣ, ψ QNF q be a strictly decreasing Squier's completion of Σ. If the labelling ψ QNF is compatible with contexts and pΣ, ψ QNF q is Peiffer decreasing with respect to the extension S sd pΣ, ψ QNF q, then S sd pΣ, ψ QNF q is a coherent presentation of the category presented by Σ.

3.2.4. Example. By Theorem 3.2.1, the five 3-cells given in 3.1.5 form a homotopy basis of the 2-polygraph ΣpB 3 q. Indeed, the 2-polygraph ΣpB 3 q is strictly decreasing for the labelling QNF defined in Example 2.4.11. This labelling being compatible with contexts, the only remaining point concerns the Peiffer confluences. Let us show that any Peiffer confluence is equivalent to a decreasing confluence diagram. Consider a Peiffer branching pfv, ugq : uv ñ pu 1 v, uv 1 q of ΣpB 3 q and its Peiffer confluence pu 1 g, fv 1 q : pu 1 v, uv 1 q ñ u 1 v 1 :

u 1 v u 1 g ( H uv fv 8 X ug 6 V u 1 v 1 uv 1 fv 1 H h
By definition of ΣpB 3 q, there exist rewriting steps f 1 : u 1 ñ u and g 1 : v 1 ñ v. It follows that this Peiffer confluence is equivalent with respect to LpΣpB 3 qq to each of the following Peiffer confluence:

pf 1 v 1 ¨ug 1 , u 1 g 1 ¨f1 vq, pu 1 g ¨f1 v 1 , f 1 v ¨ugq, pug 1 ¨fv, fv 1 ¨u1 g 1 q.
The equivalences are proved by the following diagrams:

uv 1 ug 1 8 fv 1 k u 1 v 1 f 1 v 1 B b u 1 g 1 1 Q uv ug f fv v u 1 v f 1 v V v u 1 g s u 1 v 1 f 1 v 1 # C u 1 v u 1 g B b f 1 v 4 T uv 1 fv 1 i uv ug R r fv u uv fv $ D ug i } uv 1 ug 1 @ fv 1 2 R u 1 v u 1 g t Ø u 1 v 1 u 1 g 1 S s

Finiteness homotopical and homological conditions by decreasingness

Finally, in each family of such four Peiffer confluences, one of them is decreasing with respect to the labelling ψ QNF .

3.2.5. Decreasingness from termination. Given a confluent and terminating 2-polygraph Σ, any 1-cell u of Σ 1 has a unique normal form denoted by p u. We define the labelling to the normal form ψ NF : Σ stp Ñ Σ 1 by setting for each rewriting step f, ψ NF pfq " t 1 pfq. We choose on Σ 1 the order induced by the rewrite relation defined by Σ 2 . This labelling is compatible with contexts and makes the 2-polygraph Σ strictly decreasing and Peiffer decreasing. Moreover, Σ being terminating it does not have loop and in particular the decreasing Squier completion coincides with the Squier completion. In this way, the Squier coherence theorem obtained for convergent string rewriting systems in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] is a consequence of Theorem 3.2.1: 3.2.6. Corollary ([17, Theorem 5.2]). Let Σ be a convergent 2-polygraph. Any Squier's completion SpΣq of Σ is a coherent presentation of the category presented by Σ.

3.3. Finiteness homotopical and homological conditions by decreasingness 3.3.1. Finite derivation type. A 2-polygraph Σ has finite derivation type, FDT for short, if the free p2, 1q-category Σ J 2 has a finite homotopy basis, see [START_REF] Guiraud | Polygraphs of finite derivation type[END_REF]Section 4]. Squier proved that this property is invariant for finite string rewriting systems: if Σ and Υ are two finite 2-polygraphs, then Σ has FDT if and only if Υ has FDT. As a consequence, the property can be defined on finitely presented monoids: a finitely presented monoid has FDT if it has a presentation by a 2-polygraph that has FDT.

For a convergent 2-polygraph Σ, its is well known that a family of generating confluences forms a homotopy basis of Σ J 2 . A finite convergent 2-polygraph having a finite number of critical branchings, then it has FDT. However, a finite decreasing 2-polygraph can have an infinite decreasing Squier's completion. Indeed, the set of decreasing confluences is always finite for a finite 2-polygraph but the set of elementary 2-loops may be infinite. As a consequence of Theorem 3.2.1 we can formulate the following result.

3.3.2. Proposition. Let pΣ, ψq be a strictly decreasing and quasi-convergent 2-polygraph such that the labelling ψ is compatible with contexts and Peiffer decreasing. If Σ has a finite set of 2-cells and a finite set of elementary 2-loops, then it has finite derivation type. In particular, by Theorem 3.2.1, if pΣ, ψq is a strictly decreasing 2-polygraph such that ψ is compatible with contexts and Peiffer decreasing, the coherent presentation given by the strictly decreasing Squier completion S sd pΣ, ψq induces such a partial resolution. If moreover Σ has a finite set of 2-cells and a finite set of elementary 2-loops, then it has finite homological type FP 3 . We expect that our construction can be extended in higher-dimension of homology producing infinite lenght resolutions for monoids presented by quasi-convergent presentations, and thus weakening the termination hypothesis required in construction of such resolutions as in [START_REF] Anick | On the homology of associative algebras[END_REF][START_REF] Kobayashi | Complete rewriting systems and homology of monoid algebras[END_REF]. We deduce the homology of the monoid B 3 with integral coefficients: H n pM, Zq " Z for n ď 2 and H n pM, Zq " 0, for n ě 3.

10 .

 10 Extended presentations. Let Σ be a 2-polygraph. A globular extension of the p2, 1q-category Σ J 2

Following [ 18 ,

 18 Definition 3.1], we consider the measure | ¨| from the free monoid W ˚to the set of multisets over W and defined as follows: i) for every i in W, the multiset |i| is the singleton tiu, ii) for every i in W and every 1-cell w in W ˚, we have |iw| " |i| Y |w piq |. The measure | ¨| is extended to the set of finite rewriting sequences of Σ by setting, for every rewriting sequence f 1 ¨. . . ¨fn , with f i labelled by k i for all i, |f 1 ¨. . . ¨fn | " |k 1 . . . k n |, were k 1 . . . k n is a product in the monoid W ˚. Finally, the measure | ¨| is extended to the set of finite branchings pf, gq of Σ, by setting |pf, gq| " |f| Y |g|. Recall from [18, Lemma 3.2], that for every 1-cells w 1 , w 2 in W ˚, we have |w 1 w 2 | " |w 1 |Y|w pw 1 q 2 |. As a consequence, for any rewriting sequences f and g of Σ the following relation holds |f ¨g| " |f| Y |g pfq |, where |g pfq | is defined by |g pfq | " |k 1 . . . k pl 1 ...lnq m |,

2. 4 . 5 .

 45 Example. As shown in 2.4.3, a labelling QNF makes every Peiffer branching decreasing. But, it does not necessarily makes the Peiffer confluences decreasing. In particular, it is not the case when the source uv of the Peiffer confluence is already the chosen quasi-normal form. For instance, consider the quasi-convergent 2-polygraph Σ " xa, b ˇˇα : a ñ b, β : b ñ ay. For each 1-cel u of Σ 1 , we set r u " a puq as a quasi-normal form. Let us now consider the following Peiffer diagram:

3. 1 . 3 .

 13 Squier's decreasing completion. Let pΣ, ψq be a decreasing 2-polygraph. A Squier's decreasing completion of Σ with respect to ψ is a p3, 1q-polygraph that extends the 2-polygraph Σ by a globular extension OpΣ, ψq Y LpΣq

3. 3 . 3 .

 33 Example. Let us consider the 2-polygraph Σ with only one 0-cell, Σ 1 " ta, b, c, d, d 1 u and Σ 2 " tab ñ a, ac ñ da, da ñ d 1 a, d 1 a ñ acu. This 2-polygraph presents a monoid which has not FDT, see[START_REF] Lafont | A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier)[END_REF] Section 5]. Moreover, it has only one elementary 2-loop up to equivalence and a finite number of critical branchings. As a consequence, there is no well-founded labelling compatible with contexts making the 2-polygraph Σ strictly decreasing and Peiffer decreasing.

3. 3 . 4 .

 34 Finite homological type FP 3 by decreasingness. As a final remark, let us mention another application to computation of low-dimensional homological properties of monoids. Let M be a monoid and Σ be a coherent presentation of M. Following [7, Proposition 5.3.2.], there is a partial resolutionZMrΣ 3 s d 3 / / ZMrΣ 2 s d 2 / / ZMrΣ 1 s d 1 / / ZM ε / / Z ÝÑ0 of left-modules over the free ring ZM over M, where Z denotes the trivial ZM-module and ZMrΣ i s denotes the free ZM-module generated by Σ i . The morphisms of ZM-modules are defined by εpuq " 1, for any u in M, and d 1 , d 2 and d 3 are defined on the generators by d 1 pxq " x ´1, d 2 pαq " rs 1 pαqs ´rt 1 pαqs, d 3 pAq " rs 2 pAqs ´rt 2 pAqs, for any x in Σ 1 , α in Σ 2 and A in Σ 3 , and with the bracket notations of [7, Section 5].

3. 3 . 5 .

 35 Example. Following Example 3.2.4, the monoid B 3 , admits a coherent presentation with two 1-cells s and t, two 2-cells α : sts ñ tst and β : tst ñ sts and the five 3-cells D ψ QNF tα,βs , D ψ QNF βs,tα , D ψ QNF αts,stα , D ψ QNF βst,tsβ , E α,β . Using the homotopical reduction procedure introduced in [4, 2.3.1.] with a collapsible part made of the 3-cell E α,β , we can reduce this coherent presentation to a coherent presentation of the monoid B 3 with the same k-cells for k ď 2 and with no 3-cells. Hence, we obtain the following resolution 0 ÝÑ ZMrα, βs d 2 / / ZMrs, ts d 1 / / ZM ε / / Z ÝÑ 0.

where f 1 and g 1 are rewriting steps such that ψpfq " ψpf 1 q and ψpgq " ψpg 1 q, then the confluence diagram is decreasing. Even, if the labelling pW, ψ, ăq is ‹ 0 -compatible, we do not necessarily have ψpufvq " ψpuf 1 vq and ψpugvq " ψpug 1 vq for any 1-cells u and v. Thus, the following diagram is not decreasing in general:

If ψ is a ‹ 0 -compatible labelling, for any strictly decreasing diagram pf ¨f1 , g ¨g1 q, where pf, gq is a local branching, we have ψ QNF pu 1 f 1 u 2 q ă ψ QNF pu 1 fu 2 q and ψ QNF pu 1 g 1 u 2 q ă ψ QNF pu 1 gu 2 q for every composable 1-cells u 1 and u 2 . As a consequence, any ‹ 0 -compatible labelling on a strictly decreasing 2-polygraph is compatible with contexts.

2.4.10. Example. Consider the 2-polygraph Σ defined in 2.4.5. The labelling QNF defined using the quasi-normal forms of the form r u " a puq is compatible with contexts. This is a consequence of the following equality ψ QNF pu 1 fu 2 q " dpu 1 , a pu 1 q q `ψQNF pfq `dpu 2 , a pu 2 q q for any rewriting step f and 1-cells u 1 and u 2 .

If we consider an other labelling QNF of the 2-polygraph Σ associated to quasi-normal forms of the form r u " a puq for any 1-cell u such that puq ‰ 3 and r u " b 3 for any 1-cell u such that puq " 3. Then the confluence diagram paα ¨aβ, αa ¨βaq is decreasing with ψ QNF paαq " ψ QNF pαaq " 1 and ψ QNF paβq " ψ QNF pβaq " 0. However, the confluence diagram pbaα ¨baβ, bαa ¨bβaq is not decreasing with ψ QNF pbaαq " ψ QNF pbαaq " 1 and ψ QNF pbaβq " ψ QNF pbβaq " 2. As a consequence this labelling QNF is not compatible with contexts.

2.4.11. Example. Consider the 2-polygraph ΣpB 3 q given in 2.1.9. We define a QNF labelling ψ QNF on ΣpB 3 q by associating to each 1-cell u of ΣpB 3 q 1 the quasi-normal form r u defined as follows. Setting N u " maxtn | u " pstsq n v holds in B 3 u, we define r u " pstsq Nu v. The maximality of N u ensures the unicity of such a quasi-normal form. Indeed, let us consider the following convergent presentation of the monoid B 3 : Υ " @ s, t, a ˇˇsts ñ a, tst ñ a, sa ñ at, ta ñ as D .

Suppose that a 1-cell u of ΣpB 3 q 1 has two distinct quasi-normal forms pstsq Nu v and pstsq Nu w. Those two 1-cells have respectively a Nu v and a Nu w as normal forms with respect to Υ 2 . Indeed, there is no occurrence of a in v and w, and the 1-cells sts and tst cannot divide v and w by maximality of N u . By unicity of the normal forms in a convergent 2-polygraph, the 1-cells a Nu v and a Nu w are not equal in the monoid B 3 , hence they are not the normal forms of a same 1-cell in Υ 1 . Thus, the 1-cells pstsq Nu v and pstsq Nu w are not the quasi-normal forms of a same 1-cell in ΣpB 3 q 1 , which contradicts our assumption. The labelling defined in this way is ‹ 0 -compatible. Indeed, for any rewriting steps f and g of ΣpB 3 q such that ψ QNF pgq ă ψ QNF pfq and for any composable 1-cells u 1 and u 2 , we have ψ QNF pu 1 fu 2 q ă ψ QNF pu 1 gu 2 q. Hence, the labelling ψ QNF is compatible with contexts.