Coherent Confluence inModal n-Kleene Algebras
Cameron Calk
Laboratoire de l’École Polytechnique (LIX), Paris, France
cameron.calk@inria.fr
Abstract
This work concerns the algebraic formalisation of coherence and confluence. The Church-Rosser
theorem states that the confluence of branchings and the confluence of zig-zags are equivalent properties.
On the one hand, the coherent version of this theorem has been formulated in the language of higher
dimensional globular categories. On the other hand, the Church-Rosser theorem has also beenformulated using the structure of modal Kleene algebra. This work provides an algebraic formulationof the coherent Church-Rosser theorem. To this end, we introduce the structure of n-dimensional
modal Kleene algebra satisfying globularity properties, providing a higher dimensional generalisationof modal Kleene algebra. In this setting, we give abstract definitions of coherent rewriting properties
and, via modal operators, present novel proofs of the Church-Rosser theorem with higher-dimensional
witnesses.

1

Introduction

In rewriting theory, a central theme is that of completing certain branching shapes, i.e. (local) branchingsor zig-zags, with confluences, thus obtaining confluence diagrams. This is classically described withrelations, but has more recently been formulated in the higher dimensional setting of polygraphs [2, 5].
While this approach is adapted to the study of string rewriting systems, it also provides a natural setting forthe study of coherence [5] in abstract rewriting systems. Furthermore, a point-free algebraic formalisationof confluence is given in [7]. This abstracts the relational approach to the setting of Kleene algebras,
providing a more general framework for the study of confluence. In this work, we combine these
two approaches by introducing the structure of n-Kleene algebra, a natural setting for abstract, higher
dimensional confluence proofs, and illustrate its use with the example of the Church-Rosser theorem.
In the relational setting, confluence is characterised, for an abstract rewriting system →, i.e. a binary
relation on some set, by the inclusion
∗∗

∗

∗

← · → ⊆ → · ←,where → denotes the reflexive, transitive closure of →, ← denotes its converse and · denotes relationalcomposition. The Church-Rosser property is characterised by the inclusion∗∗∗∗↔ ⊆ → · ←,where ↔ = (← ∪ →) is the symmetric, reflexive, transitive closure of →. The Church-Rosser theorem,
which states that these two properties are equivalent, can be formulated with similar expressions in Kleene
algebra using the star operation, an abstraction of the notion of reflexive, transitive closure, see Section 2.
The coherent formulation of this theorem takes place in the context of polygraphs. Roughly, it statesthat if there exists a set Γ of higher dimensional cells (with a globular shape) such that every branching canbe completed to a confluence diagram filled by some element of Γ , then every zig-zag may be completedwith a Church-Rosser diagram filled by a composition of elements in Γ , see [2]. In diagrams, thesestatements are respectively represented by:∗∗

Algebraic Coherent Confluence

u1w

Cameron Calk

uff0&

u1 og' αu0 x

gu2/ u2hf0

 β
u00~g0where α ∈ Γ and β is a composition of elements of Γ . This is a coherence result akin to e.g. Mac Lane’s
theorem for monoidal categories, since local data, i.e. existence of confluence diagrams, is constructively
used to prove a global result, i.e. existence of Church-Rosser diagrams.
In this abstract, we recall the structure of modal n-Kleene algebra from [2] and illustrate its use in thealgebraic formalisation of coherence results by formulating and giving a proof sketch of the coherent
Church-Rosser theorem. In Section 2 we provide background material, defining modal Kleene algebras
as in [3] and Γ -coherence properties, an extension of constructions from [4]. Next, we introduce thenovel structure of modal n-Kleene algebra and provide axioms for globularity in Section 3. Finally,in Section 4, we formalise the notion of coherence, state the Church-Rosser theorem in the setting ofn-Kleene algebras and give a short proof sketch.

2

Modal Kleene Algebras and Coherence

