Emmanuelle Anceaume

Yann Busnel

Ernst Schulte-Geers

Bruno Sericola

Optimization results for a generalized coupon collector problem *

Keywords: Coupon collector problem, Optimization, Schur-convex functions

We study in this paper a generalized coupon collector problem, which consists in analyzing the time needed to collect a given number of distinct coupons that are drawn from a set of coupons with an arbitrary probability distribution. We suppose that a special coupon called the null coupon can be drawn but never belongs to any collection. In this context, we prove that the almost uniform distribution, for which all the non-null coupons have the same drawing probability, is the distribution which stochastically minimizes the time needed to collect a fixed number of distinct coupons. Moreover, we show that in a given closed subset of probability distributions, the distribution with all its entries, but one, equal to the smallest possible value is the one, which stochastically maximizes the time needed to collect a fixed number of distinct coupons. An computer science application shows the utility of these results.

Introduction

The coupon collector problem is an old problem, which consists in evaluating the time needed to get a collection of different objects drawn randomly using a given probability distribution. This problem has given rise to a lot of attention from researchers in various fields since it has applications in many scientific domains including computer science and optimization, see [START_REF] Boneh | The coupon-collector problem revisited -A survey of engineering problems and computational methods[END_REF] for several engineering examples.

More formally, consider a set of n coupons, which are drawn randomly one by one, with replacement, coupon i being drawn with probability p i . The classical coupon collector problem is to determine the expectation or the distribution of the number of coupons that need to be drawn from the set of n coupons to obtain the full collection of the n coupons. A large number of papers have been devoted to the analysis of asymptotics and limit distributions of this distribution when n tends to infinity, see [START_REF] Doumas | The coupon collector's problem revisited: asymptotics of the variance[END_REF] or [START_REF] Neal | The generalised coupon collector problem[END_REF] and the references therein. In [START_REF] Brown | Coupon collecting[END_REF], the authors obtain new formulas concerning this distribution and they also provide simulation techniques to compute it as well as analytic bounds of it. The asymptotics of the rising moments are studied in [START_REF] Doumas | Asymptotics of the rising moments for the coupon collector's problem[END_REF].

We suppose in this paper that p = (p 1 , . . . , p n ) is not necessarily a probability distribution, i.e., we suppose that n i=1 p i ≤ 1 and we define p 0 = 1 -n i=1 p i . This means that there is a null coupon, denoted by 0, which is drawn with probability p 0 , but that does not belong to the collection. We are interested, in this setting, in the time needed to collect c different coupons among coupons 1, . . . , n, when a coupon is drawn, with replacement, at each discrete time 1, 2, . . . among coupons 0, 1, . . . , n. This time is denoted by T c,n (p) for c = 1, . . . , n. Clearly, T n,n (p) is the time needed to get the full collection. The random variable T c,n (p) has been considered in [START_REF] Rubin | A waiting time distribution arising from the coupon collector's problem[END_REF] in the case where the drawing probability distribution is uniform. The expected value [T c,n (p)] has been obtained in [START_REF] Flajolet | Birthday paradox, coupon collectors, caching algorithms and self-organizing search[END_REF] when p 0 = 0. Its distribution and its moments have been obtained in [START_REF] Anceaume | New results on a generalized coupon collector problem using Markov chains[END_REF] using Markov chains.

In this paper, we prove that the almost uniform distribution, denoted by v and defined by v = (v 1 , . . . , v n ) with v i = (1p 0 )/n, where p 0 is fixed, is the distribution which stochastically minimizes the time T c,n (p) such that p 0 = 1 -n i=1 p i . This result was expressed as a conjecture in [START_REF] Anceaume | New results on a generalized coupon collector problem using Markov chains[END_REF] where it is proved that the result is true for c = 2 and for c = n extending the sketch of the proof proposed in [START_REF] Boneh | The coupon-collector problem revisited -A survey of engineering problems and computational methods[END_REF] to the case p 0 > 0. It has been also proved in [START_REF] Anceaume | New results on a generalized coupon collector problem using Markov chains[END_REF] that the result is true for the expectations, that is that

[T c,n (u)] ≤ [T c,n (v)] ≤ [T c,n (p)].
We first consider in Section 2, the case where p 0 = 0 and then we extend it to one of p 0 > 0. We show moreover in Section 3, that in a given closed subset of probability distributions, the distribution with all its entries, but one, equal to the smallest possible value is the one which stochastically maximizes the time T c,n (p). This work is motivated by the worst case analysis of the behavior of streaming algorithms in network monitoring applications as shown in Section 4.

Distribution minimizing the distribution of T c,n (p)

Recall that T c,n (p), with p = (p 1 , . . . , p n ), is the number of coupons that need to be drawn from the set {0, 1, 2, . . . , n}, with replacement, till one first obtains a collection with c different coupons, 1 ≤ c ≤ n, among {1, . . . , n}, where coupon i is drawn with probability p i , i = 0, 1, . . . , n.

The distribution of T c,n (p) has been obtained in [START_REF] Anceaume | New results on a generalized coupon collector problem using Markov chains[END_REF] using Markov chains and is given by

È{T c,n (p) > k} = c-1 i=0 (-1) c-1-i n -i -1 n -c J∈Si,n (p 0 + P J ) k , (1)
where S i,n = {J ⊆ {1, . . . , n} | |J| = i} and, for every J ⊆ {1, . . . , n}, P J is defined by P J = j∈J p j . Note that we have S 0,n = ∅, P ∅ = 0 and |S i,n | = n i .

This result also shows as expected that the function È{T c,n (p) > k}, as a function of p, is symmetric, which means that it has the same value for any permutation of the entries of p. We recall that if X and Y are two real random variable then we say that X is stochastically smaller (resp. larger) than Y , and we write

X ≤ st Y (resp. Y ≤ st X), if È{X > t} ≤ È{Y > t},
for all real numbers t. This stochastic order is also referred to as the strong stochastic order. We consider first, in the following subsection, the case where p 0 = 0.

The case p 0 = 0

This case corresponds the fact that there is no null coupon, which means that all the coupons can belong to the collection. We thus have n i=1 p i = 1. For all n ≥ 1, i = 1, . . . , n and k ≥ 0, we denote by N (k) i the number of coupons of type i collected at instants 1, . . . , k. It is well-known that the joint distribution of the N (k) i is a multinomial distribution, i.e., for all k 1 , . . . , k n ≥ 0 such that

n i=1 k i = k, we have È{N (k) 1 = k 1 , . . . , N (k) n = k n } = k! k 1 ! • • • k n ! p k1 1 • • • p kn n . (2)
We also denote by U (k) n the number of distinct coupon's types, among 1, . . . , n, already drawn at instant k. We clearly have, with probability 1, U (0)

n = 0, U (1)
n = 1 and, for i = 0, . . . , n,

È{U (k) n = i} = J∈Si,n È{N (k) u > 0, u ∈ J and N (k) u = 0, u / ∈ J}.
Moreover, it is easily checked that,

T c,n (p) > k ⇐⇒ U (k) < c.
We then have

È{T c,n (p) > k} = È{U (k) n < c} = c-1 i=0 È{U (k) n = i} = c-1 i=0 J∈Si,n È{N (k) u > 0, u ∈ J and N (k) u = 0, u / ∈ J}.
Using Relation (2), we obtain

È{T c,n (p) > k} = c-1 i=0 J∈Si,n k∈E k,J k! j∈J p kj j k j ! , (3)
where E k,J is the set of vectors defined by

E k,J = {k = (k j ) j∈J | k j > 0, for all j ∈ J and K J = k} , with K J = j∈J k j .
Theorem 1 For all n ≥ 2 and p = (p 1 , . . . , p n ) ∈ (0, 1) n with n i=1 p i = 1, and for all c = 1, . . . , n, we have

T c,n (p ′ ) ≤ st T c,n (p), where p ′ = (p 1 , . . . , p n-2 , p ′ n-1 , p ′ n ) with p ′ n-1 = λp n-1 + (1 -λ)p n and p ′ n = (1 -λ)p n-1 + λp n , for all λ ∈ [0, 1].
Proof. The result is trivial for c = 1, since we have T 1,n (p) = 1, and for k = 0 since both terms are equal to 1. We thus suppose now that c ≥ 2 and k ≥ 1. The fact that k ≥ 1 means in particular that the term i = 0 in Relation ( 3) is equal to 0. We then have

È{T c,n (p) > k} = c-1 i=1 J∈Si,n k∈E k,J k! j∈J p kj j k j ! . (4)
To simplify the notation, we denote by T i (p) the ith term of this sum, that is

T i (p) = J∈Si,n k∈E k,J k! j∈J p kj j k j ! . (5)
For i = 1, we have S 1,n = {{1}, . . . , {n}} and E k,{j} = {k}. The term T 1 (p) is thus given by

T 1 (p) = n j=1 p k j .
Consider now the term T i for i ≥ 2. We split the set S i,n into four subsets depending on wether the indices n -1 and n belong to its elements. More precisely, we introduce the partition of the set S i,n in the four subsets S

(1)

i,n , S (2)
i,n , S

i,n and S

i,n defined by

S (1) i,n = {J ⊆ {1, . . . , n} | |J| = i with n -1 ∈ J and n / ∈ J} , S (2)
i,n = {J ⊆ {1, . . . , n} | |J| = i with n -1 / ∈ J and n ∈ J} , S (3)
i,n = {J ⊆ {1, . . . , n} | |J| = i with n -1 ∈ J and n ∈ J} , S (4)
i,n = {J ⊆ {1, . . . , n} | |J| = i with n -1 / ∈ J and n / ∈ J} .
These subsets can also be written as S

(1)

i,n = S i-1,n-2 ∪ {n -1}, S (2)
i,n = S i-1,n-2 ∪ {n}, S (3)
i,n = S i-2,n-2 ∪ {n -1, n}, and S (4) i,n = S i,n-2 . Using these equalities, the term T i of Relation ( 5) becomes

T i (p) = J∈Si-1,n-2 k∈E k,J∪{n-1} k!   j∈J p kj j k j !   p kn-1 n-1 k n-1 ! + J∈Si-1,n-2 k∈E k,J∪{n} k!   j∈J p kj j k j !   p kn n k n ! + J∈Si-2,n-2 k∈E k,J∪{n-1,n} k!   j∈J p kj j k j !   p kn-1 n-1 k n-1 ! p kn n k n ! + J∈Si,n-2 k∈E k,J k!   j∈J p kj j k j !   .
Let us now introduce the sets L k,J defined by

