Alexandre Maréchal
email: alex.marechal@univ-grenoble-alpes.fr

David Monniaux
email: david.monniaux@univ-grenoble-alpes.fr

Michaël Périn
email: michael.perin@univ-grenoble-alpes.fr

Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming 67

Keywords: Polyhedra, Parametric Linear Programming, Projection

Convex polyhedra capture linear relations between variables. They are used in static analysis and optimizing compilation. Their high expressiveness is however barely used in verification because of their cost, often prohibitive as the number of variables involved increases. Our goal in this article is to lower this cost. Whatever the chosen representation of polyhedra -as constraints, as generators or as bothexpensive operations are unavoidable. That cost is mostly due to four operations: conversion between representations, based on Chernikova's algorithm, for libraries in double description; convex hull, projection and minimization, in the constraintsonly representation of polyhedra. Libraries operating over generators incur exponential costs on cases common in program analysis. In the Verimag Polyhedra Library this cost was avoided by a constraints-only representation and reducing all operations to variable projection, classically done by Fourier-Motzkin elimination. Since Fourier-Motzkin generates many redundant constraints, minimization was however very expensive. In this article, we avoid this pitfall by expressing projection as a parametric linear programming problem. This dramatically improves efficiency, mainly because it avoids the post-processing minimization. We show how our new approach can be up to orders of magnitude faster than the previous approach implemented in the Verimag Polyhedra Library that uses only constraints and Fourier-Motzkin elimination, and on par with the conventional double description approach, as implemented in well-known libraries.

1 The Challenge of Verification using Polyhedra Static analyzers establish the validity of assertions in programs by discovering inductive invariants that entail them. Analyzers based on abstract interpretation consider invariants within an abstract domain [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Invariants on numeric variables are of particular interest. They may entail that software produce no arithmetic overflow, no array index out of bounds -the user may be directly interested in such properties, or an optimizing compiler may discard runtime checks for violations that cannot occur. Furthermore, proofs of more complicated properties may use numerical invariants internally -for instance proofs of sorting algorithms need invariants on indices.

An example of abstract domain suitable for program states given by vectors of n numerical variables is the domain of products of n intervals; but such a domain cannot express relationships between variables. This hinders verification even if the final goal is to prove that a given variable lies within certain bounds, for instance to prove that a string length is less than a fixed buffer size: one may need to prove that the sum of the length of two strings is less than this size, thus a relation between these lengths.

The domain of convex polyhedra comprises sets of states defined by conjunctions of linear (in)equalities over the variables [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. The analyzer needs to perform a variety of operations on these sets -least upper bound (convex hull, in the case of polyhedra), inclusion tests, projections, image and reverse image by program operations; also, in some cases, intersections and Minkowski sums. In addition to static analyzers, convex polyhedra are used inside highly optimizing compilers to reorganize loop nests [START_REF] Bastoul | Contributions to High-Level Program Optimization[END_REF].

Despite their expressiveness and 40 years of research, polyhedra are little used in verification because operations on polyhedra are still costly and do not scale to large programs [START_REF] Halbwachs | Some ways to reduce the space dimension in polyhedra computations[END_REF]. Usually, they are restricted to a small subset of program variables such as loop indices [START_REF] Henry | PAGAI: A path sensitive static analyser[END_REF] -including more variables would mean skyrocketing costs.

Most libraries for computing over convex polyhedra maintain a double description, both as generators (vertices, in the case of bounded polyhedra) or constraints (faces). A common case in program analysis is upper and lower bounds are known on all N variables -that is, the vector of variables lies within a distorted N -dimensional hypercube, which has 2 N vertices. This explains the reputation of polyhedra as unwieldy except in very low dimension, and motivated the design of the Verimag Verified Polyhedra Library (VPL) that operates on constraints-only representations [START_REF] Fouilhé | Revisiting the abstract domain of polyhedra: constraints-only representation and formal proof[END_REF][START_REF] Fouilhé | Efficient generation of correctness certificates for the abstract domain of polyhedra[END_REF]. An advantage of that approach is that it is easy to log enough information to independently check that the computed polyhedron includes the exact polyhedron that should be computed, which suffices for proving that static analysis is sound [START_REF] Fouilhé | A certifying frontend for (sub)polyhedral abstract domains[END_REF][START_REF] Fouilhé | Efficient generation of correctness certificates for the abstract domain of polyhedra[END_REF]; the certificate checker was implemented and proved correct in COQ. 4 The consequence is that many operations of the VPL, such as assignment, convex hull or Minkowski sum, were encoded as projection, finally performed by Fourier-Motzkin elimination [START_REF] Benoy | Computing convex hulls with a linear solver[END_REF]. Unfortunately, Fourier-Motzkin elimination generates numerous redundant constraints; and even by incrementally removing them after each elimination of a variable, intermediate steps may create large lists of constraints.

In 2013, the overall performance of VPL [START_REF] Fouilhé | Efficient generation of correctness certificates for the abstract domain of polyhedra[END_REF] on typical verification benchmarks was on a par with that of double description libraries, though the timings on individual operations differed: some operations are faster than in double description, some are slower -all those involving projection, including convex hull. Projection by Fourier-Motzkin was the bottleneck.

Contribution

In this article we report on an algorithmic breakthrough that speeds up typical computations on polyhedra in constraints-only representation by several orders of magnitude when polyhedra becomes large (in number of relations) or dense (in number of variables involved in each relations). Scalability results from the inseparable combination of i) the formulation of the projection via Parametric Linear Programming (PLP) ( §3); ii) the implementation of a PLP-solver over rationals, to get exact results ( §5); iii) a new normalization criterion, which ensures the absence of redundant constraints and saves the postprocessing elimination of redundancy ( §6). This normalization, its proof and an certifying implementation are the main contributions of this paper. 5We demonstrate the scalability by comparing timings of projections between the PLP-based algorithm, Fourier-Motzkin elimination and an existing library based on double description ( §7).

Related work

The high cost of general convex polyhedra was long deplored. It motivated studying restricted classes of polyhedra, with simpler and faster algorithms, such as octagons [START_REF] Miné | The octagon abstract domain[END_REF]; and even these were found to be too slow, motivating recent algorithmic improvements [START_REF] Singh | Making numerical program analysis fast[END_REF]. We instead sought to conserve the domain of polyhedra as originally described [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF], but with very different algorithms.

Our work was inspired by Howe et al.'s attempt to replace the Fourier-Motzkin elimination by a formulation as a Parametric Linear Optimization Problem (PLOP) [START_REF] Howe | Polyhedral analysis using parametric objectives[END_REF], which they solved by an ad hoc algorithm. Unfortunately, their implementation is not available. We took a step further and developed a generic PLP-solver exploiting insights by [START_REF] Jones | Lexicographic perturbation for multiparametric linear programming with applications to control[END_REF][START_REF] Jones | On polyhedral projections and parametric programming[END_REF]. Our solver, implemented in OCAML, works over rationals and generates COQ-certificates of correctness of its computations, similar to those in VPL [START_REF] Fouilhé | Revisiting the abstract domain of polyhedra: constraints-only representation and formal proof[END_REF][START_REF] Fouilhé | A certifying frontend for (sub)polyhedral abstract domains[END_REF][START_REF] Fouilhé | Efficient generation of correctness certificates for the abstract domain of polyhedra[END_REF].

Most libraries for computing over convex polyhedra for static analysis or compilation, including PolyLib, 6 Komei Fukuda's CDD, 7 the Parma Polyhedra Library, 8 the NEWPOLKA library included in Apron, 9 operate over the double description; see e.g. [START_REF] Roberto | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF] for an introduction. The costliest and most complicated operation is the conversion from one representation to the other, using Chernikova's algorithm [START_REF] Chernikova | Algorithm for discovering the set of all the solutions of a linear programming problem[END_REF][START_REF] Verge | A note on Chernikova's algorithm[END_REF]. It is rather easy to prune redundant items from one representation if one has the other, which explains the attractiveness of that approach. Its only drawback is that, as explained above, the generator representation is exponential in the dimension on very common and simple cases.

The explosive nature of the generator representation motivated approaches that detect when a polyhedron is a Cartesian product of polyhedra and compute generator representations separately for each element of the product, thereby avoiding exponential blowup in the case of the hypercube [START_REF] Halbwachs | Some ways to reduce the space dimension in polyhedra computations[END_REF][START_REF] Singh | Fast polyhedra abstract domain[END_REF].