Modal Kleene Algebras, [3]. Recall that a dioid is a semiring (S, +, ·, 0, 1) in which addition isidempotent, i.e. for all x ∈ S, we have x + x = x. In this case, the natural partial order on S is defined byx ≤ y ⇔ x + y = y. A domain semiring is a dioid (S, +, ·, 0, 1) equipped with a domain operationd : S → S that satisfies, for all x, y ∈ S, the following axioms :x ≤ d(x)x (1)d(xy) = d(xd(y)) (2)d(x) ≤ 1(3)d(0) = 0(4)d(x + y) = d(x) + d(y) (5)where juxtaposition indicates multiplication. These axioms characterise domain in the case of relational
algebras. For a more detailed account, see [3]. In particular, they imply that Sd := d(S) forms a
distributive lattice with the induced operations + as join and · as meet, bounded by 0 and 1.
The opposite of a semiring S, in which the order of multiplication has been reversed, is denoted by
Sop . A codomain semiring is a semiring equipped with a map r : S → S such that (Sop , r) is a domain
semiring. A modal semiring is both a domain semiring and a codomain semiring, with additional axioms
d ◦ r = r and r ◦ d = d, which imply that Sd = Sr . We include these definitions for use in Section 3, in
which the term modal will be justified.
A (modal) Kleene algebra is a (modal) semiring K equipped with an operator (−)∗ : K → K called
Kleene star. It satisfies, for all x, y, z ∈ K, the unfold and induction axioms
1 + xx∗ ≤ x∗
1 + x∗ x ≤ x∗
(6)
z + xy ≤ y ⇒ x∗ z ≤ yz + yx ≤ y ⇒ zx∗ ≤ y(7)In a Kleene algebra K, the Church-Rosser theorem is expressed as follows: for elements x, y ∈ K, thefollowing are equivalent:x ∗ y∗ ≤ y∗ x ∗(x + y)∗ ≤ y∗ x∗(8)(x and y semi-commute)(x and y are Church-Rosser.)Γ -Coherence Properties. Recall that an n-polygraph P is a data consisting of sets (Pk )0≤k≤n andsource and target maps (sk , tk : Pk+1 → Pk∗ )0≤k<n satisfying globularity conditions, where Pk∗ is the2Algebraic Coherent Confluence

Cameron Calk∗
free k-category generated by the globular set (P0 , P1∗ , . . . , Pk−1, Pk ). A cellular extension of P is a set Γ>>and (globular) attaching maps sn , tn : Γ → Pn , where Pn is the free (n, n − 1)-category generated byP. See [5] for a more detailed account of polygraphs and their use in rewriting theory.
Given an n-polygraph P and a cellular extension Γ , we say that P is Γ -confluent (resp. Γ -Church∗ 2>
Rosser) if, for every branching (f, g) ∈ (Pn) of n-cells (resp. every zig-zag h ∈ Pn), there exist
00>
a confluence (f , g ) and a (n + 1)-cell α ∈ Γ (resp. α ∈ Pn (Γ ), the free (n + 1, n − 1)-category
generated by (P, Γ )) such thath/= vugf− 6 u' αu1−7 v1f0 " 0 αg0u
f 0 ' u 0 (g 0 )−−α : f− ?n−1 g → f 0 ?n−1 (g 0 )−(resp. α : f → f 0 ?n−1 g 0 ),where, for n-cells f1 , f2 of P, f1 ?n−1 f2 denotes their composition with respect to the (n−1)-dimensionaltarget (resp. source) of f1 (resp. f2 ). Readers familiar with polygraphic rewriting may notice thatthe filling cells are usually oriented from left to right, rather than from top to bottom. We choose thisorientation to better reflect the approach used in the setting of Kleene algebras, in which branching shapes,
such as x∗ y∗ and (x + y)∗ , are related to confluence shapes y∗ x∗ , as recalled in (8). This will equally be
the case in n-Kleene algebra, see Section 4.
The coherent Church-Rosser theorem [2] is formulated as follows: given P a n-polygraph, and Γ acellular extension of P, if P is Γ -confluent, then P is Γ -Church-Rosser.

3Higher Dimensional Modal Kleene Algebra

n-Dioids. For n ≥ 1, an n-dioid is a structure (S, +, 0, i , 1i )0≤i<n such that (S, +, 0, i , 1i ) is adioid for 0 ≤ i < n, the lax interchange change laws hold, and units are idempotent with respect to lower
dimensional multiplications, i.e.
(A00jA )i (B0j B ) ≤ (Ai B)

