Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library^{⋆}

Roberto Bagnara^{1}, Elisa Ricci^{1}, Enea Zaffanella^{1}, and Patricia M. Hill^{2}

1 Department of Mathematics, University of Parma, Italy

           {bagnara,ericci,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK

                    hill@comp.leeds.ac.uk

Abstract. The domain of convex polyhedra is employed in several systems for the analysis and verification of hardware and software components. Current applications span imperative, functional and logic languages, synchronous languages and synchronization protocols, real-time and hybrid systems. Since the seminal work of P. Cousot and N. Halbwachs, convex polyhedra have thus played an important role in the formal methods community and several critical tasks rely on their software implementations. Despite this, existing libraries for the manipulation of convex polyhedra are still research prototypes and suffer from limitations that make their usage problematic, especially in critical applications. These limitations concern inaccuracies in the documentation of the underlying theory, code and interfaces; numeric overflow and underflow; use of not fully dynamic data-structures and poor mechanisms for error handling and recovery. In addition, there is inadequate support for polyhedra that are not necessarily closed (NNC), i.e., polyhedra that are described by systems of constraints where strict inequalities are allowed to occur. This paper presents the Parma Polyhedra Library, a new, robust and complete implementation of NNC convex polyhedra, concentrating on the distinctive features of the library and on the novel theoretical underpinnings.

Dedicated to the memory of Hervé Le Verge

1 Introduction

Convex polyhedra are regions of some n-dimensional space that are bounded by a finite set of hyperplanes. A convex polyhedron in ℝ^{n} describes a relation between n real-valued quantities. The class of all such relations turns out to be useful for the representation of the abstract properties of various kinds of complex systems.

⋆ This work has been partly supported by MURST projects “Abstract Interpretation, type systems and control-flow analysis” and “Aggregate- and number-reasoning for computing: from decision algorithms to constraint programming with multisets, sets, and maps” and by EPSRC grant GR/R53401/01.

The seminal work of P. Cousot and N. Halbwachs [16] introduced the use of convex polyhedra as a domain of descriptions to solve, by abstract interpretation [14], a number of important data-flow analysis problems such as array bound checking, compile-time overflow detection, loop invariant computations and loop induction variables. Convex polyhedra are also used, among many other applications, for the analysis and verification of synchronous languages [7, 19] and of linear hybrid automata (an extension of finite-state machines that models time requirements) [21, 23], for the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [28], for inferring argument size relationships in logic languages [5], and for the automatic parallelization of imperative programs [31]. Since the work of Cousot and Halbwachs, convex polyhedra have thus played an important role in the formal methods community and new uses continue to emerge (see, e.g., [12, 17]). As a consequence, several critical tasks, such as checking the correctness of synchronization protocols or verifying the absence of run-time errors of systems whose failure can cause serious damage, rely on the software implementations of convex polyhedra.

Traditionally, convex polyhedra are assumed to be topologically closed and described by constraint systems containing linear equations and non-strict linear inequalities. However, some tasks need to use convex polyhedra that are not necessarily closed (NNC), i.e., polyhedra that are described by constraint systems possibly containing strict linear inequalities (in addition to equations and non-strict inequalities). Strict inequalities are important, for instance, in order to directly represent non-intersecting temporal regions, as is often the case when modeling applications where synchronization protocols, asynchronous interactions and temporal constraints come into play. Recently, they have also been used for the automatic computation of linear ranking functions [12].

Prior to the release of the Parma Polyhedra Library (PPL) [2] which is the subject of this paper, four libraries for the manipulation of convex polyhedra were (and continued to be) available:^{3}

1. Polylib, designed and written by H. Le Verge and D. K. Wilde [26, 33];

2. PolyLib, the successor of the library by Le Verge and Wilde [27];

3. New Polka, by B. Jeannet [25];

4. the polyhedra library that comes with the HyTech tool [23].

All libraries,^{4} including the PPL, use the same basic technique for representing convex polyhedra (the double description method recalled in Section 3) and the same core algorithm for manipulating that representation (the implementation

3 Note that we restrict ourselves to those libraries that provide the services required by applications in static analysis and computer-aided verification. There are other libraries for convex polyhedra, such as those developed in the field of computational geometry, that, as far as we can tell, are unsuitable for the tasks of interest in this paper. Moreover, we only consider the libraries that are freely available.

4 We refer to the following versions that, at the time of writing, are the latest available: Polylib 2.1, PolyLib 5.0.4, New Polka 1.1.3c, HyTech 1.04f.

and extension of N. V. Chernikova’s algorithms [9–11] by Le Verge [26], possibly with the improvements of K. Fukuda and A. Prodon [18]).

Apart from the PPL, only New Polka supports NNC polyhedra. However, this support is incomplete, incurring avoidable inefficiencies and leaving the client application with the non-trivial task of a correct interpretation of the results.

Libraries 1 and 4 may incur overflow problems whereas 2 and 3 can use unbounded integers as coefficients. Libraries 2 and 3 can be configured to use finite integral types for extra speed but this, of course, comes with the possibility of overflows. In addition, 2 (and, according to [6], 4) can use floating point values, so that overflow, underflow and rounding errors can affect the results.

In libraries 1–4, matrices of coefficients, which are the main data structures used to represent polyhedra, cannot grow dynamically and the client application is ultimately responsible for specifying their dimensions. Since the worst case space complexity of the methods employed is exponential,^{5} in general the client application cannot make a safe and practical choice: specifying small dimensions may provoke a run-time failure; generous dimensions may waste significant amounts of memory and, again, result in unnecessary run-time failures.

The problems caused by run-time errors such as overflow and memory allocation failure could be mitigated or even solved by suitable mechanisms for error detection, handling and recovery. This requires the ability to detect the problem, releasing any affected data-structure whether it be completely or only partially constructed,^{6} and continue the computation with an alternative method (e.g., by reverting to an interval-based approximation). Library 1 detects some errors and sets an error flag whereas libraries 3 and 4 detect some errors, print an error message and abort. Library 2 detects more errors, sometimes setting a flag and sometimes printing a message and aborting. A somewhat drastic approach to error recovery is taken by STeP, the Stanford Temporal Prover [28]. STeP uses the Polka polyhedra library [21] by Halbwachs and Y.-E. Proy for the automatic generation of invariants.^{7} The manual for the latest released version of STeP [8] specifies that this facility is in an “experimental” state^{8} and run as an external process, completely independent from the STeP environment. The user can set three environment variables controlling the maximum memory and time resources allowed for the invariant computation process [8, Section 7.3]. If one or both these limits are trespassed, the invariant generation will fail. The user can also explicitly interrupt the invariant generation by clicking a button. This terminates the invariant generation, but [8, page 95]

5 For instance, an n-dimensional closed hypercube has 2n facets (that are described

by as many constraints) and 2^{n} vertices (which are individually stored in a matrix). 6 Leaving useless data-structures around is a simple memory leak problem; the pres-

ence and reachability of partially constructed objects is a more serious issue since it can result in unpredictable behavior.

7 The Polka polyhedra library is not available in source format and binaries are distributed under rather restrictive conditions (until sometimes around 1996 they could be freely downloaded.

8 Double quotes in the original.

this may leave a separate UNIX process running, which users may have to terminate independently from a UNIX prompt (see the UNIX kill command man pages).

All in all, this possibility does not look very attractive.

Libraries 1–3 are free software released under the GNU General Public License (GPL, see http://www.gnu.org/). Thus, when faced with the need to overcome the above mentioned limitations, anyone can freely take and use them as the basis for further development. However, it appears that none of the libraries provide documentation for the interfaces and code that is adequate for an outsider to make such improvements with any real confidence. This feeling of insecurity is aggravated by the discovery of some errors and imprecisions in the theoretical sections of the documentation of some libraries (for more information see [3], which itself contains an error, now corrected in [4]). Moreover, a complete solution to issues such as error recovery and fully dynamic memory allocation requires a somewhat radical departure from the existing code bases.

For all these reasons we decided to write the PPL, a robust and complete implementation of convex polyhedra. This paper describes the library concentrating on some of its distinctive features and the novel theoretical underpinnings.

The plan of the paper is as follows: Section 2 recalls some basic notation and terminology; Section 3 introduces convex polyhedra and the double description method paying attention to common pitfalls; Section 4 presents the NNC polyhedra and describes (from a theoretical perspective) how they are handled in the PPL; Section 5 briefly describes the design and implementation of the PPL and how it addresses all the limitations we have just discussed; Section 6 concludes.

A longer version of this paper, containing the proofs of the results presented here, is available as a technical report [3].

2 Preliminaries

In this paper, all topological arguments refer to the topological space ℝ^{n} with the standard topology. The topological closure of S ⊆ ℝ^{n} is denoted by ℂ(S) and defined as ℂ(S) =^{def} ⋂{ C ⊆ ℝ^{n} | S ⊆ C and C is closed }. We denote the set of all non-negative reals by ℝ_{+}. For each i ∈ {1, …, n}, v_{i} denotes the i-th component of the (column) vector v ∈ ℝ^{n}. We denote by 0 the vector of ℝ^{n}, called the origin, having all components equal to zero. A vector v ∈ ℝ^{n} can also be interpreted as a matrix in ℝ^{n×1} and manipulated accordingly using the usual definitions for addition, multiplication (both by a scalar and by another matrix), and transposition, which is denoted by v^{T}. The scalar product of v, w ∈ ℝ^{n}, denoted ⟨v, w⟩, is the real number v^{T}w = ∑_{i=1}^{n} v_{i}w_{i}. For any relational operator ▷◁ ∈ {=, ≥, ≤, <, >}, we write v ▷◁ w to denote the conjunctive proposition ⋀_{i=1}^{n}(v_{i} ▷◁ w_{i}). In contrast, v ≠ w will denote the proposition ¬(v = w). We will sometimes use the convenient notation a ▷◁_{1} b ▷◁_{2} c to denote the conjunction a ▷◁_{1} b ∧ b ▷◁_{2} c and we will not distinguish conjunctions of propositions from sets of propositions. For each set S ⊆ ℝ^{n} of finite cardinality m, we denote by matrix(S) ⊆ ℝ^{n×m} the set of all matrices having S as the set of their columns.

3 Convex Polyhedra and the Double Description Method

For each vector a ∈ ℝ^{n} and scalar b ∈ ℝ, where a ≠ 0, the linear (non-strict) inequality constraint ⟨a, x⟩ ≥ b defines a closed affine half-space. The linear equality constraint ⟨a, x⟩ = b defines an affine hyperplane. Convex polyhedra are usually described as finite systems of linear equality and inequality constraints. When working at the theoretical level, it is simpler to express each equality constraint as the intersection of the two half-spaces ⟨a, x⟩ ≥ b and ⟨−a, x⟩ ≥ −b.

Definition 1. (Closed polyhedron.) The set P ⊆ ℝ^{n} is a closed polyhedron if and only if either P can be expressed as the intersection of a finite number of closed affine half-spaces of ℝ^{n}, or n = 0 and P = ∅.

Alternatively, the definition of a convex polyhedron can be based on some of the geometric features of the set of solutions of such a system of constraints. A vector r ∈ ℝ^{n} such that r ≠ 0 is a ray (or direction of infinity) of a nonempty polyhedron P ⊆ ℝ^{n} if, for every point p ∈ P and every λ ∈ ℝ_{+}, it holds p+λr ∈ P; a vector l ∈ ℝ^{n} is a line of P if both l and −l are rays of P. The empty polyhedron has no rays and no lines. As was the case for equality constraints, the theory can dispense with the use of lines by using the corresponding pair of opposite rays. The following theorem is a simple consequence of well known theorems by Minkowski and Weyl [32].

Theorem 1. The set P ⊆ ℝ^{n} is a closed polyhedron if and only if there exist finite sets R, P ⊆ ℝ^{n} of cardinality k and ℓ, respectively, such that 0 ∉ R and, for any matrices K ∈ ℝ^{n×k} and L ∈ ℝ^{n×ℓ} where K ∈ matrix(R) and L ∈ matrix(P),

P = { Kμ + Lν ∈ ℝ^{n} | μ ∈ ℝk_{+}, ν ∈ ℝℓ_{+}, ∑_{i=1}^{ℓ} ν_{i} = 1 }.

When P ≠ ∅, we say that P is described by the generator system G = (R, P). In particular, the vectors of R and P are rays and points of P, respectively. Informally speaking, if no “supporting point” is provided then an empty polyhedron is obtained; formally, P = ∅ if and only if P = ∅. By convention, the empty system (i.e., the system with R = ∅ and P = ∅) is the only generator system for the empty polyhedron. It is worth stressing that, in general, the vectors in R and P are not the extreme rays and the vertices of the polyhedron [3]: for instance, any half-space of ℝ^{2} has two extreme rays and no vertices, but any generator system describing it will contain at least three rays and one point.

The combination of the two approaches outlined above is the basis of the Double Description (DD) method [30], which exploits the duality principle to compute each representation starting from the other one, possibly minimizing the descriptions. We will write con(C) and gen(G) to denote the polyhedra described by the finite constraint system C and generator system G, respectively.

Definition 2. (DD pair and minimal forms.) If con(C) = gen(G) = P, then (C, G) is said to be a DD pair for P, and we write (C, G) ≡ P. We say that – C is in minimal form if there does not exist C′ ⊂ C such that con(C′) = P;

– G = (R, P) is in minimal form if there does not exist G′ = (R′, P′) such that G′ ≠ G, R′ ⊆ R, P′ ⊆ P and gen(G′) = P;

– the DD pair (C, G) is in minimal form if C and G are both in minimal form.

The set of all closed polyhedra on the vector space ℝ^{n}, denoted ℂℙ_{n}, can be partially ordered by set-inclusion to form a lattice having the emptyset and ℝ^{n} as the bottom and top element, respectively. The binary meet operation is thus given by set-intersection, which is easily implemented by taking the union of the constraint systems representing the two arguments. Similarly, the binary join operation, denoted ⊎ and called convex polyhedral hull (poly-hull, for short), is implemented by taking the union of the two arguments’ generator systems. Note that, in general, the poly-hull of two polyhedra is different from their convex hull [32].

4 Handling Not Necessarily Closed Polyhedra

For each vector a ∈ ℝ^{n} and scalar b ∈ ℝ, where a ≠ 0, the linear strict inequality constraint ⟨a, x⟩ > b defines an open affine half-space. By allowing strict inequalities to occur in the system of constraints, it is possible to define polyhedra that are not necessarily closed (NNC polyhedra, for short).

Definition 3. (NNC polyhedron.) The set P ⊆ ℝ^{n} is a NNC polyhedron if and only if either P can be expressed as the intersection of a finite number of (not necessarily closed) affine half-spaces of ℝ^{n}, or n = 0 and P = ∅.

We denote by ℙ_{n} the set of all NNC polyhedra on the vector space ℝ^{n}. Obviously, we have ℂℙ_{n} ⊆ ℙ_{n} (note that ℂℙ_{n} = ℙ_{n} if and only if n = 0). When partially ordered by set-inclusion, ℙ_{n} is a lattice and ℂℙ_{n} is a sublattice of ℙ_{n}.

To the best of the authors’ knowledge, the first software library (based on the DD method) allowing for the computation over the domain ℙ_{n} was the Polka library [21], where each NNC polyhedron P ∈ ℙ_{n} is embedded into a closed polyhedron R ∈ ℂℙ_{n+1}. The additional dimension of the vector space, usually labeled by the letter ϵ, encodes the topological closedness of each affine half-space in the constraint description for P. Namely, if P = con(C), where

C = { ⟨a_{i}, x⟩ ▷◁_{i} b_{i} | i ∈ {1, …, m}, a_{i} ∈ ℝ^{n}, ▷◁_{i} ∈ {≥, >}, b_{i} ∈ ℝ },

then the representation polyhedron is defined as R = con(con repr(C)), where

con repr(C) =^{def} {0 ≤ ϵ ≤ 1}
∪ { ⟨a_{i}, x⟩ − 1 · ϵ ≥ b_{i} | i ∈ {1, …, m}, ▷◁_{i} ∈ {>} }
∪ { ⟨a_{i}, x⟩ + 0 · ϵ ≥ b_{i} | i ∈ {1, …, m}, ▷◁_{i} ∈ {≥} }.

It should be stressed that the choice of the value −1 for the coefficients of the additional variable ϵ in the constraints representing strict inequalities is rather arbitrary: any other negative value will do. Similarly, the side constraint ϵ ≤ 1 could be replaced by any other ϵ-upper-bound constraint, i.e., by any constraint ϵ ≤ δ such that δ > 0. Different, though equivalent, constraint systems C_{j} describing P may be embedded into different representation polyhedra R_{j} = con(con repr(C_{j})). We shall abuse notation by writing R = con repr(P) as a shorthand for R = con(con repr(C)), provided the constraint system C describing P is clear from context.

As far as we know, no available implementation of the double description method offers full support for NNC polyhedra. Partial support is provided by the New Polka library [25], which can be initialized to also work with strict inequalities. However, the correct encoding of the different kinds of constraints, the addition of the required side conditions on the ϵ dimension and the correct interpretation of the obtained results, are all under the user’s responsibility. This kind of approach, which requires the user to know so many implementation details, is far from being satisfactory.

4.1 The Generators of NNC Polyhedra

One of the fundamental features of the DD method, and the very reason for its name, is the ability to represent a closed polyhedron using a system of constraints or a system of generators. While being equivalent, there are contexts where each of these descriptions is the most appropriate, so that a good library should provide the client application with both possibilities.

Any NNC polyhedron can be easily described by using constraint systems containing strict inequalities, but a similar generalization of the concept of generator system seems to be missing. This causes an asymmetry in the handling of NNC polyhedra using the DD method that is reflected in existing software libraries. For instance, the following sentence comes from the documentation of New Polka [25, Section 1.1.4, page 10] (where s denotes the ϵ coefficient):

Don’t ask me the intuitive meaning of s ≠ 0 in rays and vertices !

The problem is discussed in some more detail in [20, Section 4.5, pp. 10–11]:

While strict inequations handling is transparent for constraints (being displayed accurately), the extra dimension added to the variables space is apparent when it comes to generators : one extra coefficient, resp. extra vertices (as epsilon is bounded), materialize this dimension in every generator, resp. generators system. This makes more difficult to define polyhedra with the only help of generators : one should carefully study the extra vertices with non null epsilon coefficients added to constraints defined polyhedra, in the case of large inequations, and the case of strict inequations.

A clear understanding of the generator systems of NNC polyhedra is helpful, for instance, in order to generalize to the domain ℙ_{n} those operators on closed polyhedra that are defined or implemented in terms of the generator system representation (such as the time-elapse operator of [21, 22] or the generatorsbased widening of [7]).

We will now show how, by decoupling the user interface from the details of the particular implementation, it is possible to provide an intuitive generalization of the concept of generator system, so that the geometric features of any NNC polyhedron can be accurately represented. The key step is the introduction of a new kind of generator.

Definition 4. (Closure point.) A vector c ∈ ℝ^{n} is a closure point of S ⊆ ℝ^{n} if and only if c ∈ ℂ(S).

When considering NNC polyhedra, closure points can be characterized by a property which is similar to the one used when defining rays.

Proposition 1. A vector c ∈ ℝ^{n} is a closure point of the NNC polyhedron P ∈ ℙ_{n} if and only if P ≠ ∅ and λp + (1 − λ)c ∈ P for every point p ∈ P and λ ∈ ℝ such that 0 < λ < 1.

We are now able to provide a parametric description for any NNC polyhedron.

Theorem 2. The set P ⊆ ℝ^{n} is an NNC polyhedron if and only if there exist finite sets R, P, C ⊆ ℝ^{n} of cardinality k, ℓ and m, respectively, such that 0 ∉ R and, for any matrices K ∈ ℝ^{n×k}, L ∈ ℝ^{n×ℓ}, M ∈ ℝ^{n×m} where K ∈ matrix(R), L ∈ matrix(P) and M ∈ matrix(C),

P = \{ Kμ + Lν + Mη ∈ ℝ^{n} | \begin{matrix}μ ∈ ℝk_{+}, ν ∈ ℝℓ_{+}, ν ≠ 0, η ∈ ℝm_{+}, \\ ∑_{i=1}^{ℓ} ν_{i} + ∑_{i=1}^{m} η_{i} = 1 \end{matrix} \}.

When P ≠ ∅, we say that P is described by the extended generator system G = (R, P, C). As was the case for closed polyhedra, the vectors in R and P are rays and points of P, respectively. The condition ν ≠ 0 ensures that at least one of the points of P plays an active role in any convex combination of the vectors of P and C. It follows from Proposition 1 that the vectors of C are closure points of P. Since rays and closure points need a supporting point, we have P = ∅ if and only if P = ∅.

In Figure 1, we provide a few examples of the use of extended generator systems for the description of NNC polyhedra: (closure) points are represented by small (un-) filled circles, whereas rays are represented by vectors that, for notational convenience, are applied to points.

The NNC polyhedron P_{1} is an open rectangle and is described by the closure points A, B, C, D and the point E; note that E could have been replaced by any other point of P_{1}, whereas all the four closure points have to be included in any generator system for P_{1}. The NNC polyhedron P_{2} is another rectangle that is neither closed nor open: since A′ is a point, the open segments ]A′, B′[ and ]A′, D′[ are included in P_{2}; similarly, the open segment ]B′, C′[ is included in P_{2} because E′ is a point of the generator system (note that E′ is needed, since both B′ and C′ are not in P_{2}, but it could have been replaced by any other point lying on this open segment); in contrast, the closed segment [C′, D′] is disjoint from

[figure: O; x; y; P_{1}; A; B; C; D; E; P_{2}; A′; B′; C′; D′; E′; P_{3}; F; G; ^{r^{1}}; ^{r^{2}}]

Fig. 1. Using closure points to define NNC polyhedra.

P_{2}, because neither C′ nor D′ are points of P_{2}. Finally, the NNC polyhedron P_{3} can be regarded as the translation by F of the open positive orthant. Thus the generator system includes the closure point F, the rays r_{1} and r_{2} and the point G; again, the latter could have been replaced by any other point of P_{3}.

We will now show how the high level description of an NNC polyhedron provided by an extended generator system can be mapped into an implementation based on the ϵ dimension approach. Namely, if G = (R, P, C) is the extended generator system describing P ∈ ℙ_{n}, the corresponding closed representation R ∈ ℂℙ_{n+1} is described by the generator system gen repr(G) =^{def} (R′, P′) where

R′ = { (r^{T}, 0)^{T} | r ∈ R },
P′ = { (p^{T}, 1)^{T} | p ∈ P } ∪ { (x^{T}, 0)^{T} | x ∈ P ∪ C }.

Even in this case, the value 1 for the coordinate of the ϵ dimension in the translation of points is almost arbitrary: any other positive value could be chosen. Different though equivalent extended generator systems G_{j} describing P ∈ ℙ_{n} may result in different representation polyhedra R_{j} = gen(gen repr(G_{j})). It is worth noting that the closure points of P are mapped to points of R having a zero ϵ coordinate. In contrast, the points of P are mapped to a pair of points of R, having a zero and a strictly positive ϵ coordinate, respectively; by doing this, we explicitly enforce in the closed representation the key invariant saying that any point of P is also a closure point of P.

Definition 5. (ϵ-representation.) A polyhedron R ∈ ℂℙ_{n+1} is said to be an ϵ-representation if and only if

∃δ > 0 . R ⊆ con({0 ≤ ϵ ≤ δ});  (1)
(∃ϵ > 0 . (x^{T}, ϵ)^{T} ∈ R) ⟹ (x^{T}, 0)^{T} ∈ R.  (2)

R is said to be an ϵ-representation for P ∈ ℙ_{n}, denoted R ⇛_{ϵ} P, if R is an ϵ-representation and

P = [[R]] =^{def} { x ∈ ℝ^{n} | ∃ϵ > 0 . (x^{T}, ϵ)^{T} ∈ R }.  (3)

Proposition 2. Let (C, G) ≡ P ∈ ℙ_{n}. Then we have con(con repr(C)) ⇛_{ϵ} P and gen(gen repr(G)) ⇛_{ϵ} P.

Operations such as the intersection of NNC polyhedra and the application of affine transformations can be safely performed on any of the ϵ-representations of the arguments; the same holds for the poly-hull operation, provided none of the arguments is an empty NNC polyhedron. Some care has to be taken when testing the emptyness of an NNC polyhedron or the inclusion of an NNC polyhedron into another one [21]. For instance, any ϵ-representation included in the hyperplane ϵ = 0 actually encodes the empty NNC polyhedron.

Proposition 3. Let R ⇛_{ϵ} P, R_{1} ⇛_{ϵ} P_{1} and R_{2} ⇛_{ϵ} P_{2}. Then

1. P = ∅ if and only if R ⊆ con({ϵ ≤ 0});

2. R_{1} ∩ R_{2} ⇛_{ϵ} P_{1} ∩ P_{2};

3. (P_{1} ≠ ∅ ∧ P_{2} ≠ ∅) ⟹ (R_{1} ⊎ R_{2} ⇛_{ϵ} P_{1} ⊎ P_{2});

4. let f =^{def} λx ∈ ℝ^{n} . Ax + b be any affine transformation defined on ℙ_{n}; then g(R) ⇛_{ϵ} f(P), where

g =^{def} λ (\begin{matrix}x \\ ϵ \end{matrix}) ∈ ℝ^{n+1} . (\begin{matrix}A & 0 \\ 0^{T} & 1 \end{matrix}) (\begin{matrix}x \\ ϵ \end{matrix}) + (\begin{matrix}b \\ 0 \end{matrix})

is the corresponding affine transformation on ℂℙ_{n+1}.

4.2 The Issue of Minimization

When adopting the ϵ dimension approach proposed in [21], the computed representation R ∈ ℂℙ_{n+1} of an NNC polyhedron P ∈ ℙ_{n} will depend not only on the particular constraint system considered, but also on the sequence of operations (intersections, poly-hulls, affine transformations, etc.) performed on the polyhedron. If not properly handled, such an abundance of possible representations may cause problems when trying to provide a non-redundant description of P.

The reason is that libraries such as New Polka compute the minimal forms of the closed representation R. Very often, such an approach results in a redundant description of the represented NNC polyhedron: there may be a different ϵrepresentation for P that is characterized by a smaller number of constraints (generators). The following example illustrates this point.

Consider the two NNC polyhedra P_{1}, P_{2} ∈ ℙ_{1} defined as

P_{1} =^{def} con({0 < x < 2}), P_{2} =^{def} con({2 < x < 3}).

[figure: O; x; ϵ; ϵ = 1; R_{1}; O; B; A; R_{2}; A; C; D; O; B; D; C]

Fig. 2. The ϵ-representations of P_{1} and P_{2} and of their poly-hull.

These polyhedra are encoded by the closed polyhedra R_{1}, R_{2} ∈ ℂℙ_{2} such that^{9}

R_{1} =^{def} con repr(P_{1}) = \{ (x, ϵ)^{T} ∈ ℝ^{2} | \begin{matrix}ϵ & ≥ 0 \\ x − ϵ & ≥ 0 \\ −x − ϵ & ≥ −2 \end{matrix} \},

R_{2} =^{def} con repr(P_{2}) = \{ (x, ϵ)^{T} ∈ ℝ^{2} | \begin{matrix}ϵ & ≥ 0 \\ x − ϵ & ≥ 2 \\ −x − ϵ & ≥ −3 \end{matrix} \}.

Suppose now that the user wants to compute the poly-hull of the two original polyhedra, therefore obtaining the NNC polyhedron

P_{3} =^{def} con({0 < x < 3}).

At the representation level, the situation will be the one described in Figure 2: P_{3} is represented by the closed polyhedron generated by the four vertices O, C, D, and B, whereas point A is identified as redundant. Formally,

R_{3} =^{def} \{ (x, ϵ)^{T} ∈ ℝ^{2} | \begin{matrix}ϵ & ≥ 0 \\ x − ϵ & ≥ 0 \\ −x − ϵ & ≥ −3 \\ −x − 3ϵ & ≥ −4 \end{matrix} \}.

The last non-strict inequality, which corresponds to the segment [B, D] in Figure 2, is not redundant as far as the ϵ-representation R_{3} is concerned. However, this non-strict inequality stands for the strict inequality x < 4, which is clearly redundant when considering the represented polyhedron P_{3}.

The problem outlined above is even more critical when dealing with higher dimension vector spaces: it is straightforward to devise examples where more than half of the constraints in the “minimized” representation happen to be redundant. Even when disregarding these pathological cases, redundancy could

9 In both cases, we do not explicitly include the ϵ-upper-bound constraint ϵ ≤ 1, which happens to be redundant.

[figure: O; x; ϵ; ϵ = 1; R_{1}; O; B; A; R_{4}; C; D; E; F; C; D; G; H]

Fig. 3. The “minimized” trapezium CDGH, obtained by intersecting R_{1} and R_{4} and still representing the topologically closed NNC polyhedron P_{4}, also encodes the strict inequality x > 0.

have a serious negative impact on the efficiency of some of the operations computed on the polyhedron, e.g., those characterized by a worst case complexity that is exponential in the size of the description.

Besides efficiency issues, the presence of redundant constraints may also cause headaches to the users of the library. For instance, suppose one wants to know if a given NNC polyhedron is not topologically closed. Ordinary users (i.e., all the users but the experts) may be tempted to implement such a test by checking whether the constraint system in minimal form contains any strict inequality. Unfortunately, such an approach would be unsound, as can be easily observed by considering the scenario proposed in Figure 3. Here, the NNC polyhedron P_{1} is intersected with the NNC polyhedron

P_{4} =^{def} con({1 ≤ 4x ≤ 3}),

whose representation R_{4} = con repr(P_{4}) is the rectangle having vertices C, D, E and F. The resulting trapezium is another ϵ-representation for the NNC polyhedron P_{4}, which is topologically closed. However, any constraint system describing the trapezium will also encode the strict inequality x > 0, corresponding to the closed segment [G, H].

It is therefore meaningful to address the problem of providing a minimization procedure that is able to remove all of these redundancies. To this end, the introduction of some notation will be helpful.

We say that a vector v saturates the constraint ⟨a, x⟩ ▷◁ b if and only if ⟨a, v⟩ = b. For any constraint system C and generator system G = (R, P), we define

sat con(v, C) =^{def} { c ∈ C | v saturates c };
sat gen(c, G) =^{def} { v ∈ R ∪ P | v saturates c }.

Let (C, G) ≡ R ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P. The set of strict and non-strict inequality encodings C_{>} and C_{≥} of constraint system C are defined as

C_{>} =^{def} { (⟨a, x⟩ + s · ϵ ≥ b) ∈ C | a ≠ 0, s < 0 };
C_{≥} =^{def} { (⟨a, x⟩ + s · ϵ ≥ b) ∈ C | a ≠ 0, s = 0 };

we also define the set of ϵ-upper-bounds as

C_{ϵ} =^{def} { (⟨a, x⟩ + s · ϵ ≥ b) ∈ C | a = 0, s < 0 }.

For ease of notation, a constraint c ∈ C_{ϵ} will be usually denoted as ϵ ≤ δ, where δ =^{def} b/s. Note that, by Proposition 3, we have δ > 0 whenever P ≠ ∅. Similarly, the set of closure point encodings G_{C}, the set of point encodings G_{P}, and the set of unmatched point encodings G_{U} ⊆ G_{P} of the generator system G = (R, P) are defined as follows:

G_{C} =^{def} { (p^{T}, e)^{T} ∈ P | e = 0 };
G_{P} =^{def} { (p^{T}, e)^{T} ∈ P | e > 0 };
G_{U} =^{def} { (p^{T}, e)^{T} ∈ P | e > 0, (p^{T}, 0)^{T} ∉ P }.

Definition 6. (Strong minimal form.) Let R ⇛_{ϵ} P, where (C, G) ≡ R is a DD pair in minimal form. Then, we say that

– C is in strong minimal form if there does not exist a constraint system C′ in minimal form such that (C′_{>} ∪ C′_{≥}) ⊂ (C_{>} ∪ C_{≥}) and con(C′) ⇛_{ϵ} P;

– G = (R, P) is in strong minimal form if there does not exist a generator system G′ = (R′, P′) such that G′ ≠ G, R′ ⊆ R, P′ ⊆ P and gen(G′) ⇛_{ϵ} P.

For the computation of strong minimal forms (smf’s, for short), the key step is the identification of ϵ-redundant constraints and generators.

Definition 7. (ϵ-redundancy.) Let (C, G) ≡ R ∈ ℂℙ_{n+1}. A constraint c is ϵ-redundant in C if c ∈ C_{>} and at least one of the following conditions holds:

sat gen(c, G) ∩ G_{C} = ∅;
∃c′ ∈ C_{>} \ {c} . sat gen(c, G) \ G_{P} ⊆ sat gen(c′, G).

A generator p is ϵ-redundant in G if p ∈ G_{U} and

∃p′ ∈ G_{P} \ {p} . sat con(p, C) ∩ C_{≥} ⊆ sat con(p′, C).

Proposition 4. Let R ⇛_{ϵ} P ≠ ∅, where (C, G) ≡ R is a DD pair in minimal form. Then, the following hold:

1. If c is ϵ-redundant in C, then con(C \ {c} ∪ {ϵ ≤ 1}) ⇛_{ϵ} P;

[figure: O; x; ϵ; ϵ = 1; O; B; E; C; O; C; F]

Fig. 4. The trapezium OCEB is obtained by applying the strong minimization process to the constraint system describing R_{3}. The triangle OCF is yet another representation for the NNC polyhedron P_{3}, which can be characterized by a constraint system and a generator system that are both in smf.

2. If p is ϵ-redundant in G = (R, P), then gen((R, P \ {p})) ⇛_{ϵ} P;

3. If C contains no ϵ-redundant constraint, then it is in smf;

4. If G contains no ϵ-redundant generator, then it is in smf.

It is worth stressing that, even if (C, G) is a DD pair for R ⇛_{ϵ} P, after removing all ϵ-redundant constraints and generators the resulting descriptions C′ and G′ may be such that con(C′) ≠ gen(G′), so that (C′, G′) is not a DD pair. Moreover, having one of the systems in smf does not imply that the corresponding dual description will also be in smf.

However, if the generator system is in smf, a DD pair with both components in smf can easily be computed.

Conjecture 1. Let R ⇛_{ϵ} P ≠ ∅, where (C, G) ≡ R is a minimal DD pair. If G is in smf, all the point encodings in G_{P} have the same value for the ϵ coordinate and, for all c ∈ C_{>}, sat gen(c, G) ∩ G_{C} ≠ ∅, then C is in smf.

As an example, we now compute smf’s for the polyhedron R_{3} represented in Figure 2. Let us first consider the constraint system. The two strict inequality encodings x − ϵ ≥ 0 and −x − ϵ ≥ −3, which correspond to segments [O, B] and [C, D], are not ϵ-redundant, because they are saturated by the closure point encodings O and C, respectively. In contrast, the constraint x − 3ϵ ≥ 4, corresponding to segment [B, D], is identified as ϵ-redundant (no closure point encoding saturates it) and can be removed provided we add the constraint ϵ ≤ 1. The resulting constraint system, which is in smf, defines the trapezium of vertices O, C, E, and B represented in Figure 4. Note that the generator system for this trapezium is not in smf; this additional property can be enforced by removing the ϵ-upper-bound constraint ϵ ≤ 1, therefore obtaining the triangle of vertices O, C, and F.

Starting again from polyhedron R_{3}, let us now consider the strong minimization of its generator system, which is made up of the four points O, C, D, and B.

[figure: O; x; ϵ; ϵ = 1; O; B; C; O; C; D]

Fig. 5. Other two different ϵ-representations for P_{3}, which can be obtained by applying the strong minimization process to the generator system describing R_{3}.

It is easy to observe that each one of the two unmatched point encodings is made ϵ-redundant by the other one (they both saturate the empty set of non-strict inequality encodings); as a consequence, one of them can be removed, obtaining either one of the triangles OCB and OCD represented in Figure 5, which are both in smf.

It is worth noting that, after removing an ϵ-redundant constraint, the addition of the ϵ-upper-bound constraint ϵ ≤ 1 is in general required to obtain another ϵ-representation. For instance, this happens when computing the smf of the constraint system describing the trapezium CDGH of Figure 3: the simple removal of the constraint corresponding to segment [G, H] would yield a stripe which is unbounded from above, so that it would not satisfy condition 1 of Definition 5; the addition of the ϵ-bounding constraint results in the rectangle CDEF (i.e., the ϵ-representation R_{4} of P_{4}).

5 The Parma Polyhedra Library

The Parma Polyhedra Library (PPL, http://www.cs.unipr.it/ppl/) is a collaborative project started in January 2001 at the Department of Mathematics of the University of Parma. It aims at becoming a truly professional library for the handling of approximations based on (not necessarily closed) convex polyhedra targeted at abstract interpretation and computer-aided verification. In this section we briefly review some of the key features of the library.^{10} Before continuing, it is perhaps worth stressing that the theoretical treatment of previous sections applies to polyhedra in ℝ^{n}. Not surprisingly, the implementation only deals with rational polyhedra, that is, polyhedra that can be defined by constraints with rational coefficients or, dually, generators with rational coordinates. It is easy to prove that the property of being rational is preserved by all the operations of interest for the applications the library aims at.

10 The features described here, and many others, are present in release 0.4 of the library

  available at http://www.cs.unipr.it/ppl/.

The library is written in standard C^{++} and this ensures, among other things, maximum portability across different computing platforms. Using C^{++} for the development made it easier to adopt a number of programming techniques that are the key to the library’s robustness, generality, efficiency and usability. However, for the sake of maximal code reuse and utility, care has been taken not to require the client application to be written in C^{++}. The library includes a complete C interface and thus can be interfaced to all programming languages’ implementations (there are many) that provide a C interface. There is also a Prolog interface supporting several Prolog systems and direct interfaces to other languages, such as Objective Caml and Mercury, are planned for the near future.

One of the key features of the library is robustness. In particular, this means that failure is avoided whenever possible and, in all other cases, failure is recognized and handled properly. The PPL uses arbitrary precision integer arithmetic to implement coefficients and coordinates, and is thus immune from both rounding and overflow problems. In addition, all the data structures used in the implementation are fully dynamic and can expand automatically (in amortized constant time) to any dimension allowed by the available virtual memory. Two other aspects of failure avoidance are hiding and systematic checking of the interface invariants. In contrast to other libraries, the PPL hides the implementation details almost completely. For instance, the internal representation of constraints, generators and systems thereof need not concern the client application. Similarly, implementation devices such as the positivity constraint [33] and all the matters regarding the ϵ-representation encoding of NNC polyhedra are completely invisible from outside. The client application is provided with more natural interfaces, allowing the direct manipulation of higher level concepts, such as inequalities, lines and closure points. For instance, in the appropriate contexts, ‘X < 5*Z’ and ‘X + 2*Y + 5*Z >= 7’ is valid syntax expressing a strict and a non-strict inequality, both in the C^{++} and the Prolog interfaces. Even the C interface, which is at a considerably lower level of abstraction, refers to concepts like linear expression, constraint and constraint system and not to their possible implementations such as vectors and matrices. As usual, this is important for error prevention and to allow maximum latitude for the implementation.

Forbidding access to the internal structures manipulated by the library and systematic checking of the interface invariants could impede the overall system performance. However, the resulting overhead can be completely repaid (to the point of giving rise to a speedup) if the implementation exploits the freedom it has from the user interface. Even though, at the time of writing, the PPL only exploits a small part of this freedom, everything is in place to take full advantage of it. On a related aspect, the library has been designed to support the systematic application of incremental and lazy computation techniques, from which considerable efficiency improvements can be expected.^{11}

11 For the expert: the issues of incrementality and laziness include the use of saturation matrices (that were already present in Polylib [33]) and their efficient handling, delayed and incremental minimization of systems of constraints and generators, incremental sorting of matrices and so forth.

typedef Parma_Polyhedra_Library::NNC_Polyhedron PH;
void complex_function(const PH& ph1, const PH& ph2, PH& result) {
  try {
    start_timer(max_time_for_complex_function);
    complex_function_on_polyhedra(ph1, ph2, result ...);
    stop_timer();
  }
  catch (Exception& e) {
    // Virtual memory exhausted, or timeout expired, or any other error.
    ...
    BoundingBox bb1, bb2, bb_result;
    ph1.shrink_bounding_box(bb1);
    ph2.shrink_bounding_box(bb2);
    complex_function_on_bounding_boxes(bb1, bb2, bb_result ...);
    result = Polyhedron(bb_result);
  }
}

Fig. 6. Falling back to bounding boxes when the analysis with polyhedra is too costly.

In the design of the library, particular care has been taken concerning the possibility of interfacing the library with other constraint domains and with respect to scalability issues. It is clear that any user of any polyhedra library must face the possibility of excessive CPU time consumption and/or excessive memory usage [24]. As we have seen, one far from satisfactory but possible solution is to hope for the best but eventually “kill” those processes requiring more than the available resources [8]. In contrast, what we aim at is support for the dynamic and automatic composition of the trade-off between expressivity and efficiency. In this scenario, the static analysis or verification procedures should, by default, use the more descriptive (and costly) domains, such as the convex polyhedra. When the computation of an operation on these descriptions requires too much time, or memory space, the system should detect this and perform a change of representation, for instance by approximating the input polyhedra with enclosing bounding boxes (rectangular regions with sides parallel to the axes); after the execution of the requested operation on this less precise (but much less computationally expensive) domain, the result is converted back into a convex polyhedron. Such a scenario is feasible only if the polyhedra library is implemented so that it can consistently react, without any loss of system resources, to events such as a timeout or an exception thrown by the memory allocation routines. As far as we know, the Parma Polyhedra Library is the first one to provide this facility. The idea is exemplified in Figure 6, where a robust C^{++} implementation of complex_function is sketched. The objective is to compute the polyhedron result starting from the polyhedra ph1 and ph2. The operation is first tried on the polyhedra themselves and, in case of failure, the computation is done on the bounding box approximations of ph1 and ph2. In the latter case the result of the bounding box computation, bb_result is converted into a convex polyhedron object and assigned to the output polyhedron result. The trade-off between efficiency and precision can also be controlled by means of the widening operations provided by the PPL, which are based on those originally proposed in [16] and improved in [15].

Concerning the efficiency of the PPL, at present no application can use both the PPL and another convex polyhedra library, so comparisons are not possible. However, the PPL has been integrated with the China analyzer [1] for the purpose of detecting linear argument size relations [5]. The performance of the combined system has been compared, on the same task, with the performance of the cTI analyzer [29], which uses an implementation of convex polyhedra based on the SICStus CLP(Q) package. The combined system China+PPL outperformed that version of cTI in a significant way, exhibiting termination instead of thrashing and speedups of one or more orders of magnitude.

The Parma Polyhedra Library is free software released under the GPL: code and documentation can be downloaded and its development can be followed at

http://www.cs.unipr.it/ppl/.

6 Conclusion

Convex polyhedra provide the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission critical systems. For such purposes an implementation of convex polyhedra must be firmly based on a clear theoretical framework and written in accordance with sound software engineering principles. In this paper we have presented some of the most important ideas that are behind the Parma Polyhedra Library. In particular, we have provided a novel theoretical framework for the representation and manipulation of not necessarily closed convex polyhedra. We have also briefly sketched some important features of the design and implementation of the library. We believe that all this work constitutes a significant improvement in the state of the art and an encouragement to the wider adoption of abstract interpretation techniques in static analysis and computer-aided verification.

Acknowledgments. We would like to thank Costantino Medori for the many useful discussions we had with him on the subject of this paper, Fred Mesnard for letting us play with cTI’s analyzer, and the anonymous reviewers for their helpful comments and observations.

References

1. R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, 1997. Printed as Report TD-1/97.

2. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. The Parma Polyhedra Library User’s Manual. Department of Mathematics, University of Parma, Parma, Italy, release 0.4 edition, July 2002. Available at http://www.cs.unipr.it/ppl/.

3. R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. Quaderno 286, Dipartimento di Matematica, Università di Parma, Italy, 2002. See also [4]. Available at http:

//www.cs.unipr.it/Publications/.

4. R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Errata for technical report

“Quaderno 286”. Available at http://www.cs.unipr.it/Publications/, 2002.

See [3].

5. F. Benoy and A. King. Inferring argument size relationships with CLP(R). In J. P. Gallagher, editor, Logic Programming Synthesis and Transformation: Proceedings of the 6th International Workshop, volume 1207 of Lecture Notes in Computer Science, pages 204–223, Stockholm, Sweden, 1997. Springer-Verlag, Berlin.

6. B. Bérard and L. Fribourg:. Reachability analysis of (timed) Petri nets using real arithmetic. In J. C. M. Baeten and S. Mauw, editors, CONCUR’99: Concurrency Theory, Proceedings of the 10th International Conference, volume 1664 of Lecture Notes in Computer Science, pages 178–193, Eindhoven, The Netherlands, 1999. Springer-Verlag, Berlin.

7. F. Besson, T. P. Jensen, and J.-P. Talpin. Polyhedral analysis for synchronous languages. In A. Cortesi and G. Filé, editors, Static Analysis: Proceedings of the 6th International Symposium, volume 1694 of Lecture Notes in Computer Science, pages 51–68, Venice, Italy, 1999. Springer-Verlag, Berlin.

8. N. S. Bjørner, A. Browne, M. Colón, B. Finkbeiner, Z. Manna, M. Pichora, H. B. Sipma, and T. E. Uribe. STeP: The Stanford Temporal Prover (Educational Release) User’s Manual. Computer Science Department, Stanford University, Stanford, California, version 1.4-α edition, July 1998. Available at http:

//www-step.stanford.edu/.

9. N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear equations. U.S.S.R. Computational Mathematics and Mathematical Physics, 4(4):151–158, 1964.

10. N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities. U.S.S.R. Computational Mathematics and Mathematical Physics, 5(2):228–233, 1965.

11. N. V. Chernikova. Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics, 8(6):282–293, 1968.

12. M. A. Colón and H. B. Sipma. Synthesis of linear ranking functions. In T. Margaria and W. Yi, editors, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), volume 2031 of Lecture Notes in Computer Science, pages 67–81, Genova, Italy, 2001. Springer-Verlag, Berlin.

13. P. Cousot, editor. Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, France, 2001. Springer-Verlag, Berlin.

14. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.

15. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269–295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.

16. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84–96, Tucson, Arizona, 1978. ACM Press.

17. N. Dor, M. Rodeh, and S. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In Cousot [13], pages 194–212.

18. K. Fukuda and A. Prodon. Double description method revisited. In M. Deza, R. Euler, and Y. Manoussakis, editors, Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3-5, 1995, Selected Papers, volume 1120 of Lecture Notes in Computer Science, pages 91–111. Springer-Verlag, Berlin, 1996.

19. N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, Computer Aided Verification: Proceedings of the 5th International Conference, volume 697 of Lecture Notes in Computer Science, pages 333–346, Elounda, Greece, 1993. Springer-Verlag, Berlin.

20. N. Halbwachs, A. Kerbrat, and Y.-E. Proy. POLyhedra INtegrated Environment. Verimag, France, version 1.0 of POLINE edition, September 1995. Documentation taken from source code.

21. N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In B. Le Charlier, editor, Static Analysis: Proceedings of the 1st International Symposium, volume 864 of Lecture Notes in Computer Science, pages 223–237, Namur, Belgium, 1994. Springer-Verlag, Berlin.

22. N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.

23. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1(1+2):110–122, 1997.

24. T. A. Henzinger, J. Preussig, and H. Wong-Toi. Some lessons from the hytech experience. In Proceedings of the 40th Annual Conference on Decision and Control, pages 2887–2892. IEEE Computer Society Press, 2001.

25. B. Jeannet. Convex Polyhedra Library, release 1.1.3c edition, March 2002. Documentation of the “New Polka” library available at http://www.irisa.fr/prive/

Bertrand.Jeannet/newpolka.html.

26. H. Le Verge. A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.

27. V. Loechner. PolyLib: A library for manipulating parameterized polyhedra. Avail-

able at http://icps.u-strasbg.fr/~loechner/polylib/, March 1999. Declares

itself to be a continuation of [33].

28. Z. Manna, N. S. Bjørner, A. Browne, M. Colón, B. Finkbeiner, M. Pichora, H. B. Sipma, and T. E. Uribe. An update on STeP: Deductive-algorithmic verification of reactive systems. In R. Berghammer and Y. Lakhnech, editors, Tool Support for System Specification, Development and Verification, Advances in Computing Sciences. Springer-Verlag, Berlin, 1999.

29. F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In Cousot [13], pages 93–110.

30. T. S. Motzkin, H. Raiffa, G. L. Thompson, and R. M. Thrall. The double description method. In H. W. Kuhn and A. W. Tucker, editors, Contributions to the Theory of Games – Volume II, number 28 in Annals of Mathematics Studies, pages 51–73. Princeton University Press, Princeton, New Jersey, 1953.

31. W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, 1992.

32. J. Stoer and C. Witzgall. Convexity and Optimization in Finite Dimensions I. Springer-Verlag, Berlin, 1970.

33. D. K. Wilde. A library for doing polyhedral operations. Master’s thesis, Oregon State University, Corvallis, Oregon, December 1993. Also published as IRISA Publication interne 785, Rennes, France, 1993.

A Some Errors and Imprecisions in the Literature

Before deciding to write the Parma Polyhedra Library we have conducted an extensive study of the available software and publications dealing with the manipulation of convex polyhedra using the Double Description method [30]. During this work we have discovered several small errors and imprecisions that sometimes cover the treated matter with a thin layer of ambiguity and uncertainty. We list here the problems we spotted so as to explain why our definitions and results are sometimes different from those in the literature and to save others some frustration.

The most widespread imprecision concerns the parametric representation of convex polyhedra: vertices^{12} and extreme rays^{13} are often mentioned improperly. For instance, consider the polyhedron corresponding to the full vector space ℝ^{2}: this has no vertex and no extreme ray and any generator system describing it will include at least one point and four rays (or, better, one point and two lines). In general, a polyhedron has a vertex if and only if it has no lines.

Such a problem is first found in [26, Section 6, pp. 10–11], where it is said that the parametric representation of a convex polyhedron is composed by vertices and extremal rays,^{14} implicitly excluding other kinds of generators. The example above shows that, in general, the generator system of a polyhedron P may have to include points of P which are not vertices of P.

In [33, Sections 2.4.1 and 2.6.1, pp. 10–11] the abuse of the word ‘vertices’ is explained in a footnote, but the problem with extreme rays remains. When Motzkin’s theorem is used to decompose a polyhedron, it is said that its characteristic cone can be described by a combination of lines and extreme rays of the polyhedron, thus disregarding examples such as the one mentioned above.

Another imprecision concerns the concept of polar of a polyhedron. In [33, Definition 2.25, page 12], the polar K^{∗} is defined for any closed convex set K ⊆ ℝ^{n}

12 A vertex (or extreme point) of a polyhedron P is any point of P which cannot be

expressed as the convex combination of other points of P. 13 An extreme ray of a polyhedron P is any ray of P which cannot be expressed as a

positive combination of other rays of P; note that two rays differing by a positive scalar factor (i.e., r = μr′, where μ > 0) are considered equivalent.

14 Note that the definition of extremal ray by Le Verge, provided for a cone in [26, Section 2, p. 4] and then extended to a polyhedron in [26, Section 6, p. 11], is significantly different from the definition of extreme ray used in [33], which is the one reported before.

such that 0 ∈ K as follows:^{15}

K^{∗} =^{def} { y ∈ ℝ^{n} | ∀x ∈ K : ⟨x, y⟩ ≤ 0 }.

Then it is said that K and K^{∗} are dual of each other [33, Property 2.7, page 12], even though the concept of duality has only been defined for polytopes [33, Definition 2.24, page 12]. Note that, even when restricting ourselves to the case where K is a polytope containing the origin, K^{∗} is not guaranteed to be a polytope. For an example, let P be the triangle in ℝ^{2} having vertices O = (0, 0)^{T}, A = (1, 0)^{T} and B = (0, 1)^{T}; then the cone P^{∗} happens to be equal to the third orthant, so that the concept of dual polytopes is not applicable. Moreover, P^{∗∗} is equal to the first orthant, so that P ≠ P^{∗∗} (contrary to what stated in [33, property (iii), page 12]). As far as we can tell, the cause of all these problems is the systematic confusion between the concept of polar cone K^{∗} (defined as above) as opposed to the concept of polar set K^{π}, which is defined, for an arbitrary set K ⊆ ℝ^{n}, as follows [32, (2.14.6), page 76]:

K^{π} =^{def} { y ∈ ℝ^{n} | ∀x ∈ K : ⟨x, y⟩ ≤ 1 }.

Namely, the polar of a polyhedron is the polar set of the polyhedron, and not its polar cone. Most of the stated results do hold when the two definitions are swapped; for example, if P ∈ ℂℙ_{n} is a polyhedron, we have P = P^{ππ} if and only if 0 ∈ P. However, some other statements are still wrong, such as the one above regarding the duality of polars. As a matter of fact, requiring 0 ∈ P is not enough to ensure that P^{π} is a polytope; as stated in [32, (2.14.11), page 77], this property holds if and only if P is a fully dimensional polyhedron and 0 is an inner point of P. Because of these problems, all the observations in [33] concerning the polar of a polyhedron cannot really be trusted (besides confusing the reader to a large extent).

In [33, Definition 2.14, page 8], the convex hull of a set K is defined as the smallest convex set that contains K. Then the convex union of two convex polyhedra P_{1} and P_{2} is defined as the convex hull of P_{1}∪P_{2} and convex polyhedra are said to be closed with respect to the convex union operation [33, Section 3.4 and Table 3.3, page 17]. However, this is false. A simple counter-example is obtained in the vector space ℝ^{2} by letting P_{1} = { (x, y)^{T} ∈ ℝ^{2} | x = 0 } and P_{2} = {(1, 0)^{T}}. Then, as observed in [32], the convex hull of P_{1} ∪ P_{2} is the set

K = { (x, y)^{T} ∈ ℝ^{2} | 0 ≤ x < 1 } ∪ P_{2},

which cannot be written as the intersection of a finite number of half-spaces (and thus is not a convex polyhedron).

Some of these imprecisions seems to have percolated the subsequent literature. For instance, consider [7], where a new widening operator for the domain of polyhedra is defined. In [7, Definition 7, p. 63] it is stated that

15 In fact, the textual definition states the condition ⟨x, y⟩ ≥ 0. We believe that the relation sign ‘≤’ was intended; in any case, these two definitions return sets that are isomorphic via a systematic change of signs.

The set of extreme rays form a basis which describes all directions in which the convex polyhedron is open.

The statement of [7, Theorem 2, p. 63], which is meant to be a variant of the well known theorem by Minkowski, contains the usual error concerning vertices. As a consequence, even when accepting the (somehow standard) abuse of the word “convex hull”, the definition of the convex hull based widening [7, Section 6.1, pp. 64-65] has to be taken with some care, since it is defined in terms of the cardinalities of the sets of lines, extreme rays and vertices describing the polyhedron.

B Proofs

As already observed in the paper, Theorem 1 is a simple consequence of well known theorems by Minkowski (stating the “only if” part) and Weyl (stating the “if” part). We here provide the proofs of the other formal results stated.

Lemma 1. Let P = con(C) ∈ ℙ_{n} and v ∈ ℂ(P). Let also (⟨a, x⟩ ▷◁ b) ∈ C, where ▷◁ ∈ {≥, >}. Then ⟨a, v⟩ ≥ b.

Proof. Let H be the set of affine half-spaces corresponding to the set of constraints C. Since ℂ(·) is an upper closure operator,

ℂ(P) = ℂ(⋂ H) ⊆ ℂ(⋂{ ℂ(H) | H ∈ H }) = ⋂{ ℂ(H) | H ∈ H }.

As v ∈ ℂ(P), we have v ∈ ℂ(H), for all H ∈ H. Let H_{c} ∈ H denote the affine half-space corresponding to c = (⟨a, x⟩ ▷◁ b). Hence v ∈ ℂ(H_{c}). If ▷◁ ∈ {≥}, then ℂ(H_{c}) = con({c}). On the other hand, if ▷◁ ∈ {>}, then ℂ(H_{c}) = con({c′}), where c′ = (⟨a, x⟩ ≥ b). Thus, as v ∈ ℂ(H_{c}), we obtain the thesis ⟨a, v⟩ ≥ b. ⊓ ⊔

Proof (Proof of Proposition 1). Let P = con(C) ∈ ℙ_{n}, where C = {c_{1}, …, c_{m}}.

To prove the “only if” branch, suppose that c is a closure point of P, so that c ∈ ℂ(P). Then P ≠ ∅, because the topological closure of the empty set is still empty. Considering an arbitrary point p ∈ P and a scalar λ such that 0 < λ < 1, we have to prove that vector v =^{def} λp + (1 − λ)c is such that v ∈ P. To this end, we show that v satisfies all constraints c_{i} = (⟨a_{i}, x⟩ ▷◁_{i} b_{i}) ∈ C. Since p ∈ P, it holds ⟨a_{i}, p⟩ ▷◁_{i} b_{i}; moreover, by applying Lemma 1, we also have ⟨a_{i}, c⟩ ≥ b_{i}. Therefore, we obtain

⟨a_{i}, v⟩ = ⟨a_{i}, λp + (1 − λ)c⟩
= λ⟨a_{i}, p⟩ + (1 − λ)⟨a_{i}, c⟩
▷◁_{i} λb_{i} + (1 − λ)⟨a_{i}, c⟩
▷◁_{i} λb_{i} + (1 − λ)b_{i}
= b_{i}.

To prove the “if” branch, suppose now that P ≠ ∅ and λp + (1 − λ)c ∈ P, for all p ∈ P and 0 < λ < 1. We have to show that c ∈ ℂ(P). To this end, for each i ∈ ℕ, let λ_{i} = \frac{1}{i}. For all i > 1, we have 0 < λ_{i} < 1 and thus

v_{i} =^{def} λ_{i}p + (1 − λ_{i})c ∈ P. It is easy to observe that, for any open ball centered in c having radius δ = \frac{1}{i}, the intersection of P with the ball is not empty, because all the v_{j} ∈ P such that j > i belong to the ball. Therefore, c ∈ ℂ(P). ⊓ ⊔

A direct proof of Theorem 2 would require a generalization of Minkowski’s and Weyl’s theorems. In contrast, we will provide an indirect proof, which will be based on Proposition 2 as well as on some other lemmas stating properties holding for polyhedra that are ϵ-representations. The formal proof of Proposition 2 is facilitated by the introduction of a more rigorous definition for the function ‘gen’.

Definition 8. Let G = (R, P, C) be an extended generator system, where

R = {r_{1}, …, r_{k}}, P = {p_{1}, …, p_{ℓ}}, C = {c_{1}, …, c_{m}}

are finite subsets of ℝ^{n} and 0 ∉ R. The NNC polyhedron gen(G) generated by G is defined as

gen(G) =^{def} \{ ∑_{i=1}^{k} μ_{i}r_{i} + ∑_{i=1}^{ℓ} ν_{i}p_{i} + ∑_{i=1}^{m} η_{i}c_{i} | \begin{matrix}μ ∈ ℝk_{+}, ν ∈ ℝℓ_{+}, η ∈ ℝm_{+}, \\ ν ≠ 0, ∑_{i=1}^{ℓ} ν_{i} + ∑_{i=1}^{m} η_{i} = 1 \end{matrix} \}.

For a standard generator system G = (R, P), we define gen(G) =^{def} gen((R, P, ∅)).

Proof (Proof of Proposition 2). We first show that R =^{def} con(con repr(C)) ⇛_{ϵ} P. Condition (1) of Definition 5 follows directly from the definition of con repr. To prove condition (2) of Definition 5, suppose that (v^{T}, e)^{T} ∈ R. Then this

satisfies any constraint c = (⟨a, x⟩ + s · ϵ ≥ b) ∈ con repr(C). By condition (1), e ≥ 0 and, by definition of con repr, s ≤ 0. It therefore follows that ⟨a, v⟩ ≥ b so that (v^{T}, 0)^{T} also satisfies c. As the choice of c ∈ con repr(C) was arbitrary, (v^{T}, 0)^{T} ∈ R.

To prove condition (3) of Definition 5, we have to show v ∈ P if and only if there exists e > 0 such that (v^{T}, e)^{T} ∈ R.

Suppose first that there exists e > 0 such that (v^{T}, e)^{T} ∈ R. We will show that v satisfies all constraints c ∈ C. If c = (⟨a, x⟩ ▷◁ b) ∈ C, then, by definition of con repr, there exists a constraint c′ = (⟨a, x⟩+s·ϵ ≥ b) ∈ con repr(C), where s ∈ {0, −1}. Since (v^{T}, e)^{T} satisfies c′, we have ⟨a, v⟩ + s · e ≥ b. If s = −1, then s·e < 0, so that ⟨a, v⟩ > b and v satisfies the constraint c. Otherwise, if s = 0, we have ▷◁ ∈ {≥} and ⟨a, v⟩ ≥ b, which again means that v satisfies the constraint c. As the choice of c ∈ C was arbitrary, v ∈ P.

Suppose next that v ∈ P and consider an arbitrary constraint c′ = (⟨a, x⟩ + s · ϵ ≥ b) ∈ con repr(C). Then, by definition of con repr, s ∈ {0, −1}. We show that there exists δ_{c′} > 0 such that, for all e ≤ δ_{c′}, (v^{T}, e)^{T} satisfies c′. There are two cases depending on the value of s. If s = 0, then (v^{T}, e)^{T} satisfies c′ for all e ∈ ℝ. In this case, we let δ_{c′} = 1. If s = −1, by definition of con repr, there exists a constraint c = (⟨a, x⟩ > b) ∈ C. Then, for all e ≤ ⟨a, v⟩ − b, the vector (v^{T}, e)^{T} satisfies c′. In this case, let δ_{c′} = ⟨a, v⟩ − b. Therefore, for each constraint c′ ∈ con repr(C), there exists δ_{c′} > 0 such that, for all e ≤ δ_{c′}, (v^{T}, e)^{T} satisfies c′. Letting δ be the least element of the set { δ_{c′} | c′ ∈ C }, we obtain δ > 0 and (v^{T}, δ)^{T} satisfies all constraints in con repr(C), so that (v^{T}, δ)^{T} ∈ R.

Secondly, we show that R =^{def} gen(gen repr(G)) ⇛_{ϵ} P.

To this end, let G = (R, P, C), where R = {r_{1}, …, r_{k}}, P = {p_{1}, …, p_{ℓ}} and C = {c_{1}, …, c_{m}}. Let also G′ = (R′, P′) be defined as G′ =^{def} gen repr(G), so that R′ = {r′_{1}, …, r′_{k}}, with r′_{i} = (r_{i}^{T}, 0)^{T}, and P′ = {p′_{1}, …, p′_{h}}, with h = m + 2ℓ and

p′_{i} = \begin{cases}(c_{i}^{T}, 0)^{T}, & if 1 ≤ i ≤ m; \\ (p_{i}^{T}, 1)^{T}, & if m + 1 ≤ i ≤ m + ℓ; \\ (p_{i}^{T}, 0)^{T}, & if m + ℓ + 1 ≤ i ≤ m + 2ℓ. \end{cases}

Then, by Definition 8, we have (v^{T}, e)^{T} ∈ R if and only if there exist μ ∈ ℝk_{+} and ν′ ∈ ℝh_{+} such that ∑_{i=1}^{h} ν′_{i} = 1 and

(v^{T}, e)^{T} = ∑_{i=1}^{k} μ_{i}r′_{i} + ∑_{i=1}^{h} ν′_{i}p′_{i}.  (4)

To prove condition (1) of Definition 5, let (v^{T}, e)^{T} ∈ R. Clearly, 0 ≤ e ≤ 1 holds because coefficient e is obtained in (4) as a convex combination of coefficients taken from the set {0, 1}.

To prove condition (2) of Definition 5, let (v^{T}, e)^{T} ∈ R, where e > 0. Now write (v^{T}, e)^{T} according to (4) and let ν′′ ∈ ℝh_{+} be defined as

ν′′_{i} =^{def} \begin{cases}ν′_{i}, & if 1 ≤ i ≤ m; \\ 0, & if m + 1 ≤ i ≤ m + ℓ; \\ ν′_{i−ℓ} + ν′_{i}, & if m + ℓ + 1 ≤ i ≤ m + 2ℓ. \end{cases}

Since we still have ∑_{i=1}^{h}ν′′_{i} = 1, by Definition 8 the combination

∑_{i=1}^{k} μ_{i}r′_{i} + ∑_{i=1}^{h} ν′′_{i}p′_{i} = (v^{T}, 0)^{T}

is another point of R, as required.

To prove condition (3) of Definition 5, we have to show v ∈ P if and only if there exists e > 0 such that (v^{T}, e)^{T} ∈ R.

Suppose first that there exists e > 0 such that (v^{T}, e)^{T} ∈ R. By expressing (v^{T}, e)^{T} according to (4), we also obtain

v = ∑_{i=1}^{k} μ_{i}r_{i} + ∑_{i=1}^{m} ν′_{i}c_{i}. + ∑_{i=m+1}^{m+ℓ} ν′_{i}p_{i} + ∑_{i=m+ℓ+1}^{m+2ℓ} ν′_{i}p_{i}.

Let now η = (ν′_{1}, …, ν′_{m}) ∈ ℝm_{+} and ν ∈ ℝℓ_{+} be such that ν_{i} = ν′_{m+i} + ν′_{m+ℓ+i},

for all i ∈ {1, …, ℓ}. Then it holds ∑_{i=1}^{ℓ} ν_{i} + ∑_{i=1}^{m} η_{i} = ∑_{i=1}^{h} ν′_{i} = 1 and ν ≠ 0 so that, by Definition 8, we obtain that the combination

∑_{i=1}^{k} μ_{i}r_{i} + ∑_{i=1}^{ℓ} ν_{i}p_{i} + ∑_{i=1}^{m} η_{i}c_{i} = v

is a point of P = gen((R, P, C)), as required.

Suppose next that v ∈ P. By Definition 8, there exist μ ∈ ℝm_{+}, ν ∈ ℝℓ_{+} and

η ∈ ℝm_{+} such that ν ≠ 0, ∑_{i=1}^{ℓ} ν_{i} + ∑_{i=1}^{m} η_{i} = 1 and

v = ∑_{i=1}^{k} μ_{i}r_{i} + ∑_{i=1}^{ℓ} ν_{i}p_{i} + ∑_{i=1}^{m} η_{i}c_{i}.

Let h = m + 2ℓ and ν′ ∈ ℝh_{+} be such that

ν′_{i} = \begin{cases}η_{i}, & if 1 ≤ i ≤ m; \\ ν_{i−m}, & if m + 1 ≤ i ≤ ℓ; \\ 0, & if m + ℓ + 1 ≤ i ≤ m + 2ℓ. \end{cases}

Note that ν′ ≠ 0 and ∑_{i=1}^{h} ν′_{i} = 1. Thus, by Definition 8, the combination

∑_{i=1}^{k} μ_{i}r′_{i} + ∑_{i=1}^{h} ν′_{i}p′_{i} = (v^{T}, e)^{T}

is a point of R = gen((R′, P′)). Note that ν′ ≠ 0 implies e > 0, as required. ⊓ ⊔

We now provide lemmas showing that there is no loss of generality in the choice of ϵ coefficients made by function ‘con repr’ (resp., the choice of ϵ coordinates made by function ‘gen repr’) and that all rays of an ϵ-representation have a zero ϵ coordinate.

Lemma 2. Let P ∈ ℙ_{n} and C_{1} be a constraint system in ℝ^{n+1} containing only non-strict inequalities such that con(C_{1}) ⇛_{ϵ} P. Then, there exists a mixed constraint system C such that con(con repr(C)) ⇛_{ϵ} P.

Proof. Let R_{1} = con(C_{1}). Consider the constraint system C = C′ ∪ C′′, where

C′ =^{def} { ⟨a, x⟩ > b | (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{1}, s < 0, a ≠ 0 },
C′′ =^{def} { ⟨a, x⟩ ≥ b | (⟨a, x⟩ ≥ b) ∈ C_{1}, a ≠ 0 }.

Let C_{2} =^{def} con repr(C) and R_{2} = con(C_{2}). Then, by definition of ‘con repr’, we obtain C_{2} = {0 ≤ ϵ ≤ 1} ∪ C′_{2} ∪ C′′, where

C′_{2} = { ⟨a, x⟩ − ϵ ≥ b | (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{1}, s < 0, a ≠ 0 }.

By Proposition 2, R_{2} satisfies conditions (1) and (2) of Definition 5. To complete the proof, it remains to show that [[R_{1}]] = [[R_{2}]].

Let v ∈ [[R_{1}]], so that there exists e > 0 such that (v^{T}, e)^{T} ∈ R_{1}. By definition of ‘con’, (v^{T}, e)^{T} satisfies all the constraints in C_{1}. Thus (v^{T}, e′)^{T} satisfies all the constraints in C′′ for any e′ ∈ ℝ. Suppose c_{1} =^{def} (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{1}, where s < 0 and a ≠ 0. Then (v^{T}, e)^{T} satisfies c_{1} and −s · e > 0. Moreover, if

c′ =^{def} (⟨a, x⟩ − ϵ ≥ b), then c′ ∈ C′_{2}. Thus, for any 0 < e′ ≤ −s · e, (v, e′) satisfies

c′. Thus, if e_{0} is the greatest lower bound of the set

{1} ∪ { −s · e | (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{1}, a ≠ 0 },

we obtain 0 < e_{0} ≤ 1 and (v^{T}, e_{0})^{T} satisfies all the constraints in C_{2}, so that (v^{T}, e_{0})^{T} ∈ R_{2} and hence, v ∈ [[R_{2}]], as required.

Let v ∈ [[R_{2}]], so that there exists 0 < e ≤ 1 such that (v^{T}, e)^{T} ∈ R_{2}. By definition of ‘con’, (v^{T}, e)^{T} satisfies all the constraints in C_{2}. Thus (v^{T}, e′)^{T} satisfies all the constraints in C′′ for any e′ ∈ ℝ. Let c′ =^{def} (⟨a, x⟩ − ϵ ≥ b) ∈ C′_{2},

where a ≠ 0. Then (v^{T}, e)^{T} satisfies c′. Moreover, if c_{1} =^{def} (⟨a, x⟩ + s · ϵ ≥ b), where s < 0, then c_{1} ∈ C_{1} and −\frac{e}{s} > 0. Thus, for any 0 < e′ ≤ −\frac{e}{s}, (v, e′) satisfies c_{1}. Thus, if e_{0} is the greatest lower bound of the set

\{ δ | (ϵ ≤ δ) ∈ C_{1} \} ∪ \{ −\frac{e}{s} | (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{1}, a ≠ 0 \},

we obtain e_{0} > 0 and (v^{T}, e_{0})^{T} satisfies all the constraints in C_{1}, so that (v^{T}, e_{0})^{T} ∈ R_{1} and hence, v ∈ [[R_{1}]], as required. ⊓ ⊔

Lemma 3. Let gen((R, P)) ⇛_{ϵ} P, where P ≠ ∅. Then, for all (r^{T}, e)^{T} ∈ R, e = 0.

Proof. By contraposition, suppose there exists (r^{T}, e)^{T} ∈ R such that e ≠ 0. As R is an ϵ-representation, condition (1) holds so that, there exists δ > 0 such that for any point (x^{T}, ϵ)^{T} ∈ R, 0 ≤ ϵ ≤ δ. As R is non-empty, there exists a point (v, e_{0}) ∈ R for some 0 ≤ e_{0} ≤ δ. Thus, for all μ ∈ ℝ_{+},

(v_{μ}^{T}, e_{μ})^{T} =^{def} μ(r^{T}, e)^{T} + (v^{T}, e_{0})^{T} ∈ R.

If e < 0, by taking μ > −\frac{e_{0}}{e} ∈ ℝ_{+}, we obtain e_{μ} < 0. Similarly, if e > 0, by taking μ ≥ \frac{δ}{e} ∈ ℝ_{+}, we obtain e_{μ} ≥ e_{0} +δ > δ. Thus, in both cases we contradict condition (1) of Definition 5. Therefore, it must hold e = 0. ⊓ ⊔

Lemma 4. Let P ∈ ℙ_{n} and G_{1} be a (standard) generator system in ℝ^{n+1} such that gen(G_{1}) ⇛_{ϵ} P. Then there exists an extended generator system G such that gen(gen repr(G)) ⇛_{ϵ} P.

Proof. Let G_{1} = (R_{1}, P_{1}) and R_{1} = gen(G_{1}). Consider the extended generator system G = (R, P, C) such that

R = { r ∈ ℝ^{n} | (r^{T}, 0)^{T} ∈ R_{1} },
P = { p ∈ ℝ^{n} | (p^{T}, e)^{T} ∈ P_{1}, e > 0 },
C = { c ∈ ℝ^{n} | (c^{T}, e)^{T} ∈ P_{1}, e = 0 }.

Let G_{2} = gen repr(G) = (R_{2}, P_{2}) and R_{2} = gen(G_{2}); by definition of ‘gen repr’ and Lemma 3, we have R_{2} = R_{1} and

P_{2} = { (p^{T}, 1)^{T} ∈ ℝ^{n+1} | (p^{T}, e)^{T} ∈ P_{1}, e > 0 }
∪ { (p^{T}, 0)^{T} ∈ ℝ^{n+1} | (p^{T}, e)^{T} ∈ P_{1} }.

Let k, ℓ and m be the cardinalities of R_{1}, P_{1} and P_{2}, respectively.

By Proposition 2, R_{2} satisfies conditions (1) and (2) of Definition 5. To complete the proof, it remains to show that [[R_{1}]] = [[R_{2}]].

Let p ∈ [[R_{1}]], so that there exists e > 0 such that (p^{T}, e)^{T} ∈ R_{1}. By definition of ‘gen’, there exist μ ∈ ℝk_{+} and ν ∈ ℝℓ_{+}, where ∑_{i=1}^{ℓ} ν_{i} = 1, such that

(p^{T}, e)^{T} = μR_{1} + νP_{1}.

Now, by definition of P_{2}, for each (p_{i}^{T}, e_{i})^{T} ∈ P_{1} such that e_{i} > 0 (resp., e_{i} = 0) there exists (p_{i}^{T}, e′_{i})^{T} ∈ P_{2} such that e′_{i} > 0 (resp., e′_{i} = 0). Therefore, there exists also η ∈ ℝm_{+}, where ∑_{i=1}^{m} η_{i} = 1, such that

(p^{T}, e′)^{T} = μR_{1} + ηP_{2},

where e′ > 0. Thus, (p^{T}, e′)^{T} ∈ R_{2} and p ∈ [[R_{2}]], as required.

The other inclusion is proved by a symmetric argument. ⊓ ⊔

Proof (Proof of Theorem 2). To prove the ‘only if’ branch, letting P ∈ ℙ_{n} we will prove that there exists an extended generator system G = (R, P, C) such that P = gen(G). If P = ∅, then we simply take R = P = C = ∅. Otherwise, let P ≠ ∅. By definition of NNC polyhedron, there exists a constraint system C such that P = con(C). Let R =^{def} con(con repr(C)) ∈ ℂℙ_{n+1} so that, by Proposition 2, R ⇛_{ϵ} P. By Theorem 1, there exists a (standard) generator system G′ = (R′, P′) such that R = gen((R′, P′)). Then the thesis follows by Lemma 4.

To prove the ‘if’ branch, letting G = (R, P, C) be an extended generator system, we will show that P = gen(G) is an NNC polyhedron. If P = ∅, then we obtain P = ∅ and the empty set is an NNC polyhedron. Otherwise, let P ≠ ∅, so that P ≠ ∅. Let R = gen(gen repr(G)) so that, by Proposition 2, R ⇛_{ϵ} P. By Theorem 1, there exist a constraint system C′, containing non-strict linear inequalities only, such that R = con(C′). Then the thesis follows by Lemma 2.

⊓ ⊔

Lemma 5. If P ∈ ℙ_{n} is a non-empty NNC polyhedron and R ⇛_{ϵ} P, then

ℂ(P) = { x ∈ ℝ^{n} | (x^{T}, 0)^{T} ∈ R }.

Proof. Letting P′ =^{def} { x ∈ ℝ^{n} | (x^{T}, 0)^{T} ∈ R }, we will prove P′ = ℂ(P).

First, we show that P′ ⊆ ℂ(P). Let x ∈ P′, so that (x^{T}, 0)^{T} ∈ R, and consider p ∈ P: since R ⇛_{ϵ} P, by applying property (3) of Definition 5, there exists ϵ > 0 such that (p^{T}, ϵ)^{T} ∈ R. Since R is a convex set, for all λ ∈ ℝ such that 0 < λ < 1 we have

λ(p^{T}, ϵ)^{T} + (1 − λ)(x^{T}, 0)^{T} = (λp^{T} + (1 − λ)x^{T}, λϵ)^{T} ∈ R.

Note that, since λϵ > 0, by applying again property (3) of Definition 5, we obtain λp + (1 − λ)x ∈ P. Since P ≠ ∅ and the choices of p ∈ P and λ where both arbitrary, we can apply Proposition 1 and conclude x ∈ ℂ(P).

Now we show that ℂ(P) ⊆ P′. Let x ∈ ℂ(P). For all p ∈ P and i ∈ ℕ such that i > 1, we have λ_{i} =^{def} \frac{1}{i}, 0 < λ_{i} < 1 and, by Proposition 1,

v_{i} =^{def} λ_{i}p + (1 − λ_{i})x ∈ P.

Since R ⇛_{ϵ} P, by applying first property (3) and then property (2) of Definition 5, we obtain (v_{i}^{T}, 0)^{T} ∈ R. If p = x, then v_{i} = x, so that the thesis holds. Otherwise, let p ≠ x. For any open ball of ℝ^{n+1} centered in (x^{T}, 0)^{T} and having radius δ > 0, there exists a j ∈ ℕ such that λ_{j} < δ; thus, (v_{j}^{T}, 0)^{T} ∈ R belongs to the ball and, as the choice of δ is arbitrary, (x^{T}, 0)^{T} ∈ ℂ(R). However, R ∈ ℂℙ_{n+1} is a topologically closed set, so that R = ℂ(R) and (x^{T}, 0)^{T} ∈ R. Hence, x ∈ P′, completing the proof. ⊓ ⊔

Lemma 6. Let P = gen((R, P, C)) ∈ ℙ_{n} be a non-empty NNC polyhedron and define R′ = { (r^{T}, 0)^{T} | r ∈ R } ⊆ ℝ^{n+1}. If R ⇛_{ϵ} P, then there exists Q ∈ ℝ^{n+1} such that R = gen((R′, Q)).

Proof. In this proof, to simplify notation, if A is a set of vectors we let A also denote an arbitrary element of matrix(A). The context makes it clear when the symbol denotes a set or a matrix.

Since R ∈ ℂℙ_{n+1}, by Theorem 1 there exist finite sets S′, Q ⊆ ℝ^{n+1} such that R = gen((S′, Q)). By Lemma 3, if (s^{T}, e)^{T} ∈ S′, then e = 0. Let k and ℓ denote the cardinalities of R′ and S′, respectively, and define

S =^{def} { s ∈ ℝ^{n} | (s^{T}, 0)^{T} ∈ S′ }.

Suppose μ ∈ ℝk_{+}. As P = gen((R, P, C)), if x ∈ P then v =^{def} x + μR ∈ P. Thus, by conditions (2) and (3) of Definition 5, (v^{T}, 0)^{T} = (x^{T}, 0)^{T} + μR′ ∈ R. Since this holds for any μ ∈ ℝk_{+}, it follows that R′ is a set of rays of R, so that R = gen((S′ ∪ R′, Q)).

Suppose ν ∈ ℝℓ_{+}. As R = gen((S′, Q)), if (x^{T}, e)^{T} ∈ R and e > 0, then

(v^{T}, e)^{T} =^{def} (x^{T}, e)^{T} + νS′ ∈ R. Then, by condition (3) of Definition 5, v = x + νS ∈ P. Since this holds for any ν ∈ ℝℓ_{+}, it follows that S is a set of rays of P. However, since P = gen((R, P, C)), if s ∈ S then s = μR, for some μ ∈ ℝk_{+}. As a consequence, (s^{T}, 0)^{T} = μR′. Since this holds for all the vectors in S′, then S′ is a set of redundant rays, so that R = gen((R′, Q)). ⊓ ⊔

Lemma 7. For j ∈ {1, 2}, let P_{j} = gen((R_{j}, P_{j}, C_{j})) be a non-empty NNC polyhedron; let also k_{j} be the cardinality of R_{j} and K_{j} ∈ matrix(R_{j}). Then x ∈ P_{1} ⊎ P_{2} if and only if there exist 0 ≤ λ ≤ 1, x_{1} ∈ ℂ(P_{1}), x_{2} ∈ ℂ(P_{2}),

μ_{1} ∈ ℝk_{1}_{+} and μ_{2} ∈ ℝk_{2}_{+} such that

x = λx_{1} + (1 − λ)x_{2} + μ_{1}K_{1} + μ_{2}K_{2},

where (x_{1} ∈ P_{1} ∧ λ > 0) ∨ (x_{2} ∈ P_{2} ∧ λ < 1).

Proof. For j ∈ {1, 2}, let ℓ_{j} and m_{j} be the cardinalities of P_{j} and C_{j}, respectively. By definition of the poly-hull operation, we have P_{1}⊎P_{2} = gen((R, P, C)), where R = R_{1} ∪ R_{2}, P = P_{1} ∪ P_{2} and C = C_{1} ∪ C_{2}, having cardinalities k, ℓ and m, respectively.

Suppose first that x ∈ P_{1} ⊎ P_{2}. Then, by Definition 8,

x = μK + νL + ηM

where K ∈ matrix(R), L ∈ matrix(P), M ∈ matrix(C), μ ∈ ℝk_{+}, ν ∈ ℝℓ_{+}, η ∈ ℝm_{+}, ∑ ν + ∑ η = 1 and ν ≠ 0. Therefore, we can also rewrite it as

x = μ_{1}K_{1} + μ_{2}K_{2} + ν_{1}L_{1} + ν_{2}L_{2} + η_{1}M_{1} + η_{2}M_{2}
= (ν_{1}L_{1} + η_{1}M_{1}) + (ν_{2}L_{2} + η_{2}M_{2}) + μ_{1}K_{1} + μ_{2}K_{2},

where L_{j} ∈ matrix(P_{j}), M_{j} ∈ matrix(C_{j}), μ_{j} ∈ ℝk_{j}_{+}, ν_{j} ∈ ℝℓ_{j}_{+} and η_{j} ∈ ℝm_{j}_{+},

for j ∈ {1, 2}, ∑ ν_{1} + ∑ ν_{2} + ∑ η_{1} + ∑ η_{2} = 1 and ∑ ν_{1} + ∑ ν_{2} > 0. It follows that either ν_{1} ≠ 0 or ν_{2} ≠ 0.

If ∑ ν_{1} +∑ η_{1} = 1 (so that ν_{2} = η_{2} = 0 and ν_{1} ≠ 0), then, by Definition 8, we obtain x_{1} =^{def} ν_{1}L_{1} + η_{1}M_{1} ∈ P_{1}. Taking λ = 1, we have 1 − λ = 0, so that we can take an arbitrary x_{2} ∈ ℂ(P_{2}) (there must exist one, since P_{2} ≠ ∅). Similarly, if ∑ ν_{2} + ∑ η_{2} = 1 (so that ν_{1} = η_{1} = 0 and ν_{2} ≠ 0), we obtain x_{2} =^{def} ν_{2}L_{2}+η_{2}M_{2} ∈ P_{2}, so that we can take λ = 0 and an arbitrary x_{1} ∈ ℂ(P_{1}). Otherwise, let both ∑ ν_{1} + ∑ η_{1} ≠ 0 and ∑ ν_{2} + ∑ η_{2} ≠ 0. Then, by taking λ = ∑ ν_{1} +∑ η_{1} we have λ > 0 and 1−λ = ∑ ν_{2} +∑ η_{2} > 0. Therefore we can

define x_{1} =^{def} \frac{1}{λ}(ν_{1}L_{1} + η_{1}M_{1}) and x_{2} =^{def} \frac{1}{1−λ}(ν_{2}L_{2} + η_{2}M_{2}). Thus x_{1} ∈ ℂ(P_{1})

and x_{2} ∈ ℂ(P_{2}). Moreover, by Definition 8, as ν_{1} ≠ 0 or ν_{2} ≠ 0, either x_{1} ∈ P_{1} or x_{2} ∈ P_{2}. In all the three cases above, we obtain

x = λx_{1} + (1 − λ)x_{2} + μ_{1}K_{1} + μ_{2}K_{2},

with x_{j} ∈ ℂ(P_{j}) for j = {1, 2} where either x_{1} ∈ P_{1} and λ > 0 or x_{2} ∈ P_{2} and λ < 1, as required.

To prove the other direction, suppose that x_{j} ∈ ℂ(P_{j}) and μ_{j} ∈ ℝk_{j}_{+}, for j = {1, 2}, and there exist 0 ≤ λ ≤ 1 such that

x = λx_{1} + (1 − λ)x_{2} + μ_{1}K_{1} + μ_{2}K_{2},

where either x_{1} ∈ P_{1} and λ > 0 or x_{2} ∈ P_{2} and λ < 1.

For j ∈ {1, 2}, since x_{j} ∈ ℂ(P_{j}), letting L_{j} ∈ matrix(P_{j}) and M_{j} ∈ matrix(C_{j}), there exist μ_{j} ∈ ℝk_{j}_{+}, ν_{j} ∈ ℝℓ_{j}_{+} and η_{j} ∈ ℝm_{j}_{+} such that

x_{j} = μ_{j}K_{j} + ν_{j}L_{j} + η_{j}M_{j},

where ∑ ν_{j} + ∑ η_{j} = 1 (note that it may hold ν_{j} = 0). Thus,

x = μ_{1}K_{1} + μ_{2}K_{2} + λ(ν_{1}L_{1} + η_{1}M_{1}) + (1 − λ)(ν_{2}L_{2} + η_{2}M_{2})
= μ_{1}K_{1} + μ_{2}K_{2} + λν_{1}L_{1} + (1 − λ)ν_{2}L_{2} + λη_{1}M_{1} + (1 − λ)η_{2}M_{2}

Note that

λ∑ ν_{1} + (1 − λ)∑ ν_{2} + λ∑ η_{1} + (1 − λ)∑ η_{2} = 1.

Moreover, as either x_{1} ∈ P_{1} and λ > 0 or x_{2} ∈ P_{2} and λ < 1, we obtain λν_{1} ≠ 0 or (1 − λ)ν_{2} ≠ 0. Thus, there exist K ∈ matrix(R_{1} ∪ R_{2}), L ∈ matrix(P_{1} ∪ P_{2}),

M ∈ matrix(C_{1} ∪ C_{2}), μ ∈ ℝk_{+}, ν ∈ ℝℓ_{+} and η ∈ ℝm_{+} such that ∑ ν + ∑ η = 1,

ν ≠ 0, and x = μK + νL + ηM. Then, by Definition 8, x ∈ P_{1} ⊎ P_{2}, completing the proof. ⊓ ⊔

Proof (Proof of Proposition 3).

Item (1) follows directly from condition (3) of Definition 5.

To prove item (2), we show that if R_{1} ⇛_{ϵ} P_{1} and R_{2} ⇛_{ϵ} P_{2}, then R_{1}∩R_{2} ⇛_{ϵ} P_{1} ∩ P_{2}. We have to show that conditions (1), (2) and (3) of Definition 5 hold for R_{1} ∩ R_{2} and P_{1} ∩ P_{2}.

We first prove condition (1). As R_{1} and R_{2} are ϵ-representations there exists δ_{1}, δ_{2} > 0 such that R_{1} ⊆ con({0 ≤ ϵ ≤ δ_{1}}) and R_{2} ⊆ con({0 ≤ ϵ ≤ δ_{2}}). Letting δ be the minimum of {δ_{1}, δ_{2}} we have R_{1} ∩ R_{2} ⊆ con({0 ≤ ϵ ≤ δ}).

To prove condition (2), let (p^{T}, e)^{T} ∈ R_{1} ∩ R_{2}. Then, as R_{1} and R_{2} are ϵ-representations, (p^{T}, 0)^{T} ∈ R_{1} and (p^{T}, 0)^{T} ∈ R_{2}. Hence (p^{T}, 0)^{T} ∈ R_{1} ∩ R_{2}.

To prove condition (3), we have to show p ∈ P_{1} ∩P_{2} if and only if there exists e > 0 such that (p^{T}, e)^{T} ∈ R_{1}∩R_{2}. First, let p ∈ P_{1}∩P_{2}. Then, by condition (3), there exists e_{1}, e_{2} > 0 such that (p^{T}, e_{1})^{T} ∈ R_{1} and (p^{T}, e_{2})^{T} ∈ R_{2}. Suppose, without loss of generality, that e_{1} ≤ e_{2}. By condition (2), (p^{T}, 0)^{T} ∈ R_{2}. Thus, since R_{2} is a convex set, (p^{T}, e_{1})^{T} ∈ R_{2}. Hence, (p^{T}, e_{1})^{T} ∈ R_{1} ∩ R_{2}. Secondly, suppose that there exists e > 0 such that (p^{T}, e)^{T} ∈ R_{1}∩R_{2}. Then (p^{T}, e)^{T} ∈ R_{1} and (p^{T}, e)^{T} ∈ R_{2}. By condition (3), p ∈ P_{1} and p ∈ P_{2}, so that p ∈ P_{1} ∩ P_{2}.

To prove item (3), we show that if P_{1} and P_{2} are not empty, R_{1} ⇛_{ϵ} P_{2} and R_{2} ⇛_{ϵ} P_{2}, then R_{1} ⊎ R_{2} ⇛_{ϵ} P_{1} ⊎ P_{2}. We have to show that conditions (1), (2) and (3) of Definition 5 hold for R_{1} ⊎ R_{2}. For j ∈ {1, 2}, let P_{j} = gen((R_{j}, P_{j}, C_{j})), where R_{j} has cardinality k_{j}. By Lemma 6, for j ∈ {1, 2}, there exist finite sets R′_{j}, Q_{j} ⊆ ℝn+1_{+} such that R_{j} = gen((R′_{j}, Q_{j})), where R′_{j} = { (r^{T}, 0)^{T} | r ∈ R_{j} }. By Lemma 7, if (p^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, then for some 0 ≤ λ ≤ 1, (p_{1}^{T}, e_{1})^{T} ∈ R_{1}, (p_{2}^{T}, e_{2})^{T} ∈ R_{2}, r = μ_{1}K_{1} + μ_{2}K_{2} where K_{1} ∈ matrix(R_{1}) and K_{2} ∈ matrix(R_{2}), μ_{1} ∈ ℝk_{1}_{+} and μ_{2} ∈ ℝk_{2}_{+}, we have

(\begin{matrix}p \\ e \end{matrix}) = λ (\begin{matrix}p & 1 \\ e_{1} \end{matrix}) + (1 − λ) (\begin{matrix}p & 2 \\ e_{2} \end{matrix}) + (\begin{matrix}r \\ 0 \end{matrix}) = (\begin{matrix}λp_{1} + (1 − λ)p_{2} \\ λe_{1} + (1 − λ)e_{2} \end{matrix}) + (\begin{matrix}r \\ 0 \end{matrix}) . (5)

We first prove condition (1). Suppose that (p^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, so that we can rewrite it according to (5). As R_{1} and R_{2} are both ϵ-representations, there exist δ_{1}, δ_{2} > 0 such that R_{1} ⊆ con({0 ≤ ϵ ≤ δ_{1}}) and R_{2} ⊆ con({0 ≤ ϵ ≤ δ_{2}}). Letting δ be the maximum of {δ_{1}, δ_{2}}, we obtain 0 ≤ e_{1} ≤ δ and 0 ≤ e_{2} ≤ δ, so that e = λe_{1} + (1 − λ)e_{2} satisfies 0 ≤ e ≤ δ. Thus, (p^{T}, e)^{T} ∈ con({0 ≤ ϵ ≤ δ}), as required.

To prove condition (2), suppose that (p^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, so that we can rewrite it according to (5). As R_{1} and R_{2} are ϵ-representations, (p_{1}^{T}, 0)^{T} ∈ R_{1} and (p_{2}^{T}, 0)^{T} ∈ R_{2} so that

(\begin{matrix}p \\ 0 \end{matrix}) = λ (\begin{matrix}p & 1 \\ 0 \end{matrix}) + (1 − λ) (\begin{matrix}p & 2 \\ 0 \end{matrix}) + (\begin{matrix}r \\ 0 \end{matrix}) ∈ R_{1} ⊎ R_{2}.

To prove condition (3), we have to show p ∈ P_{1} ⊎ P_{2} if and only if there exists e > 0 such that (p^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}. First suppose that p ∈ P_{1} ⊎ P_{2}. Then, by Lemma 7, p = λp_{1} + (1 − λ)p_{2} + r, for some 0 ≤ λ ≤ 1, p_{1} ∈ ℂ(P_{1}) and p_{2} ∈ ℂ(P_{2}), where p_{1} ∈ P_{1} and λ > 0 or p_{2} ∈ P_{2} and λ < 1, and r = μ_{1}K_{1} + μ_{2}K_{2} where K_{1} ∈ matrix(R_{1}) and K_{2} ∈ matrix(R_{2}), μ_{1} ∈ ℝk_{1}_{+} and μ_{2} ∈ ℝk_{2}_{+}. Suppose, without loss of generality, that p_{1} ∈ P_{1} and λ > 0. As R_{1} ⇛_{ϵ} P_{1}, by condition (3), there exists e_{1} > 0 such that (p_{1}^{T}, e_{1})^{T} ∈ R_{1}. As R_{2} is an ϵ-representation, by Lemma 5, from p_{2} ∈ ℂ(R_{2}) we obtain (p_{2}^{T}, 0)^{T} ∈ R_{2}. Thus, by letting

(\begin{matrix}p \\ e_{1} \end{matrix}) =^{def} λ (\begin{matrix}p & 1 \\ e_{1} \end{matrix}) + (1 − λ) (\begin{matrix}p & 2 \\ 0 \end{matrix}) + (\begin{matrix}r \\ 0 \end{matrix}) ,

we obtain (p^{T}, e_{1})^{T} ∈ R_{1} ⊎ R_{2}, where e_{1} > 0 as required. Secondly, suppose that there exists e > 0 such that (p^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, so that we can rewrite it according to (5). As R_{1} and R_{2} are ϵ-representations, by condition (1), e_{1}, e_{2} ≥ 0. As e > 0 and λ ≥ 0, either e_{1} > 0 and λ > 0 or e_{2} > 0 and λ < 1. Without loss of generality, we assume that e_{1} > 0 and λ > 0. As R_{1} ⇛_{ϵ} P_{1}, by condition (3), p_{1} ∈ P_{1}. As R_{2} ⇛_{ϵ} P_{2}, by Lemma 5, p_{2} ∈ ℂ(P_{2}). Thus, by Lemma 7,

p = λp_{1} + (1 − λ)p_{2} + r ∈ P_{1} ⊎ P_{2}.

To prove item (4), we show that g(R) ⇛_{ϵ} f(P). To see this observe that, if (x^{T}, ϵ)^{T} ∈ R for any x ∈ P and ϵ ∈ ℝ, then, by definition of g,

g((x^{T}, ϵ)^{T}) = (f(x)^{T}, ϵ)^{T}.

Thus, the ϵ dimension is not affected at all by the affine transformation, so that conditions (1), (2) and (3) of Definition 5 follow trivially from the hypothesis R ⇛_{ϵ} P. ⊓ ⊔

The proof of Proposition 4 requires a few additional lemmas.

Lemma 8. Let con(C) ⇛_{ϵ} P. Suppose there exists c = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C that is saturated by (v^{T}, e)^{T} ∈ con(C), where e ≠ 0. Then s ≤ 0.

Proof. As (v^{T}, e)^{T} ∈ con(C) saturates c, ⟨a, v⟩ + s · e = b. By condition (2) of Definition 5, (v^{T}, 0)^{T} ∈ con(C) so that ⟨a, v⟩ ≥ b. By condition (1) of Definition 5, e ≥ 0. By hypothesis, e ≠ 0, so that s ≤ 0. ⊓ ⊔

Lemma 9. Let (C, G) ≡ R ⇛_{ϵ} P, where G = (R, P) and P ≠ ∅. Then, there exists a constraint c^{∗} ∈ C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}) such that sat gen(c^{∗}, G) = R ∪ G_{C}. Moreover, if (C, G) is a DD-pair in minimal form, the following hold:

1. {c^{∗}} = C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ});

2. if p =^{def} (v^{T}, e)^{T} ∈ R and p_{0} =^{def} (v^{T}, 0)^{T}, then

sat con(p_{0}, C) \ {c^{∗}} = sat con(p, C) ∩ C_{≥};

3. for any c ∈ C \ {c^{∗}}, sat gen(c, G) ∩ G_{P} ≠ ∅.

Proof. As P ≠ ∅, by conditions (2) and (3) of Definition 5, there exists a point (v^{T}, 0)^{T} ∈ R. By condition (1), there exists a constraint c^{∗} = (⟨a, x⟩ + s · ϵ ≥ b) such that, for all e < 0, (v^{T}, e)^{T} does not satisfy c^{∗}. Thus, for all e < 0, we obtain ⟨a, v⟩ + s · e < b. As (v^{T}, 0)^{T} satisfies c^{∗}, ⟨a, v⟩ ≥ b. It follows that ⟨a, v⟩ = b and s > 0. Hence we have c^{∗} ∈ C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}). Also, as s > 0, any point (w^{T}, e)^{T} ∈ R saturates c^{∗} if and only if e = 0. Therefore, by Lemma 3, R ⊆ sat gen(c^{∗}, G), so that sat gen(c^{∗}, G) = R ∪ G_{C}.

We now suppose that (C, G) is a DD-pair in minimal form and prove all the remaining statements.

As P ≠ ∅, we have G_{P} ≠ ∅, so that (R, G_{C}) ≠ G. Since the condition sat gen(c^{∗}, G) = R ∪ G_{C} holds for any constraint c^{∗} ∈ C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}) and C is in minimal form, there can be only one such constraint, so that item 1 holds.

We now prove item 2. Consider c ∈ C_{≥}, so that c = (⟨a, x⟩ + 0 · ϵ ≥ b); then c ∈ sat con(p, C) if and only if c ∈ sat con(p_{0}, C), so that sat con(p_{0}, C_{≥}) = sat con(p, C_{≥}). Consider now c ∈ C_{>}, so that c = (⟨a, x⟩+s·ϵ ≥ b) where s < 0; since e > 0, we obtain ⟨a, v⟩ > b, so that p_{0} satisfies but does not saturate c; thus sat con(p_{0}, C_{>}) = ∅. Consider now c ∈ C_{ϵ}, so that c = (ϵ ≤ δ) for some δ > 0; then it follows that sat con(p_{0}, C_{ϵ}) = ∅. By all the above relations, together with item 1 proved above, we obtain

sat con(p_{0}, C) \ {c^{∗}} = sat con(p_{0}, C) ∩ (C_{>} ∪ C_{≥} ∪ C_{ϵ})

= sat con(p_{0}, C_{>}) ∪ sat con(p_{0}, C_{≥}) ∪ sat con(p_{0}, C_{ϵ})

= sat con(p, C) ∩ C_{≥}.

Finally, to prove item 3, suppose c ∈ C \ {c^{∗}}. Then, as (C, G) is in minimal form, sat gen(c, G) \ (R ∪ G_{C}) ≠ ∅. Thus, there exists a point encoding p ∈ G_{P} such that p ∈ sat gen(c, G). ⊓ ⊔

Lemma 10. Let R ⇛_{ϵ} P ≠ ∅, where (C, G) ≡ R is a DD pair in minimal form. If c is ϵ-redundant in C, then con(C′) ⇛_{ϵ} P, where C′ =^{def} C \ {c} ∪ {ϵ ≤ 1}.

Proof. By Definition 7, we have c ∈ C_{>}; thus, c = (⟨a, x⟩ + s · ϵ ≥ b), where a ∈ ℝ^{n} and s, b ∈ ℝ are such that a ≠ 0 and s < 0. Let R′ = con(C′). In order to show that R′ ⇛_{ϵ} P, we first prove that R′ is an ϵ-representation.

Consider condition (1) of Definition 5. The inclusion R′ ⊆ con({ϵ ≤ δ}) holds trivially by taking δ = 1, because the constraint ϵ ≤ 1 has been explicitly added in C′. To prove the other inclusion R′ ⊆ con({ϵ ≥ 0}), we apply Lemma 9 to polyhedron R. Namely, there exists a constraint c^{∗} ∈ C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}) such that, for all points v_{0} =^{def} (v^{T}, 0)^{T} ∈ R, c^{∗} is saturated by v_{0}. Since c ∈ C_{>}, then c ≠ c^{∗} and c^{∗} ∈ C′. Thus, condition (1) holds for R′.

Consider now condition (2). By contraposition, suppose there exists a vector v ∈ ℝ^{n} and a scalar e > 0 such that (v^{T}, e)^{T} ∈ R′, but (v^{T}, 0)^{T} ∉ R′. As a consequence, there must exist a constraint c′ = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C′ and a point (v^{T}, e′)^{T}, where 0 < e′ ≤ e, such that ⟨a, v⟩ + s · e′ = b and ⟨a, v⟩ < b. Since e′ > 0, the above conditions imply s > 0; as a consequence, c′ ≠ (ϵ ≤ 1), so that c′ ∈ C. However, this contradicts Lemma 8. Therefore (v^{T}, 0)^{T} ∈ R′.

Thus, R′ is an ϵ-representation. To show that it is indeed an ϵ-representation for P, we have to prove that [[R]] = [[R′]].

To prove the inclusion [[R]] ⊆ [[R′]], let v ∈ [[R]]. Thus, there exists e > 0 such that (v^{T}, e)^{T} ∈ R. By condition (2) of Definition 5, we also have (v^{T}, 0)^{T} ∈ R so that, as R is a convex set, there exists 0 < e′ < 1 such that p = (v^{T}, e′)^{T} ∈ R. Note that p satisfies all the constraints in C and it also satisfies the constraint ϵ ≤ 1; as a consequence, p ∈ R′ and v ∈ [[R′]], as required.

To show the other inclusion [[R′]] ⊆ [[R]], let v ∈ [[R′]]. Thus, there exists e′ > 0 such that (v^{T}, e′)^{T} ∈ R′ and, since R′ is an ϵ-representation, by condition (2) of Definition 5, v_{0} =^{def} (v^{T}, 0)^{T} ∈ R′. Let G′ = (R′, P′) be a generator system such that (C′, G′) ≡ R′. By Lemma 3 and the definition of closure point encodings, v_{0} ∈ gen((R′, G′_{C})). Also, for any c′ ∈ C′, v_{0} satisfies c′.

First we show that v_{0} ∈ R. By contraposition, suppose that v_{0} ∉ R. Then v_{0} does not satisfy c and hence ⟨a, v⟩ < b. By item 3 of Lemma 9, there must exists a point (p^{T}, e_{p})^{T} ∈ G_{P} that saturates c. Since e_{p} > 0 and s < 0, we obtain ⟨a, p⟩ > b. Thus, there exists 0 < λ < 1 such that, letting q =^{def} λv + (1 − λ)p, we have ⟨a, q⟩ = b, so that the point q_{0} =^{def} (q^{T}, 0)^{T} saturates c. Note that we have p ∈ P, so that p ∈ ℂ(P). Since P = [[R]] ⊆ [[R′]], we obtain p ∈ ℂ([[R′]]); thus, by

Lemma 5, we obtain p_{0} =^{def} (p^{T}, 0)^{T} ∈ R′. Therefore, being defined as a convex combination of two points of R′, we have q_{0} ∈ R′; since this point also saturates c, we obtain q_{0} ∈ R ∩ R′. Note that this implies sat gen(c, G) ∩ G_{C} ≠ ∅ so that, as by hypothesis c is ϵ-redundant in C, there exists a constraint c′ ∈ C_{>} \ {c} such that sat gen(c, G)\G_{P} ⊆ sat gen(c′, G). Let c′ = (⟨a′, x⟩+s′ ·ϵ ≥ b′), where a′ ≠ 0 and s′ < 0. Since c′ ∈ C′, the point (v^{T}, e′)^{T} ∈ R′ satisfies c′. Since s′ < 0 and e′ > 0, we obtain ⟨a′, v⟩ > b′. Similarly, point p_{0} ∈ R′ has to satisfy c′, so that ⟨a′, p⟩ ≥ b′. Since q ≠ p, the above conditions imply that ⟨a′, q⟩ > b′, so that q_{0} saturates c but not c′. However, q_{0} ∈ R is a positive combination of rays and points in G_{C} all saturating c. As sat gen(c, G) \ G_{P} ⊆ sat gen(c′, G), q_{0} is also a positive combination of rays and points in G_{C} that saturate c′. Thus q_{0} has to saturate c′, which is a contradiction. Therefore, we have v_{0} ∈ R, as claimed above.

Secondly we show that (v^{T}, e)^{T} ∈ R for some e > 0. By contraposition, suppose that for all e > 0 it holds ⟨a, v⟩ + s · e < b. Then, since v_{0} satisfies the constraint c, it must hold ⟨a, v⟩ = b, so that v_{0} actually saturates c. This implies v_{0} ∈ gen((R_{c}, P_{c})), where R_{c} = R ∩ sat gen(c, G) and P_{c} = G_{C} ∩ sat gen(c, G). Therefore, it cannot be the case that sat gen(c, G) ∩ G_{C} = ∅ and, since c is ϵ-redundant, there exists a constraint c′ ∈ C_{>} such that c′ ≠ c and

sat gen(c, G) \ G_{P} ⊆ sat gen(c′, G).

Note that R_{c} ∪ P_{c} ⊆ sat gen(c, G) \ G_{P}, so that point v_{0} also saturates c′. Since c′ ∈ C′_{>}, this implies that for all e > 0 the point (v^{T}, e)^{T} ∉ R′, therefore contradicting the initial assumption that v ∈ [[R′]]. As a consequence, there exists e > 0 such that (v^{T}, e)^{T} ∈ R and, by definition, v ∈ [[R]]. ⊓ ⊔

Lemma 11. Let R ⇛_{ϵ} P ≠ ∅, where (C, G) ≡ R is a DD pair in minimal form. If p is ϵ-redundant in G = (R, P), then gen(G′) ⇛_{ϵ} P, where G′ = (R, P \ {p}).

Proof. By Definition 7, we have p ∈ G_{U}, so that there exists e > 0 such that p = (v^{T}, e)^{T} ∈ P and p_{0} = (v^{T}, 0)^{T} ∉ P. Let R′ = gen(G′). Note that, since the function ‘gen’ is monotonic on both components of its argument, we have R′ ⊆ R. Moreover, for each q_{0} =^{def} (w^{T}, 0)^{T}, q_{0} ∈ R if and only if q_{0} ∈ R′. To see this, it is sufficient to observe that, since G_{C} = G′_{C} (because p ∉ G_{C}), q_{0} ∈ R if and only if q_{0} ∈ gen((R, G_{C})) if and only if q_{0} ∈ R′.

In order to show that R′ ⇛_{ϵ} P, we first prove that R′ is an ϵ-representation. Consider condition (1) of Definition 5. As R′ ⊆ R, R′ satisfies condition (1) by taking the same value δ used for R.

Consider now condition (2) of Definition 5. Let q = (w^{T}, e_{w})^{T} ∈ R′. Since R′ ⊆ R, we have q ∈ R; since R is an ϵ-representation, q_{0} =^{def} (w^{T}, 0)^{T} ∈ R. Thus, by the observation made above, q_{0} ∈ R′, as required.

Thus, R′ is an ϵ-representation. To show that it is indeed an ϵ-representation for P, we have to prove that [[R]] = [[R′]]. The inclusion [[R′]] ⊆ [[R]] holds by monotonicity of function [[·]], since R′ ⊆ R.

To prove the other inclusion, [[R]] ⊆ [[R′]], suppose that w ∈ [[R]]. Then there exists e > 0 such that q =^{def} (w^{T}, e)^{T} ∈ R. By condition (2) of Definition 5, we obtain q_{0} =^{def} (w^{T}, 0)^{T} ∈ R. Thus q_{0} ∈ gen((R, G_{C})); since p ∉ G_{C}, we have G_{C} = G′_{C} so that q_{0} ∈ R′. As q ∈ R, by definition of ‘gen’ there exist 0 ≤ λ_{p} ≤ 1 and p_{1} ∈ gen(G′) such that q = λ_{p}p + (1 − λ_{p})p_{1}. If λ_{p} = 0, then q ∈ R′, so that w ∈ [[R′]] as required.

Suppose now that λ_{p} > 0; then sat con(q, C) ⊆ sat con(p, C). Since p is ϵredundant in G, by Definition 7, there exists p′ =^{def} (y^{T}, e′)^{T} ∈ P \ {p} such that sat con(p, C) ∩ C_{≥} ⊆ sat con(p′, C) (also note that p′ ∈ R′). Thus, we obtain

sat con(q, C) ∩ C_{≥} ⊆ sat con(p′, C).

By letting p′_{0} =^{def} (y^{T}, 0)^{T} and applying item 2 of Lemma 9 twice, we obtain

sat con(q_{0}, (C_{>} ∪ C_{≥} ∪ C_{ϵ}))
= sat con(q, C_{≥})
⊆ sat con(p′, C_{≥})
= sat con(p′_{0}, (C_{>} ∪ C_{≥} ∪ C_{ϵ}))
⊆ sat con(p′_{0}, C).

Now let c =^{def} (⟨a, x⟩ + s · ϵ ≥ b) be any constraint in (C_{>} ∪ C_{≥} ∪ C_{ϵ}) so that, as p′ ∈ R, ⟨a, y⟩ ≥ b. If c ∈ sat con(q_{0}, C), then c ∈ sat con(p′_{0}, C), so that all the points lying on the line passing through q_{0} and p′_{0} saturate c. On the other hand, if c ∉ sat con(q_{0}, C), then ⟨a, w⟩ > b. Let

μ_{c} =^{def} \begin{cases}\frac{⟨a,y⟩−⟨a,w⟩}{⟨a,y⟩−b} & if ⟨a, y⟩ > ⟨a, w⟩ and ⟨a, y⟩ > b; \\ 1 & otherwise; \end{cases}
w_{c} =^{def} (1 + μ_{c})w − μ_{c}y′.

Thus (w_{c}^{T}, 0)^{T} lies on the line passing through q_{0} and p′_{0} and satisfies c. Let

μ =^{def} min{ μ_{c} ∈ ℝ | c ∈ C \ sat con(q_{0}, C) };
w_{μ} =^{def} (1 + μ)w − μy′.

Then (w_{μ}^{T}, 0)^{T} satisfies all the constraints in (C_{>}∪C_{≥}∪C_{ϵ}). By item 1 of Lemma 9, {c^{∗}} = C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}) and sat gen(c^{∗}, G) = R ∪ G_{C}. Thus (w_{μ}^{T}, 0)^{T} satisfies all the constraints in C so that (w_{μ}^{T}, 0)^{T} ∈ R. Since G_{C} = G′_{C}, we also have

