Caïus Wojcik
email: caius.wojcik@gmail.com

Luca Q Zamboni
email: zamboni@math.univ-lyon1.fr

Monochromatic factorisations of words and periodicity

Keywords: Combinatorics on words, Ramsey theory. 2010 MSC: 68R15, 05C55, 05D10

In 2006 T. Brown asked the following question in the spirit of Ramsey theory: Given a non-periodic infinite word x = x 1 x 2 x 3 • • • with values in a non-empty set A, does there exist a finite colouring ϕ : A + → C relative to which x does not admit a ϕ-monochromatic factorisation, i.e., a factorisation of the form x = u 1 u 2 u 3 • • • with ϕ(u i ) = ϕ(u j ) for all i, j ≥ 1? This question belongs to the class of Ramsey type problems in which one asks whether some abstract form of Ramsey's theorem holds in a certain generalised setting. Various partial results in support of an affirmative answer to this question have appeared in the literature in recent years. In particular it is known that the question admits an affirmative answer for all non-uniformly recurrent words and hence for almost all words relative to the standard Bernoulli measure on A N . This question also has a positive answer for various classes of uniformly recurrent words including Sturmian words and fixed points of strongly recognizable primitive substitutions. In this paper we give a complete and optimal affirmative answer to this question by showing that if x = x 1 x 2 x 3 • • • is an infinite non-periodic word with values in a non-empty set A, then there exists a 2-colouring ϕ : A + → {0, 1} such that for any factorisation x = u 1 u 2 u 3 • • • we have ϕ(u i ) = ϕ(u j ) for some i = j. In fact this condition gives a characterization of non-periodic words. It may be reformulated in the language of ultrafilters as follows: Let βA + denote the Stone-Čech compactification of the discrete semigroup A + which we regard as the set of all ultrafilters on A + . Then an infinite word x = x 1 x 2 x 3 • • • with values in A is periodic if and only if there exists p ∈ βA + such that for each A ∈ p there exists a factorisation x = u 1 u 2 u 3 • • • with each u i ∈ A. Moreover p may be taken to be an idempotent element of βA + .

Introduction

Give a non-empty (not necessarily finite) set A, let A + denote the free semigroup generated by A consisting of all finite words u 1 u 2 • • • u n with u i ∈ A, and let A N denote the set of all infinite words x = x 1 x 2 x 3 • • • with x i ∈ A. We say x ∈ A N is periodic if x = u ω = uuu • • • for some u ∈ A + . The following question was independently posed by T. Brown in [START_REF] Brown | colourings of the factors of a word[END_REF] and by the second author in [START_REF] Zamboni | A Note on colouring Factors of Words[END_REF] 1 : Question 1. Let x ∈ A N be non-periodic. Does there exist a finite colouring ϕ : A + → C relative to which x does not admit a ϕ-monochromatic factorisation, i.e., a factorisation of the form x = u 1 u 2 u 3 • • • with ϕ(u i ) = ϕ(u j ) for all i, j ≥ 1?

A finite colouring ϕ : A + → C is called a separating colouring for x (or a separating |C|-colouring for x) if for all factorisations x = u 1 u 2 u 3 • • • there exist i, j ≥ 1 such that ϕ(u i ) = ϕ(u j ). While T. Brown originally stated it as a question, Question 1 has evolved into a conjecture which states that every non-periodic word admits a separating colouring. We begin by illustrating Question 1 with an example: Consider the Thue-Morse infinite word

x = 011010011001011010010 • • •
where the nth term of x (starting from n = 0) is defined as the sum modulo 2 of the digits in the binary expansion of n. The origins of this word go back to the beginning of the last century with the works of A. Thue [START_REF] Thue | Über unendliche Zeichenreihen[END_REF][START_REF] Thue | Über die gegenseitige Lage gleicher Teile gewisser Zeichenreihen[END_REF] in which he proves amongst other things that x is overlap-free i.e., x contains no factor of the form uuu ′ where u ′ is a non-empty prefix of u.

Consider the 3 colouring ϕ : {0, 1} + → {0, 1, 2} defined by

ϕ(u) =       
0 if u is a prefix of x ending with 0;

1 if u is a prefix of x ending with 1; 2 if u is not a prefix of x.

We claim that no factorisation of x is ϕ-monochromatic. In fact, suppose to the contrary that x = u 1 u 2 u 3 • • • is a ϕ-monochromatic factorisation of x. Since u 1 is a prefix of x, it follows that ϕ(u 1 ) ∈ {0, 1}, i.e., there exists a ∈ {0, 1} such that each u i is a prefix of x terminating with a. Pick i ≥ 2 such that |u i | ≤ |u i+1 |. Then as each u i is a prefix of x, it follows that u i is a prefix of u i+1 and hence au i u i is a factor of x. Writing u i = va, (with v empty or in {0, 1} + ), we have au i u i = avava which is an overlap, contradicting that x is overlap-free. This proves that there exists a separating 3-colouring for the Thue-Morse word. Recently S. Avgustinovich and O. Parshina [1] proved that it is possible to colour {0, 1} + using only 2 colours in such a way that no factorisation of the Thue-Morse word is monochromatic.

Let us remark in the example above that since the Thue-Morse word x is not periodic, it follows that each proper suffix x ′ of x begins in some factor u which is not a prefix of x. This means that x ′ may be written as an infinite concatenation x ′ = u 1 u 2 u 3 • • • where ϕ(u i ) = 2 for all i ≥ 1. So while x itself does not admit a ϕ-monochromatic factorisation, where ϕ is the 3-colouring of {0, 1} + defined above, it turns out that every proper suffix of x does admit a ϕ-monochromatic factorisation. Moreover, this monochromatic factorisation of x ′ has an even stronger monochromatic property: The set {u n : n ≥ 1} + is ϕ-monochromatic (each element has ϕ colour equal to 2). This is because each element of {u n : n ≥ 1} is a non-prefix of x and hence the same is true of any concatenation formed by elements from this set. It turns out that a weaker version of this phenomenon is true in greater generality: Given any x ∈ A N and any finite colouring ϕ : A + → C, one can always find a suffix x ′ of x which admits a factorisation