General texts on polyhedra and linear programming include [START_REF] Dantzig | Linear Programming 2: Theory and Extensions[END_REF][START_REF] Chvatal | Linear Programming[END_REF][START_REF] Schrijver | Theory of linear and integer programming[END_REF].

Basics

Throughout the article, vectors are written in boldface lowercase, and matrices in boldface uppercase. An affine form over x is a linear combination plus constant of x 1 , ..., x n . For two vectors a and x of the same length, the dot product a , x = i a i x i is a linear function of x. Thus, we often use the notation a (x) instead of a , x .

A convex polyhedron 10 is the set of points x = (x 1 , . . . , x n ) ∈ Q n that satisfy a conjunction (or a set) of linear constraints of the form C : n i=1 a i x i b where x i are program variables, a i and b are constants in Q, and ∈ { ≤, =, ≥ }. All constraints can be assumed to use only ≥. 11 Such a constraint is the th row of a vector inequality Ax ≥ b. We use P to specifically refer to the set of points defined by the set of constraints P. Given a polyhedron P = { x | Ax ≥ b }, the same system with strict inequalities defines P, the interior of P, and x denotes a point of

P def = { x | Ax > b }.
In all the paper and without loss of generality, we focus on polyhedra with non-empty interior, meaning that equalities (explicit or implicit) are extracted and treated separately, as in most polyhedra libraries.

Before presenting our encoding of the projection operator as a PLOP, we start by recalling the fundamental Farkas' Lemma and Fourier-Motzkin's Algorithm for variable elimination.

Example 1.1. Figure 1 shows the geometrical space defined by the polyhedron

P = {C 1 : -x 1 -2x 2 + 2x 3 ≥ -7, C 2 : -x 1 + 2x 2 ≥ 1, C 3 : 3x 1 -x 2 ≥ 0, C 4 : -x 3 ≥ -10, C 5 : x 1 + x 2 + x 3 ≥ 5}
and its projection on dimensions (x 1 , x 2 ) resulting from the elimination of variable x 3 . Projecting variable x 3 from P -noted P \{ x3 } -by Fourier-Motzkin elimination consists in eliminating x 3 by combining constraints with opposite signs for x 3 . Constraints that do not involve x 3 remain unchanged. This retains constraints C 2 , C 3 and produces two new constraints: C 1 +2C 4 : -x 1 -2x 2 ≥ -27 and C 4 +C 5 : x 1 +x 2 ≥ -5. By Farkas' Lemma, the latter is redundant with respect to C 2 and C 3 as it can be expressed as a nonnegative combination of C 2 , C 3 .