L k,J = {k = (k j ) j∈J | k j > 0, for all j ∈ J and K J ≤ k} .
Using these sets and, to clarify the notation, setting k n-1 = ℓ and k n = h when needed, we obtain

T i (p) = J∈Si-1,n-2 k∈L k-1,J k!   j∈J p kj j k j !   p k-KJ n-1 (k -K J )! + J∈Si-1,n-2 k∈L k-1,J k!   j∈J p kj j k j !   p k-KJ n (k -K J )! + J∈Si-2,n-2 k∈L k-2,J k!   j∈J p kj j k j !   ℓ>0,h>0,ℓ+h=k-KJ p ℓ n-1 ℓ! p h n h! + J∈Si,n-2 k∈E k,J k!   j∈J p kj j k j !   ,
which can also be written as

T i (p) = J∈Si-1,n-2 k∈L k-1,J k! (k -K J )!   j∈J p kj j k j !   p k-KJ n-1 + p k-KJ n + J∈Si-2,n-2 k∈L k-2,J k! (k -K J )!   j∈J p kj j k j !   (p n-1 + p n ) k-KJ - J∈Si-2,n-2 k∈L k-2,J k! (k -K J )!   j∈J p kj j k j !   p k-KJ n-1 + p k-KJ n + J∈Si,n-2 k∈E k,J k!   j∈J p kj j k j !   .
We denote these four terms respectively by A i (p), B i (p), C i (p) and D i (p). We thus have, for i ≥ 2,

T i (p) = A i (p) + B i (p) -C i (p) + D i (p). We have already shown that T 1 (p) = A 1 (p) + D 1 (p), so we set B 1 (p) = C 1 (p) = 0. We then have È{T c,n (p) > k} = c-1 i=1 T i (p) = A c-1 (p) + c-2 i=1 (A i (p) -C i+1 (p)) + c-1 i=2 B i (p) + c-1 i=1 D i (p). ( 6
)
For i ≥ 1, we have

A i (p) -C i+1 (p) = J∈Si-1,n-2 k∈L k-1,J k! (k -K J )!   j∈J p kj j k j !   p k-KJ n-1 + p k-KJ n - J∈Si-1,n-2 k∈L k-2,J k! (k -K J )!   j∈J p kj j k j !   p k-KJ n-1 + p k-KJ n = J∈Si-1,n-2 k∈E k-1,J k! (k -K J )!   j∈J p kj j k j !   p k-KJ n-1 + p k-KJ n .
By definition of the set E k-1,J , we have K J = k -1 in the previous equality. This gives

A i (p) -C i+1 (p) = J∈Si-1,n-2 k∈E k-1,J k!   j∈J p kj j k j !   (p n-1 + p n ) .
Using the fact that the function x -→ x s is convex on interval [0, 1] for every non negative integer s, we have

p ′ k-KJ n-1 + p ′ k-KJ n = (λp n-1 + (1 -λ)p n ) k-KJ + ((1 -λ)p n-1 + λp n ) k-KJ ≤ λp k-KJ n-1 + (1 -λ)p k-KJ n + (1 -λ)p k-KJ n-1 + λp k-KJ n = p k-KJ n-1 + p k-KJ n ,
and in particular

p ′ n-1 + p ′ n = p n-1 + p n . It follows that A c-1 (p ′ ) ≤ A c-1 (p), A i (p ′ ) -C i+1 (p ′ ) = A i (p) -C i+1 (p), B i (p ′ ) = B i (p), D i (p ′ ) = D i (p),
and from (6) that È{T c,n (p ′ ) > k} ≤ È{T c,n (p) > k}, which concludes the proof.

The function È{T c,n (p) > k}, as a function of p, being symmetric, this theorem can easily be extended to the case where the two entries p n-1 and p n of p are any p i , p j ∈ {p 1 , . . . , p n }, with i = j.

In fact, we have shown in this theorem that for fixed n and k, the function of p, È{T c,n (p) ≤ k}, is a Schur-convex function, that is, a function that preserves the order of majorization. See [START_REF] Marshall | Inequalities via majorization -An introduction[END_REF] for more details on this subject.

Theorem 2 For every n ≥ 1 and p = (p 1 , . . . , p n ) ∈ (0, 1) n with n i=1 p i = 1, and for all c = 1, . . . , n, we have T c,n (u) ≤ st T c,n (p), where u = (1/n, . . . , 1/n) is the uniform distribution.

Proof. To prove this result, we apply successively and at most n -1 times Theorem 1 as follows. We first choose two different entries of p, say p i and p j such that p i < 1/n < p j and next to define p ′ i and p ′ j by

p ′ i = 1 n and p ′ j = p i + p j - 1 n .
This leads us to write p ′ i = λp i + (1λ)p j and p ′ j = (1λ)p i + λp j , with λ = p j -1/n p jp i .

From Theorem 1, vector p ′ obtained by taking the other entries equal to those of p, i.e., by taking p ′ ℓ = p ℓ , for ℓ = i, j, is such that È{T c,n (p ′ ) > k} ≤ È{T c,n (p) > k}. Note that at this point vector p ′ has at least one entry equal to 1/n, so repeating at most n -1 this procedure, we get vector u, which concludes the proof.

To illustrate the steps used in the proof of this theorem, we take the following example. Suppose that n = 5 and p = (1/16, 1/6, 1/4, 1/8, 19/48). In a first step, taking i = 4 and j = 5, we get p (1) = (1/16, 1/6, 1/4, 1/5, 77/240).

In a second step, taking i = 2 and j = 5, we get p (2) = (1/16, 1/5, 1/4, 1/5, 69/240).

In a third step, taking i = 1 and j = 3, we get p (3) = (1/5, 1/5, 9/80, 1/5, 69/240).

For the fourth and last step, taking i = 3 and j = 5, we get p (4) = (1/5, 1/5, 1/5, 1/5, 1/5).

The case p 0 > 0

We consider now the case where p 0 > 0. We have p = (p 1 , . . . , p n ) with

p 1 + • • • + p n < 1 and p 0 = 1 -(p 1 + • • • + p n ).
Recall that in this case T c,n (p) is the time or the number of steps needed to collect a subset of c different coupons among coupons 1, . . . , n. Coupon 0 is not allowed to belong to the collection. As in the previous subsection we denote, for i = 0, 1, . . . , n and k ≥ 0, by N (k) i the number of coupons of type i collected at instants 1, . . . , k. We then have for all k 0 , k 1 , . . . , k n ≥ 0 such that

n i=0 k i = k, we have È{N (k) 0 = k 0 , N (k) 1 = k 1 , . . . , N (k) n = k n } = k! k 0 !k 1 ! • • • k n ! p k0 0 p k1 1 • • • p kn n ,
which can also be written as

È{N (k) 0 = k 0 , N (k) 1 = k 1 , . . . , N (k) n = k n } = k k 0 p k0 0 (1 -p 0 ) k-k0 (k -k 0 )! k 1 ! • • • k n ! p 1 1 -p 0 k1 • • • p n 1 -p 0 kn . ( 7
)
Note that p/(1p 0 ) is a probability distribution since

1 1 -p 0 n i=1 p i = 1,
so summing over all the k 1 , . . . , k n ≥ 0 such that n i=1 k i = kk 0 , we get, for all k 0 = 0, . . . , k,

È{N (k) 0 = k 0 } = k k 0 p k0 0 (1 -p 0 ) k-k0 . (8)
From ( 7) and ( 8) we obtain, for all k 1 , . . . , k n ≥ 0 such that

n i=1 k i = k -k 0 , È{N (k) 1 = k 1 , . . . , N (k) n = k n | N (k) 0 = k 0 } = (k -k 0 )! k 1 ! • • • k n ! p 1 1 -p 0 k1 • • • p n 1 -p 0 kn . ( 9
)
Recall that U

(k) n
is the number of coupon's types among 1, . . . , n already drawn at instant k. We clearly have, with probability 1, U (0) n = 0, and, for i = 0, . . . , n,

È{U (k) n = i} = J∈Si,n È{N (k) u > 0, u ∈ J and N (k) u = 0, u / ∈ J}.
Moreover, we have as in Subsection 2.1,

T c,n (p) > k ⇐⇒ U (k) n < c. and so È{T c,n (p) > k | N (k) 0 = 0 } = c-1 i=0 J∈Si,n È{N (k) u > 0, u ∈ J and N (k) u = 0, u / ∈ J | N (k) 0 = k 0 }.
Using Relation ( 9), we obtain

È{T c,n (p) > k | N (k) 0 = k 0 } = c-1 i=0 J∈Si,n k∈E k-k 0 ,J (k -k 0 )!    j∈J pj 1-p0 kj k j !    , ( 10
)
where the set E k,J has been defined in Subsection 2.1.

Theorem 3 For every n ≥ 1 and p = (p 1 , . . . , p n ) ∈ (0, 1) n with n i=1 p i < 1, and for all c = 1, . . . , n, we have T c,n (u) ≤ st T c,n (v) ≤ st T c,n (p), where u = (1/n, . . . ,

1/n), v = (v 1 , . . . , v n ) with v i = (1 -p 0 )/n and p 0 = 1 - n i=1 p i .
Proof. From Relation (3) and Relation [START_REF] Zhao | Global iceberg detection over Distributed Streams[END_REF], we obtain, for all k 0 = 0, . . . , k,

È{T c,n (p) > k | N (k) 0 = k 0 } = È{T c,n (p/(1 -p 0 )) > k -k 0 }. (11)
Using [START_REF] Neal | The generalised coupon collector problem[END_REF] and unconditioning, we obtain

È{T c,n (p) > k} = k ℓ=0 k ℓ p ℓ 0 (1 -p 0 ) k-ℓ È{T c,n (p/(1 -p 0 )) > k -ℓ}. (12)
Since p/(1-p 0 ) is a probability distribution, applying Theorem 2 to this distribution and observing that u = v/(1p 0 ), we get