x ′ = u 1 u 2 u 3 • • • where ϕ(u i • • • u j ) = ϕ(u 1 ) for all 1 ≤ i ≤ j.
This fact may be obtained via a straightforward application of the infinite Ramsey theorem [START_REF] Ramsey | On a problem of formal logic[END_REF] (see [START_REF] Brown | colourings of the factors of a word[END_REF][START_REF] De Luca | On some variations of colouring problems of infinite words[END_REF] or see [START_REF] Schützenberger | Quelques problèmes combinatoires de la théorie des automates[END_REF] for a proof by M. P. Schützenberger which does not use Ramsey's theorem).

Thus Question 1 belongs to the class of Ramsey type problems in which one tries to show that some abstract form of Ramsey's theorem does not hold in certain settings. For instance, the infinite version of Ramsey's theorem [START_REF] Ramsey | On a problem of formal logic[END_REF] (for colouring of pairs) states that whenever the set Σ 2 (N) of all 2-element subsets of N is finitely coloured, there exists an infinite set X ⊆ N with Σ 2 (X) monochromatic. Hence the same applies when N is replaced by R. On the other hand, W. Sierpiński [START_REF] Sierpiński | Sur un problème de la théorie des relations[END_REF] showed that there exists a finite colouring of Σ 2 (R) such that there does not exist an uncountable set X with Σ 2 (X) monochromatic. In other words, Ramsey's theorem does not extend to the uncountable setting in R. Similarly, by a straightforward application of Ramsey's theorem, one deduces that given any finite colouring of N, there exists an infinite X ⊆ N all of whose pairwise sums {n + m : n, m ∈ X, n = m} is monochromatic. Again it follows the same is true with N replaced by R. On the other hand, N. Hindman, I. Leader and D. Strauss [START_REF] Hindman | Pairwise sums in colourings of the reals[END_REF] recently exhibited (using the Continuum Hypothesis CH) the existence of a finite colouring of R such that there does not exist an uncountable set with all its pairwise sums monochromatic. In other words, this additive formulation of Ramsey's Theorem also fails in the uncountable setting in R. A related question in these sorts of problems concerns the least number of colours necessary to avoid the presence of monochromatic subsets of a certain kind. For instance N. Hindman [START_REF] Hindman | Partitions and sums of integers with repetition[END_REF] showed that there exists a 3-colouring of N such that there does not exist an infinite subset X with X + X monochromatic, and it is an open question of Owings [START_REF] Owings | Problem E2494[END_REF] whether the same result may be obtained with only 2 colours. Again, using CH and a few more colours (288 to be precise), it is possible to extend Hindman's result to the reals (see Theorem 2.8 in [START_REF] Hindman | Pairwise sums in colourings of the reals[END_REF]). But again it is not known whether the same result can be obtained with only 2 colours [START_REF] Leader | [END_REF]. Thus a stronger version of Question 1 would read: Does every non-periodic word admit a separating 2-colouring?

Various partial results in support of an affirmative answer to Question 1 were obtained in [START_REF] Bernardino | colouring factors of substitutive infinite words[END_REF][START_REF] De Luca | A colouring problem for infinite words[END_REF][START_REF] De Luca | On some variations of colouring problems of infinite words[END_REF][START_REF] De Luca | On prefixal factorizations of words[END_REF][START_REF] Salo | Factor colourings of linearly recurrent words[END_REF]. For instance, in [START_REF] De Luca | A colouring problem for infinite words[END_REF], it is shown that Question 1 admits an affirmative answer for all non-uniformly recurrent words and various classes of uniformly recurrent words including Sturmian words. In [START_REF] Salo | Factor colourings of linearly recurrent words[END_REF], V. Salo and I. Törmä prove that for every aperiodic linearly recurrent word x ∈ A N there exists a finite colouring of A + relative to which x does not admit a monochromatic factorisation into factors of increasing lengths. And recently A. Bernardino, R. Pacheco and M. Silva [START_REF] Bernardino | colouring factors of substitutive infinite words[END_REF] prove that Question 1 admits an affirmative answer for all fixed points of primitive strongly recognizable substitutions. In addition to the fact that these partial results concern only restricted classes of non-periodic words (e.g., Sturmian words or certain fixed points of primitive substitutions), in most cases the number of colours required to colour A + in order to avoid a monochromatic factorisation of x is found to be quite high. For instance in [START_REF] Salo | Factor colourings of linearly recurrent words[END_REF], the authors prove that if x ∈ A N is an aperiodic linearly recurrent word, then there exists a constant K ≥ 2 and a colouring ϕ :

A + → C with Card(C) = 2 + K 5 -1 i=0 2K i (K + 1) 2i , such that no factorisation of x = u 1 u 2 u 3 • • • , verifying the additional constraint that |u i | ≤ |u i+1 | for each i ≥ 1, is ϕ-monochromatic.
The constant K above is chosen such that for every factor u of x, every first return w to u satisfies |w| ≤ K|u| (see for instance [START_REF] Durand | Substitutional dynamical systems, Bratteli diagrams and dimension groups[END_REF]). A similar large bound depending on the recognizability index of a substitution is obtained in [START_REF] Bernardino | colouring factors of substitutive infinite words[END_REF] in the context of fixed points of strongly recognizable substitutions. In contrast, it is shown in [START_REF] De Luca | A colouring problem for infinite words[END_REF] that every Sturmian word admits a separating 3-colouring.

In this paper we give a complete and optimal affirmative answer to Question 1 by showing that for every non-periodic word x = x 1 x 2 x 3 • • • ∈ A N , there exists a 2-colouring ϕ : A + → {0, 1} relative to which no factorisation of x is ϕ-monochromatic. Moreover, this is a characterization of periodicity of infinite words:

Theorem 1. Let x = x 1 x 2 x 3 • • • ∈ A N be an infinite word. Then x is periodic if and only if for every 2-colouring ϕ : A + → {0, 1} there exists a ϕ-monochromatic factorisation of x, i.e., a factorisation x = u 1 u 2 u 3 • • • such that ϕ(u i ) = ϕ(u j ) for all i, j ≥ 1.
Theorem 1 has several nice immediate consequences: For instance, fix a symbol a ∈ A and suppose an infinite word x ∈ A N admits a factorisation x = u 1 u 2 u 3 • • • where each u i is a prefix of x rich in the symbol a ∈ A, meaning that for each i ≥ 1 and for each factor v of x with |v| = |u i | we have f a (u i ) ≥ f a (v) where f a (u i ) denotes the frequency of a in u i . Then {n ∈ N : x n = a} is a finite union of arithmetic progressions. As another application of Theorem 1 we show that if u 1 , u 2 , u 3 , . . . , u 2k+1 ∈ A + (with k a positive integer), then any

x ∈ A N belonging to {u 1 , u 2 } N ∩ {u 2 , u 3 } N ∩ • • • ∩ {u 2k , u 2k+1 } N ∩ {u 2k+1 , u 1 } N is periodic.
Theorem 1 may be reformulated in the language of ultrafilters as follows: Let βA + denote the Stone-Čech compactification of the discrete semigroup A + which we regard as the set of all ultrafilters on A + , identifying the points of A + with the principal ultrafilters. As is well known, the operation of concatenation on A + extends uniquely to βA + making βA + a compact right topological semigroup with A + contained in its topological center (see for instance [START_REF] Hindman | Algebra in the Stone-Čech compactification: theory and applications[END_REF]). In particular by the Ellis-Numakura lemma, βA + contains an idempotent element i.e., an element p verifying p • p = p. We show that an infinite word x = x 1 x 2 x 3 • • • ∈ A N is periodic if and only if there exists p ∈ βA + such that for each A ∈ p there exists a factorisation x = u 1 u 2 u 3 • • • with each u i ∈ A. Moreover p can be taken to be an idempotent element of βA + .

Proof of Theorem 1 & Applications

Before embarking on the proof of Theorem 1, we introduce some notation which will be relevant in what follows. Let A be a non-empty set (the alphabet). We do not assume that the cardinality of A is finite. Let A * denote the set of all finite words u = u 1 u 2 • • • u n with u i ∈ A. We call n the length of u and denote it |u|. The empty word is denoted ε and by convention |ε| = 0. We put A + = A * \ {ε}. For u ∈ A + and a ∈ A, we let |u| a denote the number of occurrences of a in u. Let A N denote the set of all right sided infinite words

x = x 1 x 2 x 3 • • • with values in A. More generally, for x ∈ A N and A ⊆ A + , we write x ∈ A N if x = u 1 u 2 u 3 • • • with u i ∈ A for all i ≥ 1, that is in case x factors over the set A. We say x is periodic if x ∈ {u} N for some u ∈ A + . Proof of Theorem 1. First assume x = x 0 x 1 x 2 • • • ∈ A N is periodic, i.e.,
x ∈ {u} N for some u ∈ A + . Then the factorisation x = u 1 u 2 u 3 • • • with each u i = u is ϕ-monochromatic for any choice of ϕ : A + → {0, 1}. Next assume x is not periodic and we will define a 2-colouring ϕ : A + → {0, 1} with the property that no factorisation of x is ϕ-monochromatic. Pick any total order on the set A and let ≺ denote the induced lexicographic order on A + and A N . For u, v ∈ A + with |u| = |v|, we write u v if either u ≺ v or u = v. For each n ≥ 1, let P x (n) denote the prefix of x of length n, and for each y ∈ A N , let x ∧ y denote the longest common prefix of x and y.

For u ∈ A + , set ϕ(u) = 0 if u ≺ P x (|u|)
or if u = P x (|u|) and x ≺ y where x = uy;

1 if P x (|u|) ≺ u or if u = P x (|u|) and y ≺ x where x = uy. ( 1
)
As x is not periodic, for every proper suffix y of x we have either x ≺ y or y ≺ x, whence ϕ : A + → {0, 1} is well defined. We claim that no factorisation of x is ϕ-monochromatic. To see this, fix a factorisation

x = u 1 u 2 u 3 • • • . For each k ≥ 0 put y k = u k+1 u k+2 u k+3 • • • ∈ A N and let w k = x ∧ y k . We note that y 0 = x = w 0 . For each k ≥ 0 let S k = |u 1 | + |u 2 | + • • • + |u k | + |w k | so that S 0 = |w 0 | = +∞. Clearly S k ≥ k for each k ≥ 0 and hence lim S k = +∞. Lemma 2. Assume that ϕ(u i ) = 0 for all i ≥ 1. Then ϕ(u 1 u 2 • • • u k ) = 0 for all k ≥ 1.
Proof. We proceed by induction on k. The result is clear for k = 1 since ϕ(u 1 ) = 0. For the inductive step, fix k ≥ 1 and suppose ϕ(u

1 • • • u k ) = 0. As u 1 • • • u k is a prefix of x and ϕ(u 1 • • • u k ) = 0,
w k = u k+1 v for some v ∈ A * so that x = u k+1 vay ′ and x = u 1 u 2 • • • u k u k+1 vby ′′ . Since u k+1 is a prefix of x and ϕ(u k+1 ) = 0, it follows that P x (|vb|) = P x (|va|) va ≺ vb which combined with the fact that u 1 • • • u k+1 is a prefix of x implies that ϕ(u 1 • • • u k+1 ) = 0 as required. Lemma 3. Assume that ϕ(u i ) = 0 for all i ≥ 1. Then S k ≤ S k-1 for all k ≥ 1.
Proof. We first note that S 1 ≤ S 0 since S 0 = +∞. Now fix k ≥ 1; we will show that S k+1 ≤ S k . By the previous lemma we have that ϕ(u Returning to the proof of Theorem 1, we must show that the factorisation x = u 1 u 2 u 3 • • • is not ϕ-monochromatic. Suppose to the contrary that ϕ(u i ) = ϕ(u j ) for all i, j ≥ 0. If ϕ(u i ) = 0 for all i ≥ 1, then by the previous lemma we have that S k ≤ S k-1 for all k ≥ 1 contradicting that lim S k = +∞. If on the other hand ϕ(u i ) = 1 for all i ≥ 1, then by replacing the original order on A by the reverse order we would have ϕ(u i ) = 0 for all i ≥ 1, and hence as above the previous lemma yields the desired contradiction. This concludes our proof of Theorem 1.

1 u 2 • • • u k ) = 0.
We end this section with some applications of Theorem 1 or its proof. An infinite word x ∈ A N is called Lyndon if there exists an order on A relative to which x is strictly smaller than each of its proper suffixes. Our first application is the following result originally proved in [START_REF] De Luca | A colouring problem for infinite words[END_REF]: Corollary 4. A Lyndon word x ∈ A N does not admit a prefixal factorisation, i.e., a factorisation of the form x = u 1 u 2 u 3 • • • where each u i is a prefix of x.

Proof. Suppose to the contrary that x = u 1 u 2 u 3 • • • is a prefixal factorisation of x. Let ϕ : A + → {0, 1} be the separating 2-colouring for x defined in (1). Note that x being Lyndon is not-periodic. Since x is Lyndon we have that ϕ(u i ) = 0 for all i ≥ 1, contradicting that ϕ is a separating 2-colouring for x. Let x ∈ A N and a ∈ A. A factor u of x is said to be rich in a if |u| a ≥ |v| a for all factors v of x with |v| = |u|. Theorem 6.7 in [START_REF] De Luca | A colouring problem for infinite words[END_REF] states that a Sturmian word x ∈ {0, 1} N does not admit a factorisation of the form x = u 1 u 2 u 3 • • • where each u i is a prefix of x rich in the same letter a ∈ {0, 1}. The following generalises this result to all binary non-periodic words: Corollary 5. Let x ∈ {0, 1} N and a ∈ {0, 1}. Suppose x admits a prefixal factorisation x = u 1 u 2 u 3 • • • with each u i rich in a. Then x is periodic.

Proof. Suppose to the contrary that x is not periodic. Let ϕ : {0, 1} + → {0, 1} be the separating 2-colouring for x defined in (1) relative to the order on {0, 1} where a is taken to be the least element. For each i ≥ 1, writing x = u i y i with y i ∈ {0, 1} N , we claim that x ≺ y i . Otherwise if y i ≺ x, then we can write x = zbx ′ = u i zay ′ for some z ∈ {0, 1} * , x ′ , y ′ ∈ {0, 1} N and where {a, b} = {0, 1}. But then the factor u ′ i of length |u i | immediately preceding the suffix y ′ of x would contain one more occurrence of the symbol a than u i , contradicting that u i was rich in a. Having established that x ≺ y i , it follows that ϕ(u i ) = 0 for all i ≥ 1 contradicting that ϕ is a separating 2-colouring for x. Corollary 6. Let A be an arbitrary non-empty set, x ∈ A N and a ∈ A. Suppose x admits a prefixal factorisation x = u 1 u 2 u 3 • • • with each u i rich in a. Then {n ∈ N : x n = a} is a finite union of (infinite) arithmetic progressions.

Proof. Consider the morphism φ : A → {0, 1} given by φ(a) = 1 and φ(b) = 0 for all b ∈ A \ {a}. Then applying φ to the prefixal factorisation x = u 1 u 2 u 3 • • • gives a prefixal factorisation of φ(x) in which each φ(u i ) is rich in 1. Hence by Corollary 5 we have that φ(x) is periodic and hence the set of occurrences of 1 in φ(x), which is equal to the set of occurrences of a in x, is a finite union of arithmetic progressions. Proof. Let us assume to the contrary that x is not periodic. By Theorem 1 there exists a 2-colouring ϕ : A + → {0, 1} relative to which no factorisation of x is ϕ-monochromatic. Let Σ k (B) denote the set of all k-element subsets of B. By assumption x factors over each A ∈ Σ k (B). On the other hand, since Card(B) ≥ 2k -1, it follows that there exists a ϕmonochromatic subset A ∈ Σ k (B). This gives rise to a ϕ-monochromatic factorisation of x, a contradiction.

Corollary 8. Let x = x 1 x 2 x 3 • • • ∈ A N and k be a positive integer. Let u 1 , u 2 , u 3 , . . . , u 2k+1 ∈ A + and suppose x ∈ {u 1 , u 2 } N ∩ {u 2 , u 3 } N ∩ • • • ∩ {u 2k , u 2k+1 } N ∩ {u 2k+1 , u 1 } N . Then x is periodic.
Proof. Suppose to the contrary that x is not periodic. Pick any separating 2-colouring ϕ : A + → {0, 1} for x. Then ϕ(1) = ϕ(2i + 1) for each 1 ≤ i ≤ k. Thus x / ∈ {u 2k+1 , u 1 } N , a contradiction.

A reformulation of Theorem 1 in the language of ultrafilters

In this section give an equivalent reformulation of Theorem 1 in terms of ultrafilters and the Stone-Čech compactification of the discrete semigroup A + . We begin by recalling some basic facts. For more information we refer the reader to [START_REF] Hindman | Algebra in the Stone-Čech compactification: theory and applications[END_REF]. Let S be a non-empty set and let P(S) denote the set of all subsets of S. A set p ⊆ P(S) is called a filter on S if

• S ∈ p and ∅ / ∈ p • If A ∈ p and B ∈ p then A ∩ B ∈ p • If A ⊆ B and A ∈ p then B ∈ p.
A filter p on S is called an ultrafilter if for all A ∈ P(S) either A ∈ p or A c ∈ p where A c denotes the complement of A, i.e., A c = S \ A. Equivalently, a filter p is an ultrafilter if for each A ∈ p whenever A = A 1 ∪ • • • ∪ A n we have that at least one A i ∈ p. Each x ∈ S determines an ultrafilter e(x) on S defined by e(x) = {A ⊆ S : x ∈ A}. An ultrafilter p on S is called principal if p = e(x) for some x ∈ S. Otherwise p is said to be free. Let βS denote the collection of all ultrafilters p on S. By identifying each x ∈ S with the principal ultrafilter e(x), we regard S ⊆ βS. If S is infinite, then a straightforward application of Zorn's lemma guarantees the existence of free ultrafilters on S.

Given A ⊆ S, we put A = {p ∈ βS : A ∈ p}. Then {A : A ⊆ S} defines a basis for a topology on βS relative to which βS is both compact and Hausdorff and the mapping x → e(x) defines an injection S ֒→ βS whose image is dense in βS. In fact, if S is given the discrete topology, then βS is identified with the Stone-Čech compactification of S : Any continuous mapping from f : S → K, where K is a compact Hausdorff space, lifts uniquely to a continuous mapping βf : βS → K. Of special interest is the case in which S is a discrete semigroup. In this case the operation on S extends uniquely to βS making βS a right topological semigroup with S contained in its topological center. This means that ρ p : βS → βS, defined by ρ p (q) = q • p, is continuous for each p ∈ βS and λ s : βS → βS, defined by λ s (q) = s • q, is continuous for each s ∈ S. The operation • on βS is defined as follows: For p, q ∈ βS p • q = {A ⊆ S : {s ∈ S : s -1 A ∈ q} ∈ p}, where s -1 A = {t ∈ S : st ∈ A}. As a consequence of the Ellis-Numakura lemma, βS contains an idempotent element i.e., an element p verifying p • p = p (see for instance [START_REF] Hindman | Algebra in the Stone-Čech compactification: theory and applications[END_REF]). Subsets A ⊆ S belonging to idempotents in βS have rich combinatorial structures: Let Fin(N) denote the set of all finite subsets of N. Given an infinite sequence s n n∈N in S, let

F P ( s n n∈N ) = { n∈F s n : F ∈ Fin(N)}
where for each F ∈ Fin(N), the product n∈F s n is taken in increasing order of indices. A subset A of S is called an IP-set if A contains F P ( s n n∈N ) for some infinite sequence s n n∈N in S. IP-sets are characterised as belonging to idempotent elements: A ⊆ S is an IP-set if and only if A belongs to some idempotent element of βS (see for instance Theorem 5.12 in [START_REF] Hindman | Algebra in the Stone-Čech compactification: theory and applications[END_REF]). The following is a reformulation of Theorem 1 in the language of ultrafilters: Theorem 9. Let x = x 1 x 2 x 3 • • • ∈ A N be an infinite word. Then x is periodic if and only if there exists p ∈ βA + such that for each A ∈ p there exists a factorisation

x = u 1 u 2 u 3 • • • with each u i ∈ A.
Proof. Suppose x is periodic, i.e., x ∈ {u} N for some u ∈ A + . Then the principal ultrafilter e(u) = {A ⊆ A + : u ∈ A} obviously verifies the required condition of Theorem 9. Conversely, suppose there exists p ∈ βA + such that for each A ∈ p there exists a factorisation x = u 1 u 2 u 3 • • • with each u i ∈ A. Let ϕ : A + → {0, 1} be any 2-colouring of A + . We will show that x admits a ϕ-monochromatic factorisation. The result then follows from Theorem 1. Consider the partition A + = ϕ -1 (0) ∪ ϕ -1 (1). Since A + ∈ p, it follows that ϕ -1 (a) ∈ p for some a ∈ {0, 1}. Thus there exists a factorisation x = u 1 u 2 u 3 • • • with each u i ∈ ϕ -1 (a). In other words, x admits a ϕ-monochromatic factorisation. To see that a) =⇒ b), pick p as in a) and let ϕ : A + → C be any finite colouring of A + . Consider the partition A + = c∈C ϕ -1 (c). Then there exists some c ∈ C such that ϕ -1 (c) ∈ p. This implies that we can write x = u 1 u 2 u 3 • • • with each u i ∈ ϕ -1 (c). In other words, x admits a ϕ-monochromatic factorisation. Conversely to see that b) =⇒ a), assume b) and define φ :

