Alexandre Da

Silva Freire

Vicente Acuña

Pierluigi Crescenzi

Carlos Eduardo Ferreira

Vincent Lacroix

Paulo Vieira Milreu

Eduardo Moreno

Marie-France Sagot

A S Freire

P V Milreu

M.-F Sagot

Minimum ratio cover of matrix columns by extreme rays of its induced cone

Keywords: Extreme rays, elementary modes, matrix covering

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Given a matrix S ∈ R m×n , we say that an extreme ray of the cone

F = {v ∈ R n | Sv = 0, v ≥ 0} covers a column k if v k > 0.
In this paper, we study the problem of finding a set of extreme rays of F that cover a subset R of the columns of S.

This problem arises naturally in bioinformatics in the context of metabolic networks, particularly in the study of its elementary modes (EMs). Biologically, an EM is a minimal sub-network that enables the metabolic system to operate at steady state, that is, all internal metabolites (chemical compounds) are produced and consumed in equal quantities. Mathematically, an EM corresponds to an extreme ray of the convex cone defined by the "stoichiometric matrix" of the metabolic reactions in the system. In this matrix, each column corresponds to a reaction and each row to a metabolite. Each entry of the matrix indicates the minimum number of molecules of this metabolite that is produced (the entry is then positive) or consumed (the entry is negative) by the reaction. The number of EMs may be extremely large (several millions) even for small networks (hundreds of reactions) [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF][START_REF] Klamt | Combinatorial complexity of pathway analysis in metabolic networks[END_REF], therefore, the study of the complexity and of algorithms to enumerate all EMs of a network has been deeply explored [START_REF] Acuna | Modes and cuts in metabolic networks: Complexity and algorithms[END_REF][START_REF] Fukuda | Double description method revisited[END_REF][START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF].

Deciding if the stoichiometric matrix can be covered by elementary modes is a problem that has also been well studied [START_REF] Heiner | Petri net based model validation in systems biology[END_REF], but not the associated optimization problem (among all sets of EMs covering the matrix, which one is the "best"). The optimization criterion we introduce now is based on the key idea that not all EMs are equally interesting from the biological standpoint. In particular, nonproportional EMs, i.e. EMs which use each reaction with extremely different fluxes seem to be less relevant (or at least much harder to exploit for biologists) than proportional EMs.

To account for this, we define the ratio of a vector v as the fraction between the maximum and the minimum positive component of v. For a set of extreme rays that cover R, we introduce two different functions in order to measure how proportional a cover is. Namely, we define a local ratio, which measures the ratio of each extreme ray of the cover, and a global ratio, which measures the ratio of the vector obtained by the combination of all extreme rays of the cover.

We note that these concepts also appear naturally in the context of exact linear programming. In fact, current algorithms for scaling a matrix have a complexity that depends on the ratio of its elements [START_REF] Rote | Matrix scaling by network flow[END_REF][START_REF] Nemirovski | On complexity of matrix scaling[END_REF]. Hence, obtaining a method to find extreme rays of a cone with minimal ratio is also an interesting problem for the exact optimization community.

In Section 2, we present the definitions and notation used throughout this paper, as well as the formal definition of the minimum global ratio cover (MGRC) problem and of the minimum local ratio cover (MLRC) problem. In Section 3, we show that the MGRC and MLRC problems are both NP-hard, even in the case that |R| = 1. In Section 4, we introduce a mixed integer programming formulation for the MGRC problem, which is solvable in polynomial time if all columns should be covered, and introduce a branch-and-cut algorithm for the MLRC problem. Finally, we present in Section 5 computational experiments on data obtained from real metabolic networks.

Notation and definitions

Given a matrix S ∈ R m×n , we define the cone

F = {v ∈ R n | Sv = 0, v ≥ 0}.
The support of a vector v ∈ F, denoted by sup(v), is the set of indexes of all nonzero entries of v. A nonzero vector v ∈ F is an extreme ray (ER) of F if its support is minimal, in the sense that there is no other nonzero vector v ′ ∈ F such that sup(v ′ ) ⊂ sup(v). Let S ′ ∈ R m×n ′ be the matrix S without some columns. Note that an ER of

F ′ = {v ∈ R n ′ | S ′ v = 0, v ≥ 0}
is also an ER of F. Two vectors u and v of F are equivalent if u = γv, for some real number γ > 0. Given two ERs u and v of F, we have that sup(u) = sup(v) if and only if u and v are equivalent. Since F is a cone, each vector of F can be obtained by a conical combination of ERs of F. Moreover, given two vectors u and v in F such that u ≤ v, we have that the vector v ′ = v -u is in F.

For simplicity, given an index i ∈ {1, 2, . . . , n}, we use the term "column i" instead of "column indexed by i". A column i of S is covered by a vector v ∈ F if v i > 0. Given a set R ⊆ {1, 2, . . . , n}, we say that a set C of ERs of F covers R if each column in R is covered by at least one ER in C. Equivalently, we say that C is a cover of R. In [START_REF] Acuna | Modes and cuts in metabolic networks: Complexity and algorithms[END_REF] V. Acuña et al. introduced a polynomial time algorithm for finding an ER of F which covers a column k. Using this algorithm as a subroutine, we can design a polynomial time algorithm for solving the problem of finding a cover of a set R ⊆ {1, 2, . . . , n}.

The ratio of a nonzero vector v ∈ F is given by r(v) = maxi vi min j|v j >0 vj . The global ratio of a cover C is given by ψ(C) = r( v∈C v), and the local ratio of C is given by φ(C) = max v∈C r(v). We investigate the following two problems.

Problem 1.

[MGRC] Given a matrix S ∈ R m×n and a set R ⊆ {1, 2, . . . , n}, the minimum global ratio cover problem consists in finding a cover of R with minimum global ratio.

Problem 2.

[MLRC] Given a matrix S ∈ R m×n and a set R ⊆ {1, 2, . . . , n}, the minimum local ratio cover problem consists in finding a cover of R with minimum local ratio.

We say that a vector v ∈ F is normalized if max i v i = 1. Note that r(v) = r(γv), for any γ > 0. Thus, for any vector v ∈ F, there exists an equivalent normalized vector γv ∈ F such that r(v) = r(γv), where γ = 1 maxi vi . Considering only normalized vectors, we have that a vector v ∈ F with minimum ratio maximizes x = min i|vi>0 v i . Since we are seeking for vectors with minimum ratio, this concept of normalization helps us to design our formulations. Note that scaling the ERs of a cover does not affect its local ratio, but it can affect its global ratio, unless we use the same scalar for all ERs in the cover. Thus, for the MLRC problem, we can work only with normalized ERs. For the MGRC problem, we normalize the vector obtained by the combination of the ERs in the cover, but the ERs themselves can be non-normalized.