È{T c,n (p) > k} = k ℓ=0 k ℓ p ℓ 0 (1 -p 0 ) k-ℓ È{T c,n (p/(1 -p 0 )) > k -ℓ} ≥ k ℓ=0 k ℓ p ℓ 0 (1 -p 0 ) k-ℓ È{T c,n (u) > k -ℓ} = k ℓ=0 k ℓ p ℓ 0 (1 -p 0 ) k-ℓ È{T c,n (v/(1 -p 0 )) > k -ℓ} = È{T c,n (v) > k},
where the last equality follows from (12). This proves the second inequality.

To prove the first inequality, observe that È{T c,n (p/(1p 0 )) > ℓ} is decreasing with ℓ. This leads, using (12), to

È{T c,n (p) > k} ≥ È{T c,n (p/(1 -p 0 )) > k}.
Taking p = v in this inequality gives

È{T c,n (v) > k} ≥ È{T c,n (u) > k},
which completes the proof.

In fact, we have shown in the proof of this theorem and more precisely in Relation (11) and using Theorem 2 that for fixed n, k and k 0 , the function of p, È{T c,n (p

) ≤ k | N (k) 0 = k 0 } is a Schur-convex function, that
is, a function that preserves the order of majorization. In particular, from (12), È{T c,n (p) ≤ k} is also a Schur-convex function, even when p 0 > 0. See [START_REF] Marshall | Inequalities via majorization -An introduction[END_REF] for more details on this subject.

Distribution maximizing the distribution of T c,n (p)

We consider in this section the problem of stochastically maximizing the time T c,n (p) when p varies in a closed subset of dimension n. In the previous section the minimization was made on the set A defined, for every n and for all p 0 ∈ [0, 1), by

A = {p = (p 1 , . . . , p n ) ∈ (0, 1) n | p 1 + • • • + p n = 1 -p 0 }.
According to the application described in the Section 4, we fix a parameter θ ∈ (0, (1p 0 )/n] and we are looking for distributions p which stochastically maximizes the time T c,n (p) on the subset A θ of A defined by A θ = {p = (p 1 , . . . , p n ) ∈ A | p j ≥ θ, for every j = 1, . . . , n}.

The solution to this problem is given by the following theorem. We first introduce the set B θ defined by the distributions of A θ with all their entries, except one, are equal to θ. The set B θ has n elements given by B θ = {(γ, θ, . . . , θ), (θ, γ, θ, . . . , θ), . . . , (θ, . . . , θ, γ)}, where γ = 1p 0 -(n -1)θ. Note that since θ ∈ (0, (1p 0 )/n], we have 1p 0 -(n -1)θ ≥ θ which means that B θ ⊆ A θ .

Theorem 4 For every n ≥ 1 and p = (p 1 , . . . , p n ) ∈ A θ and for all c = 1, . . . , n, we have T c,n (p) ≤ st T c,n (q), for every q ∈ B θ .

Proof. Since È{T c,n (p) > k} is a symmetric function of p, È{T c,n (q) > k} has the same value for every q ∈ B θ , so we suppose that q ℓ = θ for every ℓ = j and q j = γ.

Let p ∈ A θ \ B θ and let i be the first entry of p such that i = j and p i > θ. We then define the distribution p (1) as p

j -p i p (1) j -p (1) i = p j -θ p j -θ + p i -θ ∈ [0, 1).
From Theorem 1, we get È{T c,n (p) > k} ≤ È{T c,n (p (1) ) > k}. Repeating the same procedure from distribution p (1) and so on, we get, after at most n -1 steps, distribution q, that is È{T c,n (p) > k} ≤ È{T c,n (q) > k}, which completes the proof.

To illustrate the steps used in the proof of this theorem, we take the following example. Suppose that n = 5, θ = 1/20, p 0 = 1/10 and q = (1/20, 1/20, 1/20, 7/10, 1/20), which means that j = 4. Suppose moreover that p = (1/16, 1/6, 1/4, 1/8, 71/240). We have p ∈ A θ and q ∈ B θ . In a first step, taking i = 1 and since j = 4, we get p (1) = (1/20, 1/6, 1/4, 11/80, 71/240).

In a second step, taking i = 2 and since j = 4, we get p (2) = (1/20, 1/20, 1/4, 61/240, 71/240).

In a third step, taking i = 3 and since j = 4, we get p (3) = (1/20, 1/20, 1/20, 109/240, 71/240).

For the fourth and last step, taking i = 5 and since j = 4, we get p (4) = (1/20, 1/20, 1/20, 7/10, 1/20) = q.

4 Application to the detection of distributed denial of service attacks

A Denial of Service (DoS) attack tries to progressively take down an Internet resource by flooding this resource with more requests than it is capable to handle. A Distributed Denial of Service (DDoS) attack is a DoS attack triggered by thousands of machines that have been infected by a malicious software, with as immediate consequence the total shut down of targeted web resources (e.g., e-commerce websites). A solution to detect and to mitigate DDoS attacks is to monitor network traffic at routers and to look for highly frequent signatures that might suggest ongoing attacks. A recent strategy followed by the attackers is to hide their massive flow of requests over a multitude of routes, so that locally, these requests do not appear as frequent, while globally each of these requests represent a portion θ of the network traffic. The term "iceberg" has been recently introduced [START_REF] Zhao | Global iceberg detection over Distributed Streams[END_REF] to describe such an attack as only a very small part of the iceberg can be observed at each single router. The approach adopted to defend against such new attacks is to rely on multiple routers that locally monitor their network traffic, and upon detection of potential icebergs, inform a monitoring server that aggregates all the monitored information to accurately detect icebergs. Now to prevent the server from being overloaded by all the monitored information, routers continuously keep track of the c (among n) most recent distinct requests. These requests locally represent at least a fraction θ of the local stream. Once collected, each router sends them to the server, and throw away all the requests i that appear with a probability p i smaller than θ. The sum of these small probabilities is represented by probability p 0 . Parameter c is dimensioned so that the frequency at which all the routers send their c last requests is low enough to enable the server to aggregate all of them and to trigger a DDoS alarm when needed. This amounts to compute the distribution of the time T c,n (p) needed to collect c distinct requests among the n ones. Theorem 3 shows that the distribution p that stochastically minimizes the time T c,n (p) is the almost uniform distribution v. This means that if locally each router receives a stream in which all the frequent requests (that is, those whose probability of occurrence is greater than or equal to θ) occur with same probability, then the complementary distribution of the time needed to locally complete a collection of c distinct requests is minimized. As a consequence the delay between any two interactions between a router and the server is minimized. Another important aspect of DDoS detection applications is their ability to bound the detection latency of global icebergs, that is the maximal time that elapses between the presence of a global iceberg at some of the routers and its detection at the server. This can be implemented through a timer that will fire if no communication has been triggered between a router and the server, which happens if locally a router has received less than c requests. Dimensioning such a timer amounts to determine the distribution of the maximal time it takes for a router to collect c distinct requests. Theorem 4 shows that the distributions p that stochastically maximizes this time T c,n (p) are all the distributions q ∈ B θ .

j

  = p i + p jθ > p j and p (1) ℓ = p ℓ , for ℓ = i, j. This leads us to write p i = λp

This work was partially funded by the French ANR project SocioPlug (ANR-13-INFR-0003), and by the DeSceNt project granted by the Labex CominLabs excellence laboratory (ANR-10-LABX-07-01).


Hermínio Arias

Nalini Júnior
email: nalini@degeo.ufop.br.

Rômulo Machado
email: rmachado@usp.br

Essaid Bilal
email: bilalessaid@gmail.com

Petrogenesis and tectonic of the Urucum granitic suite

published or not. The documents may come

minerals, feldspars and accessory minerals. Initial Sr 87 /Sr 86 ratios vary from 0.711 to 0.716, with ε Nd (580 Ma) values between -7.4 to -8.2, and Sm-Nd T DM model ages ranging from 2290 to 1840 Ma. KEYWORDS: Urucum suite; Geochemistry; Petrogenesis; Araçuaí belt.

RESUMO:

A suíte Urucum (U/Pb em zircão: 582 ± 2 Ma), situada na região do Vale do Médio Rio Doce, leste de Minas Gerais, caracteriza-se por plutons graníticos alongados (NW-SE e N-S) sin a tardi-colisionais associados à Zona de Cisalhamento de Alto Ângulo de Conselho Peña-Resplendor. São rochas foliadas, com predomínio da foliação no estado sólido em relação à foliação magmática. Foram caracterizadas quatro fácies: (i) porfirítica (Urucum), (ii) inequigranular média a grossa, (iii) com turmalina, e (iv) pegmatítica. Essas fácies são peraluminosas, com índice de saturação em alumina entre 0,98 e 1,38. Os teores em SiO 2 variam entre 70,7 e 73,7%, com valores de K 2 O entre 3,5 e 5,7%, Na 2 O entre 1,9 e 4,4%, MgO entre 0,6 e 1,2%, e CaO entre 0,3 e 0,9%. Em diagramas tipo Harker, os dados químicos mostram trends mais ou menos contínuos desde a fácies Urucum (menos evoluída) até fácies com turmalina e pegmatítica. O comportamento de vários elementos maiores e traços (Fe 2 0 3 , Mg0, Mno, CaO, TiO 2 , Al 2 O 3 , K 2 O, Rb and Ba) mostram a importância da cristalização fracionada de minerais ferromagnesianos, feldspatos (com cumulatos) e minerais acessórios. A razão inicial de Sr 87 /Sr 86 varia de 0,711 a 0,716, com ε Nd (580 Ma) entre -7,4 e -8,2, e idades modelo Sm-Nd entre 2290 e 1840 Ma.

PALAVRAS-CHAVE:

Suíte Urucum; Geoquímica; Petrogênese; Cinturão Araçuaí.

INTRODUCTION

Several papers discuss the generation of significant amounts of granites by crustal melting in the late periods of crustal thickening (collision) and also the role of erosion upon the decompression melting and its effect on increasing partial melting [START_REF] England | Pressure-temperature-time paths of regional metamorphism I. Heat transfer during the evolution of regions of thickened continental crust[END_REF][START_REF] Hollister | The role of melt in the uplift and exhumation of orogenic belts[END_REF][START_REF]Magmagenesis associated with extension in orogenic belts: examples from the Himalaya and Tibet[END_REF]. The crustal thickening is not favorable to generation of a widespread melting [START_REF] England | Pressure-temperature-time paths of regional metamorphism I. Heat transfer during the evolution of regions of thickened continental crust[END_REF]. According to [START_REF] Sylvester | Post-collisional strongly peraluminous granites[END_REF], strongly aluminous granites are formed in different types of orogens during the post-collisional phase. During the exhumation episode, which is accompanied by uplift and erosion, partial relaxation of isotherms occurs and widespread amounts of granitic melting are generated in this phase, which comes after collision [START_REF] Thompson | The pressure-temperature (P, T) plane viewed by geophisicists and petrologsts[END_REF][START_REF] England | The influence of erosion upon the mineral facies of rocks from different metamorphic environments[END_REF].