P(A + ) → {0, 1} by φ(A) = 1

if and only if for every finite partition

A = A 1 ∪ A 2 ∪ • • • ∪ A n there exists 1 ≤ i ≤ n with A i ∈ F (x)
. Then φ verifies the following three conditions for all subsets A, B ∈ P(A + ) :

(1) φ(A + ) = 1 (this is a consequence of b).

(2) A ⊆ B and φ(A) = 1 then φ(B) = 1.

(

) If φ(A) = φ(B) = 0 then φ(A ∪ B) = 0. 3
By a standard application of Zorn's lemma, it is shown that there exists p ∈ βA + such that φ(A) = 1 for all A ∈ p (see Theorem 3.11 in [START_REF] Hindman | Algebra in the Stone-Čech compactification: theory and applications[END_REF]). Finally for each A ∈ p, by considering the trivial partition A = A, we deduce that A ∈ F (x) as required.

We next show that p in Theorem 9 may be taken to be an idempotent element of βA + . For

x = x 1 x 2 x 3 • • • ∈ A N , we set F (x) = {A ⊆ A + : x ∈ A N } and U(x) = {p ∈ βA + : p ⊆ F (x)}.
Thus p ∈ U(x) if and only if x factors over every A ⊆ A + belonging to p. Thus Theorem 9 states that U(x) = ∅ if and only if x is periodic.

Theorem 11. Let x = x 0 x 1 x 2 • • • ∈ A N . Then the following are equivalent: i) x is periodic. ii) U(x) is a closed sub-semigroup of βA + . iii) U(x) contains an idempotent element. iv) The set Pref(x) consisting of all prefixes of x is an IP-set Proof. We first note that for each infinite word x, we have that U(x) is a closed subset of βA + . In fact, suppose p ∈ βA + \ U(x), then there exists A ∈ p with A / ∈ F (x). Then A is an open neighbourhood of p and any q ∈ A contains the set A and hence is not in U(x). To see that i) =⇒ ii), suppose that x is periodic. Pick the shortest u ∈ A + such that x ∈ {u} N . Then the principal ultrafilter e(u) = {A ⊆ A + : u ∈ A} clearly belongs to U(x). Thus U(x) = ∅. We note that if x is periodic, then U(x) also contains free ultrafilters. In fact, for each i ≥ 1, let A i = {u j : j ≥ i}. Then p ∈ U(x) if and only if A 1 ∈ p and any p ∈ βA + containing {A i : i ≥ 1} is a free ultrafilter belonging to U(x). It remains to show that p • q ∈ U(x) whenever p, q ∈ U(x). Let A ∈ p • q with p, q ∈ U(x). Then {s ∈ A + : s -1 A ∈ q} ∈ p and since p ∈ U(x) it follows that u n ∈ {s ∈ A + : s -1 A ∈ q} for some n ∈ N. Thus {t ∈ A + : u n t ∈ A} ∈ q and since q ∈ U(x) it follows that u m ∈ {t ∈ A + : u n t ∈ A} for some m ∈ N. In other words u n+m ∈ A and hence x factors over A. Thus p • q ∈ U(x). The implication ii) =⇒ iii) follows from the Ellis-Numakura lemma. To see iii) =⇒ iv) pick an idempotent element p ∈ U(x). We note that Pref(x) belongs to every q ∈ U(x). In fact, suppose that Pref(x) / ∈ q, for some q ∈ U(x). Then A + \ Pref(x) ∈ q which implies that x factors over A + \ Pref(x). But this is a contradiction since in any factorisation of x, the first term occurring in the factorisation belongs to Pref(x). Thus in particular Pref(x) ∈ p. Since p is an idempotent, it follows that Pref(x) is an IP-set. Finally, to see that iv) =⇒ i) assume that Pref(x) is an IP-set. Then Pref(x) contains F P ( s n n∈N ) for some infinite sequence s n n∈N of prefixes of x. This means that for each n ≥ 2, both s 1 s 2 • • • s n and s 2 • • • s n are prefixes of x. Thus x = s 1 x which implies that x is periodic.

  we can write x = w k ay ′ and x = u 1 u 2 • • • u k w k by ′′ for some y ′ , y ′′ ∈ A N and a, b ∈ A with a ≺ b. It follows that |u k+1 | ≤ |w k | for otherwise w k b is a prefix of u k+1 and we would have P x (|u k+1 |) ≺ u k+1 whence ϕ(u k+1 ) = 1, a contradiction. Thus we can write

  As in the proof of the previous lemma, we can write x = u k+1 vay ′ and x = u1 u 2 • • • u k u k+1 vby ′′ for some y ′ , y ′′ ∈ A N , v ∈ A *and a, b ∈ A with a ≺ b. We claim that |w k+1 | ≤ |v|. In fact, if |w k+1 | > |v|, then vb would be a prefix of x, and hence va ≺ vb = P x (|va|) which in turn implies that ϕ(u k+1 ) = 1, a contradiction. Thus |w k+1 | ≤ |v| = |w k | -|u k+1 | or equivalently |u k+1 | + |w k+1 | ≤ |w k | from which it follows that S k+1 ≤ S k as required.

Corollary 7 .

 7 Let x = x 1 x 2 x 3 • • • ∈ A N and k be a positive integer. Let B ⊆ A + with Card(B) ≥ 2k -1. Suppose that x ∈ A N for every k-element subset A of B. Then x is periodic.

Remark 10 .

 10 It can be shown that Theorem 9 is actually an equivalent reformulation of Theorem 1. More precisely, given an infinite wordx = x 1 x 2 x 3 • • • ∈ A N ,the following statements are equivalent: a) There exists p ∈ βA + such that for each A ∈ p we can write x = u 1 u 2 u 3 • • • with each u i ∈ A. b) For each finite colouring ϕ : A + → C there exists a ϕ-monochromatic factorisation of x.

The original formulation of the question was stated in terms of finite colourings of the set of all factors of x.


Amina Doumane
email: amina.doumane@ens-lyon.fr

Damien Pous
email: damien.pous@ens-lyon.fr

Completeness for Identity-free Kleene Lattices *

Keywords: 2012 ACM Subject Classification Theory of computation → Regular languages Kleene algebra, Graph languages, Petri Automata, Kleene theorem

We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.

Introduction

Relation algebra is an efficient tool to reason about imperative programs. In this approach, the bigstep semantics of a program P is a binary relation [P ] between memory states [START_REF] Kozen | Kleene algebra with tests[END_REF][START_REF] Kozen | On Hoare logic and Kleene algebra with tests[END_REF][START_REF] Angus | Kleene algebra with tests and program schematology[END_REF][START_REF] Hoare | Concurrent Kleene algebra[END_REF][START_REF] Anderson | Netkat: semantic foundations for networks[END_REF]. This relation is built from the elementary relations corresponding to the atomic instructions of P , which are combined using standard operations on relations, for instance composition and transitive closure, that respectively encode sequential composition of programs, and iteration (while loops). Abstracting over the concrete behaviour of atomic instructions, one can compare two programs P, Q by checking whether the expressions [P ] and [Q] are equivalent in the model of binary relations, which we write as Rel |=