We assume that S is consistent, in the sense that Problems 1 and 2 have feasible solutions. The problem of recognizing whether S is consistent or not can be solved in polynomial time [START_REF] Acuna | Modes and cuts in metabolic networks: Complexity and algorithms[END_REF].

Complexity of the MGRC and MGLC problems

Given a column k, we denote by MGRC k and MLRC k , respectively, the special case of the MGRC and MLRC problems in which R = {k}. We show that the MGRC k and the MLRC k problems are NP-hard by reducing the three dimensional matching problem to them. The 3DM problem is NP-complete [START_REF] Garey | Computers and Intractability, A Guide to the Theory of NP-Completeness[END_REF] and can be stated as follows: Let S ∈ R m×n be a matrix, where m = 3t and n = |E| + 1, such that, for each triple e i = (w, x, y) in E we have that S wi = S xi = S yi = 1, for each j ∈ {1, 2, . . . , m} \ {w, x, y} we have that S ji = 0, and for j = 1, 2, . . . , m we have that S jn = -1. Let R = {n} be the set of columns that we want to cover. Figure 1 illustrates an example of this construction. We now show that (1) I 3DM Fig. 1. An instance of the 3DM problem and the corresponding (S, R) are drawn at the left and right side, respectively. For each triple ei = (w, x, y) in E, there are edges linking the square ei to circles w, x and y. For each Sij = 1 there is arc (i, j) going from a square i to a circle j and each Suv = -1 there is an arc (u, v) going from a circle u to a square v. contains a perfect matching if and only if there exists a cover C of R with φ(C) ≤ 1 and (2) I 3DM contains a perfect matching if and only if there exists a cover C of R with ψ(C) ≤ 1.

Assume that I 3DM contains a perfect matching E * . Let v ∈ R n be a vector such that v n = 1 and, for i = 1, 2, . . . , n -1, if e i ∈ E * then v i = 1, otherwise v i = 0. Since in this construction Sv = 0 is satisfied and v ≥ 0, we have that v ∈ F. Since column n is the only one with negative coefficients, we have that all nonzero vectors in F must cover n. Observe that any nonzero vector w such that sup(w) ⊂ sup(v) does not satisfy Sw = 0. Thus, v is an ER of F and

C = {v} is a cover of R such that φ(C) = ψ(C) = 1.
Conversely, assume that there exist a cover

C of R such that ψ(C) ≤ 1. Let v = w∈C w and let E * = {e i ∈ E | v i > 0}.
Since column n is the only one with negative coefficients and Sv = 0 is satisfied, we have that v n > 0. Moreover, since column n has coefficient -1 in all rows, we have that each element of W ∪ X ∪ Y is contained in at least one triple of E * . Suppose, by contradiction, that E * contains two triples e i and e j that overlap each other at an element h ∈ W ∪ X ∪ Y . By definition of the function ψ, we have that ψ(C) ≥ 1 and thus ψ(C) = 1. This implies that all nonzero entries of v have the same value. As a consequence, we have that S h * v ≥ v i +v j -v n > 0, where S h * is the sub-matrix of S containing only row h, which is a contradiction. Thus E * is a perfect matching. Assume now that there exist a cover C ′ of R such that φ(C ′ ) ≤ 1. Applying the same arguments we can construct the perfect matching E * . Figure 2 illustrates an example of this construction. We are interested in solving the MLRC k problem because, as we show later on, one can solve Problem 2 by solving MLRC k for each column k. As we show in the next section, the MGRC problem can be solved in polynomial time if R = {1, 2, . . . , n}. However, by adapting the proof of Theorem 1 we can prove the following theorem.

Theorem 2. The MLRC problem remains NP-hard even if R = {1, 2, . . . , n}.

We achieve this by adding a column n + i to S, for each triple e i = (w, x, y) in E, such that S j,n+i = -S j,i , for j = 1, 2, . . . , m. In this way it is possible to cover each pair of columns {i, n + i} with an ER of ratio 1, except for column n, which can be covered by an ER of ratio 1 if and only if E contains a perfect matching.

MIP approaches for the MGRC and MLRC problems

In this section we present Mixed Integer Programming (MIP) approaches for the MGRC and MLRC problems.

A MIP formulation for the MGRC problem

In this section, we introduce a MIP formulation for finding a normalized vector v ∈ F which covers R and has minimum ratio. Then, by decomposing v into ERs of F, we obtain an optimal cover. max x (p mgrc ) s.t.

Sv = 0 (1) x ≤ v i -s i + 1, for i = 1, 2, . . . , n (2) 0 ≤ v i ≤ s i , for i = 1, 2, . . . n (3) s k = 1, for each k ∈ R (4) s ∈ {0, 1} n (5)
The decision variables s ∈ {0, 1} n represent the support of v. In [START_REF] Fukuda | Double description method revisited[END_REF], K. Fukuda and A. Prodon prove the following theorem. Theorem 3. Any vector v ∈ F can be expressed as a convex combination of m -n extreme rays of F.

In [START_REF] Jungers | Fast computation of minimal elementary decompositions of metabolic flux vectors[END_REF], R. M. Jungers et. al. introduce a polynomial time algorithm for finding a such decomposition with minimum cardinality. After solving (p mgrc ), we run this decomposition algorithm on v. Then, we obtain C = {w 1 , w 2 , . . . , w t }, where w 1 , w 2 , . . . , w t is the decomposition found by the algorithm. Observe that ψ(C) = r(v). Since S is consistent and x is maximized, we have that in an optimal solution, x > 0 and v is a normalized vector which covers all columns in R. Moreover, since x = min i|vi>0 v i is maximum, we have that v has minimum ratio. We now argue that C has minimum global ratio. Suppose, by contradiction, that ψ(C) is not minimum. Let C ′ be a cover of R such that ψ(C ′ ) < ψ(C). Thus, the vector h = w∈C w covers all columns in R and r(h) < r(v). Thus, there is a normalized vector γh, such that γh is a feasible solution of (p mgrc ). Moreover, γh leads to a greater value in the objective function, which is a contradiction. Therefore, this procedure solves the MGRC problem.

Observe that if R = {1, 2, . . . , n}, then all variables s are fixed (i.e., we have no decision variables in (p mgrc )). In this case, (p mgrc ) is a linear program and, thus, can be solved in polynomial time [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF]. We denoted this special case of the MGRC problem by MGRC * .

An algorithm for the MLRC problem

The MLRC problem is considerably harder to formulate as a MIP than the MGRC problem. In MGRC we solve a MIP in which the optimal solution can be a non-ER and, after that, we decompose this vector regardless of the ratio of each ER obtained in the decomposition. We cannot apply the same idea for the MLRC, because in this case we have to consider the ratio of each ER inside the cover individually. In this section, we introduce an algorithm for solving the MLRC problem, which works as follows. At each iteration, it chooses an uncovered column k ∈ R and solves the MLRC k problem, i.e. finds an ER v of F which covers k and has minimum ratio. Since the MLRC k problem is NP-hard, we introduce a MIP formulation in which an optimal solution must be an ER. This requirement is not easy to be described with simple linear inequalities and, hence, we propose a branch-and-cut algorithm to solve the problem.