(w_{μ}^{T}, 0)^{T} ∈ R′. Letting λ =^{def} \frac{1}{1+μ} we have 0 < λ < 1 and w = λw_{μ} + (1 − λ)y′. Thus, as p′ ∈ R′, we have

(w^{T}, (1 − λ)e′)^{T} = λ(w_{μ}^{T}, 0)^{T} + (1 − λ)p′ ∈ R′.

As e′ > 0 and λ < 1, (1 − λ)e′ > 0 and hence w ∈ [[R′]] as required. ⊓ ⊔

Lemma 12. Let R ⇛_{ϵ} P ≠ ∅, where R = con(C) and C is in minimal form. If C contains no ϵ-redundant constraint then it is in smf.

Proof. To prove the thesis, we assume that C is not in smf and show that C must have an ϵ-redundant constraint. As C is not in smf, there is a constraint system C′ in weak minimal form such that (C′_{>} ∪C′_{≥}) ⊂ (C_{>} ∪C_{≥}) and R′ =^{def} con(C′) ⇛_{ϵ} P. Let c ∈ (C_{>} ∪ C_{≥}) \ C′. Then there exists a ≠ 0 ∈ ℝ^{n}, s ≤ 0, and b ∈ ℝ such that

c = (⟨a, x⟩ + s · ϵ ≥ b).