[P ] = [Q].
To enable such an approach, one should obtain two properties: decidability of the predicate Rel |= e = f , given two expressions e and f as input, and axiomatisability of this relation. Decidability makes it possible to automate the verification process, thus alleviating the burden for the end-user [START_REF] Höfner | On automating the calculus of relations[END_REF][START_REF] Foster | Automated engineering of relational and algebraic methods in Isabelle/HOL -(invited tutorial)[END_REF][START_REF] Braibant | Deciding Kleene algebras in Coq[END_REF][START_REF] Krauss | Proof pearl: Regular expression equivalence and relation algebra[END_REF][START_REF] Pous | Kleene Algebra with Tests and Coq tools for while programs[END_REF]. Axiomatisation offers a better way of understanding the equational theory of relations and provides a certificate for programs verification. Indeed, an axiomatic proof of e = f can be seen as a certificate, which can be exchanged, proofread, and combined in a modular way. Axiomatisations also make it possible to solve hard instances manually, when the existing decision procedures have high complexity and/or when considered instances are large [START_REF] Kozen | Certification of compiler optimizations using Kleene algebra with tests[END_REF][START_REF] Höfner | On automating the calculus of relations[END_REF][START_REF] Armstrong | Programming and automating mathematics in the Tarski-Kleene hierarchy[END_REF].

Depending on the class of programs under consideration, several sets of operations on relations can be considered. In this paper we focus on the following set of operations: composition (•), transitive closure (_ + ), union (+), intersection (∩) and the empty relation (0).

18:2

Completeness for Identity-free Kleene Lattices

The expressions generated by this signature are called KL --expressions. An example of an The operations of composition, union and transitive closure arise naturally when defining the bigstep semantics of sequential programs. In contrast, intersection, which is the operation of interest in the present paper, is not a standard operation on programs. This operation is however useful when it comes to specifications: it allows one to express local conjunctions of specifications. For instance, a specification of the shape (a ∩ b) + expresses the fact that execution traces must consist of sequences of smaller traces satisfying both a and b.

The operations of KL -contain those of identity-free regular expressions, whose equational theory inherits the good properties of Kleene algebra (KA).We summarise them below.

First recall that each regular expression e can be associated with a set of words L(e) called its language. Valid inequations between regular expressions inequalities can be characterised by language inclusions [START_REF] Pratt | Dynamic algebras and the nature of induction[END_REF]:

Rel |= e ≤ f iff L(e) ⊆ L(f ) (1)
Second, we have the celebrated equivalence between regular expressions and non-deterministic finite automata (NFA) via a Kleene theorem: for every regular expression e, there is an NFA such that L(e) is the language of A, and conversely. Decidability follows (in fact, PSpacecompleteness). Lastly, although every purely equational axiomatisation of this theory must be infinite [START_REF] Redko | On defining relations for the algebra of regular events[END_REF], Kozen has proved that Conway's finite quasi-equational axiomatisation [START_REF] Conway | Regular algebra and finite machines[END_REF] is sound and complete [START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF]. (There is also an independent proof of this result by Boffa [START_REF] Boffa | Une condition impliquant toutes les identités rationnelles[END_REF],

based on the extensive work of Krob [START_REF] Krob | Complete systems of B-rational identities[END_REF].)

Those three results nicely restrict to identity-free Kleene algebra (KA -), which form a proper fragment of Kleene algebra [START_REF] Kozen | Typed Kleene algebra[END_REF]. It suffices to consider languages of non-empty words:

Equation (1) remains, Kleene's theorem still holds, and we have the following characterisation, where we write KA -e ≤ f when e ≤ f is derivable from the axioms of KA -:

L(e) ⊆ L(f ) iff KA -e ≤ f ( 2
)
There are counterparts to the first two points for KL --expressions. Each KL --expression e can be associated with a set of graphs G(e) called its graph language, and valid inequations of KL --expressions can be characterised through these languages of graphs. A subtlety here is that we have to consider graphs modulo homomorphisms; writing G for the closure of a set of graphs G under graph homomorphisms, we have [START_REF] Brunet | Petri automata for Kleene allegories[END_REF]:

Rel |= e ≤ f iff G(e) ⊆ G(f ) (3)
KL --expressions are equivalent to a model of automata over graphs called Petri automata [START_REF] Brunet | Petri automata for Kleene allegories[END_REF].

As for KA --expressions, a Kleene-like theorem holds [START_REF] Brunet | Petri automata[END_REF]: for every KL --expression e, there is a Petri automaton whose language is G(e), and conversely. Decidability (in fact, ExpSpacecompleteness) of the equational theory follows [START_REF] Brunet | Petri automata for Kleene allegories[END_REF][START_REF] Brunet | Petri automata[END_REF].

What is missing to this picture is an axiomatisation of the corresponding equational theory.

In the present paper, we provide such an axiomatisation, which we call KL -, and which comprises the axioms for identity-free Kleene algebra (KA -) and the axioms of distributive lattices for {+, ∩}. Completeness of this axiomatisation is the difficult result we prove here:

G (e) ⊆ G (f ) entails KL -e ≤ f ( 4
)
We proceed in two main steps. First we show that G (e) ⊆ G (f ) entails KL - e ≤ f , using a technique inspired from [START_REF] Kozen | Completeness and incompleteness in nominal kleene algebra[END_REF], this is what we call completeness for strict language inclusion.The second step is much more involved. There we exploit the Kleene theorem for

Petri automata [START_REF] Brunet | Petri automata[END_REF]: starting from expressions e, f such that G (e) ⊆ G (f ), we build two Petri automata A , B respectively recognising G (e) and G (f ). Then we design a product construction to synchronise A and B, and a Kleene-like algorithm to extract from this construction two expressions e , f such that G (e) = G (e ), KL -e ≤ f , and

G (f ) ⊆ G (f ).
This synchronised Kleene theorem suffices to conclude using the first step.

To our knowledge, this is the first completeness result for a theory involving Kleene iteration and intersection. Identity-free Kleene lattices were studied in depth by Andréka, Mikulás and Németi [START_REF] Andréka | The equational theory of Kleene lattices[END_REF]; they have in particular shown that over this syntax, the equational theories generated by binary relations and formal languages coincide. But axiomatisability remained opened. The restriction to the identity-free fragment is important for several reasons. First of all, it makes it possible to rely on the technique used in [START_REF] Brunet | Petri automata for Kleene allegories[END_REF] to compare Petri automata, which does not scale in the presence of identity. Second, this is the fragment for which the Kleene theorem for Petri automata is proved the most naturally [START_REF] Brunet | Petri automata[END_REF]. Third, 'strange' laws appear in the presence of 1 [START_REF] Andréka | Axiomatizability of positive algebras of binary relations[END_REF], e.g.,

1 ∩ (b • a) ≤ a • (1 ∩ (b • a)) • b,
and
axiomatisability is still open even in the finitary case where Kleene iteration is absent-see the erratum about [START_REF] Andréka | Axiomatizability of positive algebras of binary relations[END_REF].

Proofs of completeness for other extensions of Kleene algebra include Kleene algebra with tests (KAT) [START_REF] Kozen | Kleene algebra with tests[END_REF], nominal Kleene algebra [START_REF] Kozen | Completeness and incompleteness in nominal kleene algebra[END_REF], and Concurrent Kleene algebra [START_REF] Laurence | Completeness theorems for pomset languages and concurrent kleene algebras[END_REF][START_REF] Kappé | Concurrent kleene algebra: Free model and completeness[END_REF]. The latter extension is the closest to our work since the parallel operator of concurrent Kleene algebra shares some properties of the intersection operation considered in the present work (e.g., it is commutative and it satisfies a weak interchange law with sequential composition).

The paper is organised as follows. In Sect. 2, we recall KL --expressions, their graph language and the corresponding model of Petri automata. In Sect. 3 we give our axiomatisation and state the completeness result. Then we show it following the proof scheme presented earlier: in Sect. 4 we show completeness for strict language inclusions, we recall in Sect. 5

the Kleene theorem of KL -expressions, on which we build to show our synchronised Kleene theorem in Sect. 6.

2

Expressions, graph languages and Petri automata

Expressions and their relational semantics

We let a, b . . . range over the letters of a fixed alphabet X. We consider the following syntax of KL --expressions, which we simply call expressions if there is no ambiguity:

e, f ::= e • f | e + f | e ∩ f | e + | 0 | a (a ∈ X)
We denote their set by Exp X and we often write ef for e • f . When we remove intersection (∩) from the syntax of KL --expressions we get KA --expressions, which are the identity-free regular expressions.

If σ : X → P(S × S) is an interpretation of the letters into some space of relations, we write σ for the unique homomorphism extending σ into a function from Exp X to P(S × S).

An inequation between two expressions e and f is valid, written Rel |= e ≤ f , if for every such interpretation σ we have σ(e) ⊆ σ(f ).

Terms, graphs, and homomorphisms

We let u, v . . . range over expressions built using only letters, ∩ and •, which we call terms.

(Terms thus form a subset of expressions: they are those expressions not using 0, + and _ + .)

18:4

Completeness for Identity-free Kleene Lattices We As depicted in Fig. 1, graphs can be composed in series or in parallel, and a letter can be seen as a graph with a single edge labelled by that letter. One can thus recursively associate to every term u a graph G (u) called the graph of u. Two examples are given in Fig. 2; graphs of terms are series-parallel [START_REF] Valdes | The recognition of series parallel digraphs[END_REF].

G ∩ H G H G • H G H G (
Definition 1 (Graph homomorphism). A homomorphism from G = V, E, s, t, l, ι, o to G = V , E , s , t , l , ι , o is a pair h = f, g of functions f : V → V and g : E → E that respect the various components: s • g = f • s, t • g = f • t, l = l • g, ι = f (ι), and o = f (o).
We write G G if there exists a graph homomorphism from G to G .

Such a homomorphism is depicted in Fig. 3. A pleasant way to think about graph homomorphisms is the following: we have G H if G is obtained from H by merging (or identifying) some nodes, and by adding some extra nodes and edges. For instance, the graph G in Fig. 3 is obtained from H by merging the nodes 1, 2 and by adding an edge between the input and the output labelled by d.

The starting point of the present work is the following characterisation:

Theorem 2 ([5, Thm. 1], [15, p. 208]). For all terms u, v,

Rel |= u ≤ v iff G (u) G (v).

Graph language of an expression

To generalise the previous characterisation to KL --expressions, one interprets expressions by sets (languages) of graphs: graphs play the role of words for KA-expressions.

Definition 3 (Term and graph languages of expressions).

The term language of an expression e, written e , is the set of terms defined recursively as follows:

e • f {u • v | u ∈ e and v ∈ f } 0 ∅ e ∩ f {u ∩ v | u ∈ e and v ∈ f } a {a} e + f e ∪ f e + n>0 {u 1 • • • • • u n | ∀i, u i ∈ e }
The graph language of e is the set of graphs G(e) {G(u) | u ∈ e }.

Note that for every term u, u = {u}, so that the graph language of u thus contains just the graph of u. This justifies the overloaded notation G (u). Given a set S of graphs, we write S for its downward closure w.r.

Petri automata

We recall the notion of Petri automata [START_REF] Brunet | Petri automata for Kleene allegories[END_REF][START_REF] Brunet | Petri automata[END_REF], an automata model that recognises precisely the graph languages of our expressions.

Definition 5 (Petri Automaton).

A Petri automaton (PA) over the alphabet X is a tuple A = P, T , ι where: P is a finite set of places, T ⊆ P (P ) × P (X × P ) is a set of transitions, ι ∈ P is the initial place of the automaton.

For each transition t = ◃ t, t ▹ ∈ T , ◃ t is assumed to be non-empty; ◃ t ⊆ P is the input of t;

and t ▹ ⊆ X × P is the output of t. We write π 2 (t ▹ ) {p | ∃a, a, p ∈ t ▹ } for the set of the output places of t. Transitions with empty outputs are called final.

A PA is depicted in Fig. 4: places are represented by circles and transitions by squares.

Let us now recall the operational semantics of PA. Fix a PA A = P, T , ι for the remainder of this section. A state of this automaton is a set of places. In a given state S ⊆ P ,

a transition t = ◃ t, t ▹ is enabled if ◃ t ⊆ S.
→ A S i+1 for every i ∈ [1, n -1], S 1 = {ι} and S n = ∅.
A run of the PA from Fig. 4 is depicted in Fig. 5; this run gives rise to a graph, depicted in Fig. 6; see [START_REF] Brunet | Petri automata[END_REF]Def. 3] for a formal definition in the general case.