j (A00iB )and

1j0i 1j = 1j ,(9)opfor all A, A , B, B ∈ S and 0 ≤ i < j < n. The opposite n-semiring of S, denoted S , is that in which
the order of every multiplication operation has been reversed.
Globular n-Semirings with Domains. A domain n-semiring is an n-dioid (S, +, 0, i , 1i )0≤i<nequipped with n domain maps (di : S → S)0≤i<n , such that (S, +, 0, i , 1i , di ) is a domain semiringand di+1 ◦ di = di for all 0 ≤ i < n − 1. A n-semiring with codomains is equipped with maps
(ri : S → S)0≤i<n such that Sop is a domain n-semiring with respect to the (ri )0≤i<n .
A modal n-semiring is an n-semiring with domains and codomains, in which the coherence conditions
di ◦ ri = ri and ri ◦ di = di hold for all 0 ≤ i < n. Given S a modal n-semiring, we define forward andbackward i-diamond operators defined via (co-)domain operators in each dimension, as in [3]. For any
0 ≤ i < n, A ∈ S and φ ∈ Si , we define|Aii (φ) = di (Ai φ),andhA|i (φ) = ri (φi A).

(10)

These are modal operators on the distributive lattice Si in the sense of [6]. A modal semiring S is called
globular if the following globular relations hold for 0 ≤ i < j < n and A, B ∈ K:di ◦ dj = di and di ◦ rj = di ,(11)dj (A i B) = dj (A) i dj (B),(13)
ri ◦ dj = ri , and ri ◦ rj = ri ,(12)rj (Ai B) = rj (A)i rj (B).

Modal n-Kleene Algebra. A n-Kleene algebra is a n-semiring K equipped with maps (−)(14)∗i:K→K3

Algebraic Coherent Confluence

Cameron Calksuch that (K, +, 0, i , 1i , (−)∗i ) is a Kleene algebra for 0 ≤ i < n, and for 0 ≤ i < j < n, the Kleeneplus operator (−)+j , defined by A+j = A j A∗j , is a lax morphism with respect to the i-multiplicationof j-dimensional elements on the right (resp. left) in the sense that for all A ∈ K and φ ∈ Kj ,φ+j
≤ (φiAi A)+j,and(resp. A+ji φ ≤ (Ai φ)+j).

(15)

When the underlying semiring is globular and modal, we say that K is a globular modal n-Kleene algebra.
To provide a link to the polygraphic case, we remark that the power set of theset of n-cells in the free n-category generated by an n-polygraph P constitutes
a globular modal n-Kleene algebra K(P). Following this intuition, an element
A of a globular modal n-Kleene algebra will be represented with respect to its
i- and j-(co)domains as in the adjacent diagram.

4dj (A)⇓Adi (A)9$ri (A)rj (A)

Church-Rosser theorem