Let H(k) be the set of all ER's of F which cover column k and let H(k) be the set of all ER's of F which do not cover column k. Below we introduce a formulation for solving the MLRC k problem.

max x (p mlrc k ) s.t. Sv = 0 (6) x ≤ v i -s i + 1, for i = 1, 2, . . . , n (7) 0 ≤ v i ≤ s i , for i = 1, 2, . . . n (8) s k = 1 (9) i∈sup(h) s i + s j ≤ |sup(h)|, ∀h ∈ H(k), ∀j / ∈ sup(h) (10) i∈sup(h) s i ≤ |sup(h)| -1, for each h ∈ H(k) (11) s ∈ {0, 1} n (12)
Formulation (p mlrc k ) without constraints [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] and ( 11) is the same as (p mgrc ) for R = {k}. In this case, an optimal solution to (p mgrc ) is a vector v ∈ F which covers k and has minimum ratio. Since v can be a non-ER, we include constraints [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] and [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF] in order to guarantee that v is an ER. Constraint [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] eliminates all vectors which strictly contain the support of an ER which covers k. We could apply inequalities (10) also for the ERs which do not cover k, but in this case we introduce [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF], which is more tight, in the sense that it eliminates all vectors whose support contains (not necessarily strictly) the support of an ER which does not cover k. On the other hand, if we apply constraints [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF] to the ERs which cover k we have no feasible solutions.

Since |H(k)| and |H(k)| can be huge, instead of including constraints (10) and ( 11) a priori, we solve (p mlrc k ) by applying the so-called branch-and-cut method [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF]. To this purpose, we have to solve the separation problem for inequalities [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] and [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF]. Let (l mlrc ) be the linear relaxation of (p mlrc k ), where constraints (12) are replaced by 0 ≤ s i ≤ 1, for i = 1, 2, . . . , n. The separation problem for inequalities [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] and [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF] consist in, given a feasible solution of (l mlrc ), prove that ( 10) and ( 11) are satisfied, or find an ER which does not satisfy [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] or [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF]. One can solve these separation problems by solving their optimization versions, which are stated as follows.

Problem 4. Given a feasible solution of (l mlrc ), find an ER h in H(k) such that i∈sup(h) (1 -s i ) -s j , for some j / ∈ sup(h), is minimum.

Problem 5. Given a feasible solution of (l mlrc ), find an ER h in H(k) such that

i∈sup(h) (1 -s i ) is minimum.
We denote Problems 4 and 5 by sep (10) and sep (11) , respectively. In [START_REF] Acuna | Modes and cuts in metabolic networks: Complexity and algorithms[END_REF] the authors prove the following theorem.

Theorem 4. Given an integer t, deciding the existence of an ER v of F such that |sup(v)| ≤ t is NP-complete.

Let S ′ be the matrix S without column k. For simplicity, we assume that k = n. By finding an ER v * of

F ′ = {v ∈ R n-1 | S ′ v = 0 and v ≥ 0} which minimizes i∈sup(v * ) (1 -s ′ i )
, where s ′ = 0, we can decide the existence of an ER h of F ′ such that |sup(h)| ≤ t. Thus, the sep (11) problem is NP-hard. If we fix a column j = k, then the sep (10) problem becomes equivalent to finding an ER v * of

F ′′ = {v ∈ R n | Sv = 0, v ≥ 0 and v j = 0} which minimizes i∈sup(v * ) (1 -s ′ i )
, where s ′ = 0, and such that k ∈ sup(v * ). If we solve this problem for each k = j, we can decide the existence of an ER h of F ′′ , such that |sup(h)| ≤ t. Thus, we have that the sep (10) problem is NP-hard. Therefore, from Theorem 4 follows Corollary 2.

Corollary 2. Problems sep (10) and sep (11) are NP-hard.

Despite the drawback of Corollary 2, we introduce a MIP formulation for solving the separation of inequalities ( 10) and ( 11) at the same time, which works quite well in practice, as we show in Section 5.

min z = (2 -s k )b k + i =k (1 -s i )b i -j =k s j w j (p sep ) s.t. Sh = 0 (13) 0 ≤ h i ≤ b i , for i = 1, 2, . . . , n (14)
n i=1 h i ≥ 1 (15) j =k w j ≤ b k (16) w j + b j ≤ 1, for each j = k (17) w j ∈ {0, 1}, for each j = k (18) b ∈ {0, 1} n (19)
By constraints (13), ( 14) and (15), we have that h is a nonzero vector in F. The decision variables w are introduced in order to choose a column j which is not in the support of h. By constraints ( 16) and ( 17), if k ∈ sup(h), we have that at most one column outside sup(h) is chosen, otherwise no columns outside sup(h) is chosen. As we explain later on, we are interested only in solutions such that z -1 < 0. Thus, we can apply formulation (p sep ) to the sub-matrix of S which contains only columns in {i | s i > 0}. From a practical point of view, this is a very important property, because this sub-matrix can be much smaller than the original one.

In an optimal solution, if b k = 1, since z is minimum and the variables w have negative coefficients in the objective function, we have that j =k w j = 1 and thus z = i∈sup(h) (1 -s i ) -s j , for some j / ∈ sup(h). Let h ′ be any ER such that sup(h ′ ) ⊆ sup(h) and k ∈ sup(h ′ ). Since z is minimum and (1 -s i ) is non-negative, for i = 1, 2, . . . , n, we have that h ′ is an ER in H(k) such that i∈sup(h ′ ) (1 -s i ) -s j is minimum, where j / ∈ sup(h ′ ). In [START_REF] Acuna | Modes and cuts in metabolic networks: Complexity and algorithms[END_REF], the authors introduce a procedure, namely FindER(S, k), which receives a matrix S ∈ R m×n and a column k ∈ {1, 2, . . . , n}, and returns an ER of F which covers column k. We use this algorithm in order to find h ′ . Therefore, in this case we solve the sep (10) problem . If b k = 0, we have that j =k s j w j = 0 and z