Lemma 1 (Farkas' lemma [29, 7.1h, p.93]). A constraint C is a logical consequence of a non-contradictory set of constraints P = {C 1 , . . . , C p } iff there exists λ 0 , ..., λ p ≥ 0 such that C = λ 0 + p i=1 λ i C i , called a Farkas decomposition of C on P.

Example 1.2. The combination 4 5 C 2 + 3 5 C 3 :

x 1 + x 2 ≥ 4
5 is a logical consequence of C 2 and C 3 and it is a stronger condition than C 4 + C 5 : x 1 + x 2 ≥ -5 since 4 5 > -5. Thus, the constraint C 4 + C 5 is redundant with respect to C 2 and C 3 . Therefore the polyhedron P \{ x3 } is only formed of three constraints {C 2 , C 3 , C 1 + 2C 4 }.

Projection via Parametric Linear Programming

Naive Fourier-Motzkin elimination produces O ( |P| 2 ) 2 k constraints when eliminating k variables of a polyhedron with |P| constraints [START_REF] Simon | Exploiting sparsity in polyhedral analysis[END_REF]. Most of them are redundant: indeed, the number of faces of the projected polyhedron is O(|P| k ) [27, §4.1]. 12 Removing the redundant constraints is costly, even though there exists improved algorithms [START_REF] Maréchal | Polyhderal Approximation of Multivariate Polynomials using Handelman's Theorem[END_REF].

Jones et al. [START_REF] Jones | On polyhedral projections and parametric programming[END_REF] then Howe et al. [START_REF] Howe | Polyhedral analysis using parametric objectives[END_REF] noticed that the projection of a polyhedron can be expressed as a Parametric Linear Programming problem. In fact, PLP naturally arises when trying to generalize Fourier-Motzkin method to eliminate several variables simultaneously. In this article we achieve the work initiated by [START_REF] Howe | Polyhedral analysis using parametric objectives[END_REF], whose goal was to compute the projected polyhedron without generating redundant constraints. Let us first explain their approach.

Example 1.3. As a consequence of Farkas lemma, any constraint implied by {C 1 , ..., C 5 } is a nonnegative combination of them, written λ 0 + 5 i=1 λ i C i with λ i ≥ 0, i.e.

λ 0 + λ 1 (-x 1 -2x 2 + 2x 3 ) + λ 2 (-x 1 + 2x 2 ) + λ 3 (3x 1 -x 2 ) + λ 4 (-x 3 ) + λ 5 (x 1 + x 2 + x 3 ) ≥ -7λ 1 + λ 2 -10λ 4 + 5λ 5
The left-hand side of the inequality can be rearranged to reveal the coefficient of each variable x i and we can bring the right-hand side term of ≥ to the left.

λ 0 + (-λ 1 -λ 2 + 3λ 3 + λ 5 ) x 1 + (-2λ 1 + 2λ 2 -λ 3 + λ 5 ) x 2 + (2λ 1 -λ 4 + λ 5 ) x 3 -(-7λ 1 + λ 2 -10λ 4 + 5λ 5 ) ≥ 0 (1)
Then, any instantiation of that inequality with λ i canceling the coefficient of x 3 , i.e. that satisfies (α) 2λ 1λ 4 + λ 5 = 0, is an over-approximation of P \{ x3 } . Indeed, it does not involve x 3 and, as a Farkas combination, it is by construction a logical consequence of P. Constraints found by the FM elimination of x 3 correspond to the solutions (λ 0 , . . . , λ 5 ) ∈ {(0,0,1,0,0,0), (0,0,0,1,0,0), (0,1,0,0,2,0), (0,0,0,0,1,1)} of Equation (α). Note that it is possible to eliminate several variables simultaneously by setting an elimination equation for each variable that must be discarded.

Here is a first formulation of a projection as a PLOP. We will refine it later, as it is not sufficient to avoid redundancies in the result. Given a polyhedron P = { C 1 : a 1 (x) ≥ b 1 , . . . , C p : a p (x) ≥ b p } on variables x 1 , . . . , x n , the projection of P by elimination of k variables x e1 , . . . , x e k can be obtained as the solution of the optimization problem:

minimize the objective function z(x) = λ 0 + p i=1 λ i × (a i (x) -b i ) under the constraints (F ) λ 0 ≥ 0, ..., λ p ≥ 0 ( †) p i=0 λ i = 1 (α) α e1 (λ) = 0, ..., α ek (λ) = 0        (2)
where α i (λ) denotes the coefficient of x i in the reformulation of the objective as α 1 (λ) × x 1 + . . . + α n (λ)×x n +α 0 (λ). The unknowns λ i are called the decision variables: the solver must find a solution for them. Note the inequalities (F ) from Farkas' Lemma in addition to the (α) equations defining a projection. This problem has a parametric objective: the objective function depends on parameters x 1 , . . . , x n due to the terms a i (x) in the coefficients of the decision variables. But once x 1 , . . . , x n are fixed, both the objective function and the constraints become linear in the decision variables, thus this problem belongs to parametric linear programming.

An additional constraint, here i λ i = 1, is needed to prevent the solver from obtaining the optimal solution λ = 0 which is always valid in a projection problem, whatever the parameter values. The ( †) condition only excludes this useless null solution because any other solution can be scaled so that i λ i = 1. The presence of λ 0 in the objective can seem useless and strange to readers who are familiar with linear programming: the solution λ 0 = 1 and λ 1 = ... = λ p = 0 becomes feasible and generates a trivially redundant constraint C triv : 1 ≥ 0. The role of λ 0 will become clear in §4 and §6.

Example 1.4. The elimination of x 3 via PLP is defined by two matrices: O is built from [-b|A] and encodes the objective. The other one captures the requirement (α) and ( †). As usual in solvers, Farkas constraints (F ) are left implicit. minimize the objective function

(1, x 1 , x 2 , x 3 ) O     0 1 7 -1 0 10 -5 0 0 -1 -1 3 0 1 0 0 -2 2 -1 0 1 0 0 2 0 0 -1 1          1 λ 0 . . . λ 5      = z(x) [-b|A]
under the constraints

( †) -1 1 1 1 1 1 1 0 0 2 0 0 -1 1 α      1 λ 0 . . . λ 5      = 0                                          (3)
This formulation of the projection is correct. Unfortunately, it may still generate redundant constraints: the solutions (λ 0 , . . . , λ 5 ) ∈ {(1,0,0,0,0,0), (0,0,1,0,0,0), (0,0,0,1,0,0), (0, 1

Polyhedra as Solutions of Parametric Linear Optimization Problems

In the previous section we encoded the projection of a polyhedron as a PLOP. For interpreting the result of a PLP-solver as a polyhedron we need to go one step further into the field of PLP and look at the solutions of a PLOP.

To summarize, Parametric Linear Programming is an extension of Linear Programming where the constants in the constraints or the coefficients in the objective function may be replaced by affine combinations of parameters [START_REF] Gal | Multiparametric linear programming[END_REF]. In this article, we only deal with the case where parameters appear in the objective function. The general form of a PLOP that stems from projection is

minimize the objective function z(x) def = λ 0 + p i=1 λ i × (a i (x) -b i ) under the constraints λ 0 , ..., λ p ≥ 0, ( †) p i=0 λ i = 1, αλ = 0 (4)
where x is the vector of parameters (x 1 , ..., x n ); (a i (x) -b i ) are affine forms on the parameters; and α is a matrix. In a projection problem the system of equations αλ = 0 constrains the decision variables

λ 1 , ..., λ p but not λ 0 .
The solution is a concave, piecewise affine function z , mapping the parameters to the optimal solution:

z def = x →      z 1 (x) if x ∈ R 1 . . . z r (x) if x ∈ R r (5)
Each piece is an affine form over x, obtained by instantiating the objective function z with a solution λ; a piece can also be denoted by z λ . Each z i is associated to a region of optimality R i that designates the set of x for which the minimum of z (x) is z i (x). Regions of optimality are polyhedra; that will be clear in §5 when we will explain how they are computed by our solver (see Example 1.6.). They form a quasi-partition of the space of parameters: their union covers Q n and the intersection of the interior of two distinct regions is empty. They however do not form a partition because two regions R i , R j may overlap on their frontiers; then, their solutions z i , z j coincide on the intersection.

From optimal function to polyhedron. A PLOP can be thought of as a declarative description of the projection operator. The solution z can be interpreted as a polyhedron P that is the projection of an input polyhedron P. This requires some explanations:

• Due to the Farkas conditions λ 0 , ..., λ p ≥ 0 which preserve the direction of inequalities, the objective function of PLOP (4), i.e. λ 0 + p i=1 λ i × (a i (x) -b i ) can be interpreted as a constraint implied by the input polyhedron

P = {C 1 : a 1 (x) ≥ b 1 , ..., C p : a p (x) ≥ b p }. Actually, for a given λ, the statement z λ (x) ≥ 0 is equivalent to the constraint λ 0 + p i=1 λ i × a i (x) ≥ p i=1 λ i × b i (6)
• Minimizing the objective ensures that the λ 0 -shift of the constraint will be minimal, meaning that the constraint z λ (x) ≥ 0 will be tightly adjusted. • The requirement αλ = 0 captures the expected effect of the projection. Thus, any solution λ defines a constraint z λ (x) ≥ 0 of the polyhedron P . Now recall that a polyhedron is a set of points that satisfy linear inequalities. Therefore, it is natural to define P as { x | z (x) ≥ 0 }. The following lemma proves that this set of points is a polyhedron. (⊆) Pick up a point x ∈ { x | z (x) ≥ 0 }. By definition of z as a piecewise function defined on the whole space of parameters, then there exists i such that x ∈ R i and z (x ) = z i (x ). It follows that z i (x ) ≥ 0 since x belongs to the set of points where z is nonnegative. Moreover, the fact that x belongs to R i -the region of optimality of z i in a minimization problem -ensures that z k (x ) ≥ z i (x ) for all k and therefore, z k (x ) ≥ 0 for all k. Thus,

Lemma 2. { x | z (x) ≥ 0 } = r k=1 { x | z k (x) ≥ 0 } 6/
x ∈ { x | z k (x) ≥ 0 } for all k = 1..r. Finally, x ∈ k=1..r { x | z k (x) ≥ 0 }. (⊇) Pick up a point x ∈ r k=1 { x | z k (x) ≥ 0 }.
Then, x belongs to a least one R i because the regions form a (pseudo) partition of the whole space of parameters Q n , thus

r k=1 R k = Q n .
Yet, the affine piece that defines z on x is z i and z (x ) = z i (x ). Moreover, all the affine pieces of z are nonnegative on x since x ∈ r k=1 { x | z k (x) ≥ 0 }. Then, in particular z i (x ) ≥ 0 and the same goes for z (x ). Finally,

x ∈ { x | z (x) ≥ 0 }.
Constructing the vector inequality Z x ≥ b that defines the polyhedron P is straightforward from the solution z . If suffices to get rid of the regions of optimality and to interpret each affine piece of z as an inequality:

{ x | z (x) ≥ 0 } = (by Lemma 2) r k=1 { x | z k (x) ≥ 0 } = {x | r k=1 z k (x) ≥ 0} = {x | r k=1 z k , x -b k ≥ 0} = { x | Z x ≥ b } . Let us detail this construction.
Each piece z k of the solution is a affine form over x and z k (x) ≥ 0 defines a constraint in the form [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] which can be written Example 1.5. On our running projection problem, the PLP-solver returns the following optimal function, and the instantiation of the decision variables λ i that defines each affine piece:

n i=1 z ki x i ≥ b k i.e.
z def = (x 1 , x 2 ) →                z 2 : -x 1 + 2x 2 -1 on R 2 (for λ 2 = 1) z 3 : 3x 1 -x 2 on R 3 (for λ 3 = 1) z 4 : -1 3 x 1 -2 3 x 2 + 9 on R 4 (for λ 1 = 1 3 , λ 4 = 2 3 ) z 5 : 1 2 x 1 + 1 2 x 2 + 5 2 on R 5 (for λ 4 = 1 2 , λ 5 = 1 2 )
z 1 :

1 on R 1 (for λ 0 = 1)
from which we construct the polyhedron

P = Z         -1 2 0 3 -1 0 -1 3 -2 3 0 1 2 1 2 0 0 0 0         x   x 1 x 2 x 3   ≥ b        1 0 -9 -5 2 -1        =                C 2 : -x 1 + 2x 2 ≥ 1 C 3 : 3x 1 -x 2 ≥ 0 1 3 C 1 + 2 3 C 4 : -1 3 x 1 -2 3 x 2 ≥ -9 1 2 C 4 + 1 2 C 5 : 1 2 x 1 + 1 2 x 2 ≥ -5 2 C triv : 0 ≥ -1               
Variable x 3 does not appear anymore in the constraints of P because its column in Z is made of 0. The regions of optimality, shown on Fig. 2 that z 5 does not vanish on its region of optimality, i.e. z 5 = 0 ∩ R5 = ∅. Actually, this is true for any redundant constraint. Indeed, we will prove in §6 (Lemma 5) that z i = 0 ∩ Ri = ∅ ensures the irredundancy of the constraint z i ≥ 0 in P .

Principle of a PLP-solver

Due to space limitations we shall only sketch how our parametric linear programming solver works. It is based on a recent algorithm by Jones et al. [START_REF] Jones | Lexicographic perturbation for multiparametric linear programming with applications to control[END_REF] with some improvements: it uses a fast simplification of regions [START_REF] Maréchal | Efficient Elimination of Redundancies in Polyhedra by Raytracing[END_REF] and performs exact computations in rationals so as to avoid rounding errors. This algorithm for solving a PLOP is a generalization of the simplex algorithm which can itself be seen as an extension of Gaussian elimination for solving a system of linear equations.

Gaussian elimination proceeds by rewriting: each equation defines a variable in terms of the other ones. This equation can be used to eliminate the variable from the other equations by substitution. This operation is called a pivot. Gauss pivoting strategy leads to an equivalent system in echelon form where un/satisfiability becomes trivial.

The simplex algorithm follows the same principle but differs in the selection of the variable to eliminate. First, each inequality C : n i=1 a i x i ≤ b is changed into an equality n i=1 a i x i + x n+ = b by introducing a variable x n+ ≥ 0 called a slack variable. Second, the objective function is added to the system as an extra equation defining the variable z as a linear form z = n+r i=1 o i x i . Then, the simplex performs pivots as in Gaussian elimination until reaching an equivalent system of equations where the optimality of z becomes syntactically obvious. Let us take an example.

Example 1.6. To illustrate the behavior of a LP-solver, such as the simplex, let us instantiate the objective of PLOP (3), e.g. with x 1 = 5, x 2 = 11, x 3 = 1, to obtain a non-parametric version: z = λ 0 -18 λ 1 + 16 λ 2 +4 λ 3 +9 λ 4 +12 λ 5 . The simplex strategy chooses to define λ 1 and λ 4 in terms of the other decision variables. It exploits the equations ( †) and (α) of PLOP [START_REF] Chernikova | Algorithm for discovering the set of all the solutions of a linear programming problem[END_REF] and gets (i)

λ 1 = -1 3 λ 0 -1 3 λ 2 -1 3 λ 3 -2 3 λ 5 + 1
using (α) to eliminate λ 4 in ( †), and (ii) λ 4 = -2 3 λ 0 -2 3 λ 2 -2 3 λ 3 -1 3 λ 5 + 2 3 using ( †) to eliminate λ 1 in (α). Then, it performs two rewritings using equations (i, ii) and returns an equivalent version of the objective z = λ 0 + 16 λ 2 + 4 λ 3 + 21 λ 5 on which it is clear that choosing λ 0 , λ 2 , λ 3 , λ 5 greater than 0 would increase the value of z because their coefficients are positive. Thus, the minimum value of z is reached for λ 0 = λ 2 = λ 3 = λ 5 = 0 which entails λ 1 = 1 3 and λ 4 = 2 3 using equations (i) and (ii). This example summarizes the principle of linear programming. Now consider our minimization problem (3) with its parametric objective

z(x 1 , x 2 , x 3 ) = λ 1 (-x 1 -2 x 2 + 2 x 3 + 7) + λ 2 (-x 1 + 2 x 2 -1) + λ 3 (3 x 1 -x 2 ) + λ 4 (-x 3 + 10) +λ 5 (x 1 + x 2 + x 3 -5) + λ 0
Our PLP-solver uses the previous instantiated problem to discover the useful pivots (i, ii). Then, it replays the same rewritings on the parametric version. Those operations are efficiently implemented using the matrix representation of (3): they boils down to the addition of combinations of rows of ( †) and α to those of O. We end up with the following objective:

- 1 3 x 1 - 2 3 x 2 + 9 z 4 + λ 0 1 3 (x 1 + 2 x 2 -24) ≥ 0 : C 4.1 + λ 2 2 3 (-x 1 + 4 x 2 -15) ≥ 0 : C 4.2 + λ 3 1 3 (10 x 1 -x 2 -27) ≥ 0 : C 4.3 + λ 5 1 3 (5 x 1 + 7 x 2 -39) ≥ 0 : C 4.4
We recognize the 4 th piece of z . The argument for optimality used in the non-parametric version can be generalized: The minimality of z 4 holds if the parametric coefficients of the remaining variables are nonnegative, since increasing the values of λ 0 , λ 2 , λ 3 , λ 5 (which must be nonnegative) would make the objective value grow. This condition defines the region of optimality R 4 of z 4 as the polyhedron The PLP-solver then chooses an opposite sign condition of a parametric coefficient C 4.i -that means exploring an adjacent region by crossing a frontier -and selects a new instantiation point on this side of the constraint. The objective is then instantiated accordingly and submitted to the simplex which provides the meaningful pivots leading to another optimal affine form and its region of optimality. The benefit of PLP is that the exploration of one instance with the simplex is generalized into a whole region of optimality. The exploration goes on until the whole space of parameters has been covered by the union of regions: any new instantiation point falls in an already explored region.

{ C 4.1 , C 4.

Polyhedra in Minimal Form for Free

The previous sections showed how to compute the optimal solution of a PLOP and how to interpret the solution z as a polyhedron P = r k=1 z k (x) ≥ 0. Still, the representation of P may not be minimal: some constraints z k (x) ≥ 0 may be redundant in P . We could remove those redundancies afterwards but, as noticed by Howe et al. [START_REF] Howe | Polyhedral analysis using parametric objectives[END_REF], it is highly preferable to prevent their generation by adding a normalization constraint to the PLOP. We adapt their intuition to our formulation of the problem and we bring the proof that it indeed avoids redundancies. This requires to make a detour via normalized solutions to explain the expected effect of a normalization constraint.

Normalizing the Projection PLOP

Let us normalize the function z so that it evaluates to 1 on a given point x in the interior of P . Formally, we consider a solution z (x) def = z (x) z (x) or equivalently ∀k, z k (x

) def = z k (x) z k (x) .
The key point of this transfor- mation is that the space z ≥ 0 , which is the polyhedron P of interest, is unchanged. The normalized solution z will differ from the original one but must fulfills z ≥ 0 = z ≥ 0 which is true on the Verimag Research Report n o 4 9/17 main functions if it holds on each of their pieces, i.e. ∀k, z k ≥ 0 = z k ≥ 0 . The normalization preserves the nonnegativity space of each z k because 1 z k (x) is a positive scalar: Indeed, x belongs to the interior of P , i.e.

k z k > 0 by Lemma 2. The proof of this remark is in the appendix (see Lemma 7). Example 2. The transformation of the solution only changes the inclination of z k , not the space where they cross 0. This can easily be illustrated on one-variable constraints. Consider three constraints C 1 : 2x ≥ 5, C 2 : x ≤ 12 and a redundant one C 3 : x ≥ 2, corresponding to three affine forms z 1 (x) = 2x -5, z 2 (x) = 12 -x and z 3 (x) = x -2. On the left-hand side we plotted the functions z = z i (x) for i ∈ { 1, 2, 3 } and, on the right-hand side, their normalizations with respect to the point x = 3.

The most interesting consequence of the normalization is that a constraint is redundant iff its normalized affine form is nowhere minimal. This property does not hold on the non-normalized forms: although C 3 is redundant w.r.t. C 1 and C 2 , z 3 is minimal w.r.t. z 1 and z 2 on x ∈ [3, 7]. On the contrary, consider- ing the normalized forms, z 3 is no longer minimal, thus it will be absent from the piecewise solution of a minimization problem. One of our contribution is the proof of this result ( §6.2).

Last, but no least, the normalized pieces are not computed a posteriori from the original solutions. They are obtained directly by enforcing the normalization of the objective through an additional constraint z(x) = 1. Recall from (4) that the objective of the PLOP is z(x

) def = λ 0 + p i=1 λ i × (a i (x) -b i ). Then, the normalization constraint becomes ( ‡) λ 0 + p i=1 λ i × (a i (x) -b i ) = 1
where the a i (x) are coefficients in Q, obtained by evaluating the constraints of the input polyhedron at x. The normalization constraint replaces the previous requirement ( †)

i λ i = 1 in the PLOP: like ( †) it excludes the solution λ 0 = ... = λ p = 0. Back to Example 1.5., our PLP-solver running on the normalized PLOP only builds the irredundant constraints z 2 ≥ 0, z 3 ≥ 0 and z 4 ≥ 0 associated to the regions of Fig. 2(b).

Note that we must be able to provide a point x in the interior of P while P is not already known. Finding such a point is obvious for projection, convex-hull and Minkowski sum. It is feasible because the operators based on PLP are applied on polyhedra with non-empty interior; the treatment of polyhedra with equalities is explained in Example 3 below. For projection, x is obtained from a point x in the interior of the input polyhedron P. Removing the coordinates of variables marked for elimination provides a point x that will be in the interior of the projected polyhedron P .

Example 3. Consider the case of a polyhedron over variables x, x , x made of inequalities P and an equality E : x = f (x, x ). The computation of the projection (P ∧ E) /{ x ,x } is done in two steps: we use equation x = f (x, x ) to eliminate x from P by substitution. If implicit equalities show up we exploit them in the same way, otherwise we apply the projection via PLP on P[x /f (x, x )] to eliminate the remaining variable x .

A Normalized PLOP is Free of Redundancy

The advantage of PLP over Fourier-Motzkin comes from the following theorem: Theorem 1. Let z def = min{ z 1 , . . . , z r } be the optimal solution of a normalized parametric minimization problem. Then each solution z k that is not the constant function x → 1 is irredundant with respect to polyhedron z ≥ 0 .

Proof. Theorem 1 is a direct consequence of three intermediates results: (i) each region of optimality in a normalized PLOP is a cone pointed in x (Lemma 3); (ii) each piece z k which is not constant, is decreasing on its region of optimality along lines starting at x (Lemma 4); (iii) each piece that crosses 0 on its region produces an irredundant constraint (Lemma 5).

10/17

Verimag Research Report n o 4

Let us summarize the key facts that are needed for exposing the proof of the lemmata: Projection via PLP leads to a parametric linear minimization problem whose solution is a function z defined by pieces { z 1 on R 1 , . . . , z r on R r }; each R k is the region of optimality of z k , meaning that among all the pieces z k is the minimal one on R k , i.e. R k = {x | z (x) = z k (x)}. By construction, z (x) is the minimum of { z 1 (x), . . . , z r (x)} and z (x) = z 1 (x) = . . . = z r (x) = 1 is enforced by the ( ‡)-normalization constraint. This is where λ 0 comes into play: the fact that λ = (1, 0, ..., 0) fulfills ( ‡) and (α), hence leading to the constant function z λ = 1, sets an upper-bound on z . Therefore, any minimal piece z k , which evaluates to 1 on x, can not grow on its region of optimality otherwise it would not be minimal compared to z λ = 1. Thus, z k is either constant and equal to 1 or it satisfies ∀x ∈ Rk , 1 > z k (x) which entails its decline on the infinite region R k as meant by Lemma 4, causing its nullification in R k , hence its irredundancy (Lemma 5). The constant piece z λ = 1 arises among the solutions of a normalized PLOP when the resulting polyhedron P is unbounded as illustrated alongside.

We focus on the proof of Lemma 5 which gives a criterion of irredundancy illustrated on Fig. 2. The proofs of the other lemmata are just computational arguments; they are provided in the appendix.

Lemma 3. ∀x ∈ Q n , x ∈ Rk ⇒ x + µ(x -x) ∈ Rk , ∀µ > 0.
z k = 0 ∩ Rk = ∅ ⇒ z k ≥ 0 is irredundant w.r.t. z ≥ 0.

Proof by contradiction.

Consider z k , a piece of z such that z k = 0 ∩ Rk = ∅. Let us assume that z k is redundant. Then, by Farkas Lemma 1, ∃ (λ j ) j =k ≥ 0, ∀x ∈ Q n , j =k λ j z j (x) ≤ z k (x). Let x be a point of the nonempty set z k = 0 ∩ Rk . Then z k (x) = 0, as x ∈ z k = 0 , and the previous Farkas inequality becomes j =k λ j z j (x) ≤ 0 (7) Since x ∈ Rk , then, z k (x) < z j (x) for j = k by definition of R k as the region of optimality of z k . More precisely, 0 < z j (x) since x ∈ z k = 0 . Therefore, 0 < λ j z j (x) for j = k as λ j ≥ 0. Then, summing up this inequation for all j = k, we obtain

0 < j =k λ j z j (x) (8)
(7) and ( 8) are contradictory, proving thereby that z k is irredundant.

Minimizing Operators based on Projection via PLP

As mentioned in introduction, several polyhedral operators, e.g. Minkowski sum, convex hull, assignment and linearization, are encoded using extra variables which are then eliminated by projection. If the projection is done by PLP, all these operators produce polyhedra free of redundancy if we can provide a normalization point in the interior of the expected polyhedron. Let us give insights of the encodings.

The Minkowski sum of two polyhedra P and P is the set of points x = x + x with x ∈ P and x ∈ P . It is computed by eliminating the variables of x and x from the polyhedron P (x ) ∧ P (x ) ∧ { x = x + x }, where P (x ) (resp. P (x )) denotes the set of constraints of P (resp. P ) Verimag Research Report n o 4 11/17 over variables x (resp. x ). We use x def = x + x as normalization point where x (resp. x ) is a point lying within the interior of P (resp. P ).

The convex-hull of P and P is the smallest convex polyhedron that includes P and P . It is the set of barycentres of x ∈ P and x ∈ P which can be formally defined as P (x ) ∧ P (x ) ∧ {x =

β 1 × x + β 2 × x , β 1 + β 2 = 1, β 1 ≥ 0, β 2 ≥ 0}.
The equation defining x is non-linear but it can be linearized using a simple change of variable [START_REF] Benoy | Computing convex hulls with a linear solver[END_REF]. Then, the convex-hull is obtained by elimination of β 1 , β 2 and the variables of x and x to get a polyhedron over x. We can use x or x as normalization point.

Assignment and more generally, image by an affine map represented by a matrix M can be encoded as intersection with equalities x = M x, projection of the unprimed variables, and then renaming of the prime variables into unprimed ones; the reverse image is just substitution. We use the image by M of a point x in the interior of the input polyhedron for normalization.

Our linearization operator for computing a polyhedral over-approximation of a conjunctions of linear and polynomial constraints i g i (x) ≥ 0 is also implemented in the VPL via PLP [START_REF] Maréchal | Polyhderal Approximation of Multivariate Polynomials using Handelman's Theorem[END_REF]. However, it does not prevent redundancies as we do not know how to provide a normalization point satisfying i g i (x) ≥ 0.

Experiments

Benchmarks. We reused the benchmark suite of [START_REF] Maréchal | Efficient Elimination of Redundancies in Polyhedra by Raytracing[END_REF]. It contains polyhedra generated randomly from several characteristics: number of constraints, number of variables and density (ratio of the number of zero coefficients by the number of variables). Constraints are created by picking up a random integer between -100 and 100 as coefficient of each variable. All constraints are attached the same constant bound ≤ 20. These polyhedra have a potatoid shape, as shown on the right-hand side figure.

We compare three libraries on projection/minimization problems: NEWPOLKA [START_REF] Jeannet | APRON: A library of numerical abstract domains for static analysis[END_REF] as representative of the double description framework, VPL [START_REF] Fouilhé | Efficient generation of correctness certificates for the abstract domain of polyhedra[END_REF] based on Fourier-Motzkin elimination, and our implementation based on PLP. As we produce polyhedra in minimized form, we asked NEWPOLKA and VPL to perform a minimization afterwards.

On each problem we measure the execution time, with a timeout fixed at 300 seconds. In addition to the number of constraints C, the density D and the number of variables V , we consider the effect of the projection ratio P (number of projected variable over dimension). Fig. 3 shows the effect of these characteristics on execution time (in seconds). The vertical axis is always displayed in log scale, for readability. Each point is the average execution time for the projection and minimization of 10 polyhedra sharing the same characteristics.

Fourier-Motzkin Elimination in the VPL. As mentioned earlier, Fourier-Motzkin elimination generates many redundant constraints and the challenge of a good implementation is their fast removal. The Fourier-Motzkin elimination implemented in the VPL uses well-known tricks for dynamically removing constraints that can be shown redundant by syntactic arguments [START_REF] Maréchal | Efficient Elimination of Redundancies in Polyhedra by Raytracing[END_REF]. However, as shown by [8, 3.2.3, p. 76], this forbids the use of Kohler's redundancy criterion: when eliminating k variables, a constraint resulting from the combination of k + 1 constraints is redundant. When syntactic criteria fail to decide the redundancy of a constraint, the VPL calls a LP solver. Hence, polyhedra are minimized after each single-variable elimination.

Projection Ratio. Fig. 3(a) gives the time measurements when projecting polyhedra of 15 constraints, 10 variables and a density of 50%, with a projection ratio varying from 10 to 90%. Fourier-Motzkin is very efficient when projecting a small number of variables. Its exponential behavior mainly occurs for high projection ratio, as it eliminates variables one after the other and the number of faces tends to grow at each projection. PLP is not suitable when there is only few variables to project, e.g. in the case of a single assignment. On the contrary, it becomes interesting compared to Fourier-Motzkin elimination when the projection ratio exceeds 50%, i.e. when projecting more than half of the variables. This ratio is always reached when computing Minkowski sums or convex hulls by projection ( §6.3). It can also be the case on exits of program blocks where a whole set of local variables must be forgotten. As PLP usefulness grows with a high projection ratio we will focus on the case P = 75%, studying the effect of other characteristics. Dimension. The evolution of execution time in terms of dimension is given in Fig. 3(c). With 20 constraints, the exponential behavior of Fourier-Motzkin elimination emerges. PLP and NEWPOLKA show a similar curves with an overhead for PLP on a log scale, i.e. a proportionality factor on execution time. It would be interesting to see the effect of dimension beyond 20 variables, which takes considerable time since it requires increasing the number of constraints. Indeed, when the dimension is greater than the number of constraints, polyhedra have a really special shape with very few generators and the comparison would be distorted.

Density. The effect of density on execution time is shown on Fig. 3(d). NEWPOLKA and PLP are little sensitive to density. The case of Fourier-Motzkin can be explained: Elimination of a variable x with FM consists in combining every pair of constraints having an opposite sign for x. The more non-zero coefficients within the constraints, the greater the number of possible combinations.

What can we conclude from these experiments? On small problems our projection is less efficient than that of a double description (DD) library but the shape of the curves of NEWPOLKA and PLP is similar on a logarithmic scale, meaning that there is a proportionality factor between the two algorithms. This is an encouraging result as projection -and the operators encoded as projection -are the Achilles heel of constraints-only representation whereas it is straightforward in DD: the complexity is exponential with FM elimination but linear in the number of generators. On the other hand, the conjunction operator, which, in constraints-only representation, consists in the union of two sets followed by a fast minimization [START_REF] Maréchal | Efficient Elimination of Redundancies in Polyhedra by Raytracing[END_REF], is less efficient in DD because it triggers one step of Chernikova's algorithm per constraint.

Conclusion & Future Work

We have shown how usual operations over convex polyhedra (projection, convex hull, Minkowski sums, image by an affine map, linearization) can be formulated as PLOP instances. In short, all costly operations on polyhedra in constraints-only representation can be implemented using PLOP. This approach was made practical by the combination of an efficient PLP-solver and a normalization constraint ensuring that the solutions of the PLOP are free of redundancies, which avoids costly postprocessing minimization. This makes the VPL, a polyhedra library in constraints-only representation, competitive with other libraries in double description, and much faster on problems that have exponential generator representations.

Experiments on Minkowski sum met our expectations but raised an issue for convex-hull: On large problems with the same characteristics, we beat other libraries, but we suffer from an exponential blow-up of region subdivisions when the two polyhedra have many faces in common, which induces a high degree of degeneracy. Our PLP-solver does not have special counter-measures to deal with degeneracy. Proposals exist for tackling primal and dual degeneracies but they come with an extra-cost [START_REF] Jones | Lexicographic perturbation for multiparametric linear programming with applications to control[END_REF]. Thus, dealing with degeneracy is a trade-off and we need a deeper understanding of the phenomenon before addressing it in our PLP-solver or by a pre-processing for convex-hull.

As future work, our approach can be combined with Cartesian product factorization [START_REF] Halbwachs | Some ways to reduce the space dimension in polyhedra computations[END_REF][START_REF] Singh | Fast polyhedra abstract domain[END_REF]. While the main advantage of factorization is to avoid exponential generator representations, which we also do because we never compute generators, using low dimension factors is likely to speed up parametric linear programming.

Other avenues of research include experiments in the large on static analysis of actual programs, the parallelization of the algorithms (we already use a parallel minimization algorithm) and the increased use of floating-point computations instead of exact rational arithmetic without destroying soundness.

Figure 1 :

 1 Figure 1: Elimination of one variable in a three-dimensional polyhedron.

  z k , x ≥ b k for some vector z k = (z k1 , ..., z kn ) and some constant b k . It follows from Lemma 2 that the set of points x where z (x) is nonnegative is a polyhedron defined by the vector inequality Z x ≥ b where the rows of Z are the vectors z 1 , . . . , z r and b is the column vector (b 1 , . . . , b r ) .

Figure 2 :

 2 Figure 2: The regions of optimality of the solution z of Example 1.5. obtained by solving PLOP (3). The bold lines are the boundaries of the projected polyhedron P . Figure (a) shows regions obtained when the PLOP contains the constraint i λ i = 1. Figure (b) shows regions obtained when constraints are normalized on point x (see §6).

2 ,

 2 C 4.3 }, see Fig.2(a). C 4.4 is actually redundant with respect to C 4.1 , C 4.2 and C 4.3 . It is thus eliminated from the representation of R 4 , and therefore does not appear on Fig.2(a).

Lemma 4 .

 4 Either z k is the constant function x → 1, or it decreases on lines of R k starting at x, i.e. ∀x ∈ Rk , ∀µ > 1, z k (x) > z k (x + µ(x -x)).

12 / 17 Verimag Research Report n o 4 (

 12174 a) : C = 15, V = 10, D = 50%, P = [10%, 90%] (b) : C = [8, 60], V = 8, D = 50%, P = 75% (c) : C = 20, V = [4, 19], D = 50%, P = 75% (d) : C = 10, V = 8, D = [30%, 90%], P = 75%

Figure 3 :

 3 Figure 3: Execution time in seconds of NewPolka (blue), Fourier-Motzkin (red) and PLP (green) depending on respectively (a) projection ratio, (b) number of constraints, (c) number of variables and (d) density.

Certifying a library in double description would have likely entailed implementing and proving in COQ the correctness of Chernikova's conversion algorithm from one representation to the other.

The VPL 0.2 is available at https://github.com/VERIMAG-Polyhedra/VPL 2/17 Verimag Research Report n o 4

This follows from McMullen's bound on the number of n -k -1-faces of the polyhedron[START_REF] Mcmullen | The maximum numbers of faces of a convex polytope[END_REF][START_REF] Mcmullen | Convex polytopes and the upper bound conjecture[END_REF].4/17Verimag Research Report n o 4

,0,0, 2 3 ,0), (0,0,0,0,[START_REF] Bastoul | Contributions to High-Level Program Optimization[END_REF] 2 , 12 )} include the trivial constraint 1 ≥ 0 and 1 2 C

+ 1 2 C

which is equivalent to the redundant constraint C 4 + C 5 found by Fourier-Motzkin elimination. We shall address this point in §6.

8/17Verimag Research Report n o

Verimag Research Report n o 4

Acknowledgments. The authors thank Alexis Fouilhé, Andy King, Jacob Howe, and Paul Feautrier for their help on the early stages of this work.

This * * This work was partially supported by the European Research Council under the European Union's Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement nr. 306595 "STATOR".

A Proofs

The proofs make an intensive usage of the following remark. Lemma 6. For any affine form af , any points x and x and any scalar µ,

Proof. An affine form af is a linear form f plus a constant a, that is af (x) = a + f (x). Then,

Proof. Consider x ∈ Ri , µ > 0 and let j be the index of the piece that is minimal at x + µ(xx), i.e.

Let us prove that j = i leads to a contradiction. Since z j is affine,

It remains to be proven that x + µ(x -x) cannot lie in a boundary of R i and thus belongs to Ri . Recall that, by construction, a boundary is the intersection of two adjacent regions, say R i and R j , and their affine forms are equal on the boundary. That would mean i = j and

We already proved that it is unsatisfiable.

Lemma 4. Either z k is the constant function x → 1, or it decreases on lines of R k originated in x, i.e. ∀x ∈ Rk , ∀µ > 1, z k (x) > z k (x + µ(x -x)).

Proof. Assume x ∈ Rk . We already noticed in §6.2 that if z k is not the constant function

Proof. Let us prove by double inclusion that normalizing the solution of a PLOP does not change the resulting polyhedron P def = z ≥ 0 . Let z k be a piece of z . Then, z k (x) = z k (x) z (x) is well-defined if z k (x) = 0. Take x ∈ z k ≥ 0 . Then, z k (x) ≥ 0 and z k (x) ≥ 0 ⇔ z k (x) > 0. Repeating this reasoning for each pieces, the inclusion z ≥ 0 ⊆ z ≥ 0 is only valid if ∀k, z k (x) > 0. Reciprocally, let x ∈ z k ≥ 0 . By definition, z k (x) = z k (x) × z k (x). This time, z k (x) ≥ 0 and z k (x) ≥ 0 ⇔ z k (x) ≥ 0. Thus, z ≥ 0 ⊆ z ≥ 0 is enforced by ∀k, z k (x) ≥ 0. Finally, the point x must be chosen in the interior of z ≥ 0 to ensure ∀k, z k (x) > 0. Then, both inclusions hold, proving that normalization does not change the output polyhedron.

Verimag Research Report n o 4 17/17


Yohan Brunebarbe
email: yohan.brunebarbe@math.uzh.ch

Î T Beno

Cadorel

Benoît Cadorel
email: benoit.cadorel@univ-amu.fr

HYPERBOLICITY OF VARIETIES SUPPORTING A VARIATION OF HODGE STRUCTURE

We generalize former results of Zuo and the first author showing some hyperbolicity properties of varieties supporting a variation of Hodge structure. Our proof only uses the special curvature properties of period domains. In particular, in contrast to the former approaches, it does not use any result on the asymptotic behaviour of the Hodge metric.

Introduction

The goal of this note is to give a proof of the following result, which generalizes both [Zuo00, Theorem 0.1] and [START_REF] Brunebarbe | Symmetric differentials and variations of Hodge structures[END_REF]Theorem 0.3]. Interestingly, whereas the proofs in op. cit. use difficult results about degenerations of Hodge structure, the proof given here uses only the special curvature properties of period domains.

