Celia Picard

Ralph Matthes

Permutations in Coinductive Graph Representation

) coinductive types are mixed with inductive ones. Still, a formal development has been carried out in Coq, by using its built-in language for proof automation. Another extension of the original bisimulation relation based on cycle analysis provides indifference concerning the root node of the term graphs.

Introduction

In [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF], we have developed a complete solution to overcome guardedness issues regarding programming and subsequent verification with embedded lists in a coinductive type in the proof assistant Coq [START_REF]The Coq Development Team: The Coq Proof Assistant Reference Manual[END_REF], with the aim of graph representation (we represent single-rooted, connected graphs). In the present article, we present a more versatile bisimulation relation over those graphs than the one studied in [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF] that naturally followed from the obtained coinductive representation of graphs.

First of all, we give a brief summary of the main notions introduced in [16] that will be needed for the rest of the article. Although all of this reports on formalization work that has been carried out in Coq, we refrained from displaying Coq syntax (the Gallina language) or even of its underlying type theory -the calculus of inductive and coinductive constructions (CIC). We try to adopt standard mathematical or standard type-theoretical notation as much as possible. In case of doubt what the exact correspondence is with the CIC/Coq, we invite the reader to refer to our full proofs [START_REF] Picard | Formalization in Coq for this article[END_REF].

1.1 Summary of the Notions Introduced in [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF] The goal we were aiming at was coinductive graph representation. We explained that we needed a structure that would mimic lists without being inductive (this was necessary because of Coq's guardedness condition (see [START_REF] Bertot | Using structural recursion for corecursion[END_REF] and [START_REF] Giménez | A tutorial on [co-]inductive types in Coq[END_REF]) which is based on a productivity criterion (see [START_REF] Coquand | Infinite objects in type theory[END_REF])). Therefore, we decided to use functions (this idea has also been mentioned by Chlipala in [START_REF] Chlipala | Coq club thread "is Coq being too conservative?[END_REF]). The domain of definition of those functions is a set of n elements, n being the length of the list we want to mimic. It is defined inductively through the two following constructors: Definition 1 (Fin, Viewed Inductively).

n : N first n : Fin(n + 1)

n : N i : Fin n succ i : Fin(n + 1)
This definition has also been used by Altenkirch in [START_REF] Altenkirch | A formalization of the strong normalization proof for system F in LEGO[END_REF] and by McBride and McKinna in [START_REF] Mcbride | The view from the left[END_REF]. By construction, Fin n is a type with precisely n elements. It actually corresponds to the container view of lists [START_REF] Prince | Proving properties about lists using containers[END_REF].

Remark 1 (Notations). In the rest of the paper we will use the following notations:

-T, U for types and t (resp. u) for elements of type T (resp. U ), n, m and k for elements of N, l and q for lists and elements of ilist ("indexed lists"), to be defined below, f for functions, g for elements of Graph, to be defined below, -R for binary (endo-)relations: a relation on T has type T → T → Prop, with → right-associative (as always in this paper) and Prop the Coq universe of propositions (in standard mathematics, one would just have the two truth values in Prop, and the informal semantics of relations is the standard one, but the application notation R t 1 t 2 is used instead of R(t 1 , t 2 ) in standard mathematics), i for elements of Fin n, if a relation S depends on a relation argument R, we say that R is the base relation of S R , and that S preserves equivalence if, for every equivalence relation R, S R is an equivalence relation (likewise with reflexivity, symmetry and transitivity alone).

The type of functions that mimics lists of length n is defined as follows:

Definition 2. ilistn T n := Fin n → T However, this is not yet satisfactory as ilistn still has the length parameter n while lists do not -it is inherent to them. Therefore, we define the following structure consisting of the length and a function in the corresponding ilistn: Definition 3. ilist T := Σn : N. ilistn T n Σ denotes a strong sum type (of pairs where the type of the second component depends on the first component). Consequently, the elements of ilist T are written as pairs n, ln with ln of type ilistn T n. We call the associated projection functions lg and fct, i. e., lg n, ln = n and fct n, ln = ln. One can show that ilist is in pointwise bijection with lists that are preloaded from the standard library in Coq (to do so, we use two conversion functions ilist2list and list2ilist and show that their compositions are pointwise equal to the identity -since Coq lacks functional extensionality, this does not imply equality with the identity).

Remark 2. In the container view, n corresponds to the shape of the container, and Fin n to the type of positions (an element of Fin n is a position).

We need to lift relations on T to relations on ilist T expressing that the base relation holds element-wise. In our intended use, the type T will be the coinductive type for graphs on which Leibniz equality -the propositional equality = of Coqcannot be used. We define the following generic operation ilist rel :

Definition 4 (ilist rel ). ∀l 1 l 2 : ilist T, ilist rel R l 1 l 2 ⇔ ∃h : lg l 1 = lg l 2 , ∀i : Fin(lg l 1 ), R (fct l 1 i) (fct l 2 i h )
where i h is the result of converting i to type Fin(lg l 2 ) using hypothesis h.

This conversion is needed since the theoretical basis of Coq -the CIC -is an intensional type theory, where equal types cannot enter the type-checking process more deeply than equal terms, i. e., if a term t has type A and one can prove A = B, the term t does not have type B, but there is a construction taking t and yielding an inhabitant of B. For more details about the pattern matching feature that allows us to make this type conversion in Coq, see [START_REF]The Coq Development Team: The Coq Proof Assistant Reference Manual[END_REF]Chap. 1.2.13 and 4.5.4]. In this paper, we do not expose the technical issues with type conversion that have to be mastered in the reasoning involving ilist rel . We define the type of graphs of interest in our paper through the constructor:

Definition 5 (Graph, Viewed Coinductively). t : T l : ilist(Graph T ) mk Graph t l : Graph T
Coinductive types in Coq are written with their constructors, just as for inductive types although categorical duality would suggest to define coinductive types by their destructors (projection functions). The constructor-based format is usually preferred for programming purposes. In order to distinguish the constructorbased view of coinductive definitions from inductive definitions, we put a double line in the inference rules. This notation is also used in [START_REF] Nakata | A proof pearl with the fan theorem and bar induction -walking through infinite trees with mixed induction and coinduction[END_REF]. Call label and sons the two projection functions on Graph, i. e., label (mk Graph t l) = t and sons(mk Graph t l) = l. They correspond to the unfolding of the greatest fixed point and are more basic than the constructors in coalgebraic approaches.

Had we used lists instead of ilist, we would have had an embedded inductive type in a coinductive type, with all the problems of guardedness as described in [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF]. However, another approach to solve the same kind of problem in Coq has been proposed by Dams in [START_REF] Dams | Coq club thread "is Coq being too conservative?[END_REF], where the embedded inductive type is even extended to a coinductive one. This solution seems to be quite heavy to manipulate as there are a lot of proofs to carry out. Niqui in [START_REF] Niqui | Coalgebraic reasoning in Coq: Bisimulation and the lambda-coiteration scheme[END_REF] and Bertot and Komendantskaya in [START_REF] Bertot | Using structural recursion for corecursion[END_REF] propose solutions also for a coinductive embedded type (and not an inductive one). The latter solution is quite close to ours, but on streams instead of lists, and hence without the need to restrict to a finite domain. For the finite domain, we chose Fin n, and thus "objects" n enter types and we are forced to use techniques of dependently-typed programming. Moreover, we have to quantify existentially over n, and this constructively, as is done with the Σ-type.

The same kind of issues also appears in other proof assistants, e. g., in Agda1 , even though it has recently seen quite some progress in its termination checker. In [START_REF] Danielsson | Beating the productivity checker using embedded languages[END_REF] Danielsson describes an experimental solution to solve them (see also the extended case study with Altenkirch in [START_REF] Danielsson | Subtyping, declaratively[END_REF]). This extension by datatypes that may have both inductive and coinductive constructors is still experimental. In Coq, this is just not available.

We lift relations R on T to relations Geq R on Graph T in a generic manner:

Definition 6 (Geq, Viewed Coinductively).

g 1 g 2 : Graph T R (label g 1 ) (label g 2 ) ilist rel Geq R (sons g 1 ) (sons g 2 ) Geq R g 1 g 2
It becomes apparent that ilist rel R had to be defined for arbitrary relations, not only Leibniz equality. Preservation of equivalence by ilist rel cannot suffice to prove that Geq preserves equivalence, but still, preservation holds [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF]. With Geq, we are forced to give an order to the nodes, horizontally and vertically, while in a classical set-theoretic graph representation, there is no such order. We aim at obtaining the more liberal equivalence of the classical representation on our constructive representation, e. g., we want the graphs of Fig. 1 or of Fig. 2 to be considered equivalent. However, with respect to Geq, they are not (here and in all further examples, we implicitly use Leibniz equality = as the base relation). Indeed, their nodes are not in the same order. In the case of Fig. 1, the children of the root are inverted in the two graphs (different "horizontal" order). In Fig. 2 the second graph has been turned by 180°(different "vertical" order). The new equivalence relation should solve the two cases illustrated by Fig. 1 and Fig. 2. The first one corresponds to a permutation between the children of an element of Graph. Thus, this corresponds also to a new equivalence relation on ilist (that indicates that two elements of ilist are permutations of each other). The second one corresponds to a change in the point of view of the observation of the graph. This paper presents the development of these new relations. In Sect. 2 we present and compare various ways to represent permutations on ilist. Sect. 3 uses our favourite one to define relation GPerm on Graph to capture permutations of children (see Fig. 1), with an extended discussion about how to interpret the coinductively defined relation. Sect. 4 shows a characterization of GPerm by a sequence of relations corresponding to increasingly deep observations of the graphs involved. Finally, in Sect. 5, we present a relation on Graph that solves the two issues mentioned above (corresponding to the features of Fig. 1 and Fig. 2).

All the ideas presented in the body of this paper are original with respect to [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF]. All of the contents of this article has been formally modeled and proved in Coq (version 8.3). The development is available in [START_REF] Picard | Formalization in Coq for this article[END_REF].

Capturing Permutations on ilist

A first and standard solution would be to check that the elements of ilist we are comparing contain the same number of occurrences of each element. However, counting occurrences needs decidability of R, i. e., ∀t 1 t 2 , (R t 1 t 2 ) ∨ ¬(R t 1 t 2 ), with a strongly constructive form ∨ of disjunction that comes with evidence for the case that has been proven (in Coq, this is sumbool, which belongs to the universe Set of computationally relevant types).

The relation that ensures the same numbers of occurrences of all elements cannot replace ilist rel in the definition of Geq as its index relation is the one that we would be defining, and for which decidability cannot be already known. Anyway, a posteriori, decidability for Geq cannot be expected.

We could turn to an inductive characterization of whether an element of ilist has a certain number of occurrences. Instead, we preferred to give a direct inductive characterization of when permutations exist. In the next section we will give two equivalent such characterizations, and in Sect. 2.2 we will enrich with "witnesses" one of these. In Sect. 2.3, we give a declarative notion that does not depend on induction. In Sect. 2.4, we give a formal comparison of these notions, while we finish with a more informal discussion in Sect. 2.5.

Inductive Definitions of Permutations on ilist

We now explore notions of permutations that do not depend on decidability of the base relation. Ideally, we want to remain in the realm of logical/declarative approaches. Instead of saying what a permutation is, we will specify when it exists. We do this constructively -by an inductive generation process. Read backwards, we basically remove equivalent elements one by one. To do so, we need a function that removes an element from an ilist. The idea is that it only keeps the elements "before" and "after" the one we want to remove. We call this function remEl but we do not give a formal definition here because it is rather technical and we want to keep the article free from difficulties of dependentlytyped programming. It has type remEl (l : ilist T ) : Fin (lg l) → ilist T . It is characterized by the following assertions:

lg(remEl n + 1, ln i) = n (1) i < Fin i ⇒ fct(remEl n + 1, ln i) i = ln(weakFin i ) (2) i ≤ Fin i ⇒ fct(remEl n + 1, ln i) i = ln(succ i ) (3)
where weakFin : ∀n, Fin n → Fin(n + 1) is recursively defined by: weakFin(first n) := first(n + 1) and weakFin(succ i ) := succ(weakFin i ) This function only increases the type indices in its argument. Logically speaking, this is a kind of weakening. Please, note that 2 and 3 only type well modulo 1.

Remark 4 (Order relation on Fin). We informally use < Fin , ≤ Fin and = Fin to represent the order relation on Fin. Basically, we order the elements of Fin by the number of succ in their definition, disregarding the type indices, e. g., first 2 < Fin succ(first 1) = Fin succ(first 2). Thus, elements of different types are put into relation. One can show ∀i,weakFin i = Fin i.

The permutation relation can be defined using any one of the two following definitions (we will prove that they are equivalent):

Definition 7 (iperm, Viewed Inductively).

∀l 1 l 2 , iperm R l 1 l 2 ⇔      lg l 1 = lg l 2 = 0 or ∃i 1 i 2 , R (fct l 1 i 1 ) (fct l 2 i 2 ) ∧ iperm R (remEl l 1 i 1 ) (remEl l 2 i 2 )
Definition 8 (iperm , Viewed Inductively).

∀l 1 l 2 , iperm R l 1 l 2 ⇔ lg l 1 = lg l 2 ∧ ∀i 1 ∃i 2 , R (fct l 1 i 1 ) (fct l 2 i 2 ) ∧ iperm R (remEl l 1 i 1 ) (remEl l 2 i 2 )
Note that, iperm gives us one pair of equivalent elements that we can remove at each "level", while iperm says that at each level all elements of l 1 have an equivalent one in l 2 (and this recursively). Roughly, iperm can be seen as a particular case of iperm since, if lg l 1 > 0, there is the canonical choice of i 1 to be the first element of its domain.

Before proving the equivalence of these definitions, we observe that the following assertion: ∀l 1 l 2 , iperm R l 1 l 2 ⇒ lg l 1 = lg l 2 holds, to be proven by induction.

Theorem 1. ∀l 1 l 2 , iperm R l 1 l 2 ⇔ iperm R l 1 l 2
Proof.

[iperm ⇒ iperm] This was already discussed. Formally, it is done by induction on iperm . [iperm ⇒ iperm ] To prove this, we reason by induction on lg l 1 .

-If lg l 1 = 0 then lg l 2 = 0 (using the above observation), hence iperm is trivially true since there is no i 1 : Fin 0. -If l 1 and l 2 are not empty, the proof is much harder. As we already know that lg l 1 = lg l 2 , what we have to prove is:

iperm R l 1 l 2 ⇒ ∀i 1 ∃i 2 , R (fct l 1 i 1 ) (fct l 2 i 2 ) ∧ iperm R (remEl l 1 i 1 ) (remEl l 2 i 2 )
Its proof is quite subtle because it requires a precise case analysis on the index i 1 , which is complicated in this dependently-typed setting. A crucial role is played by interchange lemmas for two subsequent applications of remEl . For its proof, one has to think of a complete unfolding of iperm until the base case is reached. Then, one may permute the order of the obtained pairs in the relation R, just as in the classical mathematical theory of permutations.

The usefulness of having these two equivalent definitions is that they are quite different in structure. Therefore, some properties are easier to show on one or the other. In particular, this is the case for the proof that iperm and iperm preserve equivalence: symmetry is easier with Definition 7 while transitivity is easier with Definition 8 (for i 1 in l 1 , one gets i 2 in l 2 and then i 3 in l 3 , while Definition 7 yields two possibly different indices in l 2 ). These proofs are not detailed here.

We have also proved that iperm (resp. iperm ) preserves decidability (see the definition of decidability in the introduction of Sect. 2) :

Lemma 1. If R is decidable, then iperm R (resp. iperm R ) is decidable.
Proof. One possibility is a proof by induction using Definition 8 (and Theorem 1).