= (2 -s k ) + i∈sup(h)\{k} (1 -s i ) = 1 + i∈sup(h) (1 -s i ).
In the same way as we mention above, we obtain an ER h ′ in H(k), such that sup(h ′ ) ⊆ sup(h) and i∈sup(h ′ ) (1 -s i ) is minimum. Thus, in this case we solve the sep (11) problem. In both cases, we have that if z -1 < 0, then s violates either [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] or [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF], and thus we obtain a cutting-plane from sup(h ′ ) to be included explicitly in (l mlrc ). Otherwise, constraints [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] and ( 11) are satisfied and thus (s, v, x) is a feasible solution of (l mlrc ). From a practical point of view, since h ′ is an ER, we can use r(h ′ ) as an upper bound on the optimal solution of the MLRC k problem for each i ∈ sup(h ′ ). This trick can speed up quite a lot the whole process, because as we show in the algorithm below, we have to solve the MLRC k problem for i = 1, 2, . . . , n.

We now introduce an algorithm for the MLRC problem. Correctness of Algorithm 1 follows from the fact that r(v) is a lower bound for the local ratio of an optimal cover of any set R ′ such that k ∈ R ′ , where v is ER obtained in line 4.

Algorithm 1: Solves the MLRC problem.

Input: A matrix S ∈ R m×n and a set R ⊆ {1, 2, . . . , n}. Output: A cover of R with minimum local ratio.

1:

C ← ∅ 2: while C does not cover R do 3: Choose an uncovered column k ∈ R 4:
Let v be an ER obtained by solving (p mlrc k ) 5:

C ← C ∪ {v} 6: return C

In our implementation, we use some tricks to speed up Algorithm 1. We reuse the cuts found in previous iterations as soon as they violate inequalities [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] or [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF]. We use FindER as a heuristic for finding upper bounds on the minimum ratio needed to cover each column. Moreover, since each cut corresponds to an ER, all ERs found during the branch-and-cut procedure are used in order to update these upper bounds. In this way, we profit from the computational effort spent for finding violated inequalities, in order to generate feasible solutions of the problem. Since, at each iteration, we can choose arbitrarily the next column to be covered, we take one with highest upper bound and, if this upper bound is lesser than or equal to the maximum ratio among the ERs already included in C, we can stop the algorithm. With this strategy, we aim to close the gap between the lower and upper bounds on the minimum local ratio of the cover as soon as possible.

In the separation step, before solving (p sep ), we try to separate inequalities [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] and [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF] by applying a heuristic which considers only the integral entries of support s. In this case, the separation problems can be solved using a simple modification of the FindER algorithm. If we do not succeed, then we solve (p sep ) and collect all ERs which violate [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] or [START_REF] Terzer | Large-scale computation of elementary flux modes with bit pattern trees[END_REF] found during this process, not only the optimal ones (most solvers provide callback routines to this purpose).

Computational experiments

We obtained our data set by downloading metabolic networks from MetExplore [START_REF] Cottret | MetExplore: a web server to link metabolomic experiments and genome-scale metabolic networks[END_REF]. We restricted the networks to the small-molecule metabolism, meaning that reactions involving macromolecules such as nucleic acids or proteins were removed. We set the filters to exclude pairs of co-factors and common compounds, which otherwise would connect unrelated reactions. Pairs of co-factors include NAD / NADH, NADP / NADPH, ADP / ATP (for the full list, see the MetExplore documentation). Common compounds include water, proton, CO2, phosphate, diphosphate, NH3, H2O2 and O2. In order to make the matrices consistent, we removed all columns which are not covered by any ER. We used CPLEX c 12.2 as the MIP solver and the machine configurations are the following: 1 single processor 3.8GHz and 4GB of RAM. In our tests, we did not consider the time for reading the input files.

In Table 1, we show the results of the computational experiments made with our MIP approaches for the MGRC * and the MGRC problems. In the case of the MGRC problem, we made tests with several different sizes of R. We solved more than 100 different instances and report here the results that we consider more relevant. We observed that the MGRC problem becomes harder when |R| is very small, thus in the results presented here we chose small subsets of columns to be covered. Each row of Table 1 shows one execution of the MGRC * problem and the arithmetic mean of 100 executions of the MGRC problem, where in each execution a set R was randomly chosen, such that 1 ≤ |R| ≤ 5. The acronyms "NzCf" and "BBN" stand for, respectively, "nonzero entries in the input matrix" and "branch-and-bound nodes explored during the execution". 1 shows, our approach for the MGRC problem is very effective. We selected the hardest instances among all that we tested, and nevertheless each instance was solved in a few seconds. In the case of the MGRC * problem, the running time was quite short.

In Table 2, we present the results of the computational experiments made with our branch-and-cut algorithm for the MLRC problem. In our tests, we chose R = {1, 2, . . . , n}. The acronyms "MS', '"NO" and "Cuts" stand for, respectively, "MIPs solved during the procedure", "columns covered by ERs that can be nonoptimal" and "cuts generated during the branch-and-cut procedure". In our implementation, we used three parameters, namely TOTAL TL=1h, IT1 and IT2 TL=15s. We observed that different choices of these parameters can change dramatically the running time of the algorithm, as well as the number of uncovered columns and the quality of the gap, in the case that the solution found is not optimal. Moreover, some choices are good for some instances, but worse for others. At each step in which we solve the MLRC k problem, we set the time limit of either IT1 TL or IT2 TL, where IT2 TL is used only if the total time spent is greater than TOTAL TL. In the case that no optimal solution is found, we leave the corresponding column temporarily uncovered and use the lower bound obtained by the unterminated MIP as a lower bound on the minimum local ratio of the cover. If after the last iteration there are uncovered columns, we cover these columns with the best ERs that cover them and report, in column NO, how many columns were covered in this way.

As Table 2 shows, our branch-and-cut algorithm was able to solve instances of reasonable size. In most of the cases, the number of columns covered by possibly non-optimal ERs was small if compared to the total number of columns. In some cases, the gap between the solution found and an optimal one is tight. Depending on the structure of S, some columns are much harder than others to be covered. In general, in the biological applications that we are interested in, R is a small subset of columns. Thus, depending on the choice of R, our algorithm can solve instances with about 2500 columns. However, if R intersects the "hardest" columns, the algorithm may take a long time and still not solve the problem. Since the application that initially motivated this problem comes from biology, where the input can be very large, one future work is to improve the method to enable solving larger instances. In the next section, we suggest some directions that can be explored in order to improve our method.

Conclusion and future work

We showed that the MGRC and MLRC problems are NP-hard even when |R| = 1. We then presented a mixed integer programming formulation for the MGRC problem, which is solvable in polynomial time if all columns should be covered, and a branch-and-cut algorithm for the MLRC problem. We experimentally showed that our approach for the MGRC problem is very effective for solving large scale instances of the problem. In the case of the MLRC problem, we were able to solve instances of reasonable size.

As future work, we suggest some directions that can be explored in order to improve our method for the MLRC problem. Our method has the following three key points which can be explored in order to achieve a better performance:

(1) the order in which we try to cover the columns; (2) the configuration of the time outs; (3) the strength of the formulation for the MLRC k problem. With respect to (1), approximation algorithms for the MLRC k problem may lead to a better estimative of the upper bounds of the minimum local ratio needed to cover each column. This could help to find a better order to iterate over the columns. With respect to (2), since a given choice of the time outs can be good for some instances and worse for others, probably we can obtain better results by making this choice dynamically. Finally, with respect to (3), it is still not clear in which cases we can strengthen inequalities [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF]. Moreover, new classes of valid inequalities could also improve the performance of the method.

Problem 3 .

 3 [3DM] Given a set of triples E ⊆ W × X × Y , where |W | = |X| = |Y | = t and the sets W , X and Y are disjoint, determine if there exists a subset E * ⊆ E of non-overlapping triples such that |E * | = t (E * is called a perfect matching). Theorem 1. The MGRC k and the MLRC k problems are NP-hard. Proof. Given an instance I 3DM = (E, W, X, Y ) of the 3DM problem, where |W | = |X| = |Y | = t, we construct S and R in the following way. For simplicity, we assume that E = {e 1 , e 2 , . . . , e |E| } and W ∪ X ∪ Y = {1, 2, . . . , 3t}.

Fig. 2 .Corollary 1 .

 21 Fig. 2. At the left side a perfect matching in I3DM and at the right side a cover C = {v} of R such that φ(C) = ψ(C) = 1.

Table 1 :

 1 Computational experiments with the MGRC * and the MGRC problems.

	MGRC *	MGRC

Table 2 :

 2 Computational experiments with the MLRC problem, where R = {1, 2, . . . , n}.

	Instance	n m #NzCf #MS #Cuts #BBN φ(C) #NO	Time
	ONYPE335 838 174 1839 95691	13	1581	8.0	0	27m08s
	YERYP364 955 409 2393	57 33584	128	8.0	0	7m26s
	SHIFL233 1046 489 2636	10 49647	171	8.0	0	16m14s
	BUCAP86	886 282 2079	18 89772	875	8.0	0	26m31s
	DESPS65	629 297 1533	13 62580	900	11.0	0	15m32s
	BUCBP85 1137 290 2691	46 94608	512 [8 .. 9]	1	27m25s
	HELPY117 684 264 1710	15 168630	3097 [8 .. 10]	5	47m19s
	PVIVAX	1618 346 3878	130 263111	1906 [2 .. 9]	72 1h25m51s
	PLASMO 2563 411 6387	311 193590	1253 [2 .. 12] 133 2h13m51s


Frédéric Blanqui

Kim Quyen Ly

Automated verification of termination certificates

In order to increase user confidence, many automated theorem provers provide certificates that can be independently verified. In this paper, we report on our progress in developing a standalone tool for checking the correctness of certificates for the termination of term rewrite systems, and formally proving its correctness in the proof assistant Coq. To this end, we use the extraction mechanism of Coq and the library on rewriting theory and termination called CoLoR.

I. INTRODUCTION

Being able to prove the correctness of a program is important, especially for critical applications (banking, aeronautics, etc). But this is generally undecidable. So, many different and complementary approaches have been developed for tackling this problem: software engineering methodologies, testing, model-checking, formal proof, etc.

Instead of trying to prove that every possible output of a program is correct, one possible approach consists in making the tool provide, at each run, an evidence that its output is correct. This certificate can then be checked independently by another tool. Although it seems to only move the problem from one program to the other, the certificate verifier, there is in fact a gain in complexity. Typically, a program which goal is to find a solution to some numerical or symbolic problem, will use complex heuristics and optimizations, while checking that the solution found is indeed correct is often much easier. For instance, finding a boolean assignment satisfying some boolean formula (SAT problem) is (in the worst case) exponential in the number of boolean variables, while verifying the correctness of a given assignment (the certificate) is linear in the size of the formula.

Since certificate verifiers are simpler programs, they are more easily amenable to a complete formalization and proof using some proof assistant tool. In fact, various such tools (e.g. Coq [START_REF] Ly | The Coq Reference Manual[END_REF]) are themselves based on this two-level approach: they are composed of a small and hopefully safe kernel responsible of checking the correctness of proofs, and a proof development environment providing unsafe proof tactics and decision procedures for building step by step proofs that, in the end, have to be checked by the kernel to be included in the proof database.

Termination, that is, the fact that a program eventually provides an output to the user, is an important property that is also undecidable [START_REF] Dauchet | Termination of rewriting is undecidable in the one-rule case[END_REF]. Term rewriting [START_REF] Dershowitz | Rewrite systems[END_REF], [START_REF] Van Leeuwen | Term Rewriting Systems, ser[END_REF] is a simple yet very general programming paradigm and framework, based on the notion of rewrite rule, that generalizes or in which to easily encode other programming paradigms like functional or logic programs. Examples of programming languages based on rewriting are [START_REF] Nakagawa | CafeOBJ 1.4.2 User Manual[END_REF], [START_REF] Borovanský | ELAN 3.7 User Manual[END_REF], [START_REF] Bach | TOM 2.7 Manual[END_REF], [START_REF] Clavel | Maude 2.6 Manual[END_REF]. A few years ago, a formal language called CPF [START_REF]Certification Problem Format[END_REF] has been developed that defines a notion of certificate for the termination of term rewrite systems.

In this paper, we consider the problem of developing a standalone tool for checking the correctness of CPF certificates, and formally proving its correctness. In [START_REF] Blanqui | CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates[END_REF], the first author describes a CPF verifier called Rainbow1 based on the following architecture: a compiler (written in OCaml [START_REF] Leroy | The Objective Caml system release 3.12, Documentation and user's manual[END_REF]) from CPF to Gallina, the language of the Coq proof assistant [START_REF] Ly | The Coq Reference Manual[END_REF], generates a Gallina script that is then checked by Coq itself using the Coq library CoLoR [START_REF] Blanqui | CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates[END_REF]. This architecture has some advantages: it provides a way to automatically generate Coq representations of term rewrite systems and termination arguments that can be used for proving the termination of Coq functions. Indeed, in Coq, no function can be defined without proving its termination, because allowing non-terminating functions would make proof verification undecidable. But this architecture has also some disadvantages. First, compared to more standard programming languages, computation in Coq is very slow (and indeed too slow to check some complex termination certificates). Second, the compiler from CPF to Coq is not proved and can thus introduce errors not present in the certificate.

Here, we consider a different architecture based on Coq's ability to generate OCaml [START_REF] Leroy | The Objective Caml system release 3.12, Documentation and user's manual[END_REF], Haskell [START_REF] Peyton-Jones | Haskell 98 Language and Libraries, The revised report[END_REF] or Scheme [START_REF] Sperber | Revised 6 report on the algorithmic language Scheme[END_REF] programs equivalent to the functions defined in it [START_REF] Letouzey | Certified functional programming: program extraction within Coq proof assistant[END_REF]. It consists in defining the CPF verification program directly in Coq (except the parsing part), and prove its correctness. Then, Coq's extraction mechanism provides us with an OCaml, Haskell or Scheme standalone program that can be compiled and efficiently executed independently of Coq or the CoLoR library.

A similar approach has been undertaken successfully for the CPF verifier CeTA [START_REF] Sternagel | CeTA 2.4[END_REF] with the proof assistant Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF], [START_REF] Haftmann | Code generation from specifications in higher order logic[END_REF], which implements classical higher-order logic with the axiom of choice [START_REF] Church | A formulation of the simple theory of types[END_REF]. Here, we want to test this approach in the proof assistant Coq, which implements an extension of intuitionist higher-order logic [START_REF] Coquand | The calculus of constructions[END_REF], [START_REF] Paulin-Mohring | Inductive definitions in the system Coq -rules and properties[END_REF], and by using the CoLoR library.