First we show that c ∈ C_{>}. By contraposition, suppose that c ∈ C_{≥}, so that s = 0. As C is in minimal form, there exists a point p =^{def} (v^{T}, e)^{T} ∈ con(C \ {c})

that does not satisfy c. Thus p_{0} =^{def} (v^{T}, 0)^{T} does not satisfy c. As R ⇛_{ϵ} P, by Lemma 5, we have v ∉ ℂ(P). By hypothesis, R′ ⇛_{ϵ} P so that, again by Lemma 5, we have p_{0} ∉ R′. By condition (2) of Definition 5, it follows that (v^{T}, e′)^{T} ∉ R′, for all e′ ≥ 0. However, for some e′ > 0, (v^{T}, e′)^{T} satisfies every constraint in C′_{ϵ} and by hypothesis, satisfies every constraint in C′_{>} ∪ C′_{≥}. As C′ is in weak minimal form, by item 1 in Lemma 9, C′ \ (C′_{>} ∪ C′_{≥} ∪ C′_{ϵ}) = {c^{∗}}, where c^{∗} = (⟨a^{∗}, x⟩ + s^{∗} · ϵ ≥ b^{∗}) and s^{∗} > 0. Therefore (v^{T}, e′)^{T} does not satisfy c^{∗} and there exists e^{∗} > e′ such that p^{∗} = (v^{T}, e^{∗})^{T} saturates c^{∗} and satisfies every constraint in C′ \ C′_{ϵ}. As R′ ≠ ∅ and C′ is in minimal form, there exists a point q_{0} = (w^{T}, e_{w})^{T} ∈ R′ that saturates c^{∗}. As s^{∗} > 0, we can apply Lemma 8 to obtain e_{w} = 0. Thus, every convex combination of p^{∗} and q_{0} will also saturate c^{∗} and satisfy all constraints in C′ \ C′_{ϵ}. Then, for some 0 < λ < 1, the convex combination