Theorem 1.1. Let X be a compact complex manifold and D ⊂ X be a normal crossing divisor. Assume that X -D admits a complex polarized variation of Hodge structure whose period map is immersive at one point. Then (1) the logarithmic canonical bundle ω X (D) = det Ω 1 X (log D) is big, i.e. the variety X -D is of log-general type.

(2) the logarithmic cotangent bundle Ω 1 X (log D) is weakly-positive and big. Recall that a line bundle L on a compact complex manifold X is called big if there exists a positive constant c such that h 0 (X, L ⊗k ) ≥ c • k dim X for k ≫ 1. More generally, we will say in this article that a vector bundle A on X is big if there exists a positive constant c such that h 0 (X, Sym k A) ≥ c • k dim X+rk A-1 for k ≫ 1. Also, following Viehweg [Vie83, Definition 1.2], we say that a vector bundle A on a smooth projective variety X is weakly-positive if there exists a Zariski-dense open subset U ⊂ X such that for every big line bundle L on X and every positive integer α, there exists a positive integer β such that Sym α•β A ⊗ L β is generated by global sections on U . More generally, we say that a vector bundle A on a Moishezon compact complex manifold X is weakly-positive if there exists a smooth projective variety X ′ and a bimeromorphic holomorphic map ν : X ′ → X such that ν * A is weakly-positive.