The first problem to address is the representation in Coq of CPF certificates. The second one is the formalization and proof of the CPF verifier program using the Coq library on rewriting theory and termination called CoLoR [START_REF] Blanqui | CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates[END_REF]. In particular, it requires to translate the CPF data structures into the data structures used in CoLoR.

This paper is organized as follows. In section II, we introduce term rewriting systems and give some examples of termination techniques used in current automated termination provers. In section III, we describe the formal language CPF for termination certificates used in the international competition of automated termination provers [START_REF]Termination competition[END_REF]. In section IV, we introduce the proof assistant Coq and how to formalize and prove the correctness of a certificate verifier in it. In section V, we give some details on the representation of certificates in Coq. Finally, in section VI, we give some details on the formalization and proof of the verifier using the CoLoR library.

II. TERM REWRITE SYSTEMS AND THEIR TERMINATION

We first recall what is rewriting: "rewrite systems are directed equations used to compute by repeatedly replacing subterms of a given formula with equal terms until the simplest form possible is obtained" [START_REF] Dershowitz | Rewrite systems[END_REF]. More formally: Definition 1 (Term rewrite system) Let X be an infinite set of variables. Given a set F of function symbols (disjoint from X ) and an arity function α : F → N, the set T (F , X ) of (first-order) terms over F and X is the smallest set containing X and such that, if f ∈ F and t 1 , . . . , t α(f) are terms, then f(t 1 , . . . , t α(f ) ) is a term.

A substitution σ is a map from variables to terms that is extended to terms in the obvious way (xσ = σ(x) and

f(t 1 , . . . , t n )σ = f(t 1 σ, . . . , t n σ)). A context C is a term with a unique occurrence of a distinguished variable [], which substitution by u is written C[u]. A (rewrite) rule is a pair of terms written l → r. The rewrite relation → R generated by a set R of rules is the smallest relation containing R and stable by substitution (t → R u ⇒ tσ → R uσ) and context (t → R u ⇒ C[t] → R C[u]).
A relation → terminates (or is well-founded, or noetherian) if there is no infinite sequence t 0 → t 1 → . . .

A simple example of rewrite system is given by the addition on unary natural numbers:

add(zero, x) → x add(succ(x), y) → succ(add(x, y))
The termination of a TRS is undecidable in general, even with a single rule [START_REF] Dauchet | Termination of rewriting is undecidable in the one-rule case[END_REF]. So, there has been active research for finding powerful sufficient conditions. An important one consists in interpreting function symbols by monotone polynomials on natural numbers N [START_REF] Lankford | On proving term rewriting systems are noetherian[END_REF], [START_REF] Contejean | Mechanically proving termination using polynomial interpretations[END_REF]:

Theorem 2 (Polynomial interpretation) Let R be a TRS and ϕ be a function mapping a polynomial ϕ f ∈ Z[X 1 , . . . , X n ] to each function symbol f of arity n. Given a valuation α : X → N, let [[x]] ϕ α = α(x) and [[f(t 1 , . . . , t n )]] ϕ α = ϕ(f)([[t 1 ]] ϕ α , . . . , [[t n ]] ϕ α ) be the interpretation of terms in Z induced by ϕ, and t > ϕ u if, for all α, [[t]] ϕ α > N [[u]
] ϕ α , the well-founded ordering on terms induced by ϕ.

If every ϕ f is monotone in every x i , R 1 ⊆ > ϕ and → R2 terminates, then → R1∪R2 terminates.

For instance, the previous system can be proved terminating by using the following polynomial interpretation on N:

ϕ add (x, y) = 2x + y ϕ succ (x) = x + 1 ϕ zero = 1
Indeed, for the first rule, we have 2(1)+x > N x and, for the second rule, we have 2(x + 1) + y > N (2x + y) + 1, whatever are the values of x, y ∈ N.

Another very important method, at the basis of all current TRS termination provers, consists in transforming a TRS into a dependency pair (DP) problem [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF]: Definition 3 (Dependency pair) Given a set of symbols F , the set F ♯ = F ⊎ {f ♯ | f ∈ F } which consists of the disjoint union of F with some copy of F , is the set of marked and unmarked symbols (f ♯ is taken to be of same arity as f). Given a set R of rules, a symbol f is said defined if there is a rule whose left hand-side is of the form f(l 1 , . . . , l n ). Let D(R) be the set of defined symbols. The set of dependency pairs DP(R) is then the set of marked rules f ♯ (l 1 , . . . , l n ) → g ♯ (r 1 , . . . , r p ) such that f(l 1 , . . . , l n ) → r ∈ R for some r, g(r 1 , . . . , r p ) is a subterm of r not occurring in some l i , and g is defined.

The dependency graph whose nodes are DP(R) has an edge between (l 1 , r 1 ) and (l 2 , r 2 ) if there are two substitutions σ 1 and σ 2 such that r

1 σ 1 → * R l 2 σ 2 .
Indeed, → R terminates on T (F , X ) iff the composition of the reflexive-transitive closure of → R with the closure by substitution of DP(R), written → * R → DP(R)h , terminates on T (F ♯ , X ). Intuitively, dependency pairs generalizes the notion of recursive calls and call graph in functional programming [START_REF] Thiemann | The size-change principle and dependency pairs for termination of term rewriting[END_REF]. Interpretations in a well-founded domain are easily extended to deal with this more general kind of relations. Moreover, since we only consider the closure by substitution of DP(R), only one dependency pair need to strictly decrease in every cycle or, more simply, in every connected component of the dependency graph. This allows to split a DP problem into various independent DP sub-problems [START_REF] Hirokawa | Tyrolean Termination Tool: Techniques and features[END_REF].

For instance, in our simple example, there is only one dependency pair, add ♯ (succ(x), y) → add ♯ (x, y), the termination of which can be proved by taking ϕ add ♯ (x, y) = x.

III. TERMINATION CERTIFICATES

The theorem on polynomial interpretation can be described as a conditional deduction rule on termination problems:

(rule-removal-PI) Mon(ϕ) R 1 ⊆ > ϕ WF(→ R2 ) WF(→ R1∪R2 )
where Mon(ϕ) means that every ϕ f is monotone in every x i , R 1 ⊆ > ϕ that every rule of R 1 is strictly decreasing in the interpretation, and WF(→ R2 ) that → R2 terminates (is wellfounded). Similar conditional deduction rules can be written for most if not all termination methods used in current termination provers [START_REF] Giesl | The dependency pair framework: Combining techniques for automated termination proofs[END_REF]. Hence, a termination proof can be described by a deduction tree obtained by composing deduction rules like (rule-removal-PI) and axioms like:

(empty) R = ∅ WF(→ R )
For the international competition of automated termination provers [START_REF]Termination competition[END_REF], a formal language called CPF [START_REF]Certification Problem Format[END_REF] has been collectively defined for representing such deduction trees. It is given as an XML Schema or XSD file [START_REF]XML Schema Part 1: Structures[END_REF], [START_REF] Siméon | The essence of XML[END_REF]. An XSD file is like a grammar: it describes the set of XML files that are admissible. XML is a well established W3C text file standard [START_REF]Extensible Markup Language (XML) 1[END_REF] for describing tree-structured data. For instance, in CPF, a rewrite rule has to be described by the following XML text: <rule><lhs>...</lhs><rhs>...</rhs></rule> It represents a labeled tree, which root is labeled by the tag rule, having two sub-trees: the first one describes the rule left hand-side and has its root labeled by the tag lhs, and the second one describes the rule right hand-side and its root is labeled by the tag rhs. The XML Schema language (which is a subset of XML) allows to describe some set of valid XML texts by declaring what are the possible labeled trees. For instance, the XSD type used in CPF for rewrite rules is: The main type constructors allowed in XSD are, informally:

• element: if T is an XSD type and x is a string, then <element name="x">T </element> denotes the set of trees which root is labeled by x and which children belong to the set of trees corresponding to T . • sequence: if T 1 , . . . , T n are XSD types, then <sequence>T 1 . . . T n </sequence> denotes2 the set of tuples of trees (t 1 , . . . , t n ) such that t 1 is of type T 1 , . . . , t n is of type T n .

• choice:

if T 1 , . . . , T n are XSD types, then <choice>T 1 . . . T n </choice> denotes the union of the sets of trees corresponding to T 1 , . . . , T n .

IV. FORMALIZATION AND PROOF OF A CERTIFICATE

VERIFIER IN COQ The Coq proof assistant [START_REF] Ly | The Coq Reference Manual[END_REF] is a tool that allows one to formally define mathematical objects and prove statements about them. It has been successfully used in the certification of various important applications, either industrial: a JavaCard platform [START_REF] Barthe | Tool-assisted specification and verification of the JavaCard platform[END_REF] or a C compiler [START_REF] Leroy | Formal verification of a realistic compiler[END_REF], or academical: the four color theorem [START_REF] Gonthier | The four colour theorem: Engineering of a formal proof[END_REF] or Kepler's conjecture [START_REF] Hales | A revision of the proof of the Kepler conjecture[END_REF].

It is based on an extension of Girard' system F [START_REF] Girard | Proofs and Types[END_REF] and Martin-Löf type theory [START_REF] Martin-Löf | Intuitionistic type theory[END_REF], called the calculus of inductive constructions [START_REF] Coquand | The calculus of constructions[END_REF], [START_REF] Paulin-Mohring | Inductive definitions in the system Coq -rules and properties[END_REF]. It allows function definitions by pattern-matching [START_REF] Cornes | Conception d'un langage de haut niveau de représentation de preuves[END_REF] and provides a programmable proof tactic language [START_REF] Delahaye | A tactic language for the system Coq[END_REF], various decision procedures, and other important features like modules, type classes, etc.

It is therefore possible to define in Coq an inductive data type cpf for representing CPF predicates, a boolean function check:trs->cpf->bool verifying the correctness of a certificate wrt a termination problem, and formally prove that this function is correct, that is, in Coq syntax:

Theorem check_is_correct: forall R x, check R x = true -> WF (red R).
Proof. ... Qed.

In fact, in order to provide useful error messages if a certificate appears to be incorrect, to deal with certificates that the verifier does not know how to handle yet (there many different certificates in CPF and it is a really huge work to handle all of them), instead of a boolean output, we use an error monad [START_REF] Wadler | Comprehending monads[END_REF]. And since many auxiliary functions are necessary for translating CPF data structures into CoLoR data structures, we use a polymorphic error monad: Finally, since Coq includes a typed λ-calculus with inductive data types and pattern-matching, the extraction of ML-like function definitions [START_REF] Harper | Standard ML[END_REF] from Coq to OCaml [START_REF] Letouzey | Certified functional programming: program extraction within Coq proof assistant[END_REF] is almost straightforward 34 and looks about the same since Coq syntax is very close to OCaml syntax.

V. PARSING AND COQ REPRESENTATION OF CERTIFICATES

The CPF format is extended every year with new certificates and can be modified sometimes. In Rainbow, the data type used for representing certificates internally and the parsing function used to create a value of this data type from a text file are written by hand (the parsing function uses the XML-Light library [START_REF] Cannasse | XML-Light 2.2[END_REF]). This is a possible source of errors and is time-consuming.

To avoid these problems, we developed a compiler from XSD to Coq and OCaml that, from an XSD file, generates a Coq file (and hence an OCaml file after extraction from Coq) providing a data type definition for representing XML data valid wrt the given XSD file, and an OCaml file providing a parsing function for this data type (also based on XML-Light). This compiler is not intended to cover all aspects of XSD but only the one used in CPF.

The XSD type constructors described above are translated to standard OCaml data structures as follows (with some optimizations):

• sequence: tuple or list (an optional child being mapped to the OCaml option type); • choice: data type with a constructor for each case. For instance, in CPF, the type for function symbols is defined as follows:

<xs:group name="symbol"> <xs:choice> <xs:element ref="name"/> <xs:element name="sharp"> <xs:complexType> <xs:sequence> <xs:group ref="symbol"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="labeledSymbol"> <xs:complexType> <xs:sequence> <xs:group ref="symbol"/> <xs:group ref="label"/> </xs:sequence> </xs:complexType> </xs:element> </xs:choice> where <group name="x"> is a way in XSD to introduce a type definition that can be referred to by x. This XSD type is translated by our compiler to the following inductive OCaml data type:

type symbol = | Symbol_name of name | Symbol_sharp of symbol | Symbol_labeledSymbol of symbol * label
Other solutions could be chosen. Note however that not every OCaml value corresponds to an XML file validating CPF. To do so, we would need to use private data types [START_REF] Blanqui | On the implementation of construction functions for non-free concrete data types[END_REF] or a stronger type system like the one of CDuce [START_REF]CDuce 0.5.5[END_REF], [START_REF] Frisch | Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types[END_REF].