A Richer Notion of Inductive Permutations

However, sometimes, knowing that a permutation exists will not be enough, for example when considering intersection of base relations, as in Lemma 3 below. Definitions 7 and 8 do not allow us to manipulate permutations directly since only their existence is specified. Thus, we have to enrich our definition with a notion of skeleton that witnesses the existence of a permutation. The skeleton records the choices for the existentially quantified variables according to Definition 7. Hence, each skeleton consists of a tuple of pairs of elements of Fin. In each pair, the first element of Fin corresponds to an index in the first ilist, and the second one to the corresponding element in the second ilist. These skeletons form types skel type n, defined as N-indexed family of types: Definition 9 (skel type, Defined Recursively). skel type 0 := unit skel type (n + 1) := (Fin(n + 1) × Fin(n + 1)) × skel type n Here, unit is a one-element type (one might take unit := Fin 1, but unit has nothing to do with indices in ilist). Now, we can define a new notion of permutation (let's call it iperm skel ) using this notion of skeletons. Definition 8 would certainly not fit well with it, but Definition 7 does. To be able to use skel type, we need one natural number as index for both components of the pair, in other words, we need to know that lg(sons g 1 ) = lg(sons g 2 ). Therefore, we have chosen to add this as the hypothesis H lg for iperm skel . However, this is reasonable as we know that it is a direct consequence of iperm (as observed right after the definition of iperm ). We define iperm skel in lockstep with Definition 7, but with the extra data: Definition 10 (iperm skel , Viewed Inductively).

∀l 1 l 2 H lgti s, iperm skel R l 1 l 2 H lgti s ⇔      lg l 1 = 0 or ∃i 1 i 2 s , R (fct l 1 i 1 ) (fct l 2 i 2 ) ∧ "s = ((i 1 , i 2 ), s )" ∧ iperm skel R (remEl l 1 i 1 ) (remEl l 2 i 2 ) H lgti s
where H lg is the aforementioned variable assuming lg l 1 = lg l 2 and is used to build a proof H lgti of lgti(remEl l 1 i 1 ) = lgti(remEl l 2 i 2 ), s is of type skel type(lg l 1 ) and "s = ((i 1 , i 2 ), s )" is only correct up to several type conversions that are not detailed here. Notice that i 1 is of type Fin(lg l 1 ), i 2 is of type Fin(lg l 2 ) and s is of type skel type(lg(remEl l 1 i 1 )).

We can show that iperm and iperm skel are equivalent (proof not given here):

Lemma 2 (iperm ⇔ iperm skel ). ∀l 1 l 2 H lg , iperm R l 1 l 2 ⇔ ∃s, iperm skel R l 1 l 2 H lg s
We can also show that iperm skel is monotone in its relation argument (this was also true for iperm). Finally, we also obtain a lemma about relation intersection for iperm skel given a specific skeleton: Lemma 3 (Intersections in the Relation Argument of iperm skel ). For fixed l 1 , l 2 , H lg and skeleton s, iperm skel R l 1 l 2 H lgti s commutes with arbitrary intersections of non-empty sets of relations R. In particular, if for all n iperm skel Rn l 1 l 2 H lgti s, then iperm skel ∩nRn l 1 l 2 H lgti s.

Note that, without the skeleton -for iperm -this cannot be expected. This lemma will be necessary for the proof of Lemma 10 (see Sect. 4.2).

Permutations on ilist with Bijective Functions

The previous solution is constructive and does not require decidability but remains inductive. Hence, when we mix it with a coinductive definition on Graph (when defining an equivalence relation on Graph, for instance), we will have the same kind of problems as the ones we had when mixing lists with Graph (even though, as we will see in Sect. 3, since we are in the universe of propositions -not of sets, we have more ways to overcome the guardedness restrictions). Thus, we present here a last solution that does not require decidability and that is not inductive. It is based on an idea similar to the one we used for ilist as we use functions. This solution says that two elements of ilist are permutations of each other if there is a bijective function from the indices of the first one to the indices of the second one and when each pair of indices in relation points to equivalent elements.

First of all, we decide to express that a function is bijective by the following definition (where one has to give explicitly the inverse of the function) :

Definition 11 (bij ). ∀(f : T → U ) (g : U → T ), bij f g ⇔ (∀t, g(f t) = t) ∧ (∀u, f (g u) = u)
Now we can define the permutation relation using bij :

Definition 12 (ipermb). ∀l 1 l 2 , ipermb R l 1 l 2 ⇔ ∃f g, bij f g ∧ (∀i, R (fct l 1 i) (fct l 2 (f i)))
Remark 5. Note that ipermb has exactly the same logical structure as ilist rel . Actually, ilist rel can be seen as a special case of ipermb.

One easily shows that ipermb preserves equivalence, that it is monotone in its base relation and the following minimal requirement for a definition of permutation:

Lemma 4. ∀l 1 l 2 , ipermb R l 1 l 2 ⇒ lg l 1 = lg l 2

Equivalence Proofs Between the Definitions

In order to validate Definitions 7 and 12, we show that they are equivalent and that they are equivalent to a permutation relation on lists given by Contejean [START_REF] Contejean | Modeling permutations in Coq for Coccinelle[END_REF] (and thanks to Theorem 1 this will also validate Definition 8).

Equivalence between iperm and ipermb These definitions have the same coverage, in particular, they do not require decidability of R, and they achieve the same objective. We will show here that they are equivalent.

Theorem 2. ∀l 1 l 2 , iperm R l 1 l 2 ⇔ ipermb R l 1 l 2
Proof.

[Direction ⇒] Actually here, what we really do is to prove ipermb R l 1 l 2 from iperm skel R l 1 l 2 (thanks to Lemma 2). We obtain the two functions needed for ipermb from the skeleton provided by iperm skel . Then we finish the proof (for the ∀i, R (fct l 1 i) (fct l 2 (f i)) part) by induction on lg l 1 .

[Direction ⇐] Here, the proof is done by a simple induction on lg l 1 . The main difficulty is that we have to recalculate all the indices in the functions for the new elements of ilist (where one element has been removed) in order to use the induction hypothesis.

Equivalence with Contejean In [START_REF] Contejean | Modeling permutations in Coq for Coccinelle[END_REF], Contejean treats the same problem as ours but on lists. She bases her solution on the classical one presented in [START_REF]The Coq Development Team: The Coq Proof Assistant Standard Library[END_REF] but adds a base relation. It is defined as follows, using @ for list concatenation:

Definition 13 (permcont, viewed inductively).

∀R l 1 l 2 , permcont R l 1 l 2 ⇔ or l 1 = l 2 = [] ∃a b l l 1 l 2 , l 1 = a :: l 1 ∧ l 2 = l@b :: l 2 ∧ R a b ∧ permcont R l 1 (l@l 2 )
Remark 6. This definition is close to the spirit of Definition 7 but not with built-in symmetry since always the first element of l 1 is removed. Note that access to b in l@b :: l 2 is not a native operation of lists while it is in the spirit of ilist.

In order to validate the definitions we proposed here, we are going to show that iperm is equivalent to permcont (and then, by Theorem 2, ipermb will also be equivalent). As permcont applies to lists, we will need the conversion functions ilist2list and list2ilist (see Sect. 1.1 right after Definition 3).

Theorem 3. ∀l 1 l 2 , permcont R l 1 l 2 ⇒ iperm R (list2ilist l 1 ) (list2ilist l 2 )
Proof. We work by induction on permcont R l 1 l 2 , with trivial base case. The inductive case gives us a and b that we remove from l 1 and l 2 using Definition 7.

We also show the other direction (this time using ilist2list) :

Theorem 4. ∀l 1 l 2 , iperm R l 1 l 2 ⇒ permcont R (ilist2list l 1 ) (ilist2list l 2 )
Proof. We work by induction on iperm R l 1 l 2 . The main technical difficulty here is that we need to obtain elements of the form a :: l and l 1 @b :: l 2 . The first one is easy (directly given by Definition 8 -Definition 7 would not be enough here) but for the second one we will need to manipulate the "right part" and the "left part" of an ilist, which is not so trivial.

Comparison of the Obtained Notions

We have presented with details four different definitions of permutations on ilist. All of them have been shown extensionally (i. e., pointwise) equivalent. Still, they are conceptionally quite different. The first two, i. e., Definitions 7 and 8, are declarative in the sense that they do not say what a permutation is, and they are direct in the sense that they only use the concepts of ilist. We consider Definition 7 to capture the intuition and to be conceptually the definition of our choice (in the sequel, we will always work with Definition 7, unless specified otherwise). Definition 8 shares the same intuition of recursively removing pairs of elements, but with built-in extra uniformity for the possibility of choosing a pair. As mentioned before, this is good for proving transitivity but lacks symmetry in its construction, which is why we prefer Definition 7 as the reference definition. The variant with skeletons, iperm skel , only makes explicit the information contained in a derivation according to Definition 7. Having this otherwise hidden information is necessary if several base relations are considered, as it is done in Lemma 3. The skeletons represent bijective functions on the indices but this information is kept totally implicit. Indeed, we only register indices corresponding to intermediate situations -not to the initial ilist.

Definition ipermb is based on an explicit representation of bijective functions on the indices. Surjectivity is quite delicate from a constructive point of view. And instead of requiring the existence of an inverse, it is better to exhibit it directly and make it part of the definition of bijectivity as done in bij . For ipermb to hold, one requires the existence of a bijection such that the elements pointed to by the pairs of indices according to the bijection are in the base relation. Conceptually, this separates the process of finding a permutation into first giving all the pairs of indices and second verifying that the elements corresponding to each pair indeed are in the base relation.

Finally, definition permcont given by Contejean immediately allows us to define a fifth notion of permutation:

Definition 14. ∀l 1 l 2 , ipermcont R l 2 l 2 ⇔ permcont R (ilist2list l 1 ) (ilist2list l 2 )
Since ilist2list is a bijection, ipermcont is extensionally equivalent to iperm, by Theorem 3 and Theorem 4. However, as we have already explained, using lists in the coinductive definition of Graph is not an option. Therefore, we prefer a direct definition of permutations on ilist rather than through conversion between lists and ilist. Moreover, the basic notions on lists are the notions of head and tail, while getting the n th element is not built into the structure. On the contrary, on ilist, we can get the n th element directly but it is not trivial to get the tail.

A Relation on Graph Including Permutations on ilist

In this section, we use iperm to define a relation on Graph. This relation will only solve the problem of permutation between children (see Fig. 1). A refinement that also solves the other problem (change in the point of view for the observation of the graph, see Fig. 2) is presented in Sect. 5.

We define the relation transformer GPerm using the same model as for Geq:

Definition 15 (GPerm, Viewed Coinductively).

g 1 g 2 : Graph T R (label g 1 ) (label g 2 ) iperm GPerm R (sons g 1 ) (sons g 2 )
GPerm R g 1 g 2

An Unsuccessful Try with Guardedness as Implemented in Coq

Proving that GPerm preserves reflexivity should be an easy exercise. Notice that this cannot be done by induction on g in Graph T since that type is coinductive.

Since the proposition to be shown is coinductively defined, the proof naturally has to be carried out by coinduction.

Lemma 5 (GPerm Preserves Reflexivity). ∀R, Rreflexive ⇒ ∀g, GPerm R g g Proof (Coinductive proof ). After assuming R and its reflexivity, we try to show our goal by the cofix tactic of Coq. The coinductive hypothesis Hc is identical with our goal ∀g, GPerm R g g, and it suffices to prove for given g: R (label g) (label g) ∧ iperm GPerm R (sons g) (sons g) -R (label g) (label g) holds by reflexivity of R -To prove iperm GPerm R (sons g) (sons g) we may want to use the lemma that iperm preserves reflexivity. Thus, to prove iperm GPerm R (sons g) (sons g), we would only have to prove that ∀g, GPerm R g g, which is Hc. However, this proof is not correct for Coq because the use of Hc is not guarded (it should be used directly under a coinductive constructor and not through a lemma). So, we rather inline the proof of reflexivity of iperm GPerm R for the argument sons g. However, this part of the proof is by induction inside the initial coinduction (the corecursive call is in a recursive construction). Thus, the resulting proof does not pass the guardedness check of Coq.

Abort proof. This failure should not be surprising since it just repeats on the proof level the problems we would have had on the level of programming with Graph, had we not replaced the use of lists by ilist in its definition. In general, Coq support for coinductive types is quite comfortable, which is why the burden of working with ilist is compensated for by flexible coinductive definitions of graph structures. On the level of coinductive proofs about coinductively defined relations such as GPerm, this support does not seem of equal importance to us. Thus, we do not try to solve the issue of the rigid guardedness criterion of Coq as we did for Graph, but give up the use of the CoInductive command of Coq for getting a coinductive definition of GPerm. We rather define GPerm "manually" by an impredicative encoding, as shown next.

Alternative Reading of the Coinductive Definition of GPerm

We still view Definition 15 coinductively, but not according to the CoInductive keyword of Coq, as we did for all other coinductive definitions. We rather do this by an impredicative definition. This is based on Tarski's fixed point theorem that constructs a greatest fixed point in a complete lattice as the supremum of all of its post-fixed points. In the categorical picture, post-fixed points correspond to coalgebras, but in a complete lattice, we can even enforce finality without continuity. The Tarski construction can be replayed in polymorphic lambdacalculus as an impredicative encoding of greatest fixed points. All this is well explained in [START_REF] Uustalu | Least and greatest fixed points in intuitionistic natural deduction[END_REF], together with historical remarks that, for least fixed points, the corresponding encodings go back to Böhm/Berarducci and Leivant.

While the CIC was an extension of polymorphic λ-calculus (hence, with impredicative universe Set) this impredicativity is now optional (so, we did not use it for Graph), but the universe of propositions Prop remains impredicative. In particular, we can form propositions by quantifying over all propositions or all relations, as they are building blocks of propositions. We use the wellknown impredicative construction on Prop instead of Set. We thus implement GPerm R g 1 g 2 by the proposition (with R ranging over relations on Graph T ):

∃R, ∀g 1 g 2 , R g 1 g 2 ⇒ R (label g 1 ) (label g 2 )∧iperm R (sons g 1 ) (sons g 2 ) ∧R g 1 g 2 Lemma 6 (Coinduction Principle for GPerm). Let us assume ∀g 1 g 2 , R g 1 g 2 ⇒ R (label g 1 ) (label g 2 ) ∧ iperm R (sons g 1 ) (sons g 2 ) with R a relation on Graph T . Then, ∀g 1 g 2 , R g 1 g 2 ⇒ GPerm R g 1 g 2 .
Proof. Trivial by implementation of GPerm.

Lemma 7 (Unfolding Principle for GPerm).

∀g 1 g 2 , GPerm R g 1 g 2 ⇒ R (label g 1 ) (label g 2 )∧iperm GPerm R (sons g 1 ) (sons g 2 ) Lemma 8 (Constructor for GPerm). ∀g 1 g 2 , R (label g 1 ) (label g 2 )∧iperm GPerm R (sons g 1 ) (sons g 2 ) ⇒ GPerm R g 1 g 2
This final result corresponds to the way coinductive definitions are perceived for definitions by CoInductive in Coq. In our implementation, the coinduction principle is the obvious result, and the constructor the non-obvious (but wellknown for a long time by now). Therefore, these proofs are not shown here. Remark 7. GPerm can also be captured in a Mendler-style coinduction (see [START_REF] Nakata | Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: An exercise in mixed induction-coinduction[END_REF]) that is directly expressible by CoInductive in Coq and also essentially uses impredicativity of Prop. This alternative gives a provably equivalent solution, as shown in our Coq development [START_REF] Picard | Formalization in Coq for this article[END_REF].

Proof that GPerm Preserves Equivalence

With the impredicative implementation of GPerm, Lemma 5 is now easy to prove. Proof. Assume that R is reflexive. Instead of our goal ∀g, GPerm R g g, we show the more general ∀g 1 g 2 , g 1 = g 2 ⇒ GPerm R g 1 g 2 , which is of the right format for Lemma 6, taking R := = Graph T . It suffices to show that R g 1 g 2 implies R (label g 1 ) (label g 2 ) ∧ iperm R (sons g 1 ) (sons g 2 ). Since R is Leibniz-equality, we may replace g 1 by g 2 everywhere. The first conjunct is then done by reflexivity of R, and the second follows from preservation of reflexivity by iperm. GPerm also preserves symmetry and transitivity. For the former, the use of Lemma 6 is with R the "flipped" version of GPerm R , hence with interchanged arguments, and uses the good flipping behaviour of iperm and Lemma 7. For transitivity preservation, we set R g 1 g 2 ⇔ ∃g , GPerm R g 1 g ∧GPerm R g g 2 and use Lemma 6 for it. Besides Lemma 7, this requires a quite special form of transitivity of iperm whose proof must be based on Definition 8 and Theorem 1:

iperm R1 l 1 l ∧ iperm R2 l l 2 ⇒ iperm R3 l 1 l 2 with R 3 t 1 t 2 ⇔ ∃t , R 1 t 1 t ∧ R 2 t t 2

An Equivalent Approach Based on Observations

As we saw in Sect. 3.1, the problem was the embedding of inductive proofs (the existence of a permutation) in a coinductive proof that GPerm holds. This could be overcome by the impredicative encoding of GPerm, but there is also the well-known option of abandoning coinduction in favour of some observational equivalence. Here, the idea is to use inductive trees (the finite counterpart to Graph) to represent the unfolding of elements of Graph until a certain depth. Then, we define a relation transformer on these trees using iperm, and we prove that it preserves equivalence. To "observe" until a depth n means cutting off the graphs all the structure beyond depth n, which yields such inductive trees, so we can relate them by the relation on trees (obviously, we expect the relation to be decidable). If the relation holds for all depths, the graphs are considered "observationally equal". Thus, on the logical side, we only work on inductive structures (while the graphs are still coinductive structures).

Finally, adding a version of the infinite pigeonhole principle as an axiom to Coq (that could in turn be justified by the classical law of excluded middle), we prove that observational equivalence is equivalent to GPerm (for any base relation). Therefore, we get an alternative proof that GPerm preserves equivalence.

Definitions Based on Inductive Trees

We define the type of inductive trees (we call it iTree) as follows:

Definition 16 (iTree, Viewed Inductively).

t : T l : ilist(iTree T ) mk iTree t l : iTree T We call labT and sonsT the two projection functions on iTree. We use t 1 and t 2 to denote elements of iTree T . Now, we can define a relation on iTree using the permutation relation on ilist. We define it in analogy with GPerm, but inductively: Definition 17 (TPerm, Viewed Inductively).

t 1 t 2 : iTree T R (labT t 1 ) (labT t 2 ) iperm TPerm R (sonsT t 1 ) (sonsT t 2 )
TPerm R t 1 t 2 To prove that TPerm preserves equivalence, we reason by induction. As iperm is also inductive, the proofs are straightforward and do not present any difficulties.

As we have said, the purpose of using inductive trees built with the same pattern as Graph is to capture the unfolding of an element of Graph until a depth n. Therefore, we have to define a function that transforms an element of Graph into an element of iTree. We call this function G2iT . Definition 18 (G2iT , Defined Recursively).

G2iT : ∀T, N → Graph T → iTree T G2iT T 0 g := mk iTree (label g) G2iT T (n+1) (mk Graph t l) := mk iTree t (imap (G2iT T n) l)
where stands for the empty ilist and imap is the ilist analogue of the map function on lists (see [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF]) and has type ∀T U, (T → U ) → ilist T → ilist U .

We also define a notation to say that two elements of Graph extracted up to level n are equivalent through TPerm. We call it ≡:

Definition 19. ∀n g 1 g 2 , g 1 ≡ R,n g 2 ⇔ TPerm R (G2iT n g 1 ) (G2iT n g 2 ) Lemma 9 (Recursive description of ≡ R,n as a function of n). ∀g 1 g 2 , g 1 ≡ R,0 g 2 ⇔ R (label g 1 ) (label g 2 ) ∀g 1 g 2 , g 1 ≡ R,n+1 g 2 ⇔ R (label g 1 ) (label g 2 ) ∧ iperm ≡ R,n (sons g 1 ) (sons g 2 )
Remark 8. As should be expected from a relation based on finite observations, ≡ R,n preserves decidability (of R). The proof is by induction on n using Lemmas 1 and 9.

Our goal here is to prove that, if for all n, two elements of Graph transformed to iTree by G2iT n are equivalent through TPerm, then they are equivalent through GPerm and vice versa. We first define the relation on Graph that uses TPerm. We want to prove that it is equivalent to GPerm. We call it GTPerm.

Definition 20 (GTPerm). ∀g 1 g 2 , (GTPerm R g 1 g 2 ⇔ ∀n,

g 1 ≡ R,n g 2 )
One shows that GTPerm preserves equivalence using the fact that TPerm does.

Main Theorem

Theorem 5. ∀g 1 g 2 , GPerm R g 1 g 2 ⇔ GTPerm R g 1 g 2

The proof extends until the end of this section and makes use of Axiom 1 below.

Proof.

[Direction ⇒] This is proved by induction on n (depth of observation of g 1 and g 2 ) using Lemma 9. [Direction ⇐] This direction is much harder, and needed concepts and results will be introduced after showing the overall structure. We do it as a coinductive proof, i. e., we apply Lemma 6. Obviously, we use it with R := GTPerm R . Given g 1 , g 2 and GTPerm R g 1 g 2 , we have to show R (label g 1 ) (label g 2 ) and iperm GTPerm R (sons g 1 ) (sons g 2 ). For the first part, we use the definition of GTPerm R with n := 0 and the base case of Lemma 9. The second part is guaranteed by Lemma 10.

Lemma 10. ∀g 1 g 2 , GTPerm R g 1 g 2 ⇒ iperm GTPerm R (sons g 1 ) (sons g 2 )
[Proof of Lemma 10] Actually, here, the main challenge is a problem of continuity. Indeed, unfolding the definition of GTPerm, we obtain the goal:

∀g 1 g 2 , (∀n, g 1 ≡ R,n g 2 ) ⇒ iperm ∩n≡ R,n (sons g 1 ) (sons g 2 )
So this actually means that we can "fix" a permutation for (sons g 1 ) and (sons g 2 ) that will be valid for any depth of extraction through G2iT . This is not trivial, because some permutations may be valid until a certain depth but not afterwards. For example, in Fig. 3, only the permutation symbolized by the thick plain arrows would be valid for the level with depth = 2. The thick dashed one would be valid for depth = 1 but not afterwards (given standard equality on the labels). However, in the opposite direction, there is no problem. Indeed, if a permutation is valid at a certain depth n, then for all shallower depths m (m ≤ n), this same permutation is valid. We express this result only partly in Lemma 11 since we do not capture in what sense this is the "same permutation". The proof is not detailed here.

Lemma 11. ∀g 1 g 2 n m, m ≤ n ∧ g 1 ≡ R,n g 2 ⇒ g 1 ≡ R,m g 2 0 1 1 2 3 0 1 1 2 3

Fig. 3. Graphs with various possibilities of permutations on the first level

To prove Lemma 10, we use a specific formulation of the infinite pigeonhole principle. It informally states that if an infinity of items is put into a finite number of holes, then at least one hole must contain an infinity of items.

Although obviously true, this principle has no constructive justification since no finite observation of the infinite process of putting the items into the holes allows to determine which hole is used infinitely often.

For our problem, the infinitely many items are the unfolding levels (for the elements of Graph) and the holes are the possible permutations (as sons g 1 and sons g 2 are finite, the number of possible permutations also is, as we only consider the permutations on the top level). However, this requires us to be able to manipulate permutations. Hence, we have to use the definition of iperm skel given in Sect. 2.2. We can do this directly since we showed that it was equivalent to iperm.

The infinite pigeonhole principle will only be needed for the finite types of the form skel type m. We have to assume it as an axiom on top of the intuitionistic type theory CIC that underlies Coq. It could be justified by the classical law of excluded middle which is consistent with the CIC.

Axiom 1 (Infinite Pigeonhole Principle). ∀m ∀P : N → skel type m → Prop, (∀n∃s : skel type m, P n s) → ∃s 0 : skel type m, (∀n∃n , n ≥ n ∧ P n s 0 )

Here, we use the letter P for the relation that describes which "pigeon" n "goes" into which "hole"/skeleton s. We can now come back to Lemma 10 itself. We want to prove that:

GTPerm R g 1 g 2 ⇒ iperm GTPerm R (sons g 1 ) (sons g 2 )
It is easy to prove lg(sons g 1 ) = lg(sons g 2 ) (call its proof H lg ) using the definition of GTPerm with n:=1. We can also prove the following assertion H 1 :

∀n∃s : skel type(lg(sons g 1 )), iperm skel ≡ R,n (sons g 1 ) (sons g 2 ) H lg s Indeed, for argument n, the definition of GTPerm R g 1 g 2 can be used at depth n + 1, and Lemma 9 allows to infer iperm ≡ R,n (sons g 1 ) (sons g 2 ), from which we get the skeleton by Lemma 2.

The application of the pigeonhole principle (Axiom 1) gives us the "good" permutation skeleton s 0 for infinitely many levels, as expressed in the property

∀n∃n , n ≥ n ∧ iperm skel ≡ R,n (sons g 1 ) (sons g 2 ) H lg s 0 (H 2 )
In fact, s 0 is already the "good" skeleton for all levels: using Lemma 2, we can change the goal of the proof to:

iperm skel GTPerm R (sons g 1 ) (sons g 2 ) H lg s 0 and by Lemma 3, we can transform it again into ∀n, iperm skel ≡ R,n (sons g 1 ) (sons g 2 ) H lg s 0

Given n, we choose n according to H 2 . Then, by Lemma 11, ≡ R,n is a subrelation of ≡ R,n . Therefore, using the monotonicity of iperm skel in its relation argument, we obtain the goal from the main property of n that H 2 guarantees.

This ends the proof of Lemma 10 and hence completes that of Theorem 5.

The Final Relation

The preceding two sections solve the issue of permutations in the children. We are going to integrate it in a solution that also solves the issue of change of root.

The Idea

Graph allows to represent single-rooted connected graphs, i. e., there is a path to any node of the graph from the root. If we are able to change the "point of view", i. e., to represent the same graph but with another node as the root (see Fig. 2), then there is a path from the new root to the old one and inversely.

Remark 9. This change is only allowed for a "general" view, not for the inner nodes. For example, we do not want the graphs of Fig. 4 to be equivalent. We will call g 1 and g 2 the two elements of Graph that represent the same graph but with a different root. Saying that there is a path from g 1 to g 2 and from g 2 to g 1 means that g 1 is "included" in g 2 and that g 2 is "included" in g 1 . In [START_REF] Picard | Coinductive graph representation: the problem of embedded lists[END_REF] we have presented a notion of strict inclusion that we have called GinG. This inclusion was built using Geq. Here, we want to add permutations, so we want to have the same kind of relation but using GPerm. So we can define it in a general way (for any relation on Graph) and then we will instantiate it for GPerm. We define it as follows (with R G a relation on Graph T ):

Definition 21 (GinG * , Viewed Inductively). R G g in g out GinG * RG g in g out GinG * RG g in (fct(sons g out ) i) GinG * RG g in g out To find properties of GinG *
, we need to know more about the behaviour of R G regarding propagation towards the children. We instantiate GinG * for GPerm:

Definition 22 (GinGP ). GinGP R := GinG *

GPermR

For GinGP , we can prove various properties among which preservation of transitivity and compatibility with relation GPerm R in its two arguments.

GeqPerm

Using this relation of inclusion, we can now define the final relation on Graph that takes into account permutations over the children and a change in the point of view of the representation. We call it GeqPerm. It checks that the first element of Graph is included in the second, and inversely. The case when there is no change in the point of view for the observation is managed by the fact that GinG * preserves reflexivity (first case of the definition). We define GeqPerm as follows:

Definition 23 (GeqPerm). ∀g 1 g 2 , GeqPerm R g 1 g 2 ⇔ GinGP R g 1 g 2 ∧ GinGP R g 2 g 1
As GinGP preserves reflexivity and transitivity, GeqPerm preserves equivalence.

It is now possible to show that the graphs of Fig. 1 and Fig. 2 are equivalent and that the graphs of Fig. 4 are not. The proofs that two elements of Graph are not equivalent may be tedious because we have to test all possible permutations (in the example of Fig. 4 the nodes only have one child, so the proof is short). Of course, one can also mix the features of Fig. 1 and Fig. 2.

Remark 10. We now have at our disposal the relation on Graph that we would natively have obtained with a standard set-theoretic definition of graphs. But, we have the computational advantages of our constructive definitions.

Conclusions

In this paper, we have presented and compared various solutions to capture permutations on ilist modulo some possibly undecidable base relation R on the elements of the ilist. This was crucial since decidability cannot be guaranteed (not even expected) for our graph representation Graph. We have shown that these relation transformers preserve equivalence (map equivalence relations to equivalence relations). And we proved that they are all equivalent. Then, we have integrated one of these relations (the one that we considered to capture best the intuition of permutations) into a relation GPerm to include permutations over children. Using ilist instead of lists was needed since with lists, the coinductive representation of graphs would not have allowed programming in Coq.

We have also presented a solution that allows us to observe our graphs on finite structures (the inductive trees iTree) via the function G2iT that converts elements of Graph to elements of iTree up to a certain depth. We provide a relation transformer TPerm for iTree in analogy with what we did for Graph, including permutations over the children of the elements of iTree. We can thus formulate that two graphs are "bisimilar" up to any depth by reference to G2iT and TPerm, which yields the relation GTPerm. For a decidable base relation, we obtained that "bisimilarity" up to any given depth is decidable. We have included into the main text a proof of equivalence of GPerm with GTPerm (Theorem 5), hence between the coinductive concept and the one based on observations. Finally, we included our permutation-aware relation on Graph into a wider relation taking into account changes in the point of view of the representation of the elements of Graph (GeqPerm). We proved that this final relation (transformer) preserves equivalence and that it indeed solved the issues presented in Sect. 1.2. In the course of our research we observed that even for lists, the standard library would not have solved our problems concerning permutations parameterized freely by a possibly undecidable relation (see [START_REF]The Coq Development Team: The Coq Proof Assistant Standard Library[END_REF] and [START_REF]The Coq Development Team: The Coq Proof Assistant Standard Library[END_REF]). We are currently working on an extension of Contejean's [START_REF] Contejean | Modeling permutations in Coq for Coccinelle[END_REF] in the style of our solutions for ilist.

If we chose to ignore multiplicities in ilist, we could define a new relation corresponding to the equivalence between two sets. This could be an interesting direction to investigate to obtain an even more liberal relation on graphs.

Berger [START_REF] Berger | From coinductive proofs to exact real arithmetic: theory and applications[END_REF] uses an embedded inductive definition in a coinductive one for the purpose of real number computability, with extraction of Haskell programs. We wonder if his work could be formalized in Coq using the methods presented here.

Finally, it would be interesting to extend GeqPerm to a wider class of graphs covering also non-connected graphs, e. g., by using the notion of forest of graphs.

Remark 3 . 2

 32 The two graphs on the right are equivalent through Geq. If one wanted to differentiate between these two structures, one could use the type {A, B} × N instead of N and thus give an identity to the nodes. Need for a More Liberal Relation on Graph -Content Overview

Fig. 1 . 1 1 0Fig. 2 .

 1112 Fig. 1. Different order in children

Fig. 4 .

 4 Fig. 4. Graphs with inner cycle turned

http://wiki.portal.chalmers.se/agda/pmwiki.php

Acknowledgements We warmly thank our reviewers for their attentive reading and interesting propositions and challenges.

This work has been funded by the project CLIMT of the French Agence Nationale de la Recherche (ANR-11-BS02-016).


Zhenzhen You

Michel E Vandenberghe

Yael Balbastre

Nicolas Souedet

Philippe Hantraye

Caroline Jan

Anne-Sophie Herard

Thierry Delzescaux

Automated cell individualization and counting in cerebral microscopic images

Keywords: Cell individualization, neuron counting, segmentation, microscopic images, min-max cartography

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Cell segmentation is a major biological research tool which can provide useful information about cell number and organization in the tissue. In neurodegenerative disease, for example, it allows to investigate neuronal loss in pathological brains. Microscopic images are commonly used in biology and provide high resolution images in which cytoarchitecture can be investigated. Traditionally, stereology methods [START_REF] West | Unbiased stereological estimation of the total number of neurons in thesubdivisions of the rat hippocampus using the optical fractionator[END_REF] are used by the biologists to perform robust cell counting in an anatomical region based on manual segmentation performed in several samples. But this manual operation is time consuming and cumbersome. In addition, its accuracy depends on the complexity of images and the experience of the biologists. In order to overcome these limitations, an automated, accurate and robust method is requested. So far, several image processing methods have been proposed, but most of them are highly specific. Mathematical morphology [START_REF] Nedzved | Morphological segmentation of histology cell images[END_REF] and concavity detection [START_REF] Bai | Touching Cells Splitting by Using Concave Points and Ellipse Fitting[END_REF], [START_REF] Kothari | Automated cell counting and cluster segmentation using concavity detection and ellipse fitting techniques[END_REF] can only segment cells in simple images where only few cells are touching. However with histological tissue, a tremendous quantity of data is to be analyzed. Some anatomical regions like the dentate gyrus consist of massively packed neurons which are extremely difficult to individualize. Watershed algorithms [START_REF] Cousty | Watershed Cuts: Minimum Spanning Forests and the Drop of Water Principle[END_REF] can segment touching cells but can easily cause over-and under-segmentation. Snakes [START_REF] Xu | Gradient vector flow: a new external force for snakes[END_REF]- [START_REF] Suri | Shape recovery algorithms using level sets in 2-D/3-D medical imagery: a state-of-the-art review[END_REF] can avoid over-segmentation but the initial contour and a pertinent external force are essential for a good segmentation. More recently, the iCut algorithm [START_REF] He | iCut: an Integrative Cut Algorithm Enables Accurate Segmentation of Touching Cells[END_REF] has been proposed to segment touching cells based on a size prior and concavity detection. This paper presents a new image processing protocol which aims at automatically segmenting individual cells in two steps. First, segmentation of cells from tissue and background is performed using Random Forest (RF) classifier. The second step concerns the individualization of touching cells. We propose to use an original min-max filter that exacerbates local extrema to recover valuable information about cell centers and boundaries. The generated cartography can then guide a competitive region growing scheme. An optimization of the parameters of the proposed method is realized on a dataset manually segmented by experts and this method is compared to two methods of reference (watershed, iCut). Our method is then applied to segment cells on the hippocampus region, one of the most challenging anatomical regions to study due to its size and complex organization.

Materials and Methodology

Biological material

This work is based on a macaque brain which was cut after euthanasia into 40-µm-thick sections. About 150 brain sections were produced and stained using a neuronal marker NeuN. They were digitized using an AxioScan.Z1 (Zeiss) with an in plane resolution of 0.22 µm (x20-magnification). In this preliminary work, sub-parts of one brain section corresponding to 120 GB were extracted and processed. A training set of ten representative images (512x512 pixels) were extracted and manually segmented into 3 classes (neurons, non-stained tissue and background) by an expert. To validate our individualization method, a centroid set of eighty images (256x256 pixels) presenting different levels of fraction of cell surface occupation were extracted. In these images, each cell was manually segmented by 2 experts by marking a point in its center providing information about cell number and cell center location. Finally, the proposed method was applied to an image of the left hippocampus corresponding to about 5 GB (44000x28000 pixels) in order to count neurons and compute neuron density in complex manually segmented sub-regions (CA1, CA2, CA3, CA4, dentate gyrus, subiculum).

Tissue segmentation

A RF model (100 trees) that we've previously described [START_REF] Vandenberghe | Robust supervised segmentation of neuropathology whole-slide microscopy images[END_REF] is generated using the training set. The features considered are H, S, V color channels and local intensity (gray level intensity computed in disk of 5 pixels radius). Then the centroid set are segmented into 3 classes with the RF model. Additionally, color images are converted to gray level images [START_REF]Studio encoding parameters of digital television for standard 4:3 and wide-screen 16:9 aspect ratios[END_REF] noted I gray in the following sections.

Cell individualization

To individualize touching neurons, we propose a new method by computing an image in which neuron centers and boundaries can be visualized at the same time. To achieve this purpose, I gray is first filtered by a Gaussian kernel with a standard deviation σ to improve SNR. This parameter σ is optimized to minimize the count error (see section 2.4). The filtered image I g is then masked with the RF segmentation so that all background and non-stained pixels are set to 0.

        D N p S p G p I e   (1)
Consequently, pixels whose filtered value is -1 are absolutely minima in the local disk while those whose value is 1 are absolutely maxima. d is fixed at 10 pixels as it is the expected minimum neuron radius (2.5 µm [START_REF] Andersen | The Hippocampus Book[END_REF]). This two-step process (Gaussian smoothing, min-max filtering) can be repeated n times to sharpen the extrema. n is optimized to minimize the count error (see section 2.4). Pixels of value -1 are selected as neuron centroids and each centroid is assigned to a unique label as the identification (id) of neurons.

The final segmentation is obtained with a discrete contour-based model. Contours are initialized as 5pixel-radius circles centered on each centroid and all pixels inside them are labeled with the same id of their centroid. As neuron boundaries are close to maxima in I e , we propose to give each contour point an expanding speed that depends on the contour curvature and I e 's intensity. Let p a contour point, κ(p) the curvature-dependent term, µ(p) the intensity-dependent term, o the position of the neuron centroid. The next position of p noted p' is obtained through equation [START_REF] Nedzved | Morphological segmentation of histology cell images[END_REF].

    p p op op op op       ' (2)
Let k(p) the contour curvature at point p and c an optimal curvature. κ(p) is obtained through equation ( 3), making the contour expanding for curvatures smaller than c and shrinking for curvatures greater than c.

    p k c p    (3)
The intensity-dependent term is inspired by [START_REF] Perona | Scale space and edge detection using anisotropic diffusion[END_REF]. Let t a coefficient empirically set to 0.8×max(I e ). µ(p) is obtained through equation ( 4).

                     2 2 1 exp t p I p e  (4)
After each iteration, when the distance between two consecutive points p and q is superior to a predefined maximal distance d max , new points are interpolated automatically according to equation [START_REF] Cousty | Watershed Cuts: Minimum Spanning Forests and the Drop of Water Principle[END_REF].

                           N i i N pq op op d pq N i 1 1 1 max (5)
Then pixels surround each contour point p within d max are examined. For those nearer to their centroid than p and not yet labeled are assigned to the same id of their centroid.

All cell contours are simultaneously expanded, and contour crossing is forbidden. In our experiment, we fixed the number of expanding iterations at 30. This number can be arbitrarily high, and should be chosen so that the computation time is low enough but contours have enough time to reach the cell boundaries. Once the process is finished, the remaining unlabeled pixels are assigned according to their neighbors by majority voting.

Parameters optimization and validation

To optimize parameters (σ and iteration number n), our protocol is applied to the centroid set with σ values ranging from 1 to 8 pixels and iteration number from 1 to 3. The relative count error ε is defined as the absolute difference between the automatic count (N a ) and the expert count (N e ) divided by the expert count: In addition, a classification score that takes into account the position of the segmented neurons is defined. For each automatically segmented neuron, the number of expert centroids contained in the neuron is computed. If exactly one expert centroid is contained, this neuron is considered as a true positive. Else, it is either over segmented (zeros expert centroids) or under segmented (more than 1 expert centroids). Recall (R), precision (P) and F-score (F) are calculated as follows:

P R P R F N N P N N R a t e t      2 ; ; (7)
where N t is the number of correctly automatic segmented neurons. The bigger the values of those criteria are, the better the performance of method is.

Results and Discussion

Parameters optimization

Fig. 1 shows an example of different iterations applied to touching neurons (σ=4). A number of two iterations of min-max cartography computation is optimal because one iteration lead underdetection of neurons and three iterations to over-detection. A consistent estimation between the expert and automated method is obtained for two iterations (10 centroids detected). This setting enables to force the detection of small, blurred or brighter neurons which are very difficult to detect. Relative count errors resulting from the optimization of σ and iteration number n are calculated in Table 1 for expert 1 (similar results are obtained for expert 2). Based on the minimal relative count error calculated, parameters σ=4 and 2 iterations are selected as optimal.

Neuron individualization

We have applied the proposed method to the centroid set. Fig. 3 presents the results obtained on the same images using two methods of reference: iCut and watershed. All these methods perform well in the simple cases. However, in the more complicated situations, the results of iCut method and watershed are not accurate. iCut separates touching neurons based on the features taking into account neuron size, spatial location, intervening contours and concave contours. In dense neuronal regions, information of concavity contours is not helpful anymore. iCut estimates the number of neurons by their mean area and gives a homogeneous segmentation result which doesn't correspond visually to real neurons ( over-and under-segmentation making the final contours unnatural (straight borders, large neurons detected). Visually, the proposed method provides a better neuron individualization result. In addition, a quantitative evaluation applied to the centroid set among the 3 methods is illustrated in Table 2. It shows that the proposed method provides the best performances. Moreover, the standard deviation of our method is smaller, demonstrating that the proposed method is more robust for both simple and complicated cases. Another important fact to mention for iCut and watershed methods is that despite relatively high scores observed all superior to 0.8, the segmentation of the neurons is questionable (visual evaluation). It is thus important to define a more sensitive quality index.

Application to the study of hippocampal sub-regions

Fig. 4a presents the left hippocampus and the sub-regions manually segmented (CA1 to CA4, dentate gyrus (DG) and subiculum (S) shown in Fig. 4b) to which our method is applied. Table 3 presents the fraction of neuron surface occupation (F), the number of neurons detected (N) and neuron density (D, the number of neurons per mm²) in each sub-region using the optimal parameters. Our method performs well on large images of several GB in reasonable computational time (about 5 hours in this case on a recent workstation).

Conclusion

This paper presents an efficient method to individualize touching cells in cerebral microscopic images. Some promising segmentation results have been obtained above on neuronal staining in macaque. The accuracy of our method is higher compared to state-of-the-art methods as assessed qualitatively and quantitatively. The method has been successfully applied to a hippocampus of macaque brain, one of the most challenging anatomical regions to study in neuroscience. Perspectives of this work will be to extend this study to the entire brain sections or brains to alleviate the issue of big data processing [START_REF] Vandenberghe | High-throughput 3D whole-brain quantitative histopathology in rodents[END_REF]. The automated detection of millions of cells is still challenging and an in-depth comparison of strengths and complementarities between stereology and image processing methods should be carefully addressed in the future. This generic tool should also help to address major biological issues such as understanding of pathology mechanisms or evaluation of novel therapies.

  The min-max cartography I e is then computed. For each pixel p of I g , let D(d, p) the disk (not including p) of radius d centered on p, let N(D) the number of pixels in D(d, p), let S(p) the number of values in D(d, p) smaller than I g (p) and G(p) the number of values greater or equal to I g (p). The output value is then:

Figure 1 :

 1 Figure 1: Creation of min-max cartography (σ=4). a) Original color image. b) One iteration I e . c) Two iterations I e . d) Three iterations I e . Red crosses are neuron centroids marked by expert while green crosses are the detected neuron centroids.