Experimental models show that crustal anatexis of rocks of different compositions is a common process in levels of middle and lower crust [START_REF] Stevens | Fluid-absent melting and the roles of fluids in the lithosphere: a slanted summary?[END_REF], and it takes place after collision [START_REF] England | Pressure-temperature-time paths of regional metamorphism I. Heat transfer during the evolution of regions of thickened continental crust[END_REF]. They also reveal that widespread amounts of melt can only be generated under H 2 0-saturated conditions, situation more common in upper crust.

Moreover, under H 2 0-undersaturated conditions, appreciable amounts of melt can only be generated as a result of dehydrations involving muscovite, biotite and hornblende [START_REF] Clemens | Fluids, P-T paths and the fates of anatetic melts in the Earth's crust[END_REF]Vielzeuf & Holloway 198;[START_REF] Patiño Douce | Dehydration-melting of biotite gneiss and quartz amphibolite from 3 to 15 kbar[END_REF].

The CaO/Na 2 O ratios are used to separate pelites-derived strongly peraluminous granites from sandstone-derived ones. The first tends to show values lower than 0.30, while the second one, values higher than 0.30 [START_REF] Sylvester | Post-collisional strongly peraluminous granites[END_REF].

The studied area is located in the Mid-Rio Doce Valley, between Galileia and Conselheiro Peña municipalities, Minas Gerais State -Brazil (Fig. 1A). It belongs to the central segment of the Araçuaí Belt (sensu [START_REF] Pedrosa-Soares | The Araçuaí-West-Congo Orogen in Brazil: an overview of a confined orogen formed during Gondwanaland assembly[END_REF]Pedrosa-Soares & Wiedeman-Leonardos 2000) or Northern Mantiqueira Province [START_REF] Almeida | O pré-cambriano do Brasil[END_REF]. In this internal domain (or Eastern Sector, according to Siga Jr. 1986) of the Araçuaí Belt, the regional structures strike between N-S and N-NW, stressing expressive high-angle, ductile shear zones, such as the Resplendor-Conselheiro Pena Shear Zone [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF].

The Urucum suite granitoids, focus of this study, correspond to the most expressive peraluminous granitic magmatism of the Rio Doce Valley. They are constituted by two batholiths (of ~120 km 2 and ~100 km 2 ) and smaller plutons, one of 25 km 2 and the others of 5 km 2 . The larger bodies are elongated along NW-SE and N-S, and are 17 and 5 km long and 2 and 1.8 km wide, respectively; their emplacement was controlled by the high-angle Resplendor-Conselheiro Peña Shear Zone [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF][START_REF] Nalini | A importância da tectônica transcorrente no alojamento de granitos pré a sincolisionais na região do vale do médio Rio Doce: o exemplo das suítes graníticas Galiléia e Urucum[END_REF]. Their margins and inner parts are characterized by a foliated structure dominated by a solid-state foliation and usually by mylonitic and protomylonitic textures. The contacts with surrounding rocks are tectonic. The granites are leuco-to mesocratic and present a coarse-grained, porphyritic texture. Microcline megacrystals (up to 10 cm-sized) represent, together with plagioclase (oligoclase), 30 to 80% in volume of the rock. GRANITOIDS Siga Jr. (1986), using Rb/Sr and U/Pb radiometric data, divided the Neoproterozoic granitoids of the Araçuaí belt in three groups: (1) syn-to late-tectonic (650 -550 Ma); (2) late-to post-tectonic (550 -500 Ma), and (3) post-tectonic (500 -450 Ma) granitoids.

THE REGIONAL CONTEXT OF THE NEOPROTEROZOIC

The results of the 1/100,000 scale Projeto de Levantamento Geológico Básico (PLGB -Basic Geologic Survey Project) carried out by CPRM in the Rio Doce Valley led to the classification of the granitoid massifs into three main tectonic groups related to: (1) pre-to synregional metamorphism; (2) syn-transcurrent faulting, and (3) post-transcurrent faulting (Féboli 1993et al. b;.

The most deformed rocks were included in the first group and strike concordant with the regional structures. They have expanded composition (tonalite-granodiorite-granite), of calcalkaline and meta-aluminous geochemical characteristics, having evolved in volcanic-arc and with intraplate settings. The second group is represented by elongated, batholith-showing mylonitic and cataclastic foliation along the borders which grades inwards to an isotropic structure. The geochemical characteristics are very similar to those of the previous group, differing in the peraluminous terms and its post-collisional tectonic. Small plutons are included in the third group.

They are ring-and oval-shaped, zoned and concentric, commonly associated with charnockitic, basic, intermediate and ultrabasic rocks (Aimorés, Lagoa Preta, Várzea Alegre massifs, among others). This group is characterized as I-type granites of calc-alkaline and tholeiitic affinities and of with intraplate and volcanic-arc settings or related to post-orogenic and post-collisional uplift [START_REF] Féboli | Estratigrafia[END_REF][START_REF] Vieira | Geologia da Folha Baixo Guandú[END_REF]).

In the eastern portion of the studied area, there is located the Brasiliano Rio Doce magmatic arc developed within the 590 -480 Ma interval [START_REF] Figueiredo | Geochemistry of the Rio Doce magmatic arc, Southeastern Brazil[END_REF]. It corresponds to the same magmatic arc described by [START_REF] Wiedemann | The evolution of the Early Paleozoic, Late-to Post-Collisional Magmatic Arc of the Coastal Mobile Belt in the State of Espírito Santo, eastern Brazil[END_REF]. [START_REF] Figueiredo | Geochemistry of the Rio Doce magmatic arc, Southeastern Brazil[END_REF] and [START_REF] Neto | The Rio Doce orogeny, southeastern Brazil[END_REF] divided this magmatism in pre-collisional (590 to 570 Ma), syn-collisional (560 to 530 Ma) and post-collisional (520 and 480 Ma), whereas [START_REF] Wiedemann | The evolution of the Early Paleozoic, Late-to Post-Collisional Magmatic Arc of the Coastal Mobile Belt in the State of Espírito Santo, eastern Brazil[END_REF] divided it in syn-orogenic (590 to 580 Ma) and late-to post-orogenic (520 to 450 Ma). [START_REF] Bilal | Granitóides neoproterozóicos da região do Rio Doce, Minas Gerais, Brasil[END_REF][START_REF] Bilal | Neoproterozoic granitoid suites in southeastern Brazil[END_REF] divided the Neoproterozoic granitic magmatism of the Rio Doce Valley in four groups: (i) a pre-tectonic group, represented by the Galileia suite, which yields an U/Pb age of 595 Ma; (ii) a syn-tectonic group, represented by the Urucum suite, of 582 Ma (U/Pb age); (iii) a late-to post-tectonic group, including the intrusive ring complexes such as Aimorés and Ibituba-Itapina, of 537 to 520 Ma; and (iv) a post-tectonic group, represented by the Ibituruna Syenite, which yields a Rb/Sr age of 511 Ma. Conventional U/Pb zircon ages of 594 Ma and 582 Ma were also obtained respectively for the Galileia suite and the Urucum suite [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF]Nalini et al. 2000a).

The Neoproterozoic granitic magmatism of the Araçuaí belt was divided by Pedrosa Soares et al. (1999) into five suites (G1 to G5), from the oldest to the youngest: G1-syn-tectonic suite, constituting the orogen anatectic core, with I-type gneissic batholiths; G2-calc-alkaline syn-tectonic suite, with S-type granitoids; G3-late-tectonic suite, with S-type peraluminous granites; G4-high-K, calc-alkaline, late-to post-tectonic suite, with I-type granites, including massifs of the charnockitic association (Aimorés, Padre do Paraíso, among others); G5-post-tectonic suite, with predominance of S-type peraluminous granites in zoned massifs, with biotite-granites in the center and two-mica granites or muscovite-garnet granites at the borders. The origin of suite G1 is related to regional anatexis of metasedimentary rocks during crustal thickening, with the generation of suite G3 during the late stage of the process. Suites G2 and G4 are related to the successive stages of a continental magmatic arc evolution. Suite G2 represents the arc root, linked to a subduction zone dipping eastwards [START_REF] Pedrosa-Soares | Neoproterozoic oceanic remnants in eastern Brazil: Further evidence and refutation of an exclusively ensialic evolution for the Araçuaí-West Congo Orogen[END_REF], 1999), whereas G4, generated at deep crustal levels, is related to crust/mantle interactions. Suite G5, emplaced at shallower levels (6 to 12 km), was generated in parts of a thickened crust [START_REF] Pedrosa-Soares | Metasomatic Evolution of Granites, Northeast Minas Gerais State, Brazil[END_REF], 1999). Later, Pedrosa Soares and [START_REF] Pedrosa-Soares | Evolution of the Araçuaí Belt and its conection to the Ribeira Belt, eastern Brazil[END_REF] considered the suite G2 (now named G1) older than suite G1 (now named G2), characterizing the former as pre-collisional (between 625 and 595 Ma) and the latter as syn-collisional (between 595 and 575 Ma).

The collection of geochronological data is still not sufficient for good interpretations regarding the Araçuaí Belt Brasiliano granites. Pb/Pb dating (of zircon by the evaporation method) carried out for six massifs (and a granitic vein) of suites G1, G2 and G5 defined the following ages: G1/G2-591 ± 4 Ma (Ataléia); 582 ± 5 Ma (Wolf), 595 ± 3 Ma (Brasilândia); 575 ± 2 Ma (Guarataia); 576 ± 5 Ma (São Vitor/Pescador); G5-519 ± 2 Ma (Caladão/Padre Paraíso), and 503 ± 9 Ma (granitic veins crosscutting the Caladão Massif) [START_REF] Noce | Chronology of late proterozoic-cambrian granitic magmatism in the Araçuaí belts, eastern Brazil, based on dating by single zircon evaporation[END_REF][START_REF] Noce | Chronology of late proterozoic-cambrian granitic magmatism in the Araçuaí belts, eastern Brazil, based on dating by single zircon evaporation[END_REF].