More importantly, in XSD, type definitions are unordered and a type definition can refer to types defined later in the file. This is not a problem in itself for OCaml or Coq since these languages support mutually defined types too. However, if CPF is represented in Coq as a single big set of mutually defined types, then Coq will generate a single big induction principle for all types that will be very difficult to use in proofs. It is therefore better to have as many minimal sets of mutually defined types as possible. And because in Coq and OCaml, the type names used in a type definition can only refer to type names of the same set of mutually defined types or to previously defined types, it is necessary to order the XSD type definitions wrt their dependencies: Definition 4 (Type dependency relation) For our purpose 5 , we can consider that a type T is defined by a finite set of constructors the arguments of which are of type T 1 , . . . , T n respectively. Then, we say that a type T depends on a type U, written U⊳T, if there is a constructor of T having an argument of type U. And we say that a type U must be defined before a type T, written U T, if (U, T) is in the reflexive and transitive closure of ⊳. We then denote by ≃ the symmetric closure of (it is an equivalence relation), and by ≺ = -≃ its strict part.

The minimal sets of mutually dependent types correspond then to the equivalence classes of the ≃ equivalence relation, and these classes can be ordered topologically by using ≺.

VI. DEFINITION AND PROOF OF A TERMINATION

CERTIFICATE VERIFIER IN COQ The first problem to address is the translation of CPF data structures for symbols, terms, rules, polynomials, etc. to the corresponding CoLoR data structures. In fact, this is more or less straightforward except for terms.

In CoLoR, every definition or theorem is parametrized by a given signature: providing the set of symbols, their arity and a boolean function on symbols ensuring that equality on symbols is decidable.

Then, new sets are introduced when needed, like it is the case for marked symbols in the dependency pairs transformation. Moreover, some termination techniques may change the arity of symbols. For instance, arguments filtering [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] may transform a TRS where f is of arity n ≥ 1 into a TRS where f is of arity n -1 by removing the first argument of f in every rule where f occurs.

Hence, in CoLoR, the set of symbols and their arity may evolve dynamically during the verification of a certificate, and differently wrt the deduction branch followed (a certificate has a tree structure), while, in CPF, there is only one big type for all the possible symbols. Defining a function for converting a CPF term into a CoLoR term following the same dynamic would be complicated.

Instead, we use the fact that the CPF type for symbols include all possible symbols that can be generated in the course of a verification, and chose the CPF type itself for the set of CoLoR symbols. Hence, only the arity function needs to evolve dynamically. Note that this is correct to do so since signature extension reflects termination: given a set R of rules on T (F , X ), if F ⊆ G, then → F R terminates iff → G R terminates, where → A R is the relation generated by R on T (A, X ) [START_REF] Ohlebusch | A simple proof of sufficient conditions for the termination of the disjoint union of term rewriting systems[END_REF].

As a consequence, we need to translate CoLoR data structures for new symbols back into the cpf data type. To prove that this transformation reflects termination, we use the following theorem on signature morphisms formalized in CoLoR:

Theorem 5 (Signature morphism) Let F and G be two sets of symbols whose arity functions are α and β respectively, and let ϕ be a map from F to G that respects arities, i.e. forall f ∈ F, β ϕ(f) = α f . The map ϕ then naturally extends to terms as follows: ϕ(x) = x and ϕ(f(t 1 , . . . , t n )) = ϕ(f)(ϕ(t 1 ), . . . , ϕ(t n )).

If R is a set of rules on T (F , X ) and → ϕ(R) terminates on T (G, X ), then → R terminates on T (F , X ).

Note that no property is required for ϕ other than to respect arities. In particular, it does not need to be injective.

We now show how this applies on the DP transformation. Let F be the set of symbols corresponding to the data type symbol defined in the previous section. To simplify, we do not consider the constructor Symbol_labeledSymbol. So, F can be seen as the solution of the equation X = N ⊎ {f @ | f ∈ X}, where N is the set of values of type name and @ stands for the constructor Symbol_sharp to distinguish it from the symbol ♯ used in the DP transformation. Let R be a set of rules on F with no symbol of the form f @ such that → * R → Dh terminates, where D = ϕ(DP(R)) with ϕ(f ♯ ) = f @ and ϕ(f) = f otherwise. Then, by the theorem on signature morphisms, → * R → DP(R)h terminates and, by the DP theorem, → R terminates.

VII. CONCLUSION

We started to develop a standalone tool for verifying the correctness of termination certificates for term rewrite systems [START_REF] Dershowitz | Rewrite systems[END_REF] following the CPF format [START_REF]Certification Problem Format[END_REF] used in the international competition of automated termination provers [START_REF]Termination competition[END_REF], and formally prove its correctness in the proof assistant Coq [START_REF] Ly | The Coq Reference Manual[END_REF] using the Coq library on rewriting theory and termination CoLoR [START_REF] Blanqui | CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates[END_REF] and Coq extraction mechanism [START_REF] Letouzey | Certified functional programming: program extraction within Coq proof assistant[END_REF].

We first developed a simple compiler for generating a Coq data type definition for representing XML Schema data types, and an XML parser for CPF. We also defined and proved in Coq a small verifier for two important termination techniques: dependency pairs [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] and polynomial interpretations [START_REF] Contejean | Mechanically proving termination using polynomial interpretations[END_REF]. But much more has to be done to be able to compete with the verifier CeTA developed in the proof assistant Isabelle/HOL [START_REF] Sternagel | CeTA 2.4[END_REF].

  Inductive result (A : Type) : Type := | Ok : A -> result A | Ko : error -> result A. Definition term : cpf_term -> result color_term := ... Theorem check_is_correct: forall R x, check R x = Ok unit -> WF (red R).

  Record Signature : Type := mkSignature { symbol :> Type; arity : symbol -> nat; beq_symb : symbol -> symbol -> bool; beq_symb_ok : forall x y, beq_symb x y = true <-> x = y }.

http://color.inria.fr/rainbow.html

In the complete definition, every type T i can be equipped with two attributes a ∈ N and b ∈ N ∪ {∞} specifying the minimum and maximum numbers (∞ meaning arbitrary) of children of type T i .

Note however that parallel pattern-matching and pattern-matching with patterns of depth greater than 1 are not primitive in Coq. They are compiled into sequences of non-parallel pattern-matching with patterns of depth 1, leading to important code duplication in some cases.

This is however not the case of more complex Coq constructions[START_REF] Letouzey | Certified functional programming: program extraction within Coq proof assistant[END_REF],[START_REF] Glondu | Vers une certification de l'extraction de Coq[END_REF].

This is the class of OCaml types to which XSD types are compiled.