Let K be a globular modal n-Kleene algebra and 0 ≤ i < j < n. Given elements φ and ψ of Kj , we saythat A ∈ K is a i-confluence filler for (φ, ψ) if |Aij (ψ∗i i φ∗i ) ≥ φ∗i i ψ∗i .
In the modal n-Kleene algebra K(P) corresponding to a polygraph P, taking i = n − 2, j = n − 1,letting ψ be the set of (n − 1)-cells of P and letting φ be the set of their inverses, this signifies that A isa set of n-cells containing a filling cell for a confluence diagram corresponding to each branching of(n − 1)-cells.
4.1. Theorem (Coherent Church-Rosser in globular n-MKA). Let K be a globular modal n-Kleene
algebra. Given φ, ψ ∈ Kj , for 0 < j < n, for any i-confluence filler A ∈ K for (φ, ψ), we have^ ∗j ij (ψ∗i φ∗i ) ≥ (φ + ψ)∗i ,|A^ := (φ + ψ)∗i i A i (φ + ψ)∗i .
where A^ ∗j ij (ψ∗i φ∗i ) ≥ (φ + ψ)∗i signifies that the domain of A^ ∗j , when
Note that the expression |A∗i ∗i∗irestricted on the right to confluences ψ φ , contains at least all of the zig-zags (φ + ψ) .
To finish this section, we provide a sketch of the proof, a detailed version of which can be found in [2].
To ease notation, juxtaposition will denote i-multiplication. By (7) and (15), we have^ ∗j ij (ψ∗i φ∗i ) ≤ |A
^ ∗j ij (ψ∗i φ∗i ) ⇒ (φ + ψ)∗i ≤ |A
^ ∗j ij (ψ∗i φ∗i )1i + (φ + ψ)|A^ ∗j ij (ψ∗i φ∗i ), it remains to show thatObserving that 1i ≤ ψ∗i φ∗i ≤ |A
^ ∗j ij (ψ∗i φ∗i ) ≤ |A
^ ∗j ij (ψ∗i φ∗i ).
(φ + ψ)|ABy distributivity, we may prove this for each of the summands. Below, we show the formal calculationsin the n-Kleene algebra on the left, which are reflected in the diagrammatic representations on the right:^ ∗j ij (ψ∗i φ∗i ) ≤ |φA^ ∗j ij (φψ∗i φ∗i )φ|A^ ∗j ij (|Aij (ψ∗i φ∗i )φ∗i )≤ |φA^ ∗j ij (|Aφ∗i ij (ψ∗i φ∗i φ∗i ))≤ |φA^ ∗j j Aφ∗i ij (ψ∗i φ∗i )≤ |φA^ ∗j j Ai^ j (ψ∗i φ∗i )≤ |A^ ∗j ij (ψ∗i φ∗i )≤ |A4·φ(φ+ψ)∗i/·oψ∗iψ∗i⇓ Aφ∗i^ ∗j⇓ φAφ∗i!

>·φ∗i·/= ·Algebraic Coherent Confluence

Cameron Calk^ ∗j ij (ψ∗i φ∗i ) ≤ |ψA^ ∗j ij (ψψ∗i φ∗i )ψ|A^ ∗j ij (ψ∗i φ∗i )≤ |ψA^ ∗j ij (ψ∗i φ∗i )≤ |A·ψ/·o(φ+ψ)∗i=⇓ ψA</ ·^ ∗jψ∗ iψ∗ iφ∗i"+··5Conclusion

By introducing the structure of modal n-Kleene algebra, we have provided an algebraic framework forcoherent confluence proofs in higher dimensional rewriting theory. A more detailed account of thisstructure and its properties can be found in [2]. There, in addition to the Church-Rosser theorem, a notionof termination in modal n-Kleene algebras is formalised, and a coherent version of Newman’s lemma is
formulated and proved in the setting of globular modal n-Kleene algebra.
Perspectives for future work most notably include a formulation of the coherent confluence Squiertheorem [5] for abstract rewriting systems in globular modal n-Kleene algebras. This result concerns
homotopical properties of polygraphs considered as cofibrant objects in the folk model structure of
ω-categories. A central goal is thus to formalise the notion of cofibrant object in the language of modal
n-Kleene algebras, and thereby relate these to questions in homotopy type theory. Other avenues offuture work include formalising the structure of modal n-Kleene algebra in the proof assistant Isabelle,
following [1], and developing a cubical approach.

References[1] A. Armstrong, V. Gomes, and G. Struth. Algebras for program correctness in Isabelle/HOL. volume8428, 04 2014.
[2] C. Calk, E. Goubault, P. Malbos, and G. Struth. Algebraic coherent confluence and higher-dimensional
Kleene algebras. Work in progress, 2020.
[3] J. Desharnais and G. Struth. Internal axioms for domain semirings. Science of Computer Programming,
76(3):181–203, 2011.
[4] Y. Guiraud, E. Hoffbeck, and P. Malbos. Convergent presentations and polygraphic resolutions ofassociative algebras. Math. Z., 293(1-2):113–179, 2019.
[5] Y. Guiraud and P. Malbos. Polygraphs of finite derivation type. Math. Structures Comput. Sci.,
28(2):155–201, 2018.
[6] B. Jónsson and A. Tarski. Boolean algebras with operators. Part I. American Journal of Mathematics,
73(4):891–939, 1951.
[7] G. Struth. Abstract abstract reduction. J. Log. Algebr. Program., 66(2):239–270, 2006.

5