The original scheme of Pedrosa Soares et al. (1999) was modified by Pedrosa Soares et al. (2001). The granitoids from Araçuaí belt of group 3 were subdivided into G3I and G3S. The first group is characterized by calc-alkaline magma emplaced along oblique to strike-slip shear zones.

The second group has peraluminous signature and consists of a series of small coalesced our isoled sillimanite-cordierite-garnet leocogranitic bodies [START_REF] Pedrosa-Soares | The Araçuaí-West-Congo Orogen in Brazil: an overview of a confined orogen formed during Gondwanaland assembly[END_REF]). Later, Pedrosa Soares et al. (2008) returned to the groups and, more recently, designated them as supersuites [START_REF] Pedrosa-Soares | Late Neoproterozoic-Cambrian granitic magmatism in the Araçuaí orogeny (Brazil), the Eastern Brazilian Province and related mineral resources[END_REF].

FIGURES 01A AND 1B AQUI

THE URUCUM GRANITIC SUITE [START_REF] Barbosa | Geologia das quadriculas Barra do Cuité e Conselheiro Pena, MG, Relatório do Arquivo Técnico do DGM[END_REF] used for the first time the term "Urucum" to name the two-mica granites of the Urucum ridge, east of Galileia. Later, [START_REF] Silva | Geologia da Folha SE-24-Rio Doce[END_REF] defined the Urucum suite, including the Urucum Granite, the Palmital Granodiorite [START_REF] Barbosa | Geologia das quadriculas Barra do Cuité e Conselheiro Pena, MG, Relatório do Arquivo Técnico do DGM[END_REF]) and associated pegmatites. They also describe xenoliths of São Tomé Group schists and suggest an origin of this granites by melting epi-to mesozonal of the base of this group and of their lower units (Crenaque Group) and of part of the Pocrane Complex.

The Urucum suite in Minas Gerais occupies about 250 km 2 . It consists of three main plutons: (1) Urucum (porphyritic facies), ( 2) Palmital (inequigranular facies) and (3) tourmaline granite (tourmaline-bearing facies). These plutons are elongated (Palmital) and rounded (Urucum), and oriented in direction NW-SE and N-S. They are foliated, especially at its borders and in the vicinity of shear zones and host rocks. The foliations are steep-to vertical-dipping (Fig. 1b). These plutons are located in the central part of a NW-trending brachyanticlinal structure, located east of Galileia (Moura et al. 1978b[START_REF] Filho | Reconhecimento de pegmatitos da província oriental brasileira entre Aimorés e Itambacuri, MG. In: 31º Congresso Brasileiro de Geologia[END_REF]. Their emplacement is associated with the Conselho Peña-Resplendor Shear corridor [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF][START_REF] Nalini | A importância da tectônica transcorrente no alojamento de granitos pré a sincolisionais na região do vale do médio Rio Doce: o exemplo das suítes graníticas Galiléia e Urucum[END_REF].

The rocks of Urucum suite are characterized by the foliations developed in solid and magmatic states, related to the first regional deformation phase (D 1 ). This phase is also recorded in the São Tomé Formation schists (Sn-foliation) [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF][START_REF] Nalini | A importância da tectônica transcorrente no alojamento de granitos pré a sincolisionais na região do vale do médio Rio Doce: o exemplo das suítes graníticas Galiléia e Urucum[END_REF]. The metamorphic assemblage of these rocks (staurolite and almandine) suggests metamorphism of lower amphibolitefacies, that occurred under the following conditions: P-about 4-5 kbar, and T ranging from 500 to 600ºC [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF]. In this sense, the emplacement of the Urucum Suite is considered syn-tectonic with respect to D 1 -phase, and its generation is related to a regional metamorphic event that affected the above schists and that took place during crustal thickening [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF]).

In the Rio Doce Valley, peraluminous granites (S-type) are associated with pegmatitic bodies, being well-known the Marilac of Galilelia-Conselheiro Peña pegmatitic fields (Correia [START_REF] Neves | A província pegmatítica oriental do Brasil à luz dos conhecimentos atuais[END_REF]). The Marilac pegmatitic field, situated northwest of the Governador Valadares city, is 30 -40 km wide and stretches out for 90 -100 km along an almost N-S direction. The Conselheiro Peña-Galileia pegmatitic field, situated east of Governador Valadares, is 35 -45 km wide and stretches out for 100 km along an almost N-direction. These pegmatites are emplaced in garnet-and staurolite mica-schists of the São Tomé Group and in Neoproterozoic granitoids of the Galileia and Urucum suites.

Petrography

The Urucum suite is constituted by four main facies: (i) a porphyritic (Urucum facies), (ii) a medium-to coarse inequigranular (Palmital facies), (iii) a tourmaline-bearing, and (iv) a pegmatitic facies. The predominant facies are the first two (Fig. 1b). The tourmaline-bearing facies can constitute bodies of ca. 15 km 2 , as the one that occurs in the southeastern region of Conselheiro Peña. These granites are less deformed than those of the Palmital facies and are emplaced in quartzites of the Crenaque Group [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF]). Their texture is granular, and the rock-forming minerals are biotite, muscovite, potassic feldspar (microcline and orthoclase) and plagioclase. The Millimeter-sized apatite is the most abundant accessory mineral and commonly occurs as inclusion in biotite.

Geochemistry

Twenty five representative samples of all compositions, textures and grain size of the Urucum suite were selected for whole-rock analysis (major and trace elements), 8 being from the porphyritic (Urucum) facies, 12 from the medium-to coarse inequigranular (Palmital) facies, 2 from the tourmaline-bearing facies, 2 from the pegmatitic facies, and 1 from the aplitic vein that crosscuts the other facies.

The samples were selected so as to represent the whole range of textures, compositions and grain-sizes of each facies. Special attention was given to samples that showed, under the microscope, cummulatic features, defined by both ferromagnesian minerals and feldspars, or even accessory minerals as apatite, zircon etc. Attention was also given to samples that showed some indication of fluid-phase interaction, either as incipient alteration of feldspars, biotite or amphibole, mainly related to silicification, albitization or greisenization.

The chemical analyses were carried out at the Geochemistry Laboratory of the Saint-Etienne School of Mines, France. The precision of the results was ensured by comparison/control with certified international standards, simultaneously analyzed with each group of samples.

The data were obtained by X-ray fluorescence spectrometry model PW 1404 Philips spectrometer and ICP (Induced Coupled Plasma) emission spectrometry, model JY38PI + JY32P spectrometer.

The major-element analysis carried out by X-ray fluorescence and ICP methods, enabling the comparison between results and/or their use as complementary analytical methods. Major elements are very accurate by ICP and were perfomed for MgO, MnO, CaO and TiO 2 , considering that the contents of such components are rather low for the more evolved granites.

Characterization of the Urucum Suite granitoids

The leucogranites of Urucum suite are characterized by plot mainly in the granite and adamellite fields of the chemical-mineralogical diagram of [START_REF] Debon | A chemical-mineralogical classification of common rocks and associations[END_REF], and follow a trend that approaches the calc-alkaline trend defined by these authors (Fig. 2).

Figures 2 to 5

In Figure 3, the analyzed samples define two fields in the domain of the peraluminous twomica granites: one representing the predominance of muscovite over biotite (field I), and another, the predominance of biotite over muscovite (field II). The peraluminous character of these rocks is attested by the alumina saturation diagram (A/CNK vs. A/NK, Fig. 4); the index values fall in the 0.98-1.38 interval, with an average of 1.13. These values are compatible with the interval defined by [START_REF] Chappell | I-and S-type granites in the Lachlan Fold Belt[END_REF] for Australian S-type granites (1.01-1.39).

The peraluminous character of the Urucum suite granitoids is expressed by the presence of muscovite, garnet and tourmaline as the primary mineral assemblage, as well as by the presence of normative corindon (up to 4.7%).

The CaO/Na 2 O ratios of the different facies of studied suite are equal to 0.28. This value is within the range of pelitic-derivated sequences post-collisional strongly peraluminous granites [START_REF] Sylvester | Post-collisional strongly peraluminous granites[END_REF]).

The behavior of major elements

To study the element behavior during the crystallization process, the sum Fe 2 O 3 t + MgO + MnO + TiO 2 (FMMT), which well discriminates the different facies, was used as a differentiation index.

In general, an increase in SiO 2 occurs with the decrease of FMMT during the differentiation process of the magma (Figs. 5 and6). This behavior suggests the fractionation of biotite, tourmaline and garnet. The MgO/TiO 2 ratio varies from 2.14 to 5.33, being higher than that for the I-type granitoids (Galileia suite: varies from 2.25 to 3.45), suggesting that the rocks studied here were originated from melting of metapelitic sequences.

FIGURES 6 TO 11 aqui Sample MD 29 (Fig. 5) has a relatively higher SiO 2 content (73%), despite relatively high MgO (0.75%) and low Na 2 O contents (1.8%). This behavior strongly suggests that changes in composition were resultant from greisenization.

The same diagram shows that samples of the tourmaline-bearing facies contrast from the others, yielding relatively lower SiO 2 contents (70.9 and 71.9 %). Sample MD07.2 is more Al 2 O 3 , CaO and Na 2 O enriched than CP05A (15.1, 1.6 and 4.3% vs. 13.7, 1.1 and 3.8%, respectively). One of the samples (CP05A) has significant tourmaline content.

The ternary diagrams, including alkaline and earth alkaline metals, alumina and total ferromagnesian minerals (FMMT), show the variation and mobility of these elements (Fig. 7).

Diagram CaO-Al 2 O 3 -FMMT shows plagioclase enrichment for most of the granite samples of the Palmital facies (Fig. 7). These samples show depletion of P 2 O 5 (< 0.16%) (Fig. 8) and MnO (Fig. 9). In general, an increase in MnO/(MnO+Fe 2 O t ) values is observed from the Urucum suite granites to the pegmatites (Fig. 9). This explains the importance of garnet crystallization in the more evolved (pegmatitic and tourmaline-bearing) facies.