λp^{∗} + (1 − λ)q_{0} = (y^{T}, λe^{∗})^{T}

satisfies all the constraints in C′ and saturates c^{∗}. As λe^{∗} > 0 and s^{∗} > 0, q′_{0} =^{def} λp_{0} +(1−λ)q_{0} does not satisfy c^{∗}. Thus condition (2) of Definition 5 does not hold for R′ contradicting the hypothesis that R′ is an ϵ-representation.

We can therefore assume that c ∈ C_{>} and hence, s < 0. Suppose first that no points in gen((R, G_{C})) saturate c; this implies sat gen(c, G) ∩ G_{C} = ∅ and it follows from Definition 7 that c is ϵ-redundant in C. Otherwise, suppose that c is saturated by at least one point in gen((R, G_{C})).

We next show that, for each point

p_{0} =^{def} (v^{T}, 0)^{T} ∈ gen((R, G_{C})),

there exist c′ ∈ C′_{>} that is saturated by p_{0} but not satisfied by (v^{T}, e)^{T}, for any e > 0. Since s < 0, we have (v^{T}, e)^{T} ∉ R, for all e > 0. As R ⇛_{ϵ} P, by condition (3) of Definition 5, v ∉ P and, by Lemma 5, we have v ∈ ℂ(P). Since by hypothesis R′ ⇛_{ϵ} P, by applying again condition (3) of Definition 5 and Lemma 5, we obtain (v^{T}, e)^{T} ∉ R′, for all e > 0, and p_{0} ∈ R′. As a consequence, there must exist c′ = (⟨a′, x⟩+s′ ·ϵ ≥ b′) ∈ C′ such that c′ is saturated by p_{0} but not satisfied by (v^{T}, e)^{T}, for any e > 0. Thus we have s′ < 0, so that c′ ∈ C′_{>}.