Definition 7 (Graph language of a PA). The graph language of a PA A , written G (A ), consists of the graphs of its runs.

PA are assumed to be safe (in standard Petri net terminology, places contain at most one token at any time-whence the definition of states as sets rather than multisets) and to accept only series-parallel graphs. These two conditions are decidable [START_REF] Brunet | Petri automata[END_REF]. Here we moreover assume that all PA have the same set of places P .

PA and KL --expressions denote the same class of graph languages:

18:6

Completeness for Identity-free Kleene Lattices Theorem 8 (Kleene theorem [START_REF] Brunet | Petri automata[END_REF]Thm. 18]).

e ∩ (f ∩ g) = (e ∩ f ) ∩ g e ∩ f = f ∩ e e ∩ e = e e ∩ (f + g) = (e ∩ f ) + (e ∩ g) e ∩ (e + f ) = e e + (e ∩ f ) = e e + (f + g) = (e + f ) + g e + f = f + e e + e = e e•(f •g) = (e•f )•g e•(f +g) = e•f +e•g (e+f )•g = e•g +f •g e+0 = e e•0 = 0 = 0•e e + e•e + = e + = e + e + •e e•f + f = f ⇒ e + •f + f = f f •e + f = f ⇒ f •e + + f = f
(i) For every expression e, there is a Petri automaton A such that G (e) = G (A ).

(ii) Conversely, for every Petri automaton A , there is an expression e such that G (e) = G (A ).

Axiomatisation and structure of completeness proof

Let us introduce now our axiomatisation.

Definition 9. The axioms of KL -are the union of the axioms of identity-free Kleene algebra (KA -) [START_REF] Kozen | Typed Kleene algebra[END_REF], and the axioms of a distributive lattice for {+, ∩}.

It is easy to check that those axioms are valid for binary relations, whence soundness of KL -:

Theorem 10 (Soundness). If KL -e ≤ f then Rel |= e ≤ f .
The rest the paper is devoted the converse implication, which thanks to Thm. 4 amounts to:

Theorem 11 (Completeness). If G(e) ⊆ G(f ) then KL -e ≤ f .
The following very weak form of Thm. 11 is easy to obtain from the results in the literature:

Proposition 1. For all terms u, v, G (u) G (v) entails KL -u ≤ v.
Proof. Follows from Thm. 4, completeness of semilattice-ordered semigroups [START_REF] Andréka | Representation of distributive lattice-ordered semigroups with binary relations[END_REF] for relational models, and the fact the the axioms of KL -entail those of semilattice-ordered semigroups.

As explained in the introduction, our first step consists in proving KL -completeness w.r.t. strict graph language inclusions, i.e., not modulo homomorphisms:

Theorem 12 (Completeness for strict language inclusions). If G(e) ⊆ G(f ) then KL -e ≤ f .
The proof is given in Sect. 4. Our second step is to get the following theorem (Sect. 6):

Theorem 13 (Synchronised Kleene Theorem). If A , B are PA such that G(A ) ⊆ G(B),
then there are expressions e, f such that:

G (A ) = G (e) , KL -e ≤ f , and G (f ) ⊆ G (B) .
The key observation for the proof is that the state-removal procedure used to transform a PA into a KL -expression is highly non-deterministic. When considering two PA at a time, one can use this flexibility in order to synchronise the computation of the two expressions, so that they become easier to compare axiomatically. The concrete proof is quite technical and requires us to first recall many concepts from the proof [START_REF] Brunet | Petri automata[END_REF] of Thm. 8(ii) (Sect. 5); it heavily relies on both Thm. 12 and Prop. 1.

Completeness of KL -follows using Thm. 8(i) and Thm. 12 as explained in the introduction.

Completeness for strict language inclusion

Recall that the graph language of an expression e, G(e), is defined as the set of graphs of the term language of e, e . We first prove that KL -is complete for term language inclusions:

Proposition 2. If e ⊆ f then KL -e ≤ f .
Proof. We follow a technique similar to the one recently used in [START_REF] Kozen | Completeness and incompleteness in nominal kleene algebra[END_REF]. We consider the maximal KA --subexpressions, and we compute the atoms of the Boolean algebra of word languages generated by those expressions. By KA -completeness [START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF][START_REF] Kozen | Typed Kleene algebra[END_REF], we get KA -(and thus KL -) proofs that those are equal to appropriate sums of atoms. We distribute the surrounding intersections over those sums and replace the resulting intersections of atoms by fresh letters. This allows us to proceed recursively (on the intersection-depth of the terms), using substitutivity to recover a KL -proof of the starting inequality.

The difference between the term language and the graph language is that intersection is interpreted as an associative and commutative operation in the latter. We bury this difference by defining a 'saturation' function s on KL --expressions such that for all e, ( †) KL -s(e) = e, and ( ‡)

s(e) = {u | G(u) ∈ G(e)} .
Intuitively, this function uses distributivity and idempotency of sum to replace all intersections appearing in the expression by the sum of all their equivalent presentations modulo associativity and commutativity. For instance, s(a ∩ (b ∩ c)) is a sum of twelve terms (six choices for the ordering times two choices for the parenthesing). Technically, one should be careful to expand the expression first by maximally distributing sums, in order to make all potential n-ary intersections apparent. For instance, ((a

∩ b) + d) ∩ c expands to ((a ∩ b) ∩ c) + (d ∩ c) so that
its saturation is a sum of twelve plus two terms. For the same reason, all iterations should be unfolded once: we unfold and expand (a

∩ b) + ∩ c into ((a ∩ b) ∩ c) + ((a ∩ b) • (a ∩ b) + ∩ c)
before saturating it. We finally obtain Thm. 12 using ( ‡), Prop. 2, and ( †):

G(e) ⊆ G(f ) ⇒ s(e) ⊆ s(f ) ⇒ KL -s(e) ≤ s(f ) ⇒ KL -e ≤ f 5

Kleene theorem for Petri automata

To prove the synchronised Kleene theorem (Thm. 13), we cannot use the Kleene theorem for PA (Thm. 8) as a black box: we use in a fine way the algorithm underlying the proof of the second item. We thus explain how it works [START_REF] Brunet | Petri automata[END_REF] in details.

Recall that to transform an NFA A to a regular expression e, one rewrites it using the rules of Fig. 8 until one reaches an automaton where there is a unique transition from the initial state to the final one, labelled by an expression e. While doing so, one goes through generalised NFA, whose transitions are labelled by regular expressions instead of letters.

18:8

Completeness for Identity-free Kleene Lattices

σ τ B ρ A C σ ρ A • B * • C → σ ρ A B σ ρ A ∪ B → Figure 8
Rewriting rules for state-removal procedure.

We use the same technique for PA: we start by converting the PA into a NFA over a richer alphabet, which we call a Template Automaton (TA), then we reduce this automaton using the rules of Fig. 8 until we get a single transition labelled by the desired expression.

To get some intuitions about the way we convert a PA into an NFA, consider the run in Fig. 5 and its graph in Fig. 6. One can decompose the run and the graph as follows: The graph can thus be seen as a word over an alphabet of 'boxes', and the run as a path in an NFA whose states are sets of places of the PA. The letters of the alphabet, the above boxes, can be seen as 'slices of graphs'; they arise naturally from the transitions of the starting PA (Fig. 4 in this example).

Template automata

In order to make everything work, we need to refine both this notion of states and this notion of boxes to define template automata:

states (sets of places) are refined into types. We let σ, τ range over types. A type is a tree whose leaves are labelled by places. When we forget the tree structure of a type τ , we get a a state τ . See [START_REF] Brunet | Petri automata[END_REF]Def. 10] for a formal definition of types, which is not needed here. We call singleton types those types whose associated state is a singleton.

letters will be templates: finite sets of boxes like depicted above but with edges labelled with arbitrary KL --expressions; we define those formally below.

Given a directed acyclic graph (DAG) G, we write min G (resp. max G) for the set of its sources (resp. sinks). A DAG is non-trivial when it contains at least one edge.

Definition 14 (Boxes). Let σ, τ be types. A box from σ to τ is a triple -→ p , G, ←p where G is a non-trivial DAG with edges labelled in Exp X , -→ p is a map from σ, the input ports, to the vertices of G, and ←p is a bijective map from τ , the output ports, to max G, and where an additional condition relative to types holds [START_REF] Brunet | Petri automata[END_REF]Def. 11]. (This condition can be kept abstract here.) A basic box is a box labelled with letters rather than arbitrary expressions.

A 1-1 box is a box between singleton types.

We let α, β range over boxes and we write β : σ → τ when β is a box from σ to τ .

We represent boxes graphically as in Fig. 15. Inside the rectangle is the DAG, with the input ports on the left-hand side and the output ports on the right-hand side. The maps -→ p and ←p are represented by the arrows going from the ports to vertices inside the rectangle. The key property enforced by the condition on types (kept abstract here) is the following:

Lemma 15. A 1-1 box is just a series-parallel 2-pointed graph labelled in Exp X .
Accordingly, one can extract a KL --expression from any 1-1 box β, which we write e (β) and call its expression.

Definition 16 (Templates).

A template Γ : σ → τ is a finite set of boxes from σ to τ . A

1-1 template is a template of 1-1 boxes. The expression of a 1-1 template, written e (Γ), is the sum of the expressions of its boxes.

Templates can be composed like boxes, by computing all pairwise box compositions. As expected, the box language of a template Γ : σ → τ only contains boxes from σ to τ .

Thanks to Lem. 15, when Γ is a 1-1 template, its box language can actually be seen as a set of graphs, and we have:

Proposition 3. For every 1-1 template Γ, we have B(Γ) = G (e (Γ)).
We can finally define template automata:

Definition 18 (Template automaton (TA)). A template automaton is an NFA whose states are types, whose alphabet is the set of templates, whose transitions are of the form σ, Γ, τ where Γ : σ → τ , and with a single initial state and a single accepting state which are singleton types. A basic TA is a TA whose all transitions are labelled by basic boxes.