The diagrams (Figs. 9 and 10) show a wide dispersion of total alkalis contents. This behavior may be explained by wide variation in the content of potassic feldspar megacrystals in the outcrop scale. Al 2 O 3 and total alkalis contents increase from the Urucum facies to the pegmatitic facies (Figs. 9 and 10). The Urucum suite leucogranites are relatively more Na 2 O enriched than the Himalayan Manaslu leucogranites [START_REF] Vidal Ph | Geochemical investigations of the origin of the Manaslu leucogranite (Himalaya, Nepal)[END_REF]) (Fig. 11).

The behavior of trace elements

The contents of transition elements (Co, V, Zn, Ga, Ni and Cr) decrease with differentiation, exhibiting steeper gradients for V, Co and Ni, but a less steep gradient for Ga (Fig. 12). Most of the tourmaline-bearing samples are enriched in transition elements, which reflect the role played by this mineral in the incorporation of such elements.

FIGURE 12 AQUI

The dispersion of Rb (between 121 and 262 ppm) and Ba (< 500 ppm) contents results from the crystallization of potassic feldspar megacrystals. On the other hand, the increase of Ba/Sr values (excepting for microgranites) reflects plagioclase crystallization (Fig. 10).

Despite the dispersion seen in Figure 13, Th contents decrease with the evolution from the Urucum granite to the pegmatites. Some Palmital (MD60-22.6 ppm; MD59-15.7 ppm; MD79-14.1 ppm) and Urucum (MD56-20.5 ppm) granite samples are relatively more Th enriched, probably due to their higher monazite content, which explains why they do not plot in main trend.

The Th/U ratio, between 0.30 and 4.33, is relatively low when compared to the usual values (from 3 to 5) yielded by granitic rocks [START_REF] Fourcade | Géochimie des granitoides[END_REF]), but are comparable with the values obtained by Cuney et al. (1984) for the Himalayan Manaslu leucogranites (0.2 < Th/U < 8). This ratio is controlled by monazite extraction, and the resulting fractionation effect has been used to explain the low values found for the Himalayan leucogranites [START_REF] Vidal Ph | Geochemical investigations of the origin of the Manaslu leucogranite (Himalaya, Nepal)[END_REF].

FIGURES 13 TO 18 AQUI

In general, the solubility of zircon decreases with temperature, while magma acidity and the peraluminous character increase [START_REF] Watson | Zircon saturation in felsic liquids: experimental data and applications to trace element geochemistry[END_REF][START_REF] Watson | Zircon saturation revisited: temperature and composition effects in a variety of crustal magma[END_REF][START_REF] Watson | Accessory minerals and the geochemical evolution of crustal magmatic systems: a summary and prospectus of experimental approaches[END_REF]. However, the saturation level depends strongly upon molar (Na 2 O+K 2 O)/Al 2 O 3 ) of the melts, with remarkably little sensitivity to temperature, SiO 2 concentration, or melt Na 2 O/K 2 O. [START_REF] Watson | Zircon saturation in felsic liquids: experimental data and applications to trace element geochemistry[END_REF] experiments show that in peraluminous melts and melts lying in the quartz-orthoclase-albite composition plane, less than 100 ppm Zr is required for zircon saturation. The mains conclusion of author is that any felsic, no-peralkaline magma is likely to contain zircons crystals, because the saturation level is so low for these compositions.

Zr contents decrease with differentiation and show negative correlation with U (except for pegmatites) (Fig. 14), showing that at the last stages of the magmatic crystallization U behaves as an incompatible element, thus leading to U enrichment in the residual liquids, fact confirmed by the presence of U minerals in the pegmatites.

Y contents are controlled by zircon in the less evolved facies (Urucum and Palmital granites) and by garnet in the more evolved facies (tourmaline-bearing granites and pegmatites) (Fig. 15).

Discrimination diagrams for tectonic settings

The composition of the Urucum suite granitoids is comparable to that of syn-collisional granites of [START_REF] Batchelor | Petrogenetic interpretation of granitoids series using multicationic parameters[END_REF] (Fig. 16). This observation is confirmed by the Rb/30-Hf-Ta*3 diagram of [START_REF] Harris | Post-collision magmatism and tectonics in northwest Turkey[END_REF] (Fig. 17) and the Y/44-Rb/100-Nb/16 diagram of Thiéblemont and Cabanis (1990) (Fig. 18). These parameters indicate that the composition of Urucum suite is similar to that of syn-collisional granites described by those authors. Ta contents (determined by neutron activation) increase from the Urucum to the tourmaline-bearing facies and then decrease to the pegmatitic granite, indicating that during the crystallization of the latter Ta behaved as an incompatible element. Ta enrichment in the residual pegmatitic liquid is confirmed by the crystallization of niobium tantalates in the pegmatites.

In the multi-element diagrams of et al. 1984). The high Rb contents of these granites are in many cases because they are derived from melting of metapelites. Negative anomalies result for Ba, Ta, Hf, Zr and Yb.

FIGURE 19 AQUI

The pegmatitic granites behave in a relatively distinct way. These feldspar-rich rocks show positive Rb and Nb anomalies. On the other hand, the values for elements such as Ba, Th and Ta approach those for oceanic-ridge granites, whereas Ce, Hf, Zr, Sm, Y and Yb show values around 0.1 times the normalization values (Fig. 19).

DISCUSSION

The Urucum suite is characterized by peraluminous granitoids whose alumina saturation index is comparable to those for the Australian S-type granites [START_REF] Chappell | Two contrasting granite types[END_REF]. However, the Urucum suite granites are more Na 2 O enriched (average 3.5 vs. 2.5 %) and more MgO and CaO depleted (average 0.58 and 1.0 % vs. 1.0 and 1.7%, respectively) than the average S-type granites [START_REF] Chappell | I-and S-type granites in the Lachlan Fold Belt[END_REF]. The CaO/Na 2 O ratios (0.28) are compatible with derivated-pelitic sequences peraluminous granites [START_REF] Sylvester | Post-collisional strongly peraluminous granites[END_REF]. The composition of the Urucum suite granitoids is comparable, nevertheless, to that of the syn-collisional granites (Nalini et al. 2000b).

Harker-type diagrams show more or less continuous trends from the (less evolved) Urucum to the (more evolved) tourmaline-bearing and pegmatitic facies, which puts in evidence the fractionation by ferromagnesian minerals, feldspars and accessory minerals during the crystallization of the Urucum suite granitoids. On the other hand, the dispersion illustrated in the alkaline metal diagrams is compatible with crystallization of potassic feldspar as important cummulatic phase, particularly in the pegmatitic facies. Al 2 O 3 enrichment also takes place, as suggested by the petrographic observations.

The decrease in transition elements and concentrations (Fig. 12) during magma evolution is due to biotite, tourmaline and garnet fractionation.

Isotopic data available for the Urucum suite (six samples) yield initial Sr 87 /Sr 86 ratios in the 0.711 -0.716 interval, and ε Nd (580 Ma) values between -7.4 and -8.2 are compatible as a magma produced by crustal melting of the pelitic sedimentary sequences [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF], Nalini et al. 2000a).

Model ages calculated according to depleted mantle (De Paolo 1981) and obtained for six Urucum suite samples yielded ages in the 1840 -2290 Ma interval, which is confirmed by inherited zircon U/Pb ages of 2000 ± 300 Ma, suggesting the involvement of Paleoproterozoic protoliths in the origin of the Urucum suite (Nalini et al. 2000a).

Geothermometric data were obtained by three methods: (a) apatite and zircon saturation [START_REF] Watson | Accessory minerals and the geochemical evolution of crustal magmatic systems: a summary and prospectus of experimental approaches[END_REF], (b) content of light rare earth in granitic liquids [START_REF] Montel | Experimental determination of the solubility of Ce-monazite in SiO2-Al2O3-K2O-Na2O melts at 800 °C, 2 kbar, under H2O-saturated conditions[END_REF], and

(c) substitution in mica [START_REF] Monier | Muscovite solid solutions in the system K20-MgO-FeO-A1203-SiO2-H20:an experimental study at 2 kbar PH2O and comparison with natural Li-free white micas[END_REF]. These results indicate crystallization temperatures in the range of 700 -750 ºC for the Urucum and Palmital facies, from 650 -700ºC for the tourmaline-bearing facies, and about 600 -650ºC for the pegmatitic facies [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF]). As previously mentioned, barometric data suggest minimum pressure conditions around 4 kbar [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF].

The comparison of the data presented here with those available in the literature shows that the age for the granitoids of the Urucum suite (582 Ma) falls in the interval of the syn-collisional magmatism of the Araçuaí Orogeny (595 and 575 Ma) and of the Ribeira belt (600 to 590/570 and even 560/540 Ma) in Rio de Janeiro State, respectively [START_REF] Heilbron | A orogênese Brasiliana no segmento central da Faixa Ribeira, Brasil[END_REF]2004;[START_REF] Machado | U/Pb geochronology of the central Ribeira belt: implications for the evolution of brasiliano orogeny[END_REF][START_REF] Machado | Litogeoquímica e tectônica dos granitóides neoproterozóicos do cinturão Paraíba do Sul no Estado do Rio de Janeiro[END_REF][START_REF] Machado | Caracterização geoquímica e tectônica dos granitóides précolisionais neoproterozóicos do Cinturão Paraíba do Sul no Estado do Rio de Janeiro[END_REF][START_REF] Trouw | The central segment of the Ribeira Belt[END_REF][START_REF] Heilbron | Timing of terrane accretion in the Neoproterozoic-Eopaleozoic Ribeira orogen (SE Brazil)[END_REF][START_REF] Silva | Zircon U-Pb SHRIMP dating of the Serra dos Órgãos and Rio de Janeiro gneissic granitic suites: implications for the (560 Ma) Brasiliano/Pan-African collage[END_REF][START_REF] Pedrosa-Soares | Geotectonic significance of the Neoproterozoic granitic magmatism in the Araçuaí belt, Eastern Brazil: a model and pertinent questions[END_REF][START_REF] Pedrosa-Soares | The Araçuaí-West-Congo Orogen in Brazil: an overview of a confined orogen formed during Gondwanaland assembly[END_REF], 2008;[START_REF] Pedrosa-Soares | Evolution of the Araçuaí Belt and its conection to the Ribeira Belt, eastern Brazil[END_REF], and correspond the same range of pre-collisional magmatism of the Rio Docearc/orogeny [START_REF] Figueiredo | Geochemistry of the Rio Doce magmatic arc, Southeastern Brazil[END_REF][START_REF] Neto | The Rio Doce orogeny, southeastern Brazil[END_REF].