Let Q =^{def} sat gen(c, G) \ G_{P} and G_{Q} =^{def} (R ∩ Q, P ∩ Q). Suppose that, for each constraint c_{i} ∈ C′_{>} = {c_{1}, …, c_{k}}, there exists a point q_{i} ∈ gen(G_{Q}) that does not saturate c_{i}. Then the convex combination

\frac{1}{k} ∑_{i=1}^{k} q_{i} ∈ gen(G_{Q})

saturates c, but does not saturate any constraint in C′_{>}, contradicting the previous paragraph. As a consequence, there exists a constraint c′ ∈ C′_{>} that is saturated by all the points in gen(G_{Q}). As there exists a point in R that saturates c, (P ∩ Q) ≠ ∅. Thus, as all points in gen(G_{Q}) are obtained by summing a positive combination of the rays in R ∩ Q with a convex combination of the points in P ∩ Q, we obtain Q ⊆ sat gen(c′, G). It then follows from Definition 7 that c is ϵ-redundant in C. ⊓ ⊔

Lemma 13. Let R ⇛_{ϵ} P ≠ ∅, where R = gen(G) and G is in minimal form. If G contains no ϵ-redundant generator then it is in smf.

Proof. To prove the thesis, we assume that G is not in smf and show that G must have an ϵ-redundant generator. As G = (R, P) is not in smf, by Definition 6, there exists a generator system G′ = (R′, P′) ≠ G such that R′ ⊆ R, P′ ⊆ P and gen(G′) ⇛_{ϵ} P.