Fig. 2

 2 presents the results obtained on 3 different images presenting different levels of fraction of neuron surface occupation. Images 1 represent simple images with a few individual neurons, images 2 represent moderately dense images in which several neurons touch and images 3 represent extremely dense images in which many neurons touch. A simple classification (neuron and unstained tissue) illustrated in Fig 2. b1-b3 is insufficient to segment neurons when touching neurons are present. Fig 2. c1-c3 present two iterations min-max cartographies in which neuron centers appear in black and neuron boundaries in bright (visually very close compared to the final neuron contours automatically detected). The proposed individualization method provides good results visually assessed in Fig 2. d1-d3.

Figure 2 :

 2 Figure 2: Neuron segmentation results obtained in images presenting different levels of fraction of neuron surface occupation. a1-a3) Original images. Red crosses are neuron centroids marked by expert. a1) a few individual neurons, a2) several touching neurons, a3) lots of touching neurons. b1-b3) Classification results by random forest. c1-c3) Two iterations min-max cartographies Ie. d1-d3) Individualization results obtained by our method.

  Fig.3presents the results obtained on the same images using two methods of reference: iCut and watershed. All these methods perform well in the simple cases. However, in the more complicated situations, the results of iCut method and watershed are not accurate. iCut separates touching neurons based on the features taking into account neuron size, spatial location, intervening contours and concave contours. In dense neuronal regions, information of concavity contours is not helpful anymore. iCut estimates the number of neurons by their mean area and gives a homogeneous segmentation result which doesn't correspond visually to real neurons (Fig 2.a1-a3). The watershed results present