Remarks 1.2.

(1) Note that, contrarily to [START_REF] Zuo | On the negativity of kernels of Kodaira-Spencer maps on Hodge bundles and applications[END_REF] and [Bru], we make no assumption on the monodromy at infinity of the local system underlying the variation of Hodge structure. Also, we don't need X to be projective or Kähler.

(2) If in addition X is assumed to be projective, then the first assertion is a consequence of the second, since the determinant of a weakly-positive and big vector bundle is big (cf. Lemma 3.1). Alternatively, one can also appeal to a result of Campana and Pȃun [START_REF] Campana | Orbifold generic semi-positivity: an application to families of canonically polarized manifolds[END_REF] which says that a projective logpair with a big logarithmic cotangent bundle is of log-general type. Since we make no projectivity assumption on X, we give a direct proof of (1) without knowing (2). (3) In the situation of the theorem, the logarithmic cotangent bundle Ω 1 X (log D) is not big in the sense of Viehweg in general. For example, the logarithmic cotangent bundle of a locally hermitian symmetric variety not covered by the ball is never Viehweg-big.

Corollary 1.3. Let X be a compact complex manifold. Assume that on a dense Zariski-open subset of X there exists a complex polarized variation of Hodge structure whose period map is immersive at one point. Then X is Moishezon.