By definition, a word accepted by a TA is a sequence of templates that can be composed into a single 1-1 template Γ, and thus gives rise to a set of graphs B(Γ). The graph language of a TA E , written G (E ), is the union of all those sets of graphs.

An important result of [START_REF] Brunet | Petri automata[END_REF] is that we can translate every PA into a TA: Proposition 4. For every PA A , there exists a basic TA E such that G (A ) = G (E ).

18:10

Completeness for Identity-free Kleene Lattices TA were defined so that they can be reduced using the state-removal procedure from Fig. 8.

Templates can be composed sequentially and are closed under unions, so that now we only miss an operation _ * on templates to implement the first rule. Since we work in an identityfree (and thus star-free) setting, it suffices to define a strict iteration operation _ + ; and to rely on the following shorthands ∆

• Γ * = ∆ ∪ ∆ • Γ + and Γ * • ∆ = ∆ ∪ Γ + • ∆.
Such an operation is provided in [START_REF] Brunet | Petri automata[END_REF]:

Proposition 5. There exists a function _ + on templates such that if the TA obtained from a PA A through Prop. 4 reduces to a TA E by the rules in Fig. 8, then G (A ) = G (E ). 1One finally obtains the Kleene theorem for PA by reducing the TA until it consists of a single transition labelled by a 1-1 template Γ: at this point, e (Γ) is the desired KL --expression.

Computing the iteration of a template

We need to know how the above template iteration can be defined to obtain our synchronised Kleene theorem, so that we explain it in this section. This section is required only to understand how we define a synchronised iteration operation in Sect. [START_REF] Angus | Kleene algebra with tests and program schematology[END_REF].

First notice that templates on which we need to compute _ + are of type σ → σ. We first define this operation for a restricted class of templates, which we call atomic. Notice that the bowtie of a box is not unique. For instance, the atomic box in Fig. 10 contains two bowties: the blue and the red nodes.

We compute the iteration of an atomic box as follows. First choose a bowtie for this box, then split it at the level of this node into the product α = β • γ. The box γ • β is 1-1, we can thus extract from it a term e (γ • β). We set α + to be the template consisting of α and the box obtained from α by replacing the bowtie by an edge labelled e (γ • β) + . For the sake of conciseness, we denote this two-box template as on the right below, with an edge labelled with a starred expression.

α = β γ α + = β γ e (γ • β) * Data: Atomic template Γ Result: A template Γ + s.t. B(Γ + ) = B(Γ) + if Γ = ∅ then Return ∅ else Write Γ = ∆ ∪ {α} ∪ Σ such that supp (∆) ⊆ supp (α) and supp (Σ) ∩ supp (α) = ∅;
Choose a bowtie for α; Split α into β • γ at the level of this bowtie;

Return (∆ + • Σ * ) ∪ (∆ * • Σ + ) ∪ (∆ * • δ • ∆ * • Σ * ),
where δ is the two-box template depicted on the right. end It is not difficult to see that B(α + ) = B(α) + . Depending on the bowtie we have chosen, the box α + will be different. This is why we will write α + to say that the bowtie has been selected for the computation of the iteration. Now we need to generalise this construction to compute the iteration of an atomic template. For this, we need the following property, saying that the supports of atomic boxes of the same type are either disjoint or comparable:

β γ e (γ • ∆ * • β) *
Lemma 21. For all atomic boxes β, γ : σ → σ, we have either 1) supp (β) ⊆ supp (γ), or

2) supp (γ) ⊆ supp (β), or 3) supp (β) ∩ supp (γ) = ∅.

We can compute the iteration of an atomic template by the algorithm in Fig. 11; intuitively, atomic boxes with disjoint support can be iterated in any order: they cannot interfere; in contrast, atomic boxes with small support must be computed before atomic boxes with strictly larger support: the iteration of the latter depends on that of the former. (Also note that since supp (∆) ⊆ supp (α) we have also supp (∆ + ) ⊆ supp (α) thus the template γ • ∆ * • β is 1-1 and it gives rise to an expression e (γ • ∆ * • β).)

We finally compute the iteration of an arbitrary template Γ : σ → σ as follows: from each connected component of the graph of each box in Γ stems an atomic box; let At(Γ) be the set of all these atomic boxes; we set Γ + = At(Γ) + .

The overall algorithm contains two sources of non-determinism. First, one can partially choose in which order to process the atomic boxes. This is reflected by the choice of the box α, which we will call the pivot. For instance if Γ = {α 1 , α 2 , β} such that supp (α 1 ) = supp (α 2 )

and supp (β) ∩ supp (α 1 ) = ∅, then we can choose either α 1 or α 2 as the pivot, and the computation will respectively start with the computation of α + 2 or that of α + 1 , yielding two distinct expressions. (In contrast, choices about boxes with disjoint support do not change the final result.) Second, every box of the template is eventually processed, and one must thus choose a bowtie for all of them. We write Γ + ,≤ to make explicit the choice of the bowties and the computation order.

18:12

Completeness for Identity-free Kleene Lattices 6 Synchronised Kleene theorem for PA

We can now prove Thm. 13. To synchronise the computation of two expressions e, f for two PA A , B respectively, we construct a synchronised product automaton E × F between a TA E for A and a TA F for B.

The states of this automaton are triples σ, η, τ where σ and τ are types, i.e., states from the TA E and F , and η : τ → σ is a function used to enforce coherence conditions.

Its transitions have the form σ, η, τ , Γ, ∆ , σ , η , τ where σ, Γ, σ is a transition of E , τ, ∆, τ is a transition of F , and Γ and ∆ satisfy a certain condition which we call refinement, written Γ ≤ ∆.

The overall strategy is as follows. We reduce E × F using the rules of Fig. 8, where the operations • and ∪ are computed pairwise. The operation _ * is also computed pairwise, but in a careful way, exploiting the non-determinism of this operation to ensure that we maintain the refinement relation. We eventually get a single transition labelled by a pair of Initialisation: define E × F so that refinement holds;

Stability:

show that the refinement relation is maintained during the rewriting process;

Finalisation: show that refinement between 1-1 templates entails KL -provability.

Refinement relation

We first generalise graph homomorphisms to templates; this involves dealing with multiple ports, with finite sets, and with edge labels which are now arbitrary KL --expressions. For the latter, we do not require strict equality but KL --derivable inequalities.

Definition 22 (Box and template homomorphisms). Let σ, τ, σ , τ be four types with two functions η : σ → τ and η :

σ → τ . Let β = - → p β , V β , E β , s β , t β , l β , ← -p β be a box of type τ → τ and let α = - → p α , V α , E α , s α , t α , l α , ← -p α be a box of type σ → σ . A homomorphism from α to β is a pair f, g of functions f : V α → V β and g : E α → E β s.t.: s β • g = f • s α , t β • g = f • t α , ∀e ∈ E α , KL -l β • g(e) ≤ l α (e), If {v} ⊆ V α is a trivial connected component, so is f (v). - → p β • η = f • - → p α and ← -p β • η = f • ← -p α . (We call this condition (η, η )-compatibility.)
We write β η,η α when there exists such a homomorphism. For two templates Γ : τ → τ and ∆ : σ → σ , we write Γ η,η ∆ if for all β ∈ Γ, there exists α ∈ ∆ such that β η,η α.

We abbreviate Γ η,η ∆ as Γ ∆ when Γ, ∆ are 1-1 templates, or when σ = τ , σ = τ and η, η are the identity function id. A box homomorphism is depicted in Fig. 12.

The above relation on templates is not enough for our needs; we have to extend it so that it is preserved during the rewriting process. We first write Γ ∆ when B(Γ) ⊆ B(∆), for two templates Γ, ∆ of the same type. Refinement is defined as follows:

Definition 23 (Refinement). We call refinement the relation on templates defined by

≤ η,η η,η • ( id,id ∪ ) *
, where _ * is reflexive transitive closure.

The following proposition shows that refinement implies provability of the expressions extracted from 1-1 templates. This gives us the finalisation step. Proof. When ∆ ⊆ Γ, it follows from Prop. 3 and Thm. 12; when ∆ Γ, it follows from Prop. 1. We conclude by transitivity. If T is a 2-TA, we denote by π 1 (T ) (resp. π 2 (T )) the automaton obtained by projecting the alphabet, the states and the transitions of T on the first (resp. last) component. Note that π 1 (T ) and π 2 (T ) are TA.

Synchronised product automaton (initialisation)

Definition 25 (Synchronised product of TA). Let E , F be two TA. The synchronised product of E and F , written E × F is the 2-TA where τ, η, σ , Γ, ∆ , τ , η , σ is a transition of

E × F iff τ, Γ, τ is a transition of E , σ, ∆, σ is a transition of F and Γ ≤ η,η ∆. (And
with initial and accepting states defined from those of of E and F .)

Note that we enforce refinement in the definition of this product, so that

π 1 (E × F ) is a sub-automaton of E and π 2 (E × F ) is a sub-automaton of F . Thus G (π 1 (E × F )) ⊆ G (E ) and G (π 2 (E × F )) ⊆ G (F ). When E , F are TA coming from PA A , B such that G (A ) ⊆ G (B)
, we can use the results from [START_REF] Brunet | Petri automata[END_REF] about simulations to strengthen the first inclusion into an equality:

Theorem 26. Let A , B be two PA, E , F be basic TA such that G (A ) = L(E ) and
G (B) = L(F ) (given by Prop. 4). If G (A 1 ) ⊆ G (A 2 ) then: G (π 1 (E × F )) = G (A ); G (π 2 (E × F )) ⊆ G (B).

18:14

Completeness for Identity-free Kleene Lattices

Proof. The second point follows from the observation above. The first one comes from the simulation result ([11, Prop. 9.10]) for PA. Indeed, if G (A ) ⊆ G (B), then there is a simulation ([11, Def. 9.2]) between A and B. This implies that for every run τ 1 , Γ 1 , τ 2 , . . . , Γ n-1 , τ n of E , there is a run σ 1 , ∆ 1 , σ 2 , . . . , ∆ n-1 , σ n of F and a set of mapping η i :

σ i → τ i , i ∈ [1, n] such that Γ i ηi,ηi+1 ∆ i for every i ∈ [1, n -1].

Maintaining refinement during reductions

Let us finally show that refinement is stable by composition, union, and iteration.

Theorem 27 (Stability of refinement by • and ∪).

If Γ 1 ≤ η,η Γ 2 and ∆ 1 ≤ η ,η" ∆ 2 then Γ 1 • ∆ 1 ≤ η,η" Γ 2 • ∆ 2 . If Γ 1 ≤ η,η Γ 2 and ∆ 1 ≤ η,η ∆ 2 then Γ 1 ∪ ∆ 1 ≤ η,η Γ 2 ∪ ∆ 2 .
Proof. To show the first property it suffices to show the following results:

If Γ 1 η,η Γ 2 and ∆ 1 η ,η Γ 2 then Γ 1 • ∆ 1 η ,η Γ 2 • ∆ 2 . (L 1 ) If Γ 1 Γ 2 and ∆ 1 ∆ 2 then Γ 1 • ∆ 1 Γ 2 • ∆ 2 . (L 2 ) If Γ 1 Γ 2 and ∆ 1 ∆ 2 then Γ 1 • ∆ 1 ( • ) * Γ 2 ∪ ∆ 2 . (L 3 ) To show (L 1 ), consider a box α 1 ∈ Γ 1 and β 1 ∈ ∆ 1 . By hypothesis, there is a box α 2 ∈ Γ 2
and an (η, η )-compatible homomorphism h = f, g from α 2 to α 1 and a box β 2 ∈ ∆ 2 and an (η , η )-compatible homomorphism h = f , g from β 2 to β 1 . Let h = f , g , where f equals f in dom (f ) and f in dom (f ), and g" equals g in dom (g) and g in dom (g ).