Figure 3 :

 3 Figure 3: Segmentation results of 2 reference methods. a) represents iCut method, b) Watershed method. Images 1, 2, 3 represent different levels of fraction of neuron surface occupation.

Figure 4 :

 4 Figure 4: a) Hippocampus of one macaque brain section. b) 6 sub-regions segmented by expert.

Table 1 : Relative count error ε based on n and σ.

 1

	a	b	c	d
	Error			Iteration number n
	Expert 1		1	2	3
		1	0.20±0.19	0.55±0.44	1.48±0.86
		2	0.22±0.19	0.32±0.30	0.95±0.62
		3	0.23±0.19	0.16±0.19	0.48±0.41
	σ	4 5	0.24±0.19 0.26±0.19	0.12±0.16 0.14±0.17	0.25±0.26 0.16±0.19
		6	0.29±0.19	0.18±0.17	0.14±0.17
		7	0.31±0.20	0.22±0.18	0.16±0.18
		8	0.35±0.20	0.26±0.19	0.21±0.18

Table 2 : Comparison of performances among 3 neuron individualization methods based on 2 experts segmentation. Highest scores are shown in bold.

 2

	Method		Expert 1	Performances	Expert 2
		Recall	0.88±0.13		0.83±0.14
	iCut	Precision	0.87±0.14		0.90±0.11
		F-score	0.86±0.11		0.85±0.10
		Recall	0.88±0.18		0.82±0.14
	Watershed	Precision	0.82±0.13		0.86±0.09
		F-score	0.84±0.09		0.83±0.09
	Proposed method	Recall Precision F-score	0.92±0.09 0.94±0.07 0.92±0.06		0.85±0.11 0.97±0.05 0.90±0.07

Table 3 : F, N and D obtained in each sub-region.

 3

	Region	CA1	CA2	CA3	CA4	DG	S
	F	0.17	0.24	0.18	0.12	0.29	0.15
	N	5160	3079	12323	4409	11689	3641
	D	2241	3310	2598	1515	4079	1852