A fortiori, if in addition X admits a Kähler metric, then it is necessarily projective.

Observe that it follows readily from Theorem 1.1 that any complex polarized variation of Hodge structure on the complex line C is constant, as already proved by Griffiths and Schmid [GS69, Corollary 9.4]. More generally, we obtain as a direct application of Theorem 1.1 that complex algebraic varieties supporting a variation of Hodge structure satisfy the following analogue of the Green-Griffiths-Lang conjecture:

Corollary 1.4. Let U be a smooth complex algebraic variety admitting a complex polarized variation of Hodge structure V. If Deg(V) ⊂ U denotes the closed (algebraic) subvariety where the period map is not immersive, then:

• every entire curve of U is contained in Deg(V);

• every algebraic subvariety of U which is not of log-general type is contained in Deg(V).

Remarks 1.5.

(1) The period map being holomorphic, it is clear that Deg(V) is a closed analytic subset of U . In fact it turns out to be an algebraic subvariety.

(2) When U is defined over the ring of integers of a number field, the Lang-Vojta type conjectures predicts that all but finitely many integer points belong to Deg(V). This follows easily from Faltings results when V is a Z-polarized variation of Hodge structure of weight one, but is open otherwise.

Once we know the curvature properties of period domains (that are recalled in section 2.1), Theorem 1.1 is a consequence of the following result of independent interest:

Theorem 1.6. Let X be a compact complex manifold, D ⊂ X be a normal crossing divisor and h be a singular hermitian metric with semi-negative curvature on the tangent sheaf T X | X-D restricted to X -D. Assume moreover that in restriction to a dense Zariski-open subset of X -D the metric h is smooth and has negative holomorphic sectional curvature, bounded from above by a negative constant. Then the logarithmic canonical line bundle ω X (D) is big (so that X is in fact necessarily Moishezon) and the logarithmic cotangent bundle Ω 1 X (log D) is weakly-positive. If moreover the metric h is smooth and Kähler in the neighborhood of a point of X -D, then the logarithmic cotangent bundle Ω 1 X (log D) is big.

Proofs

2.1. Preliminaries on variations of Hodge structure and curvature properties of period domains. Recall that a complex polarized variation of Hodge structure on a complex manifold X is the data of a holomorphic vector bundle E equipped with an integrable connection ∇, a ∇-flat non-degenerate hermitian form h and for all x ∈ X a decomposition of the fibre E x = p∈Z E p satisfying the following axioms:

• for all x ∈ X, the decomposition E x = p∈Z E p x is h x -orthogonal and the restriction of h x to E p x is positive definite for p even and negative definite for p odd,

• the Hodge filtration F r := q≥ rE q varies holomorphically with x,