Using (η, η )-compatibility of h and (η , η )-compatibility of h , it is easy to show that h is an (η, η )-compatible homomorphism from α 2 • β 2 to α 1 • β 1 , which concludes the proof of (L 1 ). (L 2 ) follows easily from the definition of . For (L 3 ), note that ∆ 1 ∆ 1 (we choose the identity homomorphism), thus by (L 1 ), we have that

Γ 1 • ∆ 1 Γ 2 • ∆ 1 . By (L 2 ), we have that Γ 2 • ∆ 1 Γ 2 • ∆ 2 , which concludes the proof.
To show the first property, we proceed by induction on the length of the sequences justifying that Γ 1 ≤ η,η Γ 2 and ∆ 1 ≤ η ,η" ∆ 2 , using (L 1 ), (L 2 ) and (L 3 ) for the base cases.

To show the second property, we follow the same proof schema, showing results similar to (L 1 ) -(L 3 ) where • is replaced by ∪.

Remark. Thm. 27 justifies our definition of ≤ η,η . Indeed, a more permissive definition would seem natural, but the first property of Thm 27 would fail. For instance, if

Γ 1 Γ 2 and ∆ 1 η,η ∆ 2 , we do not have in general that Γ 1 • ∆ 1 ≤ η,η Γ 2 • ∆ 2 .
The main theorem of this section is Thm 28, stating that the refinement relation is stable under iteration.

Theorem 28 (Stability of refinement by _ + ). If Γ ≤ η,η ∆ then there are bowtie choices , and computation orders , , for Γ and ∆ respectively, such that:

Γ + , ≤ η,η ∆ + , .
Proof. To prove Thm. 28, it is enough to show the following properties.

If Γ ∆ then, for every bowtie choices , , and every computation orders , for Γ and ∆ respectively, we have that Γ + , ∆ + , .

If Γ η,η ∆ then there are two bowtie choices , and two computation orders , , for Γ and ∆ respectively, such that Γ + , ≤ η,η ∆ + , .

The first property follows from B(Γ + , ) = B(Γ) + for every bowtie choice and order .

For the sake of clarity, we give here the proof of the second proposition in the case where Γ and ∆ are singletons of atomic boxes {α} and {β} respectively. The general case is treated in App. B. Let , be bowtie choices for α and β respectively, and let h = f, g be a homomorphism from β to α.

Let us first treat the case where f -1 ( ) = { } (we say that α, β are bowtie compatible). This is illustrated by the boxes α, β of Fig. 13, where the bowties are the red nodes. and β + are depicted in Fig. 13. Let us show that there is a homomorphism from β + to α + .

The homomorphism h induces a homomorphism h 1 from β 1 to α 1 and a homomorphism h 2 from β 2 to α 2 (Lem. 42 in App. B). Combining h 1 and h 1 , we get almost a homomorphism from β + to α + (See Fig. 13), we need only to show that KL -e ≤ f . But this follows from Prop. 6: indeed, we can combine h 1 and h 2 to get a homomorphism from

β 2 • β 1 to α 2 • α 1 .
We have thus that α + η,η β + ((η, η)-compatibility is easy).

Let us now treat the case where N := f -1 ( ) is not necessarily { } (N is illustrated by the red node of β in Fig. 14). Let γ be the box obtained from β by merging the nodes N (see Fig. 14). There are two bowtie choices for γ: a bowtie b inherited from β (blue in Fig. 14) and a bowtie r coming from the nodes of N (red in Fig. 14).

Let h be the homomorphism from β to γ that maps each node (and each edge) to itself, except for the nodes of N which are mapped to r . If we consider the bowtie b for γ, then β and γ are bowtie compatible w.r.t. to h , thus γ + b β + using the previous case.

Let h be the homomorphism from γ to α, which is exactly h except that it maps the node r to the bowtie of α. If we consider the bowtie r for γ, then γ and α are bowtie compatible w.r.t. h , thus α + η,η γ + r using the previous case again.

Notice finally that γ + r γ + b . To sum up, we have:

α + η,η γ + r γ + b β + .
The last case in this proof explains the need to work with refinement (≤) rather than just homomorphisms ( ): when starting from templates that are related by homomorphism and iterating them, the templates we obtain are not necessarily related by a single homomorphism, only by a sequence of homomorphisms and inclusions.

Future work

We have proven that KL -axioms are sound and complete w.r.t. the relational models of identity-free Kleene lattices, and thus also w.r.t. their language theoretic models, by the results from [START_REF] Andréka | The equational theory of Kleene lattices[END_REF].

Whether one can obtain a finite axiomatisation in presence of identity remains open.

This question is important since handling the identity relation is the very first step towards handling tests, which are crucial in order to model the control flow of sequential programs precisely (e.g., as in Kleene algebra with tests [START_REF] Kozen | Kleene algebra with tests[END_REF]).

A Iteration of a template

In this section, we address in detail the definitions relative to the construction of the iteration of a template.

We have seen that there are two sources of non-determinism when computing the iteration of a template (Algorithm 11). The first is the bowtie choice and the second is the computation order. Let us introduce them more precisely.

A.1 Bowtie choice for a template

We have seen in Sec. 5.2 that the non-trivial connected component of an atomic box can be associated with a specific node called its bowtie (Lem.20). We do the same for non atomic boxes.

A.2 Computation order

Let us analyse computation order of algorithm 11 in the simple case where Γ = {α, β}. If supp (α) β then the algorithm starts necessarily by processing α. If supp (α)∩supp (β) = ∅, then the order in which the computation proceeds does not matter, and we will get the same result no matter if we start with processing α or β. The only case where we have a freedom to choose the computation order, and in which this order may affect the result is when supp (α) = supp (β). In general, to specify the computation order, it is enough to order the elements of Γ having the same support.

Definition 33 (Computation order). A computation order for an atomic template Γ is a partial order on its elements such that if α β then supp (α) = supp (β).

A.3 Atomic template of a template

To compute the iteration of a template, we start by decomposing its boxes into atomic ones.

Definition 34 (At(Γ)). Let β : σ → σ be a box. From each C ∈ C(β) stems an atomic box of the same type having C as a connected component. We set At(β) to be the set of atomic boxes stemming from its connected components.

If Γ : σ → σ is a template we write At(Γ) for the set of boxes stemming from the connected components of the boxes of Γ.

For instance, the boxes of Figure 16 are the boxes stemming from the connected components of the box of Figure 15.

Remark. Note that every bowtie choice for Γ induces a bowtie choice for At(Γ).

Definition 35. A computation order for a template Γ is a computation order for At(Γ).

A.4 The iteration algorithm

Fig. 18 shows the algorithm computing the iteration of an atomic template, parameterised by a bowtie choice and a computation order.

If is a bowtie choice and is a computation order for Γ, we set Γ + , := At(Γ) + , .

B Stability of ≤ under iteration

In the whole section, we will work under the following proviso: Proviso 1. We suppose that all templates are of type τ → τ and that all the box and template homomorphisms are (η, η)-compatible, where τ is a fixed type and η : τ → τ a fixed mapping. We will not write explicitly η,η for (η, η)-compatible homomorphisms but simply

- → p (x) = [n] if - → p (x) = n and ← -p (x) = [n] if ← -p (x) = n.
Definition 39 ( 2 ). Let α, β be two boxes. We set α 2 β if there is a bowtie choice In other words, α 2 β if α is obtained by "merging" the bowties of two connected components of β. Figure 20 show two boxes α, β such that α 2 β.

To show that can be decomposed into 1 and 2 (Prop. 7), we need the following lemma, which says that the converse image of a connected component by a homomorphism is a collection of connected components.

Lemma 40. Let α, β be two boxes and h be a box homomorphism from β to α. For every

C ∈ C(α), there is a set {C 1 , . . . , C n } ⊆ C(β) such that h -1 (C) = C 1 ∪ • • • ∪ C n .
Proof. Let C ∈ C(α). By contradiction suppose that there is a connected component C ∈ C(β) and two nodes x, y ∈ C such that x, a, y is a vertex of the graph of α, h(x) ∈ C and h(y) / ∈ C. Since h is a homomorphism, we have that there is a vertex in the graph of β between h(x) and h(y), thus h(y) ∈ C. This gives us a contradiction.

Let us show now that we can indeed decompose into 1 and 2 .

Proposition 7. We have that ⊆ ( 1 ∪ 2 ) + , where the operation _ + is the transitive closure on relations. Proof. Let us show that if Γ ∆ then there is Σ 1 , . . . , Σ n such that Σ 1 = Γ, Σ n = ∆ and for every i ∈ [1, n -1] either Σ i 1 Σ i+1 or Σ i 2 Σ i+1 . For that, we proceed by induction on the size of Γ.

Let α ∈ Γ and set Σ = Γ \ {α}. Since Γ ∆, there is a box β ∈ ∆ such that α β.

Let h be a homomorphism from β to α and let , be two bowtie choices for α and β respectively.

Let us show first that there are two boxes γ and δ such that α 1 γ, γ + 2 δ and δ 1 β. We The box δ has two possible bowtie choices: one inherited from the bowtie of β (the black bowties of δ in Figure 21) and another coming from the nodes b(C, C ) that have being merged (the red and the blue bowties for δ in Figure 21). We call the former 1 and the later 2 .

If we take 1 as a bowtie choice for δ, then we have easily that δ 1 β.

β C = δ C • σ C β D = δ D • σ D α C•D = δ C•D • σ C•D

  inequality in the corresponding theory is Rel |= (a ∩ c) • (b ∩ d) ≤ (a • b) + ∩ (c • d): when a, b, c, d are interpreted as arbitrary binary relations, we have (a ∩ c) • (b ∩ d) ⊆ (a • b) + ∩ (c • d).

a) a Figure 1 Figure 2

 a12 Figure 1 Operations on graphs.

  t. : S {G | G G , G ∈ S}. We obtain: Theorem 4 ([10, Thm. 6]). For all expressions e, f , Rel |= e ≤ f iff G (e) ⊆ G (f ).

Figure 5 Figure 6

 56 Figure 3 A graph homomorphism.

Figure 7

 7 Figure7KL -: the first three lines correspond to distributive lattices, the last three to KA -.

Figure 9 Figure 10

 910 Figure 9 Two boxes and their composition.

Definition 17 (

 17 Box language of a template). A basic box is generated by a box β if it can be obtained by replacing each edge x e --→ y of its DAG by a graph G ∈ G (e) with input vertex x and output vertex y. The box language of a template Γ, written B(Γ), is the set of basic boxes generated by its boxes.

Definition 19 (

 19 Atomic boxes and templates, Support). A box β = -→ p , G, ←p : σ → σ is atomic if its graph has a single non-trivial connected component C, and if for every vertex v outside C, there is a unique port p ∈ σ such that -→ p (p) = ←p (p) = v. An atomic template is a template composed of atomic boxes. The support of a box β : σ → σ is the set supp (β) p -→ p (p) = ←p (p) . The support of a template is the union of the supports of its boxes. The following property of atomic boxes, makes it possible to compute their iteration: Lemma 20 ([11, Lem. 7.18]). The non-trivial connected component of an atomic box β : σ → σ always contains a vertex c, s.t. for every port p mapped inside that component, all paths from -→ p (p) to a maximal vertex visit c. We call such a vertex a bowtie for β.