We first show that P′ ⊂ P. By contraposition, suppose that P′ = P, so that R′ ⊂ R. Let r ∈ R \ R′ and define R′′ = R \ {r}, so that R′ ⊆ R′′ ⊂ R. By monotonicity of function ‘gen’, we obtain

gen(G′) ⊆ gen((R′′, P)) ⊂ gen(G),

where the strict inclusion holds by Definition 2, since by hypothesis G is in (weak) minimal form. Note that, since gen(G′) ⇛_{ϵ} P and gen(G) ⇛_{ϵ} P, by exploiting the monotonicity of [[·]] we also obtain gen((R′′, P)) =^{def} R′′ ⇛_{ϵ} P. We will now show that [[R′′]] ⊂ P, therefore deriving the required contradiction.

Since P ≠ ∅, there exists (w^{T}, e_{w})^{T} ∈ R such that e_{w} > 0. Then, by condition 2 of Definition 5, (w^{T}, 0)^{T} ∈ R. By Lemma 3, we can assume that r = (y^{T}, 0)^{T}. As r ∉ R′′ and G is in minimal form, there exists μ ≥ 0 such that, if w_{μ} =^{def} w + μy, then (w_{μ}, 0) ∉ R′′. Since R′′ ⇛_{ϵ} P, by Lemma 5, w_{μ} ∉ ℂ(P). Thus, again by Lemma 5, (w_{μ}, 0) ∉ R, contradicting the assumption that r ∈ R.