CONCLUSIONS

During the interpretation of the Urucum suite geochemical data, a strong relation between the evolution of (major and trace) elements and the fractional crystallization of feldspars, ferromagnesian and accessory minerals was stressed out. The accumulation of alkaline feldspar Urucum and pegmatitic facies was not confirmed in the diagrams using K.

As a whole, the different facies define an evolution in the following sequence: Urucum suite granites, pegmatitic granites, Palmital granite and tourmaline-bearing granite. Thus, the fractional crystallization can be explained on the basis of variations exhibited by the major and trace element variation diagrams, in which the behavior of compatible elements, such as Mg, Ti, Fe, Ba, Zr, Th, Co, V, Zn, Ga, Ni and Cr, is explained by the conspicuous biotite fractionation. On the other hand, alkalies, Mn, P, Li, Ta, U and B show incompatible behavior during magma evolution.

The tourmaline crystallization (tourmaline-bearing facies) is compatible with fractional crystallization of the essential minerals and biotite presents in the magma and progressive B enrichment in the residual magma. However, the crystallization of small quantities of tourmaline as observed in the Urucum suite tourmaline facies (usually < 1 -2%) is not enough to significantly deplete the residual liquid in B [START_REF] Pichavant | An experimental study of the effect of boron on a water satured haplogranite at 1 kbar vapour pressure[END_REF]). This fact is confirmed by the extensive presence of tourmaline in the rare element-bearing pegmatites associated with the granites.

Geothermobarometric data available for the Urucum suite suggest crystallization under conditions temperatures varying between 750 (Urucum and Palmital facies) and 600ºC (pegmatitic facies), and minimum pressures around 4 -5 kbar (or 12 -15 km depths) [START_REF] Nalini | Caractérisation des suites magmatiques néoprotérozoïques de la region de Conselheiro Pena et Galiléia (Minas Gerais, Brésil)[END_REF]. These data are compatible with the behavior showed by major and trace element diagrams.

Sr and Nd isotopic data available for the Urucum suite granitoids are similar to those obtained for syn-collisional granites (suite G 2 of Pedrosa-Soares & Wiedemann-Leonardos 2000) of the northern portion of the Araçuaí belt [START_REF] Martins | Geologia isotópica do plutonismo Neoproterozóico da Faixa Araçuaí, região nordeste de Minas Gerais[END_REF][START_REF] Martins | Sr and Nd characteristics of Brasiliano/Pan-African granitoid plutons of the Araçuaí Orogen, Southeastern Brazil: tectonic implications[END_REF], thus stressing out a strong crustal contribution during the generation of these rocks. The high initial isotopic ratios yielded by the four facies of the Urucum suite (0.7465 -isochron value, or from 0.7114 to 0.7165individual samples), which correspond to strongly negative ε Nd (580 Ma) values (between -7.4 and -8.2), are compatible with a wide partial melting of pelitic sequences to generation of its magmatism.