Figure 11

 11 Figure 11Iteration of an atomic template.

1- 1

 1 templates Γ and ∆ such that B(Γ) = G (A ), B(∆) = G (B), and Γ ≤ ∆. To conclude, it suffices to deduce KL -e (Γ) ≤ e (∆) from the latter property. To sum-up, what we need to do now is: Refinement: define the refinement relation ≤ on templates;

Figure 13 Figure 14 Proposition 6 .

 13146 Figure 12 A box homomorphism.

24 ( 2 -

 242 Template automata (2-TA)). A 2-template automaton is an NFA whose states are tuples of the form τ, η, σ where τ, σ are types and η : σ → τ , whose alphabet is the set of pairs of templates, whose transitions are of the form σ, η, τ , Γ, ∆ , σ , η , τ where Γ : σ → σ , ∆ : τ → τ , and Γ ≤ η,η ∆, and with a single initial state and a single accepting state which consist of singleton types.

  If we decompose α and β at the level of their bowties, we get α = α 1 • α 2 and β = β 1 • β 2 , where α 2 • α 1 and β 2 • β 1 are 1-1 boxes. We write e = e (α 2 • α 1 ) and f = e (β 2 • β 1 ). The boxes α +

Figure 15 Figure 16

 1516 Figure 15 Example of a box.

Figure 17

 17 Figure 17 Decomposition of an atomic box.

Figure 19 Figure 20

 1920 Figure 19 Boxes α, β such that α 1 β.

  for β and C, D ∈ C(β) such that when we set N = { (C), (D)} we have α = β| ≡{N } . If Γ, ∆ are templates, we set Γ 2 ∆ if Γ = Σ ∪ {α} and ∆ = Σ ∪ {β} such that α 2 β.

Figure 21

 21 Figure 21 Decomposing α β into α 1 γ, γ + 2 δ and δ 1 β.

  will illustrate the construction of γ and δ by Figure 21. In this figure, α has two connected components C and D, and β has three connected components C 1 , C 2 and D 1 such that h(C 1 ∪ C 2 ) = C and h(D 1 ) = D. The bowtie choices for α and β are illustrated by the nodes in the middle of each connected component.Let us construct δ. By Lem. 40, we know that for every connected componentC of α, h -1 (C) = C 1 ∪ • • • ∪ C n where C i ∈ C(β). We set C -1 = {C 1 , . . . , C n }. For every C ∈ C -1 we set: b(C, C ) = h -1 ( (C)) ∩ C Let δ = β| ≡{b(C,C ) | C∈C(α),C ∈C -1 } . As illustrated by Figure21, δ is obtained from β by merging in every connected component the nodes that are mapped to a bowtie of α by h.

  connected components, and coincide. We extend and to bowtie choices for Γ and ∆. Let β C , β D and α C•D be the atomic boxes stemming respectively from the connected component C, D and C•D. Observe that we can write At(Γ) and At(∆) as At(Γ) = Θ∪{α C•D } and At(∆) = Θ ∪ {β C , β D }. Let be a template order on At(Γ) for which α C•D is minimal. Let be a template order on At(∆) for which β C and β D are maximal elements. We set Γ C = {δ | δ ∈ Θ, supp (δ) ⊆ supp (α C )} and Γ D = {δ | δ ∈ Θ, supp (δ) ⊆ supp (α D )}. The computation of At(Γ) + , starts with the computation of (Γ C ∪Γ D ∪{α C•D }) + , and that of At(∆) + , starts with the computation of (Γ C ∪ Γ D ∪ {β C , β D }) + , . Both carry on in exactly the same way, using respectively (Γ C ∪Γ D ∪{α C•D }) + , and (Γ C ∪Γ D ∪{β C , β D }) + , as black-boxes. It is thus enough to show that:(Γ C ∪ Γ D ∪ {α C•D }) + , ≤ (Γ C ∪ Γ D ∪ {β C , β D }) + ,We decompose β C , β D and α C•D as follows (See Figure22):

  on the elements of Θ, we will write Γ + C (resp. Γ + D )for the iteration of Γ C (resp. Γ D ) under the bowtie choice and the template order or under the bowtie choice and the template order .Since supp(Γ C ) ∩ supp (Γ D ) = ∅, we have that Γ + C • Γ + D = Γ + D • Γ + C ,we denote this product simply by Γ + C•D . We have also that:(Γ C ∪ Γ D ∪ {α C•D }) + , = Γ + C•D ∪ (Γ * C•D • α + C•D • Γ * C•D ) (Γ C ∪ Γ D ∪ {β C , β D }) + , ⊇ Γ + C•D ∪ (Γ * C•D • β + C • β + D • Γ * C•D )Where α + C•D and β + C • β + D are the boxes depicted in Figure 23. It is not difficult to see that α + C•D β + C • β + D , whence the result.

  Remark. When β is atomic, it has only one connected component, so we may identify the bowtie choice that maps this component to a node, with the node itself. Consider the box of Figure15. It has two connected components. The first has two bowtie choices: the red and the green node. The second has only one bowtie choice, the blue node.

	Definition 29 (Connected component of a box). If β = -→ p , G, ← -p is a box, we denote
	by C(β) the set of non-trivial connected components of G, which we call simply connected
	component of β.
	Lemma 30 (Bowtie lemma [11, Lem. 7.1]). Let B = -→ p , G, ← -p be a box of type τ → τ . For every C ∈ C(β) there is a vertex c such that for every port p where -→ p (p) ∈ C, all paths from -→ p (p) to a maximal vertex of C visit c. We call such a vertex a bowtie for C.
	Example 32. Notation 1. If α is an atomic box and	is a bowtie choice for α, then we can decompose

Definition 31 (Bowtie choice for a template). A bowtie choice for a box is a function mapping a bowtie to every connected component.

A bowtie choice for a template is a function mapping a bowtie to every connected component of every box.

α at the level of this bowtie to get two boxes such that α = α 1 • α 2 . We write α = α 1 • α 2 for this decomposition. In Fig.

17

, the box α can be decomposed at the level of its bowtie (the blue node) into α 1 and α 2 .

This statement is not simpler because, unfortunately, there is no function _ + on templates such that B(Γ + ) = B(Γ) + ).

Funding This work has been funded by the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157). This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR). * Full version of the extented abstract in Proc. CONCUR

Data: Atomic template Γ, a bowtie choice and a computation order for Γ Result: A template Γ + , such that B(Γ + , ) = B(Γ) + if Γ = ∅ then Return ∅ else Write Γ = ∆ ∪ {α} ∪ Σ such that supp (∆) ⊆ supp (α), ∀α ∈ ∆ if supp (α) = supp (α) then α α, and supp (Σ) ∩ supp (α) = ∅; Set := (C), where C(α) = {C}.

where δ is the two-box template depicted on the right. end . All the theorems, propositions, lemmas of this section hold under this proviso, which will not be mentioned explicitly in their statements.

In this section, we will show the following theorem: Theorem 36. If ∆ Γ then there are two bowtie choices , for ∆ and Γ respectively, and two computation orders , for ∆ and Γ respectively such that: ∆ + , ≤ Γ + , .

To prove theorem 36, we will show that template homomorphisms can be decomposed into simpler template homomorphisms 1 and 2 (Def. 37, Def. 39, Prop. 7). It is thus enough to show Thm. 36 in the case where ∆ 1 Γ and ∆ 2 Γ, these results are precisely Prop. 8

and Prop. 9.

B.1 Decomposing into 1 and 2

Let us first define the template homomorphisms 1 and 2 .

Definition 37 ( 1 ). Let α, β be two boxes. We set α 1 β if there are bowtie choices , for α and β respectively, and a box homomorphism h from β to α such that:

If Γ, ∆ are templates, we set Γ 1 ∆ if for every α ∈ Γ, there is β ∈ ∆ such that α 1 β.

Figure 19 shows two boxes α, β such that α 1 β. Indeed, the blue connected component of β and its bowtie are mapped to the blue connected component of α and its bowtie. The same holds for the red connected component.

To define the homomorphism 2 , we need to define formally the operation of "merging" (or "identifying") nodes in a graph.

Let us construct γ now. We set -1 (C) = h -1 ( (C)). Note that we have

In If we consider the bowtie choice of α and the bowtie choice 3 of γ induced by merging the nodes -1 (C) of β (The red node of γ in Figure 21), it is easy to see that α 1 γ.

Let us make a final observation before showing the general result. Notice that if B, B are two boxes, and Θ is a template, then

Let us go back to the proof of our result. Recall that Γ = Σ {α}, that β ∈ ∆, and that

Proof. To show this result, let us make first the following observation. If α, β are atomic boxes such that α β then:

Let us see why this observation holds. We set α = -→ p α , G, ←p α and β = -→ p β , H, ←p β , and let h be a homomorphism from β to α.

Suppose by contradiction that there is p ∈ supp (β) such that η(p) / ∈ supp (α). We

Let us go back to the proof of our lemma. Suppose that supp (α 1 ) ⊆ supp (α 2 ) and let p ∈ supp (β 1 ). By the observation above, we have that η(p) ∈ supp (α 1 ) thus η(p) ∈ supp (α 2 ).

By the above observation again, we have η(p) ∈ supp (α 2 ).

18:24

Completeness for Identity-free Kleene Lattices

Suppose that p ∈ supp (β 1 ) ∩ supp (β 2 ). By the above observation, we have that η(p) ∈ supp (α 1 ) ∩ supp (α 2 ).

Lemma 42. Let α, β be two atomic boxes and h be a homomorphism from β to α. Let , be bowtie choices for α, β, and let

Proof. We show that the homomorphism h induces a homomorphism from β i to α i , for i = 1, 2. For that we only need to show that h maps the graph of β 1 to the graph of α 1 and maps the graph of β 2 to the graph of α 2 . In other words, for i = 1, 2:

Suppose (by symmetry) that there is a node n of

There is a path from n to in the graph of β. This path can be mapped by h to a path from h(n) to in the graph of α. This is not possible by well-typedness of the α.

Let us show now Prop. 8. Let , be the bowtie choices for Γ and ∆ respectively, witnessing that Γ 1 ∆. We set Γ = {α 1 , . . . , α n }. Since Γ ∆, we have that for every i ∈ [1, n], there is

Proof of

Let be a template order for Γ. Let us define a template order for Σ. Note that if supp (β i ) = supp (β j ), by Lem. 41 we cannot have supp (α i ) ∩ supp (α j ) = ∅, thus by Lem. 21, either supp (α i ) ⊆ supp (α j ) or supp (α j ) ⊆ supp (α i ). We set define as follows:

or supp (α i ) = supp (α j ) and α i α j

Let us show now, by induction on Γ, that Γ + , ≤ Σ + , . We decompose Γ into Γ 1 ∪{α m }∪Γ 2 such that:

Let us show that this decomposition of Σ is relevant for the computation of its iteration, in particular that β m can be chosen as a pivot.

(By item 1 above and Prop. 41)

(By item 3 above and Prop. 41).

To compute the iteration of Γ and Σ, we decompose the pivots α m and β m at the level of their bowtie choices:

A. Doumane and D. Pous 18:25

Boxes α, β in the proof of Prop. 9 If we set Γ + i = (Γ i ) + , and Σ + i = (Σ i ) + , , for i = 1, 2 then we have:

Where α m + are and β m + are the following boxes.

(e (δ2

1 and σ 1 δ 1 ). We can thus conclude by Prop. 6.

B.3 2 is stable under iteration