Thus, we have P′ ⊂ P. Let p = (v^{T}, e)^{T} ∈ P \ P′ and define P′′ = P \ {p}, so that P′ ⊆ P′′ ⊂ P. By monotonicity of function ‘gen’ and because G is in (weak) minimal form, we obtain

gen(G′) ⊆ gen((R, P′′)) ⊂ gen(G),

and p ∉ R′′. As already observed, since gen(G′) ⇛_{ϵ} P and gen(G) ⇛_{ϵ} P, by monotonicity of [[·]] we also obtain gen((R, P′′)) =^{def} R′′ ⇛_{ϵ} P. We show that p is ϵ-redundant in G.

We start by showing that p = (v^{T}, e)^{T} ∉ G_{C}, i.e., that e > 0. Suppose, by contraposition that e = 0. Then, by Lemma 5, v ∈ ℂ(P). Thus, as R′′ ⇛_{ϵ} P, again by Lemma 5, p = (v^{T}, 0)^{T} ∈ R′′ which is a contradiction. Therefore p ∈ G_{P}.

Letting C be a constraint system in weak minimal form such that con(C) = R, we next show that there must exist p′ ∈ G_{P} \ {p} such that

sat con(p, C) ∩ C_{≥} ⊆ sat con(p′, C).  (6)