• (Griffiths' transversality) ∇(F p ) ⊂ F p-1 ⊗ OX Ω 1
X for all p. Fix x 0 ∈ X, and let E := E x0 , h := h x0 and r p = dim(E p x0 ) for every p ∈ Z. The associated period domain D is by definition the set of all h-orthogonal decompositions E = p∈Z E p with dim E p = r p such that the restriction of h to E p is positive definite for p even and negative definite for p odd. The group G := U(E, h) ≃ U( p odd r p , p even r p ) acts transitively on D, with isotropy group V = p U(h p ) ≃ p U(r p ). By associating to any decomposition E = p∈Z E p the corresponding filtration F p := q≥p E q of V , one identifies D with an open subset (for the Euclidean topology) of a flag variety. This provides D with a canonical structure of complex homogeneous manifold. The data of a polarized complex variation of Hodge structure with ranks r p on X is then equivalent to the data of its monodromy representation π 1 (X, x 0 ) → G along with the associated period map, which is a π 1 (X, x 0 )-equivariant holomorphic map p : X → D from the universal cover X of X which is tangent to the so-called horizontal subbundle of the tangent bundle of D (this last condition corresponds to Griffiths' transversality).

The period domain D admits a canonical G-invariant hermitian metric. Griffiths and Schmid proved that its holomorphic sectional curvatures corresponding to horizontal directions are at most a negative constant [GS69, Theorem 9.1], see also [START_REF] Carlson | Period mappings and period domains[END_REF]Theorem 13.3.3]. Since the period map p : X → D is always tangent to the horizontal subbundle of T D and the holomorphic sectional curvature decreases on submanifolds, one gets by pulling-back the metric on D a canonical hermitian metric g with negative holomorphic sectional curvature on the Zariski-open subset U ⊂ X where p is an immersion. Peters showed that g has nonpositive holomorphic bisectional curvature on U [Pet90, Corollary 1.8, Lemma 3.1]. Finally, g is a Kähler metric on U (even though the metric on D is only a hermitian metric) [Lu99, Theorem 1.2].

2.2.

Preliminaries on singular hermitian metrics on vector bundles. We recall here very briefly the basic definitions concerning singular hermitian metrics of semi-negative curvature on vector bundles, after [BP08, Pȃu16, PT14, HPS16].

Definition 2.1. A singular hermitian inner product on a finite-dimensional complex vector space V is a function • : V → [0, +∞] with the following properties:

(1) λ • v = |λ| • v for every λ ∈ C\{0} and every v ∈ V , and 0 = 0.

(2) v + w ≤ v + w for every v, w ∈ V , where by convention ∞ ≤ ∞.

(

) v + w 2 + v -w 2 = 2 • v 2 + 2 • w 2 for every v, w ∈ V . 3
Let V 0 (resp. V fin ) be the subset of V of vectors with zero (resp. finite) norm. It follows easily from the axioms that both V 0 and V fin are linear subspaces of V . By definition, • is said positive definite if V 0 = 0 and finite if V fin = V .

Definition 2.2. (compare [HPS16, Definition 17.1] and [Pȃu16, Definition 2.8]) Let X be a connected complex manifold and A be a non-zero holomorphic vector bundle on X. A singular hermitian metric on A of semi-negative curvature is a function h that associates to every point x ∈ X a singular hermitian inner product • h,x : A x → [0, +∞] on the complex vector space A x , subject to the following two conditions:

• h is finite and positive definite almost everywhere, meaning that for all x outside a set of measure zero, • h,x is a hermitian inner product on A x .

• the function x → log s(x) h,x is plurisubharmonic whenever U ⊂ X is open and s ∈ H 0 (U, A).
Note that in particular the singular hermitian inner product • h,x is finite at each point of X. Conversely, we have the:

Lemma 2.3. Let A be a non-zero holomorphic vector bundle on a connected complex manifold X. Let U be an open dense subset of X, and h be a singular Hermitian metric with semi-negative curvature on A |U . The following two assertions are equivalent:

(1) h is a restriction to U of a singular Hermitian metric with semi-negative curvature on A, (2) the function x → s(x) h,x is locally bounded in the neighborhood of every point of X for every local section s ∈ H 0 (U, A). Moreover, the metric extending h is unique when it exists.

Proof. This is a direct application of Riemann extension theorem for plurisubharmonic functions.

2.3. Proof of Theorem 1.6. Proposition 2.4. Let X be a complex manifold, D ⊂ X be a normal crossing divisor and h be a singular hermitian metric with semi-negative curvature on the tangent bundle T X | X-D restricted to X -D. Assume moreover that in restriction to a dense Zariski-open subset the metric h is smooth and has negative holomorphic sectional curvature, bounded from above by a negative constant -A. Then h extends uniquely to a singular hermitian metric with semi-negative curvature on the logtangent bundle T X (-log D).

Proof. In view of Lemma 2.3, one has to prove that for any analytic open subset U of X and any local section t of T X (-log D) on U , the function

t |U-D h : U -D → [0, +∞), x → t |U-D (x) h is locally bounded. In particular, it is sufficient to show that for X = ∆ n , D = ∪ r i=1 {z = (z 1 , • • • , z n ) ∈ ∆ n | z i = 0} and t a global section of T X (-log D), the function x → t |U-D (x) h is bounded in a neighborhood of the origin. Writing t = r i=1 a i • z i ∂ ∂zi + n i=r+1 a i • ∂ ∂zi ,
where the a i are holomorphic functions on ∆ n , we see that it is sufficient to prove that z i ∂ ∂zi h (resp. ∂ ∂zi h ) are bounded in a neighborhood of the origin for 1 ≤ i ≤ r (resp. for r + 1 ≤ i ≤ n). In the first case, since the holomorphic sectional curvature decreases in submanifold, the Ahlfors-Schwarz Lemma (see below) applied to the punctured unit disk passing through z and directed by ∂ ∂zi (z) gives that

z i ∂ ∂z i h ≤ 2 A • 1 -log |z i | .
Similarly, in the second case one gets

∂ ∂z i h ≤ 2 A • 1 (1 -|z i | 2 )
.

This finishes the proof.

Lemma 2.5 (Ahlfors-Schwarz Lemma, cf. [Dem97, lemma 3.2]). Let h(t) = h 0 (t)idt ∧ d t be a singular hermitian metric on the unit disk ∆, where log h 0 is a subharmonic function such that i∂ ∂ log h 0 (t) ≥ A • h(t) in the sense of currents, for some positive constant A. Then h can be compared with the Poincaré metric of ∆ as follows:

h(t) ≤ 2 A • |dt| 2 (1 -|t| 2 ) 2 .
Similarly, if h is a singular hermitian metric on the punctured unit disk ∆ * satisfying the same assumptions as above, then the following inequality holds:

h(t) ≤ 2 • |dt| 2 |t| 2 (log |t|) 2 .
End of the proof of Theorem 1.6. We keep the notations of the statement. Thanks to Proposition 2.4, the log-tangent bundle T X (-log D) is endowed with a singular hermitian metric h with semi-negative curvature. This metric induces a singular hermitian metric with semi-negative curvature on the line bundle det T X (-log D). Denoting by Θ(h) the curvature of h at a point of X where the metric h is smooth, the curvature of the induced metric det h on det T X (-log D) is given by tr(Θ(h)). For any nonzero v ∈ T 1,0

x X, that we complete in a h

x -orthogonal basis v = u 1 , • • • , u n of T 1,0 x X, we have tr(Θ(h))(v, v) = n i=1 h(Θ(h)(v, v)(u i ), u i ).
Since by our assumptions h has semi-negative curvature, all the terms in the sum are non-positive. But h is also assumed to have negative holomorphic sectional curvature at x, hence the first term h(Θ(h)(v)(v, v), v) is negative and the sum is negative. Using [Pop08, Theorem 1.3] (which generalizes [Bou02, Theorem 1.2] to the non-necessarily Kähler manifolds), one gets that the line bundle ω(D) = (det T X (-log D)) ∨ is big. In particular, X is Moishezon. By taking a modification, one can assume that X is projective (this does not change the conclusions of the Theorem). Since the log-tangent bundle T X (-log D) admits a singular hermitian metric h with semi-negative curvature, it follows from a theorem of Pȃun and Takayama (cf. [Pȃu16, Theorem 2.21] and [PT14, Theorem 2.5.2]) that the logarithmic cotangent bundle is weakly-positive. Finally, we prove that Ω 1 X (log D) is big if we assume that h is Kähler in the neighborhood of a point x ∈ X -D where it is smooth. The argument is completely similar to what has been done in [START_REF] Cadorel | Symmetric differentials on complex hyperbolic manifolds with cusps[END_REF], so we will only sketch it briefly. Denote by ĥ the metric induced by h on the tautological line bundle O(1) -→ P (T X (-log D)).

Since h has semi-negative curvature, ĥ has positive curvature in the sense of currents, and [Pop08, Theorem 1.3] (or [Bou02, Theorem 1.2] in the Kähler case) implies that (1) vol(O(1)) ≥ i 2π

2n-1

Θ( ĥ)

2n-1 ac where Θ( ĥ) ac is the absolutely continuous part of the positive current Θ( ĥ). Since ĥ is smooth on a Zariski open subset of P(T X (-log D), the integral in (1) is equal to the integral of Θ( ĥ) 2n-1 on the open set where ĥ is smooth. Moreover, since h is Kähler in the neighborhood of some point x ∈ X -D, it follows from [BKT13, Lemma 1.4] that there exists v ∈ T X,x such that Θ( ĥ

It follows that the right hand side of (1) is positive, so Ω 1 X (log D) is big.

Appendix

Lemma 3.1. If E is a big and weakly-positive vector bundle on a projective variety X, then its determinant line bundle det E is big.

Proof. Fix A an ample line bundle on X. Since E is big, there exists an integer k ≥ 1 and an injective map of O X -modules 0 → A → Sym k E. This can be completed in an exact sequence of O X -modules 0 → A → Sym k E → Q. Observe that Q, being a quotient of a symmetric power of weakly-positive vector bundle, is weakly-positive too [Vie83, Lemma 1.4]. The previous exact sequence implies that det(Sym k E) ≃ A⊗det Q. The right hand-side is a big line bundle and the left-hand side can be expressed as a positive tensor power of det E, hence det E is big.