The relative coherence of T DM model ages from 1.8 Ga to 2.3 Ga, obtained for all facies, with the inherited zircon ages around 2.2 Ga, also suggesting melting of sediment derived from Paleoproterozoic rocks as probable sources of magma generation. This interpretation implicates a crustal residence of ca. 1.5 Ga for the granite protolith(s). Vein of granite.

  accessory minerals are apatite, garnet, zircon, monazite and tourmaline.The Urucum and Palmital facies show transitional contact between each other. It is marked by increasing of potassic feldspar megacrystals toward Urucum facies, with the texture passing of inequigranular to porphyritic. Centimeter-sized (6 to 8 cm) potassic feldspar megacrystals (microcline) are common in this facies. Essential minerals are plagioclase and potassic feldspar (50-70% of rock volume), with variable quartz, muscovite and biotite contents. Plagioclase crystals rimmed by albite are included in potassic feldspar megacrystals. Frequent accessory minerals are garnet, tourmaline, ilmenite and apatite. Feldspar megacrystals are usually aligned and possibly define a magmatic foliation. In the vicinity of shear zones occurs solide-state deformation observed under the microscope, being commom protomylonitic texture with potassic feldspar porphyroclasts they involved by a finer matrix showing composed of recrystallized quartz, plagioclase, mica and microcline together with an expressive amount of myrmekite.Two types of plagioclase are distinguished: euhedral to sub-euhedral, poikilitic (millimeterto centimeter-sized) megacrystals with muscovite, biotite, quartz and microcline inclusions, and sub-euhedral crystals that compose the matrix. Usually, the latter contains mineral inclusions, but in smaller amounts than the first one. The first type of plagioclase also occurs as inclusions or surrounding potassic feldspar megacrystals. An albite reaction rim is also observed, in the subhedral plagioclase grains.The microcline is more common than orthoclase. It occurs mainly in the matrix, being rare as megacrystal. They are anhedral to sub-euhedral and exhibit characteristic geminations, and contain mica, quartz and albite-rimmed plagioclase inclusions. Microcline usually occurs as interstitial crystals or develops along plagioclase fractures.Quartz is either strongly recrystallized or occurs as hexagon-shaped, euhedral crystals with triple junctions and also as tear drop-shaped inclusions in micas and feldspars. Euhedral to subeuhedral, reddish brown biotite crystals present varied sizes and frequently occur in clusters, forming cummulatic textures.Muscovite occurs in some Urucum suite granites and, with biotite, defines the foliation of the rock. Two types of muscovite are distinguished: primary and secondary. The first type is present as phase essential mineral (5 -10%) and contains inclusions of quartz, zircon and monazite. The second type is less abundant than first and lies along the cleavage planes of plagioclase (either megacrystals or crystals of the matrix) or potassic feldspar.

  Figure 19 (values normalized to mid-ocean ridge granites of Pearce et al. 1984), a similar behavior is observed for the Palmital, Urucum and tourmalinebearing facies. These facies altogether present enrichment in large-ion lithophile elements (LILE), K 2 O, Rb and Ba. Additionally, positive Rb, Th, Nb and Sm anomalies are observed. The relatively high Rb values are typical of syn-collisional granites, implicating an important fluid phase (Pearce

From

  the exposed above, the Urucum suite granites (U/Pb age of 582 Ma) are (~30 to 40 Ma) older than the syn-collisional granites (ages between 560 and 530 Ma) of the Rio Doce magmatic arc. Alternatively, they correspond to the syn-collisional magmatism (ages between 591 and 575 Ma) of the Araçuaí belt and also to the syn-collisional magmatism (ages between 600 and 590/570 Ma) of the Ribeira belt in Rio de Janeiro State. The existence of S-type granites (Urucum suite) with (U-Pb zircon ages of 582 ±2 Ma (Palmital facies) and 573 ±4 Ma (megaporphyritic facies) suggests an interval of about 10 Ma between the end of the I-type calc-alkaline magmatism (Galileia suite, U-Pb age of 594 ±6 Ma) and the beginning of the peraluminous magmatism in the Rio Doce Valley.Tectonic models of continental collision involving significant crustal thickening (Alpine-Hymalaian type) are compatible with tectonic models proposed for the Araçuaí belt. In this sense, it is assumed in this work that the peraluminous granites from the Urucum suite were generated during late-collisional stage, similarly to what was interpreted for the S-type granites of the Rio de Janeiro state[START_REF] Machado | Revisão e discussão do significado tectônico dos granitóides do tipo-S no estado do Rio de Janeiro[END_REF].

Figure 1 .

 1 Figure 1. (A) Simplified geological map of the Araçuaí orogen and adjacent regions of the São Francisco Craton (modified from Pedrosa-Soares et al. 2007 and 2008). (B) Geologic map of the

Figure 12 .

 12 Figure 12. Distribution of granitic facies of Urucum suite based on the diagram with trace elements. Symbols: (+) Pegmatitic Granite; Tourmaline granite; (0) Palmital Granite; • Urucum Granite; Vein of granite.

Figures

  Figures 13 to 18. Distribution of granitic facies of Urucum suite based on the diagrams: (13) FMMT-Th, (14) Zr vs. U), (15) Y-Zr/10-Mn O* 100 ,(16) Batchelor & Bowden (1985), (17) Harris et al. (1994) and (18) Thièblemont & Cabanis (1990). Symbols: (+) Pegmatitic Granite; Tourmaline granite; (0) Palmital Granite; •Urucum Granite;

Figure 19 .

 19 Figure 19. Distribution patterns of the granitic facies of Urucum suite based on the multi-

ACKNOWLEDGMENTS

The authors (Machado R. and Nalini Jr. H.A.) thank the National Council for Scientific and Technological Development (CNPq) for the concession of productivity in research grants (processes 300423/82-9 and 303810/2010, respectively). The authors also thank the comments and suggestions of the two anonymous reviewers for improving of the manuscript.


Ali Assaf

Raphaël Cauderlier

We use Dedukti as a logical framework for interoperability. We use automated tools to translate different developments made in HOL and in Coq to Dedukti and we combine them to prove new results.

Mixing HOL and Coq in Dedukti (Rough Diamond)

1 Intro
Interoperability is an emerging problem in the world of proof systems. Whether they are interactive or automated, theorem provers are developed independently and cannot usually be used together effectively. The theorems of one system can rarely be used in another, and it can be very expensive to redo the proofs manually. The obstacles are many, ranging from differences in the logical theory and in the representation of data types, to the lack of a standard and effective way of retrieving proofs. One solution to this problem is to use a logical framework like Dedukti [START_REF] Saillard | Dedukti: a universal proof checker[END_REF]. The idea is to have a language that is expressive and flexible enough to define various logics and to faithfully express proofs in those logics, at a relatively low cost. Translating all the different systems to this common framework is a first step in bringing them closer together.

Several tools have been developed [START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo[END_REF][START_REF] Assaf | Translating HOL to Dedukti[END_REF][START_REF] Delahaye | Zenon modulo: When Achilles outruns the tortoise using deduction modulo[END_REF][START_REF] Burel | A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo[END_REF] to translate the proofs of various systems to Dedukti. The proofs, represented as terms of the λΠ-calculus modulo rewriting, can be checked independently by Dedukti, adding another layer of confidence over the original systems. This approach has been successfully used to verify the formalization of several libraries and the proof traces of theorem provers on large problem sets.

In this paper, we take one step further and show that we can combine the proofs coming from different systems in this same framework. A theorem can therefore be split into smaller blocks to be proved separately using different systems, and large libraries formalized in one system can be reused for the benefit of developments made in another one.

We used Holide and Coqine to translate proofs of HOL and Coq respectively to Dedukti. We examined the logical theories behind those two systems to determine how we can combine them in a single unified theory while addressing the problems mentioned above. Finally, we used the resulting theory to certify the correctness of a sorting algorithm involving Coq lists of HOL natural numbers 4 . 4 Our code is available online at http://dedukti-interop.gforge.inria.fr/.

Tools used

Dedukti

Dedukti5 is a functional language with dependent types based on the λΠcalculus modulo rewriting [START_REF] Saillard | Dedukti: a universal proof checker[END_REF][START_REF] Saillard | Towards explicit rewrite rules in the λΠ-calculus modulo[END_REF]. The type-checker/interpreter for Dedukti is called dkcheck. It accepts files written in the Dedukti format (.dk) containing declarations, definitions, and rewrite rules, and checks whether they are well-typed.

Following the LF tradition, Dedukti acts as a logical framework to define logics and express proofs in those logics. The approach consists in representing propositions as types and proofs as terms inhabiting those types, as in the Curry-Howard correspondence. Assuming the representation is correct, a proof is valid if and only if its corresponding proof term is well-typed. That way we can use Dedukti as an independent proof checker.

Holide

Holide6 translates HOL proofs to the Dedukti language. It accepts proofs in the OpenTheory format (.art) [START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF], and generates files in the Dedukti format (.dk). These files can then be verified by Dedukti to check that the proofs are indeed valid. The translation is described in details in [START_REF] Assaf | Translating HOL to Dedukti[END_REF].

The generated files depend on a handwritten file called hol.dk. This file describes the theory of HOL, that is the types, the terms, and the derivation rules of HOL. The types of HOL are those of the simply-typed λ-calculus. The propositions are the terms of type bool. type : Type.

term : type → Type. bool : type.

proof : term bool → type. arrow : type → type → type.

...

Coqine

Coqine7 translates Coq proofs to the Dedukti language. It takes the form of a Coq plugin that can be called to export loaded libraries (.vo) to generate files in the Dedukti format (.dk). These files can then be verified by Dedukti to check that the proofs are indeed valid.

A previous version of the translation is described in [START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo[END_REF]. However, that translation is outdated, as it does not support the universe hierarchy and universe subtyping of Coq. The translation has since been updated to support both features following the ideas in [START_REF] Assaf | A calculus of constructions with explicit subtyping[END_REF].

The generated files depend on a handwritten file describing the theory of the calculus of inductive constructions (CIC) called coq.dk. There is a type prop that represents the universe of propositions and a type type i for every natural number i that represents the i-th universe of types. We will write type i and term i for type i and term i respectively. type : nat → Type.

term : Πi : nat. type i → Type. prop : Type.

proof : prop → Type. ...

Mixing HOL and Coq

HOL and Coq use very different logical theories. The first is based on Church's simple type theory, is implemented using the LCF approach, and its proofs are built by combining sequents in a bottom-up fashion. The second is based on the calculus of inductive constructions and checks proofs represented as lambdaterms in a top-down fashion. Translating these two systems to Dedukti was a first step to bringing them closer together but there are still important differences that sets them apart. In this section, we examine these differences and show how we were able to bridge these gaps.

Type inhabitation

The notion of types is different between HOL and Coq. In HOL, types are those of the simply-typed λ-calculus where every type is inhabited. In contrast, Coq allows the definition of empty types, which in fact play an important role as they are used to represent falsehood. A naïve reunion of the two theories would therefore be inconsistent: the formula ∃x : α, , where α is a free type variable, is provable in HOL but its negation ¬∀α : Type, ∃x : α, is provable in Coq.

Instead, we match the notion of HOL types with that of Coq's inhabited types, as done in [START_REF] Keller | Importing HOL Light into Coq[END_REF]. We define inhabited types in the Coq module holtypes:

Inductive type : Type := inhabited : forall (A : Type), A -> type. This is all that we need to interpret hol.type, hol.term, and hol.arrow: hol.type ; coq.term 1 holtypes.type. hol.arrow a b ; holtypes.arrow a b. hol.term a ; coq.term 1 (holtypes.carrier a).

It is then easy to prove in

Booleans and propositions

In Coq, there is a clear distinction between booleans and propositions. Booleans are defined as an inductive type bool with two constructors true and false. The type bool lives in the universe Set. In contrast, following the Curry-Howard correspondence, propositions are represented as types with proofs as their inhabitants. These types live in the universe Prop. Both Set and Prop live in the universe Type 1 . As a consequence, Prop is not on the same level as other types such as bool or nat (the type of natural numbers), a notorious feature of the calculus of constructions. Moreover, since Coq is an intuitionistic system, there is no bijection between booleans and propositions. The excluded middle does not hold, though it can be assumed as an axiom.

In HOL, there is no distinction between booleans and propositions and they are both represented as a single type bool. Because the system is classical, it can be proved that there are only two inhabitants and ⊥, hence the name. Moreover, the type bool is just another simple type and lives on the same level as other types such as nat. To combine the two theories, one must therefore reconcile the two pictures in Figure 1. One solution is to interpret the types of HOL as types in Set. To do this, we must rely on a reflection mechanism that interprets booleans as propositions, so that we can retrieve the theorems of HOL and interpret them as theorems in Coq. In our case, it consists of a function istrue of type hol.bool → coq.prop, which we use to define hol.proof.

hol.proof b ; coq.proof (istrue b).

Another solution is to translate hol.bool as coq.prop. To do this, we must therefore translate the types of HOL as types in Type 1 instead of Type 0 . In particular, if we want to identify hol.nat and coq.nat, we must have coq.nat in Type 1 . Fortunately, we have this for free with cumulativity since any element of Type 0 is also an element of Type 1 .

We choose the first approach as it is more flexible and places less restrictions (e.g. regarding Prop elimination in Coq) on what we can do with booleans. In particular, it allows us to build lists by case analysis on booleans, which is needed in the sorting algorithm.

A concrete example: sorting Coq lists of HOL numbers

We proved in Coq the correction of the insertion sort algorithm on polymorphic lists and we instantiated it with the canonical ordering of natural numbers defined in HOL. More precisely, on the Coq side, we defined polymorphic lists, the insertion sort function, the sorted predicate, and the permutation relation. We then proved the following two theorems:

Theorem sorted_insertion_sort: forall l, sorted (insertion_sort l). Theorem perm_insertion_sort: forall l, perm l (insertion_sort l).

On the HOL side, we used booleans, natural numbers and the ordering relation on natural number as defined in the OpenTheory packages bool.art and natural.art. By composing the results, we obtain two theorems: Πl : coq.term 1 (coq_list hol_nat). proof (sorted (insertion_sort compare l)). Πl : coq.term 1 (coq_list hol_nat). proof (perm l (insertion_sort compare l)).

where compare is the translation of HOL comparison to Coq booleans.

The composition takes place in a Dedukti file named interop.dk. This files takes care of matching the interfaces of the proofs coming from Coq with the proofs coming from HOL. Most of the work went into proving that HOL's comparison is indeed a total order in Coq:

Πm n : nat. if (compare m n) then m ≤ n else n ≤ m.
where nat := holtypes.carrier hol_nat. We prove it using the following theorems from OpenTheory:

Πm n : hol_nat. m < n → m ≤ n Πm n : hol_nat. m ≤ n ↔ n < m
and some lemmas on if . . . then . . . else.

We chose this example because the interaction between Coq and HOL types is very limited thanks to polymorphism: there is no need to reason about HOL natural numbers on the Coq side and no need to reason about lists on the HOL side so the only interaction takes place at the level of booleans which we wanted to study. The resulting implementation is illustrated in Figure 2. All components were successfully verified by Dedukti.

Limitations

Scalability Our experiment, while successful, required a lot of manual tinkering. We attribute this to some technical limitations of the tools we used, which should be addressed before using this approach on a larger scale:

-The translations produce code intended for machines that is not very usable by humans. The linking of theories together should therefore either be more automated or benefit from a more readable output. -The current implementation of Coqine does not support modules and universe polymorphism. We must therefore redefine some types that are in the standard library to avoid using these features. Executability Even though we have constructed a sorting "algorithm" on lists of HOL natural numbers and we have proved it correct, there is no way to actually execute this algorithm. Indeed, there is no notion of computation in HOL, so when the sorting algorithm asks compare for a comparison between two numbers, it will not return something which will unblock the computation. Therefore, insertion_sort [START_REF] Burel | A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo[END_REF][START_REF] Assaf | A calculus of constructions with explicit subtyping[END_REF][START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo[END_REF][START_REF] Assaf | Translating HOL to Dedukti[END_REF] is not computationally equal to [START_REF] Assaf | A calculus of constructions with explicit subtyping[END_REF][START_REF] Assaf | Translating HOL to Dedukti[END_REF][START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo[END_REF][START_REF] Burel | A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo[END_REF]. However, the result is still provably equal to what is expected: we can show that insertion_sort [4, 1, 3, 2] is equal to [START_REF] Assaf | A calculus of constructions with explicit subtyping[END_REF][START_REF] Assaf | Translating HOL to Dedukti[END_REF][START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo[END_REF][START_REF] Burel | A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo[END_REF]. A constructivization of HOL will be necessary before we can obtain truly executable code. Holide is a good starting point for such a project.

  Coq that given inhabited types A and B, the arrow type A → B is also inhabited: Definition carrier (A : type) : Type := match A with inhabited B b => B end. Definition witness (A : type) : carrier A := match A with inhabited B b => b end. Definition arrow (A : type) (B : type) : type := inhabited (carrier A -> carrier B) (fun _ => witness B).

Fig. 1 .

 1 Fig. 1. Booleans and propositions in HOL and Coq. Boxes represent universes.

Fig. 2 .

 2 Fig. 2. Components of the implementation. Solid frames represent source files. Dashed frames represent automatically generated files. Arrows represent dependencies.

Available at: http://dedukti.gforge.inria.fr/

Available at: https://www.rocq.inria.fr/deducteam/Holide/

Available at: http://www.ensiie.fr/~guillaume.burel/blackandwhite_coqInE/