By condition 3 of Definition 5, since p ∈ R and e > 0, we have v ∈ P; and, since also [[R′′]] = P, there must exists e_{q} > 0 such that q =^{def} (v^{T}, e_{q})^{T} ∈ R′′. Hence, q ∈ gen((R, P′′)) and, since e_{q} > 0, there must exist a point encoding p′ ∈ G_{P} \ {p} that plays an active role (i.e., has a positive coefficient) in the combination generating q. Consider a non-strict inequality encoding c′ ∈ sat con(p, C) ∩ C_{≥}. Since c′ ∈ C_{≥}, we have c′ = (⟨a, x⟩ + 0 · ϵ ≥ b) so that c′ is also saturated by q. This in turn implies that c′ is saturated by p′. Since the choice of c′ ∈ C_{≥} was arbitrary, we obtain the condition (6).

To show that p is ϵ-redundant, we have to show that p ∈ G_{U}. By contraposition, suppose that p_{0} =^{def} (v^{T}, 0)^{T} ∈ P. Suppose p′ = (y^{T}, e′)^{T} and p′_{0} =^{def} (y^{T}, 0)^{T}; then p′_{0} ∈ R by condition (2) of Definition 5. By item 2 of Lemma 9, we have

sat con(p_{0}, C) ∩ C_{≥} = sat con(p, C) ∩ C_{≥},
sat con(p′_{0}, C) ∩ C_{≥} = sat con(p′, C) ∩ C_{≥},

so that, by the condition (6) proved above, we obtain

sat con(p_{0}, C) ∩ C_{≥} ⊆ sat con(p′_{0}, C) ∩ C_{≥}.  (7)

Suppose first that e < e′. Let p′_{e} =^{def} (y^{T}, e)^{T}; then, letting λ = \frac{e}{e′} (note that

0 ≤ λ ≤ 1), the point q_{e} = (w^{T}, e)^{T} =^{def} λp′ + (1 − λ)p_{0} is a convex combination of p′ and p_{0} and hence in R. Let also r =^{def} p − q_{e}; then r cannot be a ray of R, since otherwise we would have p ∈ gen(R, {p′, p_{0}}), contradicting the

hypothesis that G is in minimal form. For each μ ∈ ℝ_{+}, let p_{μ} =^{def} p_{0} + μr. Since r is not a ray of R, there must exist μ′ ∈ ℝ_{+} such that, for all μ > μ′, we have p_{μ} ∉ R. If μ′ > 0, then p_{μ′} ≠ p_{0}; thus, p_{0} can be expressed as a convex combination of p_{μ′} and p′_{0}, contradicting the hypothesis that G is in minimal form. Therefore, it must hold μ′ = 0 (i.e., p_{μ′} = p_{0}). As a consequence, there must exist a constraint c ∈ C such that p_{0} saturates c but p′_{0} does not saturate c. As C is in minimal form, by item 2 of Lemma 9, C \ C_{>} ∪ C_{≥} ∪ C_{ϵ} = {c^{∗}} and sat gen(c^{∗}, G) = R ∪ G_{C} so that p_{0} and p′_{0} saturate c^{∗}. Thus, by item 1 of Lemma 9, since p′_{0} does not saturate c we obtain c ∈ C_{>} ∪ C_{≥} ∪ C_{ϵ}; from this and the fact that p_{0} saturates c, by item 2 of Lemma 9, we obtain c ∈ C_{≥}; However, this contradicts the condition (7) established above, so that we cannot have e < e′.

Secondly suppose that e ≥ e′. Let p_{e′} =^{def} (v^{T}, e′)^{T}; then, p_{e′} ∈ R can be obtained as a convex combination of p and p_{0}. Let also r′ =^{def} p′−p_{e′}; then r cannot be a ray of R, since otherwise we would have p′ ∈ gen(R, {p, p_{0}}), contradicting

the hypothesis that G is in minimal form. By letting p_{μ} =^{def} p_{0} − μr′, we obtain p_{μ} ∉ R for all μ > 0. Thus, we are in the same situation identified before and a contradiction can be derived by the same argument. As a consequence, p_{0} ∈ P cannot hold so that p ∈ G_{U}, completing the proof. ⊓ ⊔

Proof (Proof of Proposition 4). Items 1, 2, 3, and 4 have been proved as Lemmas 10, 11, 12, and 13 respectively. ⊓ ⊔