Under consideration for publication in Formal Aspects of Computing

Not Necessarily Closed Convex Polyhedra and the Double Description Method^{1}

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

1 Department of Mathematics, University of Parma, Italy, ^{2} School of Computing, University of Leeds, UK

Abstract. Since the seminal work of Cousot and Halbwachs, the domain of convex polyhedra has been employed in several systems for the analysis and verification of hardware and software components. Although most implementations of the polyhedral operations assume that the polyhedra are topologically closed (i.e., all the constraints defining them are non-strict), several analyzers and verifiers need to compute on a domain of convex polyhedra that are not necessarily closed (NNC). The usual approach to implementing NNC polyhedra is to embed them into closed polyhedra in a higher dimensional vector space and reuse the tools and techniques already available for closed polyhedra. In this work we highlight and discuss the issues underlying such an embedding for those implementations that are based on the double description method, where a polyhedron may be described by a system of linear constraints or by a system of generating rays and points. Two major achievements are the definition of a theoretically clean, high-level user interface and the specification of an efficient procedure for removing redundancies from the descriptions of NNC polyhedra.

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.

The seminal work of Cousot and Halbwachs [CH78] introduced the use of convex polyhedra as a domain of descriptions to solve, by abstract interpretation [CC77], 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 [BJT99, Hal93] and of linear hybrid automata (an extension of finite-state machines that models time requirements) [HPR94, HHWT97], for the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [MBB^{+}99], for inferring argument size relationships in logic languages [BK97], and for the automatic parallelization of imperative programs [Pug92]. 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., [CS01, DRS01]). 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.

1 This work has been partly supported by MURST projects “Aggregate- and number-reasoning for computing: from decision algorithms to constraint programming with multisets, sets, and maps” and “Constraint Based Verification of Reactive Systems.”

Correspondence and offprint requests to: R. Bagnara, P. M. Hill, and E. Zaffanella

Traditionally, convex polyhedra are assumed to be topologically closed. When adopting the double description (DD) method [MRTT53], a closed convex polyhedron can be specified in two ways, using a constraint system or a generator system: the constraint system contains a finite set of linear non-strict inequality constraints; the generator system contains two finite sets of vectors, collectively called generators, which are rays and points of the polyhedron.

However, some applications of static analysis and verification, including recent proposals such as [CS01], need to compute on the domain of not necessarily closed (NNC) convex polyhedra. By definition, any NNC polyhedron can be represented by a so-called mixed constraint system, that is, a constraint system where a further finite set of linear strict inequality constraints is allowed to occur. No similar generalization of the concept of generator system is available, so that the DD method cannot be directly applied to the domain of NNC polyhedra. In contrast, the usual approach for implementing NNC polyhedra is to embed them into closed polyhedra in a vector space with one extra dimension. While this idea, originally proposed in [HPR94] and also described in [HPR97], proved to be quite effective, its direct application in the development of software libraries for the manipulation of convex polyhedra results in a low-level user interface, where most of the geometric intuition of the DD method gets lost under the “implementation details.” This has a direct, negative impact on the usability of the resulting software (on this subject, see the discussion in Section 7, which also includes quotations taken from [HKP95, Section 4.5, pp. 10–11] and [Jea02, Section 1.1.4, page 10]).

In this paper, we propose a much cleaner approach, where the concept of generator of an NNC polyhedron is extended to also account for the closure points of the polyhedron. In particular, we show that any NNC polyhedron can be defined directly by means of an extended generator system, namely, a triple of finite sets containing rays, points and closure points of the polyhedron. By combining the mixed constraint systems with these extended generator systems for describing NNC polyhedra we can obtain a two-fold improvement over the proposal in [HPR94, HPR97]: easier generalizations and a natural, implementation-independent interface.

Easier generalizations: Several operators, whose definition is in terms of the rays and points of the standard generator systems for closed polyhedra, need to be generalized to NNC polyhedra. Examples are given by the time-elapse operator of [HPR94, HPR97], the extrapolation operator ‘∝’ defined in [HH95], the generator-based extrapolation operators sketched in [BJT99], and the new widening operator proposed in [BHRZ03b]. The notion of extended generator system proves to be very effective in the definition and justification of these generalizations. As a remarkable example, in Section 4.2 it will be shown how the usual implementation of the inclusion test for closed polyhedra can be easily adapted to the case of NNC polyhedra. The elegance of this generalization is better appreciated by comparing it with the specification of the inclusion test for the low-level implementation of [HPR94], which appears to be much more tricky and obscure. The reason is that in [HPR94] the reader has no high-level interpretation of the generators occurring in the low-level encoding.

A natural, implementation-independent interface: The combination of mixed constraint systems and extended generator systems offers another improvement over the proposal in [HPR94, HPR97]: a high-level user interface that is completely separate from the implementation. On the one hand, an NNC polyhedron can be presented to the client application directly in terms of its defining strict and non-strict constraints or its generating rays, points and closure points; there is no need for the client to be aware of the use of an additional space dimension in the implementation and all issues related to its correct handling, such as the side constraints on this space dimension. On the other hand, by relying on the high-level specification only, the client application will be unaffected by the wider adoption of lazy and incremental computation techniques in the procedures implementing the operators on convex polyhedra. Moreover, if all the functionalities and invariants of the interface are maintained, it is then possible to change the low-level data structures without affecting the application.

In this paper we will also exploit the latter possibility by introducing two alternative classes of closed polyhedra for implementing the NNC polyhedra, both instances of the same basic class. The basis of this representation is a simple generalization of the class of polyhedra used in [HPR94, HPR97]. The new class continues to employ an additional dimension to encode whether or not each affine half-space defining the NNC polyhedron is closed and relies on the same semantic function for extracting the NNC polyhedron it embeds. We describe two alternative specializations of this class for representing the NNC polyhedra. One of these, shown to be biased for the use of the constraint representation, corresponds to the embedding defined in [HPR94] while the other, which is biased for the use of the generator representation, is new to this paper.

The Parma Polyhedra Library^{2}, a modern C^{++} library for the manipulation of convex polyhedra, has been extended so as to implement both approaches. One interesting and potentially useful consequence of having the option of these alternative encodings is that an improved implementation may choose to dynamically switch between them, depending on the particular descriptions needed to perform a given operation; for instance, the constraint-biased encodings may be used when computing intersections of polyhedra, whereas the generator-biased encodings would be preferred when computing convex polyhedral hulls.

Minimization procedures for the descriptions of NNC polyhedra: Another major contribution of this paper will be the identification of an important issue related to the above mentioned embedding of an NNC polyhedron into a closed polyhedron. It will be shown that the usual procedures for minimizing the constraint and generator descriptions of the topologically closed representation of an NNC polyhedron are not enough to obtain a non-redundant description of the NNC polyhedron itself. We will propose a solution for this problem, which affects both the constraint-biased and the generator-biased representations of NNC polyhedra, by providing procedures that are able to efficiently identify the semantically redundant constraints and generators, therefore allowing for the computation of truly minimal descriptions. A preliminary experimental evaluation will show how the use of the new minimization procedures may have a great impact on the efficiency of some of the most important operators on the domain of NNC polyhedra.

The paper is structured as follows: Section 2 recalls the required concepts and notations; Section 3 briefly presents the theoretical framework underlying the double description method for the representation and manipulation of closed convex polyhedra; Section 4 provides a generalization of this framework to also allow for the manipulation of convex polyhedra that are not necessarily closed; Section 5 presents a general class and two special subclasses of the set of closed polyhedra that are appropriate for the representation of NNC polyhedra; Section 6 identifies a problem related to the minimization of these NNC polyhedra representations and proposes a solution based on the notion of ϵ-minimal forms; Section 7 presents an implementation of the ideas contained in this paper, providing an informal comparison with other libraries offering some support for NNC polyhedra and discussing a preliminary experimental evaluation we have conducted. Section 8 concludes. The Appendix contains proofs of the formal results stated in the main part of the paper.

This paper is a combined, extended and improved version of [BHZ03] and [BRZH02].

2. Preliminaries

The set of non-negative reals is denoted by ℝ_{+}. In the paper, all topological arguments refer to the Euclidean topological space ℝ^{n}, for any positive integer n. If S ⊆ ℝ^{n}, then the topological closure of S is defined as ℂ(S) =^{def} ⋂{ C ⊆ ℝ^{n} | S ⊆ C and C is closed }.

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} having all components equal to zero. A vector v ∈ ℝ^{n} can also be interpreted as a matrix in ℝ^{n×1} and manipulated accordingly with 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.

Let S ⊆ ℝ^{n} be a set of vectors. The orthogonal of S is S^{⊥} =^{def} { w ∈ ℝ^{n} | ∀v ∈ S : ⟨v, w⟩ = 0 }. If S has finite cardinality m, then matrix(S) ⊆ ℝ^{n×m} denotes the set of all matrices having S as the set of their columns. In the following, we will abuse notation by letting S also denote a fixed arbitrary element of matrix(S). The context makes it clear when the symbol denotes a set or a matrix.

2 Publicly available at URI http://www.cs./unipr.it/ppl/. The library is currently based on the constraint-biased representation of NNC polyhedra; an implementation of the generator-biased representation is available in the alt nnc branch of the PPL’s CVS repository.

3. 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 topologically closed affine half-space of ℝ^{n}. The linear equality constraint ⟨a, x⟩ = b defines an affine hyperplane. A topologically closed convex polyhedron is usually described as a finite system of linear equality and non-strict inequality constraints. Theoretically speaking, it is simpler to express each equality constraint as the intersection of the two half-spaces β^{+} = (⟨a, x⟩ ≥ b) and β^{−} = (⟨−a, x⟩ ≥ −b); in such a case, we say that β^{+} and β^{−} are singular constraints for polyhedron P and write {β^{+}, β^{−}} ⊆ eq(P). We do not distinguish between syntactically different constraints defining the same affine half-space so that, e.g., x ≥ 2 and 2x ≥ 4 are considered to be the same constraint.

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

We write con(C) to denote the polyhedron P ⊆ ℝ^{n} described by the finite constraint system C. Formally, we define

con(C) =^{def} { p ∈ ℝ^{n} | ∀β = (⟨a, x⟩ ≥ b) ∈ C : ⟨a, p⟩ ≥ b }.

The function ‘con’ enjoys an anti-monotonicity property, meaning that C_{1} ⊆ C_{2} implies con(C_{1}) ⊇ con(C_{2}).

Alternatively, the definition of a topologically closed convex polyhedron can be based on some of its geometric features. A vector r ∈ ℝ^{n} such that r ≠ 0 is a ray (or direction of infinity) of a non-empty polyhedron P ⊆ ℝ^{n} if, for every point p ∈ P and every non-negative scalar ρ ∈ ℝ_{+}, it holds p + ρr ∈ P; the set of all the rays of a polyhedron P is denoted by rays(P). A vector l ∈ ℝ^{n} is a line of P if both l and −l are rays of P; in such a case, we say that l and −l are singular rays for polyhedron P and write {l, −l} ⊆ lines(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 singular rays. Moreover, when vectors are used to denote rays, no distinction will be made between different vectors having the same direction so that, e.g., r_{1} = (1, 3)^{T} and r_{2} = (2, 6)^{T} are considered to be the same ray in ℝ^{2}. The following theorem is a simple consequence of well-known theorems by Minkowski and Weyl [SW70].

Theorem 3.2. The set P ⊆ ℝ^{n} is a closed polyhedron if and only if there exist finite sets R, P ⊆ ℝ^{n} of cardinality r and p, respectively, such that 0 ∉ R and

P = gen((R, P)) =^{def} { Rρ + P π ∈ ℝ^{n} | ρ ∈ ℝr_{+}, π ∈ ℝp_{+}, ∑_{i=1}^{p} π_{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. Thus, each point of the generated polyhedron is obtained by adding a non-negative combination of the rays in R and a convex combination of the points in P. 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. We define a partial order relation ‘⊑’ on generator systems, which is the component-wise extension of set inclusion. Namely, for any generator systems G_{1} = (R_{1}, P_{1}) and G_{2} = (R_{2}, P_{2}), we have G_{1} ⊑ G_{2} if and only if R_{1} ⊆ R_{2} and P_{1} ⊆ P_{2}; if, in addition, G_{1} ≠ G_{2}, we write G_{1} ⊏ G_{2}. The function ‘gen’ enjoys a monotonicity property, as G_{1} ⊑ G_{2} implies gen(G_{1}) ⊆ gen(G_{2}).

The vector v ∈ P is an extreme point (or vertex) of the polyhedron P if it cannot be expressed as a convex combination of some other points of P. Similarly, r ∈ rays(P) is an extreme ray of P if it cannot be expressed as a non-negative combination of some other rays of P. It is worth stressing that, in general, the vectors in R and P are not the extreme rays and the vertices of the polyhedron: 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 method due to Motzkin et al. [MRTT53], which exploits the duality principle to compute each representation starting from the other one, possibly minimizing both descriptions. Clever implementations of this conversion procedure, such as those based on the extension by Le Verge [Le 92] of the Chernikova’s algorithms [Che64, Che65, Che68], are the starting point for the development of software libraries based on the DD method. While being characterized by a worst case computational cost which is exponential in the size of the input, these algorithms turn out to be practically useful for the purposes of many applications in the context of static analysis.

Definition 3.3. (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 is in minimal form if there does not exist G′ ⊏ G such that gen(G′) = P;

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

A polyhedron may be described by different constraint systems (resp., generator systems) in minimal form. As a matter of fact, since we are expressing the equality constraints (resp., lines) by using non-strict inequality constraints (resp., rays), these equivalent descriptions in minimal form may also have a different number of constraints (resp., rays).

Stronger characterizations for the descriptions of a polyhedron may be obtained by specifying further properties, besides the above minimality requirement. For any constraint β = (⟨a, x⟩ ≥ b), the slope of β is

defined as slope(β) = a; for a constraint system C, let slope(C) =^{def} { slope(β) | β ∈ C }.

Definition 3.4. (Orthogonal forms.) Let (C, G) ≡ P ≠ ∅ be a DD pair for the non-empty polyhedron P. We say that

• C is in orthogonal form if I ⊆ E^{⊥}, where I =^{def} slope(C \ eq(P)) and E =^{def} slope(C ∩ eq(P));

• G = (R, P) is in orthogonal form if (R \ L) ∪ P ⊆ L^{⊥}, where L =^{def} R ∩ lines(P).

For a topologically closed polyhedron, all descriptions in minimal form that are also in orthogonal form have the same set of non-singular inequality constraints, the same set of non-singular rays and the same set of points, whereas the sets of singular constraints and singular rays may still differ. Orthogonal forms can be computed by applying a simple variant of the well-known Gram-Shmidt orthogonalization procedure to a description such that, if the original description was in minimal form, then the derived orthogonal description is still in minimal form.

In the following, minimal forms and orthogonality are not assumed unless explicitly stated.

3.1. Operations on Closed Polyhedra

In this section we show that the ability to switch from a constraint description to a generator description, or vice versa, can be usefully exploited to provide simple implementations for the basic operations on the domain of closed polyhedra.

The set of all closed polyhedra on the vector space ℝ^{n}, denoted ℂℙ_{n}, can be partially ordered by setinclusion to form a lattice having the empty set and ℝ^{n} as the bottom and top element, respectively. The binary meet operation, returning the greatest closed polyhedron smaller than or equal to the two arguments, is easily seen to correspond to set-intersection. The binary join operation, returning the least closed polyhedron greater than or equal to the two arguments, is denoted ‘⊎’ and called convex polyhedral hull (poly-hull, for short); note that, in general, the poly-hull of two polyhedra is different from their convex hull [SW70].

When adopting the double description method, set-intersection is easily implemented by taking the union of the constraint systems representing the two arguments, whereas the poly-hull is implemented by taking the component-wise union of the generator systems representing the two arguments; as said above, the test for emptiness can be implemented by checking whether the generator system contains no points at all.

Probably, the elegance of this formalization is most appreciated when considering the implementation of the lattice partial order relation, i.e., subset inclusion. We say that point p ∈ ℝ^{n} satisfies the constraint β = (⟨a, x⟩ ≥ b) if p belongs to the closed affine half-space defined by β, i.e., if ⟨a, p⟩ ≥ b holds. Similarly, a ray r ∈ ℝ^{n} satisfies β if the corresponding direction of infinity is included in the half-space defined by β, i.e., if ⟨a, r⟩ ≥ 0 holds. Now, if P_{1} = gen(G_{1}) and P_{2} = con(C_{2}), the inclusion P_{1} ⊆ P_{2} holds if and only if each generator in G_{1} satisfies all the constraints in C_{2}.

Static analysis and verification applications adopting the domain of convex polyhedra need to provide correct approximations to other concrete semantics operators, besides the lattice theory operators mentioned above. For instance, in the context of imperative languages, one of the most frequent operations is the assignment of an expression to a variable. Suppose that the set of all possible current values of the program variables is approximated by a convex polyhedron; then, if the considered assignment expression is a linear function of the variables’ values, its effect will be correctly modeled by computing the image of the polyhedron under the affine transformation corresponding to the considered assignment expression. When adopting the double description method, the result of such an affine image operator will be the polyhedron described by the generator system obtained by applying the affine transformation to the generators of the argument polyhedron. A similar approach, but using the constraint description of the polyhedron, allows for the computation of the affine pre-image of a polyhedron, which is of interest when considering a backward semantic construction, where the initial values of program variables are approximated starting from their final values.

4. 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 convex polyhedra that are not necessarily closed (NNC polyhedra, for short).

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

Formally, we overload function ‘con’ so that, for any mixed constraint system C, that is, a constraint system possibly containing both strict and non-strict inequality constraints, we have

con(C) =^{def} { p ∈ ℝ^{n} | ∀β = (⟨a, x⟩ ▷◁ b) ∈ C : ⟨a, p⟩ ▷◁ b },

where ▷◁ ∈ {≥, >}. Note that ‘con’ still satisfies the anti-monotonicity property.

4.1. The Generators of NNC Polyhedra

One of the fundamental features of the double description method, and the very reason for its name, is the possibility of representing a closed polyhedron using a system of constraints or a system of generators. As we have shown when discussing the implementation of operations on closed polyhedra, there are contexts where each of these equivalent descriptions is the most appropriate.

Any NNC polyhedron can be easily described by using mixed constraint systems, but a similar generalization of the concept of generator system seems to be missing. Since by using lines, rays and points we can only represent closed polyhedra, the key step for the parametric description of NNC polyhedra is the introduction of a new kind of generator.

Definition 4.2. (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 the following property.

Proposition 4.3. 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 every σ ∈ ℝ such that 0 < σ < 1.

In the above proposition, it should be observed that not all of the possible convex combinations of p and c are considered. In particular, by neglecting the case when σ = 0 we do not force p to belong to P. The case when σ = 1 would be harmless, but it is left out for the sake of symmetry.

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

Theorem 4.4. The set P ⊆ ℝ^{n} is an NNC polyhedron if and only if there exist finite sets R, P, C ⊆ ℝ^{n} of cardinality r, p and c, respectively, such that 0 ∉ R and

P = gen((R, P, C)) =^{def} \{ Rρ + P π + Cγ ∈ ℝ^{n} | \begin{matrix}ρ ∈ ℝr_{+}, π ∈ ℝp_{+}, π ≠ 0, γ ∈ ℝc_{+}, \\ ∑_{i=1}^{p} π_{i} + ∑_{i=1}^{c} γ_{i} = 1 \end{matrix} \}.

O  x y  A  B C D  E  P_{1}  F  G H I  J P_{2}  K  ^{r_{1}}  ^{r_{2}} L  P_{3}

Fig. 1. Using closure points to define NNC polyhedra on ℝ^{2}.

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 4.3 that the vectors of C are closure points of P. Since both rays and closure points need a supporting point, we have P = ∅ if and only if P = ∅. The partial order relation ‘⊑’ on generator systems is easily extended to also take into account the closure points component, so that the overloading of the function ‘gen’ still satisfies the monotonicity property. It is also worth stressing that, once we consider both mixed constraint systems and extended generator systems, then the notions of DD pair and minimal forms, exactly as stated in Definition 3.3, also apply to the representations of NNC polyhedra. The same observation holds for the notion of orthogonal form stated in Definition 3.4; however, in the case of an NNC polyhedron, the orthogonality requirement is less useful, as it will be soon clear that minimal orthogonal forms are insufficient to uniquely identify the non-singular components of a description.

In Figure 1, we provide a few examples of the use of extended generator systems for the description of NNC polyhedra in ℝ^{2}: (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 all the four closure points have to be included in any generator system for P_{1}, whereas E could have been replaced by any other point of P_{1}; moreover, since P_{1} has no rays, all generator systems for P_{1} in minimal form are also in orthogonal form, so that, as said above, minimality with orthogonality are not enough to uniquely identify the points in a generator system for P_{1}. The NNC polyhedron P_{2} is another rectangle that is neither closed nor open: since F is a point, the open segments ]F, G[ and ]F, I[ are included in P_{2}; similarly, the open segment ]G, H[ is included in P_{2} because J is a point of the generator system (note that J is needed, since both G and H 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 [H, I] is disjoint from P_{2}, because neither H nor I are points of P_{2}. Finally, the NNC polyhedron P_{3} can be regarded as the translation by K of the open positive orthant. Thus the generator system includes the closure point K, the rays r_{1} and r_{2} and the point L; again, the latter could have been replaced by any other point of P_{3}.

4.2. Operations on NNC Polyhedra

We denote by ℙ_{n} the set of all NNC polyhedra on the vector space ℝ^{n}. As was the case for the domain ℂℙ_{n}, when partially ordered by set-inclusion, ℙ_{n} is a lattice having the empty set and ℝ^{n} as the bottom and top element, respectively; the set-intersection and poly-hull operators are the binary meet and join of the lattice, respectively. Obviously, we have ℂℙ_{n} ⊆ ℙ_{n} and, in particular, ℂℙ_{n} is a sublattice of ℙ_{n}.

When representing NNC polyhedra using the double description method as generalized above, all the lattice operations on ℙ_{n} can be implemented by following the same approach adopted for the domain ℂℙ_{n}. Thus, a mixed constraint system representing the set-intersection of two NNC polyhedra is obtained by taking the union of the mixed constraint systems representing the two arguments; an extended generator system representing the poly-hull of two NNC polyhedra is obtained by taking the component-wise union of the extended generator systems representing the two arguments; the emptiness test is implemented, as before, by checking whether the extended generator system has no points at all (disregarding the closure points).

Even the implementation of the inclusion test P_{1} ⊆ P_{2} is still based on checking that each generator in an extended generator system for P_{1} satisfies all the constraints in a mixed constraint system for P_{2}. Clearly,

Table 1. Testing if the constraint ⟨a, x⟩ ▷◁ b is satisfied by the generator g.

Generator type

Constraint type  ray  point  closure point
non-strict inequality  ⟨a, g⟩ ≥ 0  ⟨a, g⟩ ≥ b  ⟨a, g⟩ ≥ b
strict inequality  ⟨a, g⟩ ≥ 0  ⟨a, g⟩ > b  ⟨a, g⟩ ≥ b

a suitable extension is needed for these satisfaction tests, covering the new combinations provided by the additional constraint and generator types, i.e., strict inequalities and closure points. All the possible cases are shown in Table 1. It can be seen that such an extension is fairly intuitive. As long as we consider nonstrict inequalities, closure points behave the same as points. In contrast, when considering strict inequality constraints, only the points of the polyhedron are required to respect the strict inequality relation; both closure points and rays are just required to satisfy the corresponding non-strict inequality. This is because closure points are limit points of the polyhedron, but are not required to actually belong to it.

Similar generalizations are easily obtained for all the usual semantic operators. For instance, an extended generator system representing the affine image of an NNC polyhedron can be computed by applying the affine transformation to all the elements of the extended generator system representing the argument.

5. Implementing NNC Polyhedra Using Closed Polyhedra

In the previous section, we have shown how the representation of closed polyhedra in terms of constraint and generator systems can be suitably generalized to also allow for the case of NNC polyhedra. Moreover, we have shown that the availability of these representations naturally leads to corresponding generalizations of the operations defined on the domain of polyhedra. However, in our path from the original problem toward the solution, an intermediate, very important step is still missing.

The most critical operation in the DD framework is the so-called conversion algorithm. This comes into play whenever one of the two possible representations is needed, but only the other one is available. Such a change of representation is typically needed as a pre-processing step in most of the discussed operations on both closed and NNC polyhedra, to ensure that the most appropriate representation is available for each of the arguments of the operation. Thus, a direct implementation of the DD method for the domain of NNC polyhedra requires the generalization of this conversion algorithm. Even though this would be a really interesting line of research, the few existing software libraries (based on the DD method) providing support for the domain of NNC polyhedra all adopt an alternative, indirect approach that, to the best of our knowledge, was originally proposed in [HPR94] and also described in [HPR97].^{3} In this section we present a generalization and formal justification of this approach. We will also show the exact correspondence between this “low-level implementation” and the “high-level interface” proposed in the previous section.

The basic idea is to encode each NNC polyhedron of ℙ_{n} into a closed polyhedron of ℂℙ_{n+1}. In the following, we denote by ϵ the variable corresponding to the (n + 1)-st Cartesian axis of ℝ^{n+1}. The interpretation function [[·]]: ℂℙ_{n+1} → ℙ_{n} maps any closed polyhedron in ℂℙ_{n+1} to an NNC polyhedron in ℙ_{n}; in particular, points in the closed polyhedron with a positive ϵ coordinate correspond to points in the NNC polyhedron.

Definition 5.1. (Represented NNC polyhedron.) A polyhedron R ∈ ℂℙ_{n+1} is said to represent the NNC polyhedron P ∈ ℙ_{n} if and only if

P = [[R]] =^{def} { v ∈ ℝ^{n} | ∃e ∈ ℝ . (e > 0 ∧ (v^{T}, e)^{T} ∈ R) }. (1)

Note that any closed polyhedron that is included in the half-space defined by the constraint ϵ ≤ 0 actually represents the empty NNC polyhedron.

Not all the polyhedra in ℂℙ_{n+1} are good candidates for representing an NNC polyhedron in ℙ_{n}. The rationale driving the choice of an appropriate subclass of ℂℙ_{n+1} is that most of the operators defined on the domain of closed polyhedra could be used, with no more than minor modifications, to implement the corresponding operators on the represented domain ℙ_{n} of NNC polyhedra. For instance, one would like to

3 According to [HPR97], the idea has to be credited to Pascal Raymond.

O  x ϵ  A  B R_{1}  C  D E R_{2}  F G  H I J R_{3}  K  L R_{4}  M N P P′  R_{5}

Fig. 2. Only R_{2}, R_{3} and R_{4} are ϵ-polyhedra.

implement the intersection and the poly-hull of two NNC polyhedra by computing the intersection and the poly-hull of their closed representations, respectively. Under such a requirement, we will define two alternative representations for NNC polyhedra. The two classes of closed polyhedra used for these representations are instances of a more general class of closed polyhedra.

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

∃δ ∈ ℝ . (δ > 0 ∧ R ⊆ con({ϵ ≤ δ}));  (2)
∀v ∈ ℝ^{n}, e ∈ ℝ : (v^{T}, e)^{T} ∈ R ⟹ (v^{T}, 0)^{T} ∈ R.  (3)

The polyhedron R is said to be an ϵ-polyhedron for P ∈ ℙ_{n}, denoted R ⇛_{ϵ} P, if R is an ϵ-polyhedron and P = [[R]].

Condition (3) that every point in the ϵ-polyhedron R has a projection on the hyperplane defined by the constraint (ϵ = 0) corresponds to a dual property concerning the constraints for R.

Proposition 5.3. Let R ∈ ℂℙ_{n+1} be such that R ⊆ con({ϵ ≤ δ}), where δ > 0. Then R is an ϵ-polyhedron if and only if

R ⊆ con({⟨a, x⟩ + s · ϵ ≥ b}) ⟹ R ⊆ con({⟨a, x⟩ + 0 · ϵ ≥ b}). (4)

In Figure 2 we show several examples of polyhedra in ℂℙ_{2} (representing NNC polyhedra in ℙ_{1}), a subset of which happens to be ϵ-polyhedra. In particular, the semi-column polyhedron R_{1}, which according to Definition 1 represents the closed interval P_{1} = con({1 ≤ x ≤ 3}), is not an ϵ-polyhedron, because it is not provided with a finite upper-bound on the ϵ coordinate, therefore violating condition (2) of Definition 5.2. The triangle R_{2} is an ϵ-polyhedron for the open segment P_{2} = con({4 < x < 8}). Polyhedron R_{3} is an ϵ-polyhedron for the segment P_{3} = con({10 < x ≤ 12}), which is neither closed nor open. Similarly, R_{4} is an ϵ-polyhedron for the closed segment P_{4} = con({14 ≤ x ≤ 16}). Finally, polyhedron R_{5} represents the NNC polyhedron P_{5} = con({18 ≤ x ≤ 20}), but it is not an ϵ-polyhedron because it violates condition (3) of Definition 5.2. For instance, even though P ∈ R_{5}, we have P′ ∉ R_{5}.

Figure 3, which shows the poly-hulls of some of the polyhedra in Figure 2, provides a graphical and informal justification for the two conditions stated in Definition 5.2. Let us suppose we do not enforce condition (2) of Definition 5.2, thus admitting polyhedra such as R_{1}, and consider the convex polyhedral hull P_{1}⊎P_{2} = con({1 ≤ x < 8}). The poly-hull R_{1}⊎R_{2} of the two encodings for P_{1} and P_{2} represents a wrong result, since [[R_{1} ⊎ R_{2}]] = con({1 ≤ x ≤ 8}). Suppose now we do not enforce condition (3) of Definition 5.2, thus allowing for polyhedra such as R_{5}, and consider the poly-hull P_{4} ⊎ P_{5} = con({14 ≤ x ≤ 20}). Again, the computation of this poly-hull using the closed encodings of its arguments provides a wrong result, since we have [[R_{4} ⊎ R_{5}]] = con({12 < x ≤ 20}).

If we are to provide an implementation-independent interface for the user, we need to be able to extract from the constraint and generator systems describing an ϵ-polyhedron, the corresponding mixed constraint system and extended generator system describing the NNC polyhedron it represents. Reasoning at the intuitive level, consider an arbitrary ϵ-polyhedron, such as R_{3} in Figure 2. Then, it is worth noting that

O  x ϵ  A  D R_{1}  R_{2} R_{1} ⊎ R_{2}  R_{4}  R_{5} K  L  N R_{4} ⊎ R_{5}

Fig. 3. R_{1} ⊎ R_{2} (resp., R_{4} ⊎ R_{5}) does not represent the NNC polyhedron P_{1} ⊎ P_{2} (resp., P_{4} ⊎ P_{5}).

any facet that is parallel to the ϵ axis, such as the segment [I, J], corresponding to an inequality constraint having a zero coefficient for the ϵ variable, will encode a non-strict inequality constraint of the represented NNC polyhedron P_{3} (in this case, the constraint x ≤ 12). On the other hand, any facet such as the segment [J, F], corresponding to an inequality constraint having a negative coefficient for the ϵ variable, will encode a strict inequality constraint of the represented NNC polyhedron P_{3} (in this case, the constraint x > 10). Equivalently, we could have noted that in polyhedron R_{3} the points having a strictly positive ϵ coordinate can be chosen arbitrarily close to vertex F = (10, 0)^{T}, but all the points having value 10 for their x coordinate happen to have a non-positive ϵ coordinate. Thus, the vector F′ = (10) ∈ ℝ^{1} represented by F is not a point of the NNC polyhedron P_{3}, but it is one of its closure points. All of the above observations can be formalized as follows.

Definition 5.4. (Encoded descriptions.) Let (C, G) ≡ R ∈ ℂℙ_{n+1} be a DD pair for a closed polyhedron. Then, if [[R]] ≠ ∅, the mixed constraint system encoded by C is defined as con enc(C) = C_{S} ∪ C_{NS}, where

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

If [[R]] = ∅, then we define con enc(C) =^{def} {x_{1} > 0, −x_{1} > 0}. Also, the extended generator system encoded by G = (R, P) is defined as gen enc(G) = (R′, P′, C′), where

R′ =^{def} { r | (r^{T}, 0)^{T} ∈ R },
P′ =^{def} { p | (p^{T}, e)^{T} ∈ P, e > 0 },
C′ =^{def} { c | (c^{T}, 0)^{T} ∈ P, c ∉ P′ }.

The following proposition states the correctness of the two mappings introduced above.

Proposition 5.5. Let (C, G) ≡ R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. Then

[[R]] = con(con enc(C)) = gen(gen enc(G)).  (5)

Hence, Definition 5.4 provides a high-level, more user-friendly, interpretation of the constraint and generator systems describing an ϵ-polyhedron. Thus the condition (3) of Definition 5.2, can be interpreted as saying “every point is also a closure point.” Similarly, the dual condition stated in Proposition 5.3 may be interpreted as “every valid strict inequality is also a valid non-strict inequality.” Even though these two assertions are trivially true in the encoded domain ℙ_{n}, the corresponding conditions on the encoding domain ℂℙ_{n+1} are essential if we are to avoid the problems such as those illustrated in Figure 3 by the computation of the poly-hull R_{4} ⊎ R_{5}.

5.1. Constraint- and Generator-Biased Representations

We now consider two special subclasses of the class of ϵ-polyhedra. The first of these requires the value zero to be a lower bound for the ϵ dimension.

Definition 5.6. (C-ϵ-polyhedron.) An ϵ-polyhedron R ∈ ℂℙ_{n+1} is said to be constraint-biased and called a C-ϵ-polyhedron if and only if R ⊆ con({ϵ ≥ 0}). We write R ⇛_{C} P if R is a C-ϵ-polyhedron and R ⇛_{ϵ} P.

The set of constraint-biased ϵ-polyhedra corresponds, essentially, to the class of polyhedra originally proposed in [HPR94, HPR97]. (This is also the same class that was considered in [BRZH02], where these polyhedra were called ϵ-representations.)

A C-ϵ-polyhedron for an NNC polyhedron P can be easily constructed starting from either a mixed constraint system or an extended generator system for P.

Definition 5.7. (‘con repr_{C}’ and ‘gen repr_{C}’.) Let P ∈ ℙ_{n} be an NNC polyhedron such that (C, G) ≡ P. The constraint-biased representation of C is the constraint system con repr_{C}(C) on the vector space ℝ^{n+1} where

con repr_{C}(C) =^{def} {0 ≤ ϵ ≤ 1}
∪ { ⟨a, x⟩ − 1 · ϵ ≥ b | (⟨a, x⟩ > b) ∈ C }
∪ { ⟨a, x⟩ + 0 · ϵ ≥ b | (⟨a, x⟩ ≥ b) ∈ C }.

The constraint-biased representation of G = (R, P, C) is the generator system gen repr_{C}(G) = (R′, P′) on the vector space ℝ^{n+1} where

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

Observe that, in the mapping defined by the representation function ‘gen repr_{C}’ and using the notation in Definition 5.7, each point in P corresponds to two distinct points in P′, having a positive and a zero ϵ coordinate, respectively. This ensures that condition (3) of Definition 5.2 is met. In general, the above encodings require a constant number of additional constraints versus a linear number of additional generators: this is the reason why ϵ-polyhedra in this subclass are called “constraint-biased.”

The second special subclass of ϵ-polyhedra requires that −e_{ϵ} =^{def} (0^{T}, −1)^{T} is a ray of all the non-empty ϵ-polyhedra, so that there is no lower bound for the ϵ dimension.

Definition 5.8. (G-ϵ-polyhedron.) An ϵ-polyhedron R ∈ ℂℙ_{n+1} is said to be generator-biased and called a G-ϵ-polyhedron if and only if R = ∅ or −e_{ϵ} ∈ rays(R). We write R ⇛_{G} P if R is a G-ϵ-polyhedron and R ⇛_{ϵ} P.

As for the constraint-biased case, generator-biased ϵ-polyhedra can also be used for representing any NNC polyhedron. In particular, a G-ϵ-polyhedron for an NNC polyhedron P may be constructed directly from any mixed constraint system or extended generator system describing P.

Definition 5.9. (‘con repr_{G}’ and ‘gen repr_{G}’.) Let P ∈ ℙ_{n} be an NNC polyhedron such that (C, G) ≡ P. The generator-biased representation of C is the constraint system con repr_{G}(C) on the vector space ℝ^{n+1} where

con repr_{G}(C) =^{def} {ϵ ≤ 1}
∪ { ⟨a, x⟩ − 1 · ϵ ≥ b | (⟨a, x⟩ > b) ∈ C }
∪ { ⟨a, x⟩ + 0 · ϵ ≥ b | (⟨a, x⟩ > b) ∈ C }
∪ { ⟨a, x⟩ + 0 · ϵ ≥ b | (⟨a, x⟩ ≥ b) ∈ C }.

The generator-biased representation of G = (R, P, C) is the generator system gen repr_{G}(G) = (R′, P′) on the vector space ℝ^{n+1} where

R′ =^{def} {−e_{ϵ}} ∪ { (r^{T}, 0)^{T} | r ∈ R },
P′ =^{def} { (p^{T}, 1)^{T} | p ∈ P } ∪ { (q^{T}, 0)^{T} | q ∈ C }.

It can be seen that, for each strict inequality contained in C, the representation function ‘con repr_{G}’ adds both the strict and the non-strict inequality encodings. This is similar to what is done for points in Definition 5.7 and, by virtue of Proposition 5.3, ensures that condition (3) of Definition 5.2 is met. In contrast, for each point in the generator system, the function ‘gen repr_{G}’ does not add the corresponding closure point. In fact, these closure points are not needed, because they can be generated by combining the corresponding point with the ray −e_{ϵ}, which is always added. Since the encodings for ϵ-polyhedra in this subclass require a linear number of additional constraints versus a constant number of additional generators, they are called “generator-biased.”

For both the constraint-biased and generator-biased representations, it should be noted that the choice of the value −1 for the ϵ coefficients in the constraints representing strict inequalities is arbitrary: any other negative value will do. Also, the side constraint ϵ ≤ 1 could be replaced, as stated in condition (2) of Definition 5.2, by any other constraint ϵ ≤ δ such that δ > 0. Dually, the choice of the value 1 for the ϵ coordinate of the points of P′ encoding the points of P could be replaced by any other positive value.

Returning to Figure 2, it can be observed that R_{2} is a constraint-biased ϵ-polyhedron, R_{4} is a generatorbiased ϵ-polyhedron, whereas the ϵ-polyhedron R_{3} is neither constraint-biased nor generator-biased. By comparing R_{3} with R_{2} and R_{4} it can be seen that those ϵ-polyhedra that are not members of one of the two subclasses can require both a linear number of additional constraints and a linear number of additional generators (with respect to the original NNC descriptions), resulting in a significant waste of both memory space and computation time.

The following result formalizes the correctness of the encodings introduced in Definitions 5.7 and 5.9.

Proposition 5.10. Let (C, G) ≡ P ∈ ℙ_{n}. Then

1. con(con repr_{C}(C)) ⇛_{C} P, con(con repr_{G}(C)) ⇛_{G} P;

2. gen(gen repr_{C}(G)) ⇛_{C} P, gen(gen repr_{G}(G)) ⇛_{G} P.

By suitably combining the previous definitions and formal results, we are now able to systematically convert a mixed constraint system C for the NNC polyhedron P = con(C) ∈ ℙ_{n} into a corresponding extended generator system G such that gen(G) = P; or, viceversa, we can start from any extended generator system for P to obtain a corresponding mixed constraint system.

The first of these conversions is obtained as follows, where we assume that the constraint-biased representation is adopted. We first apply Definition 5.7 to obtain the constraint system representation of a C-ϵ-polyhedron for P, i.e., we compute C′ = con repr_{C}(C); then, by letting R = con(C′) ∈ ℂℙ_{n+1}, we apply to C′ the usual conversion algorithm for closed polyhedra to obtain a (standard) generator system G′ such that gen(G′) = R; finally, we apply Definition 5.4 to extract from G′ the extended generator system G = gen enc(G′). By virtue of Propositions 5.5 and 5.10, we obtain gen(G) = P. The dual conversion can be obtained similarly. By combining the above conversion procedure with the specifications provided in Section 4.2, we obtain a complete implementation of all the operations defined on the domain of NNC polyhedra.

5.2. Operations on ϵ-Polyhedra

It should be noted that the encoding of operations’ arguments from ℙ_{n} into corresponding arguments of ℂℙ_{n+1} and the decoding of the corresponding results are only needed when performing input-output operations, to provide the end-user with the high-level view presented in Section 4. In all the other cases (and, in particular, for all the intermediate results obtained during the computation of a sequence of operations) these translations can be easily and efficiently filtered away. Namely, the next proposition shows that most of the operators defined on the domain of NNC polyhedra ℙ_{n} can be easily mapped into the corresponding operators on the class of ϵ-polyhedra defined on ℂℙ_{n+1}.

Proposition 5.11. Letting ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}, suppose that R ⇛_{Y} P, R_{1} ⇛_{Y} P_{1} and R_{2} ⇛_{Y} P_{2}. Then

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

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

O  x ϵ  ϵ = 1 R_{3} R_{1}  A B  R_{2}  C D

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

3. let f =^{def} λx ∈ ℝ^{n} . Ax + b be any affine transformation defined on ℙ_{n}; then g(R) ⇛_{Y} 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}.

Hence, operations such as the intersection of NNC polyhedra and the application of affine transformations can be safely performed on any ϵ-polyhedra for the arguments; the same is true for the poly-hull operation, provided neither of the arguments is empty. Moreover, both the constraint-biased and the generator-biased subclasses are closed under the application of these operators.

6. The Issue of Minimization

When adopting the ϵ dimension approach proposed in [HPR94], no matter if constraint- or generator-biased, each NNC polyhedron P ∈ ℙ_{n} may be represented by different (actually, an infinite number of) closed polyhedra in ℂℙ_{n+1}. In the previous section we have shown that all of these possible representations are equally good for computing many operations required by applications such as static analysis. However, the choice of a particular ϵ-polyhedron R ∈ ℂℙ_{n+1} for representing an NNC polyhedron P ∈ ℙ_{n} turns out to be critical when trying to provide a non-redundant high-level description for P.

The problem is that the computation of minimal forms for the descriptions of an arbitrary closed representation R ⇛_{ϵ} P is not enough to ensure that the encoded NNC descriptions for P are in minimal form too. Namely, letting (C, G) ≡ R, even though the DD pair (C, G) is in minimal form, it may well happen that con enc(C) or gen enc(G) are a mixed constraint system and an extended generator system containing redundant constraints and generators, respectively. The following example illustrates this point.

Consider the two NNC polyhedra P_{1} = con(C_{1}) and P_{2} = con(C_{2}) of ℙ_{1}, where

C_{1} = {0 < x < 2}, C_{2} = {2 < x < 3}.

These polyhedra can be represented by the C-ϵ-polyhedra R_{1}, R_{2} ∈ ℂℙ_{2} such that

R_{1} = con(con repr_{C}(C_{1})) = \{ (x, ϵ)^{T} ∈ ℝ^{2} | \begin{matrix}0 ≤ ϵ & ≤ 1 \\ x − ϵ & ≥ 0 \\ −x − ϵ & ≥ −2 \end{matrix} \},

R_{2} = con(con repr_{C}(C_{2})) = \{ (x, ϵ)^{T} ∈ ℝ^{2} | \begin{matrix}0 ≤ ϵ & ≤ 1 \\ x − ϵ & ≥ 2 \\ −x − ϵ & ≥ −3 \end{matrix} \}.

In Figure 4, these two polyhedra correspond to the triangles having vertices O, A, B and A, C, D, respectively. Note that, in both cases, the ϵ upper bound constraint ϵ ≤ 1 happens to be redundant.

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

P_{3} = P_{1} ⊎ P_{2} = con({0 < x < 3}).

At the representation level, as shown in Figure 4, P_{3} will be described by the ϵ-polyhedron R_{3} generated

O  x ϵ  ϵ = 1 R_{1}  A B  R_{4} G H R_{5} E  F I J

Fig. 5. The “minimized” trapezium EF IJ, 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.

by the four vertices O, C, D, and B, whereas point A is identified as redundant. Formally,

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

Note that the chosen constraint system

C_{3} = {ϵ ≥ 0, x − ϵ ≥ 0, x + ϵ ≤ 3, x + 3ϵ ≤ 4}

describing polyhedron R_{3} is in minimal form; in particular, the last non-strict inequality constraint x+3ϵ ≤ 4, which corresponds to the segment [B, D] in Figure 4, is not redundant as far as the ϵ-polyhedron R_{3} is concerned. However, this non-strict inequality is actually encoding the strict inequality constraint x < 4, which is clearly redundant when considering the encoded polyhedron P_{3} = [[R_{3}]]. Formally, the mixed constraint system encoded by C_{3} is

C′_{3} = con enc(C_{3}) = {0 < x < 3, x < 4},

which, according to Definition 3.3, is not in minimal form. In this case, we say that x + 3ϵ ≤ 4 is an ϵ-redundant constraint in C_{3}.

The same problem as above can be observed when considering a generator system for the ϵ-polyhedron R_{3}. Namely, we have R_{3} = gen(G_{3}), where G_{3} = (∅, P_{3}) and

P_{3} = {(0, 0)^{T}, (3, 0)^{T}, (2.5, 0.5)^{T}, (1, 1)^{T}}.

Even though G_{3} is a generator system in minimal form, by Definition 5.4 we obtain

G′_{3} = gen enc(G_{3}) = (∅, P′_{3}, C′_{3}),

where P′_{3} = {1, 2.5} and C′_{3} = {0, 3}. Since the point 1 ∈ P′_{3} (resp., 2.5 ∈ P′_{3}) is redundant in G′_{3}, the encoded generator system is not in minimal form. In this case, we say that (2.5, 0.5)^{T} ∈ P_{3} (resp., (1, 1)^{T} ∈ P_{3}) is an ϵ-redundant generator in G_{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 or generators in any minimized description for an ϵ-polyhedron happen to be ϵ-redundant. Even when disregarding these pathological cases, this form of redundancy can have a serious negative impact on the efficiency of most of the operations computed on the ϵ-polyhedron; in particular, this is true when converting between constraint and generator systems. Moreover, it must be stressed that efficiency degradation is not the only issue. It turns out that the unnoticed presence of ϵ-redundant constraints may also cause headaches to the users of a software library computing on the domain of NNC polyhedra (and adopting the ϵ dimension approach). As an example, suppose one wants to know if a given NNC polyhedron is not topologically closed. Ordinary users of the software library (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 constraint. If the considered software library merely computes a minimal description for the ϵ-polyhedron representing the NNC polyhedron, then such an approach would be unsound, as illustrated by the scenario proposed in Figure 5. Here, the NNC polyhedron P_{1} defined previously is intersected with the NNC polyhedron

P_{4} = con({5 ≤ 4x ≤ 7}) ∈ ℙ_{1}, whose representation R_{4} = con(con repr_{C}(P_{4})) ∈ ℂℙ_{2} is the rectangle having vertices E, F, G and H. The resulting trapezium (having vertices E, F, I and J) is another ϵ-representation for the NNC polyhedron P_{4}, which is clearly topologically closed. However, any constraint system describing the trapezium will also encode the (redundant) strict inequality constraint x < 2, corresponding to the closed segment [I, J].

It is therefore meaningful to address the problem of providing a minimization operator that, starting from an arbitrary description of an ϵ-polyhedron R ⇛_{ϵ} P, is able to compute a description of a (possibly different) ϵ-polyhedron R′ ⇛_{ϵ} P that encodes a non-redundant high-level description for the NNC polyhedron P. The result of this computation is said to be a description in ϵ-minimal form.

Definition 6.1. (ϵ-minimal forms.) Let R ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P and let (C, G) ≡ R be a DD pair for R. Then

• C is in ϵ-minimal form if and only if con enc(C) is in minimal form;

• G is in ϵ-minimal form if and only if gen enc(G) is in minimal form.

The computation of ϵ-minimal forms will be based on the identification of all the ϵ-redundant constraints and generators. These will be either removed or replaced by other constraints and generators that are not ϵ-redundant in the resulting description.

While still reasoning at the informal level, it is worth stressing that this notion of redundancy has a double nature. In the examples just presented, ϵ-redundancy shows its semantic nature, meaning that the redundant information is encoded in the ϵ-polyhedron itself, rather than in one of its constraint or generator descriptions. Namely, all constraint systems and generator systems describing R_{3} necessarily contain the ϵ-redundant constraint and generators identified above. As a consequence, this kind of redundancy can only be eliminated by choosing a different ϵ-polyhedron R′_{3} representing the same NNC polyhedron P_{3}.

There are also examples where ϵ-redundancy only has a syntactic nature, meaning that the redundancy can be eliminated by choosing a particular constraint or generator description for the same ϵ-polyhedron. Clearly, this happens when a description contains some constraints or generators that are redundant (in the classical sense) for the ϵ-polyhedron itself. However, this may also happen when starting from a description in minimal form. For instance, let R = con(C) ∈ ℂℙ_{2} be the ϵ-polyhedron defined by the constraint system

C = {0 ≤ x ≤ 0, ϵ ≥ 0, x + ϵ ≤ 1}.

Even though C is in minimal form, it is not in ϵ-minimal form, because the mixed constraint system con enc(C) = {0 ≤ x ≤ 0, x < 1} contains the redundant strict inequality constraint x < 1. However, the ϵ-polyhedron R can also be described by the constraint system

C′ = {0 ≤ x ≤ 0, 0 ≤ ϵ ≤ 1},

where the ϵ-redundant constraint x + ϵ ≤ 1 has been replaced by the ϵ upper bound constraint ϵ ≤ 1, obtaining a description in ϵ-minimal form for the same ϵ-polyhedron R. It will be shown that this syntactic kind of ϵ-redundancy cannot occur if we consider minimal descriptions in orthogonal form. As a matter of fact, for the particular example considered above, the constraint system C′ is in orthogonal form, whereas this property does not hold for C.

6.1. The Computation of ϵ-Minimal Forms

The efficient detection of ϵ-redundant constraints and generators is based on the checking of particular saturation conditions. The following notation is needed for a formal definition of these conditions.

We say that a point p (resp., a ray r) saturates a constraint β = (⟨a, x⟩ ≥ b) if and only if ⟨a, p⟩ = b (resp., ⟨a, r⟩ = 0). For any point p and constraint system C, we define

sat con(p, C) =^{def} { β ∈ C | p saturates β };

and, for any constraint β and generator system G = (R, P), we define

sat gen(β, G) =^{def} ({ r ∈ R | r saturates β }, { p ∈ P | p saturates β }).

Let (C, G) ≡ R ∈ ℂℙ_{n+1} be a DD pair for an ϵ-polyhedron. The set of strict and non-strict inequality encodings C_{>} and C_{≥} of the 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 }.

The sets of ray encodings G_{R} ⊆ R, point encodings G_{P} ⊆ P and closure point encodings G_{C} ⊆ P of the generator system G = (R, P) are defined as

G_{R} =^{def} { (v^{T}, e)^{T} ∈ R | e = 0 };
G_{P} =^{def} { (v^{T}, e)^{T} ∈ P | e > 0 };
G_{C} =^{def} { (v^{T}, e)^{T} ∈ P | e = 0 }.

We are now ready to provide the formal definition of strong ϵ-redundancy. As the name suggests, this notion gives sufficient conditions for the identification of an ϵ-redundant constraint or generator in a description of an ϵ-polyhedron.

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

sat gen(β, (G_{R}, G_{C})) ⊑ (G_{R}, ∅);
∃β′ ∈ C_{>} \ {β} . sat gen(β, (G_{R}, G_{C})) ⊑ sat gen(β′, G).

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

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

The next proposition shows that strongly ϵ-redundant constraints and generators can be safely removed from (or replaced in) the descriptions of an ϵ-polyhedron without affecting the represented NNC polyhedron. If the ϵ-polyhedron was constraint- or generator-biased, it remains constraint- or generator-biased, respectively.

Proposition 6.3. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}. Assume (C, G) ≡ R ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} are such that R ⇛_{Y} P ≠ ∅. Suppose that β is a strongly ϵ-redundant constraint in C and p is a strongly ϵ-redundant generator in G = (R, P). Then the following hold:

con((C \ {β}) ∪ {ϵ ≤ 1}) ⇛_{Y} P;  (6)
gen((R, P \ {p})) ⇛_{Y} P.  (7)

According to Definition 6.2, only the strict inequality encodings and the point encodings of an ϵpolyhedron can be identified as strongly ϵ-redundant constraints and generators, respectively. The following result shows that such a restriction is inconsequential; intuitively, all the non-strict inequality encodings, the ray encodings and the closure point encodings can only give rise to the syntactic kind of ϵ-redundancy.

Proposition 6.4. Let R, R′ ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P ≠ ∅ and R′ ⇛_{ϵ} P; let also (C, G) ≡ R. Then

∀β ∈ C_{≥} : R′ ⊆ con({β});  (8)
∀r ∈ G_{R} : r ∈ rays(R′);  (9)
∀p ∈ G_{C} : p ∈ R′.  (10)

When all the strongly ϵ-redundant constraints or generators have been filtered away, the descriptions of an ϵ-polyhedron no longer contain ϵ-redundancies of the semantic kind. Thus, descriptions in ϵ-minimal form can be obtained by the computation of minimal orthogonal forms.

Proposition 6.5. Let R ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P ≠ ∅ and let (C, G) ≡ R be a DD pair in minimal orthogonal form. Then the following hold:

O  x ϵ  ϵ = 1 B  C D K

Fig. 6. The trapezium OCKB is an ϵ-representations for P_{3}, obtained by applying the ϵ-minimization process to the constraint system describing R_{3}.

O  x ϵ  ϵ = 1 B  C D

Fig. 7. The triangles OCB and OCD are other two different ϵ-representations for P_{3}, which can be obtained by applying the ϵ-minimization process to the generator system describing R_{3}.

1. If C contains no strongly ϵ-redundant constraint, then it is in ϵ-minimal form;

2. If G contains no strongly ϵ-redundant generator, then it is in ϵ-minimal form.

It is worth stressing that, even if (C, G) is a DD pair for R ⇛_{C} P, after removing all strongly ϵ-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 ϵ-minimal form does not imply that the corresponding dual description will also be in ϵ-minimal form.

As an example, we now compute the ϵ-minimal forms for the polyhedron R_{3} represented in Figure 4. 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 strongly ϵ-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 strongly ϵ-redundant (no closure point encoding saturates it) and can be replaced by the ϵ upper bound constraint ϵ ≤ 1. The resulting constraint system, which is in ϵ-minimal form, defines the trapezium of vertices O, C, K, and B represented in Figure 6. Note that the generator system for this trapezium is not in ϵ-minimal form. 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 ϵ-minimal form of the constraint system describing the trapezium EF IJ of Figure 5: the removal of the constraint corresponding to segment [I, J] would yield a strip which is unbounded from above, so that it would not satisfy condition 2 of Definition 5.2; the addition of the ϵ upper bound constraint results in the rectangle EF GH (i.e., the ϵ-representation R_{4} of P_{4}).

Starting again from polyhedron R_{3}, let us now apply the ϵ-minimization process to its generator system, which is made up of the four points O, C, D, and B. It is easy to observe that each one of the two point encodings is made strongly ϵ-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 7, whose corresponding generator systems are both in ϵ-minimal form.

7. Implementation and Evaluation

All the ideas presented in this paper have been implemented and incorporated into the Parma Polyhedra Library (PPL, http://www.cs.unipr.it/ppl/). The PPL is a collaborative project started in January 2001 at the Department of Mathematics of the University of Parma and 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.

This implementation allowed us, first of all, to demonstrate the real benefits of having an implementationindependent interface based on mixed constraint and generator systems. In order to fully appreciate the advantages from the users’ point of view, it is instructive to compare the new interface with the ones provided by the only two polyhedra libraries —among those based on the DD method that provide the services required by applications in static analysis and computer-aided verification— that support NNC polyhedra. These are “Polka” [HKP95] by Halbwachs, A. Kerbrat, and Y.-E. Proy, and “New Polka”, by B. Jeannet [Jea02]. While the “Polka” polyhedra library is not available in source format and binaries are distributed under rather restrictive conditions (until about the year 1996 they could be freely downloaded), “New Polka” is free software. Both libraries can be compiled so as to work with strict inequalities. However, this support is incomplete, incurring avoidable inefficiencies and leaving the client application with the non-trivial task of a correct interpretation of the obtained results. In particular, even though an NNC polyhedron can be easily described by using constraint systems containing strict inequalities, the libraries lack the corresponding generalization of generator systems (i.e., the introduction of closure points), resulting into an asymmetric user interface. For instance, the following sentence comes from the documentation of “New Polka” [Jea02, 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 also present in “Polka” and discussed in more detail in [HKP95, 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.

This kind of approach, which requires the user to be aware of so many implementation details, is far from being satisfactory. Finally, neither “Polka” nor “New Polka” provide support for the minimization of the descriptions of an NNC polyhedron, therefore suffering from the issues exposed in Section 6.

In order to asses the practical relevance of the minimization procedures proposed in this paper, we have conducted a preliminary experimental evaluation. Table 2 summarizes the results for four simple experiments, where a pair of rows corresponds to a single experiment. Each of the four experiments, takes four NNC polyhedra P_{1}, P_{2}, P_{3}, P_{4} defined by extended generator systems G′_{1}, G′_{2}, G′_{3}, G′_{4}, respectively and aims to compute a constraint description for the NNC polyhedron P = (P_{1}∩P_{2})⊎(P_{3}∩P_{4}). The four input polyhedra all have the same shape (they are equivalent up to translation and scaling transformations); in particular, if G′_{i} = (∅, P′_{i}, C′_{i}), then # P′_{i} and # C′_{i} are invariant for i = 1, …, 4 (# P′_{i} and # C′_{i} are given in the first column of the table). Each row of a pair of rows corresponds to one of two alternative evaluation strategies:

• the first row reports the measurements obtained when adopting the standard evaluation strategy which does not compute the ϵ-minimal forms;

• the second row reports the measurements obtained when adopting the enhanced evaluation strategy which computes the ϵ-minimal forms of the polyhedra descriptions just before the application of each operator (i.e., before computing the two intersections and before computing the poly-hull), as well as at the end of the overall computation.

All experiments start by computing the constraint-biased representation G_{i} of G′_{i}, as given in Definition 5.7, which define the C-ϵ-polyhedra R_{i} = gen(G_{i}) ⇛_{C} P_{i}; they then compute a constraint system C for the C-ϵ-polyhedron R = (R_{1} ∩ R_{2}) ⊎ (R_{3} ∩ R_{4}). To compute the two intersections R_{12} = R_{1} ∩ R_{2} and R_{34} = R_{3} ∩ R_{4}, the conversion algorithm is applied to obtain the constraint systems C_{i} such that R_{i} = con(C_{i}). In the second and third columns we give the cardinalities of G_{i} and C_{i}, respectively. Note that, in the case of the enhanced evaluation strategy, these constraint systems are in ϵ-minimal form, so that # C_{i} for the enhanced evaluation strategy is less than that for the standard evaluation strategy. The constraint systems for R_{12} and R_{34} are then computed and the conversion algorithm applied so as to obtain the generator systems G_{12} and G_{34} such that R_{12} = gen(G_{12}) and R_{34} = gen(G_{34}); the corresponding cardinalities are shown in the fourth and fifth columns where again, in the case of the enhanced evaluation strategy, the generator systems G_{12} and G_{34} are in ϵ-minimal form. Then, the poly-hull R = R_{12} ⊎ R_{34} is computed and the conversion algorithm is again applied to obtain a constraint description C of R; the cardinality of C is reported in the sixth column. Even though not necessary for the correctness of the computation, in the case of the enhanced evaluation strategy C is put into ϵ-minimal form. Note that, by Definitions 5.4 and 6.1, the cardinality of a minimal constraint system for P is just one or two less than the value of # C reported for

Table 2. Exploiting ϵ-minimal forms to improve efficiency.

4 × (# P′_{i} + # C′_{i}) 4 × # G_{i} 4 × # C_{i} # G_{12} # G_{34}  # C overall time (s) ϵ-mf time (s)
4 × (4 + 8)  4 × 16  4 × 37  130  76  332  0.36
4 × 16  4 × 22  39  16  33  0.02  0.00
4 × (8 + 8)  4 × 24  4 × 55  208  124  520  1.05
4 × 24  4 × 30  49  20  43  0.07  0.00
4 × (8 + 10)  4 × 26 4 × 109  413  304 2693  52.84
4 × 26  4 × 46  57  24  127  0.48  0.01
4 × (16 + 10)  4 × 42 4 × 163  696  656 4994  503.27
4 × 42  4 × 66  77  28  152  2.18  0.05

the enhanced evaluation strategy. The last two columns give the time in seconds taken for the computations. The first of these reports the total time for computing C while, for the enhanced evaluation strategy only, the final column reports just the time spent computing the ϵ-minimal form for the constraint system for R.

Note that the results are explained in terms of the low-level implementation details of the two evaluation strategies; these inner steps are in fact transparent to an end-user of the library. Also, we adopted the constraint-biased implementation supported by the Parma Polyhedra Library [BHRZ03a, BRZH02], but similar results have been obtained when considering the generator-biased implementation.

Even though the considered examples are not meant to provide a faithful representation of typical computation patterns, we can make a couple of observations based on these experiments. The application of even a few operators on the closed representations of NNC polyhedra may produce a huge number of constraints and/or generators that are strongly ϵ-redundant; these can slow-down subsequent computations considerably and are likely to confuse anyone who looks at the final output. Moreover, the computation of ϵ-minimal forms seems to have a negligible cost (see the last column in Table 2), so the adoption of the enhanced evaluation strategy is likely to result in significant efficiency gains even when considering more general computation patterns. On the other hand, the enhanced evaluation strategy does not come with an improved efficiency guarantee, because there can be cases where the representations in ϵ-minimal form, even though having fewer constraints or generators, happen to be more expensive. The conjecture, which is fully justified by our experiments, is that any efficiency losses will be both less frequent and less significant than efficiency gains.

As a final remark, it must be observed that the enhanced computation strategy can be made smarter than in the above example. It can be observed that the standard evaluation strategy allows for the application of the incremental version of the conversion algorithm: for instance, we start from the DD pair (C_{1}, G_{1}) for the ϵ-polyhedron R_{1} and incrementally add the constraints C_{2} describing the ϵ-polyhedron R_{2}, keeping the generator system of the result up-to-date so that, at the end of the computation of the intersection R_{1} ∩ R_{2}, we still have a DD pair (i.e., the generator system G_{12} will be already up-to-date). In contrast, the enhanced evaluation strategy does not fit very well with this incremental approach, because after computing the ϵminimal form for C_{1}, we no longer have a DD pair; thus, the generator representation for the intersection R_{1} ∩ R_{2} has to be recomputed from scratch. The same happens when computing the other intersection and the poly-hull operation. Since the number of strongly ϵ-redundant elements contained in a description can be efficiently computed, an improved evaluation strategy may heuristically predict and compare the gains coming from the computation of ϵ-minimal forms with respect to the losses coming from the lack of incrementality, therefore choosing the evaluation strategy that seems to be more appropriate for the considered context.

8. Conclusion

Convex polyhedra provide the basis for several abstractions used in static analysis and computer-aided verification of complex system. Some of these applications require the manipulation of convex polyhedra that are not necessarily closed. In this work we have proposed an elegant way of decoupling the essential geometric features of NNC polyhedra from their traditional implementation. This separation, besides providing a natural and easy to use interface, enables the search for new implementation techniques and makes their eventual integration into existing software libraries seamless (i.e., transparent to the client application). In fact, we have shown that the standard implementation of NNC polyhedra, which happens to be biased for constraint-intensive computations, has a dual that is biased for generator-intensive computations. For both kinds of implementations, we have provided new minimization procedures that allow to extract a non-redundant constraint or generator description of an NNC polyhedron from its low level encodings.

We have implemented all these ideas in the Parma Polyhedra Library a modern C^{++} library for the manipulation of convex polyhedra. Since it is based on the high level interface for the specification of NNC polyhedra and it implements the new minimization procedures introduced in this work, the Parma Polyhedra Library can be regarded as the first software library (based on the DD method) providing full support for the domain of NNC polyhedra. Some very preliminary experiments on purely synthetic benchmarks have shown that a careful use of the new minimization procedures for NNC polyhedra can have a dramatic effect on the size of the representations and, thus, on the efficiency of the algorithms operating upon them.

The Parma Polyhedra Library has also been extended to experiment with the two alternative implementations of NNC polyhedra. In this respect, it seems likely that the performance of one encoding with respect to the other will depend on the particular application and, more specifically, on the kind of polyhedra and operations that are more common in that application. For future work, given the dual characteristics of the two representations, it would be interesting to investigate whether efficient techniques can be devised so as to use both constraint- and generator-biased encodings, switching dynamically from one to the other in an attempt to maximize performance.

Acknowledgments. We would like to thank Elisa Ricci, who participated to the early stage of this work, and the anonymous reviewers of [BRZH02] for their helpful comments and observations.

References

[BHRZ03a] 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.5 edition, April 2003. Available at http://www.cs.

unipr.it/ppl/.

[BHRZ03b] R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337–354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.

[BHZ03] R. Bagnara, P. M. Hill, and E. Zaffanella. A new encoding and implementation of not necessarily closed convex polyhedra. In M. Leuschel, S. Gruner, and S. Lo Presti, editors, Proceedings of the 3rd Workshop on Automated Verification of Critical Systems, pages 161–176, Southampton, UK, 2003. Published as TR Number DSSE-TR-2003-2, University of Southampton.

[BJT99] 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.

[BK97] F. Benoy and A. King. Inferring argument size relationships with CLP(R). In J. P. Gallagher, editor, Logic Program 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.

[BRZH02] R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 213–229, Madrid, Spain, 2002. Springer-Verlag, Berlin.

[CC77] 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, New York, 1977. ACM Press.

[CH78] 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.

[Che64] 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.

[Che65] 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.

[Che68] 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.

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

[DRS01] N. Dor, M. Rodeh, and S. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In P. Cousot, editor, Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, pages 194–212, Paris, France, 2001. Springer-Verlag, Berlin.

[Hal93] 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.

[HH95] T. A. Henzinger and P.-H. Ho. A note on abstract interpretation strategies for hybrid automata. In P. J. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 252–264. Springer-Verlag, Berlin, 1995.

[HHWT97] 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.

[HKP95] 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.

[HPR94] 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.

[HPR97] 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.

[Jea02] 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.

[Le 92] H. Le Verge. A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes,

France, 1992.

[MBB^{+}99] 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, pages 174–188. Springer-Verlag, Berlin, 1999.

[MRTT53] 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.

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

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

A. Proofs

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

A.1. Proofs of the Results Stated in Section 4

In order to simplify the proof of Proposition 4.3, we introduce the following lemma.

Lemma A.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_{β} ∈ H denote the affine half-space corresponding to β = (⟨a, x⟩ ▷◁ b). Hence v ∈ ℂ(H_{β}). If ▷◁ ∈ {≥}, then ℂ(H_{β}) = con({β}). On the other hand, if ▷◁ ∈ {>}, then ℂ(H_{β}) = con({β′}), where β′ = (⟨a, x⟩ ≥ b). Thus, as v ∈ ℂ(H_{β}), we obtain the thesis ⟨a, v⟩ ≥ b.

Proof of Proposition 4.3 on page 6. Let P = con(C) ∈ ℙ_{n} be an NNC polyhedron defined by the mixed constraint system C = {β_{1}, …, β_{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 = σp + (1 − σ)c is such that v ∈ P. To this end, we show that v satisfies all constraints β_{i} = (⟨a_{i}, x⟩ ▷◁_{i} b_{i}) ∈ C. Since p ∈ P, it holds ⟨a_{i}, p⟩ ▷◁_{i} b_{i}; moreover, by applying Lemma A.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⟩ ≥ σb_{i} + (1 − σ)b_{i} = b_{i}.

It follows that if ▷◁_{i} ∈ {≥}, then ⟨a_{i}, v⟩ ≥ b_{i} and, if ▷◁ ∈ {>}, ⟨a_{i}, v⟩ > b_{i}. Therefore, in both cases we obtain ⟨a_{i}, v⟩ ▷◁_{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}, B_{i} be the open ball centered in c with radius σ_{i}, and v_{i} = σ_{i+1}p + (1 − σ_{i+1})c; then, as 0 < σ_{i+1} < σ_{i} < 1, we have v_{i} ∈ P ∩ B_{i}. As this holds for any i ∈ ℕ, c ∈ ℂ(P).

A direct proof of Theorem 4.4 would require a generalization of Minkowski’s and Weyl’s theorems. In contrast, we will provide an indirect proof: this will be based on the standard (i.e., non-generalized) version of Minkowski’s and Weyl’s theorems, stated as Theorem 3.2, as well as on Propositions 5.5 and 5.10. Thus, the proof of Theorem 4.4 will appear at the end of the next section.

A.2. Proofs of the Results Stated in Section 5

Proof of Proposition 5.3 on page 9. Let R = con(C). We first assume that (4) holds for any constraint β ∈ C and show that R is an ϵ-polyhedron. Condition (2) of Definition 5.2 holds by hypothesis. We prove condition (3) holds. Let β = (⟨a, x⟩ + s · ϵ ≥ b). Then, by (4), R ⊆ con({⟨a, x⟩ + 0 · ϵ ≥ b}). Thus, for any point (v^{T}, e)^{T} ∈ R we have ⟨a, v⟩ + 0 · e ≥ b, so that also ⟨a, v⟩ + s · 0 ≥ b and hence (v^{T}, 0)^{T} satisfies β. As β was an arbitrary constraint in C, (v^{T}, 0)^{T} ∈ R and condition (3) holds.

Second we assume that R is an ϵ-polyhedron and prove that (4) holds. Suppose β = (⟨a, x⟩+s·ϵ ≥ b) and that R ⊆ con({β}). Then, any point (v^{T}, e)^{T} ∈ R satisfies β. By condition (3) of Definition 5.2, (v^{T}, 0)^{T} ∈ R and therefore satisfies β. Thus we have ⟨a, v⟩ ≥ b. Hence, if β_{0} = (⟨a, x⟩ + 0 · ϵ ≥ b), (v^{T}, e)^{T} satisfies β_{0}. As (v^{T}, e)^{T} was an arbitrary point in R, R ⊆ con({β_{0}}).

To prove Proposition 5.5, we need a few additional lemmas.

Lemma A.2. Let R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. If (r^{T}, e)^{T} ∈ rays(R) and r ≠ 0, then (r^{T}, 0)^{T} ∈ rays(R).

Proof. Since R has a ray, it is not empty. Thus, let (v^{T}, e′)^{T} ∈ R. By condition (3) of Definition 5.2, we have (v^{T}, 0)^{T} ∈ R. Since (r^{T}, e)^{T} is a ray of R, we have (v^{T}, 0)^{T} + ρ(r^{T}, e)^{T} = ((v + ρr)^{T}, ρe)^{T} ∈ R for all ρ ∈ ℝ_{+}. From this, again by condition (3) of Definition 5.2, we obtain ((v + ρr)^{T}, 0)^{T} = (v^{T}, 0)^{T} + ρ(r^{T}, 0)^{T} ∈ R, proving that also (r^{T}, 0)^{T} is a ray of R.

Lemma A.3. Let R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. If (r^{T}, e)^{T} ∈ rays(R), then e ≤ 0. Moreover, if R is a C-ϵ-polyhedron, then e = 0.

Proof. Since R is an ϵ-polyhedron, condition (2) of Definition 5.2 holds so that, for some δ > 0 every point in R satisfies the constraint ϵ ≤ δ. Since R has a ray, it is non-empty, so that there exists a point (v^{T}, e_{0})^{T} ∈ R such that e_{0} ≤ δ. Thus, for all ρ ∈ ℝ_{+}, (vρ^{T}, e_{ρ})^{T} = (v^{T}, e_{0})^{T} + ρ(r^{T}, e)^{T} ∈ R. By condition (2) of Definition 5.2, e_{ρ} = e_{0} + ρe ≤ δ. Therefore, as this holds for all ρ ∈ ℝ_{+}, we have e ≤ 0.

By Definition 5.6, if R is a C-ϵ-polyhedron then it also satisfies the constraint ϵ ≥ 0. By repeating the above argument, we obtain e_{ρ} = e_{0} + ρe ≥ 0. As this holds for all ρ ∈ ℝ_{+}, we also have e ≥ 0, i.e., e = 0.

In the following lemmas, for any (C, G) ≡ R ∈ ℂℙ_{n+1} such that R ⇛_{ϵ} P ≠ ∅, we assume the notations C_{>}, C_{≥}, G_{R}, G_{P}, and G_{C} introduced in Section 6.1. Moreover, we will denote the set of ϵ upper bounds of the constraint system C as

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

A constraint β ∈ C_{ϵ} will be usually denoted as ϵ ≤ δ. Since P ≠ ∅, we have δ > 0.

Lemma A.4. Let R = gen(G) ∈ ℂℙ_{n+1} be an ϵ-polyhedron, where G = (R, P). Let also (v^{T}, e′)^{T} ∈ R for some e′ ∈ ℝ and take e_{max} ∈ ℝ to be the maximal ϵ coordinate such that (v^{T}, e_{max})^{T} ∈ R. Then (v^{T}, e_{max})^{T} ∈ gen((G_{R}, G_{P} ∪ C′)), where C′ = { (c^{T}, 0)^{T} ∈ G_{C} | ∀e′ ∈ ℝ : (c^{T}, e′)^{T} ∉ G_{P} }.

Proof. By hypothesis, (v^{T}, e_{max})^{T} ∈ gen((R, P)) so that

(v^{T}, e_{max})^{T} = (ρ_{1}r_{1} + ⋯ + ρ_{r}r_{r}) + (π_{1}p_{1} + ⋯ + π_{p}p_{p}), (11) where r ≥ 0, {r_{1}, …, r_{r}} ⊆ R, ρ_{1}, …, ρ_{r} > 0 and p > 0, {p_{1}, …, p_{p}} ⊆ P, π_{1}, …, π_{p} > 0 and ∑_{i=1}^{p} π_{i} = 1.

For all 1 ≤ i ≤ r, let r_{i} = (vi^{T}, e_{i})^{T}. Suppose that, for some 1 ≤ j ≤ r, we have e_{j} ≠ 0. Then, as R is an ϵ-polyhedron, by Lemma A.3, e_{j} < 0. If v_{j} = ∅ then, by removing the ray r_{j} in (11), we would obtain

(v^{T}, e_{max})^{T} − ρ_{j}r_{j} = (v^{T}, e_{max} − ρ_{j}e_{j})^{T} ∈ R.

On the other hand, if v_{j} ≠ ∅, then, by Lemma A.2, r_{0} = (vj^{T}, 0)^{T} ∈ rays(R). Thus, in this case, by replacing the ray r_{j} by r_{0} in (11), we again obtain

(v^{T}, e_{max})^{T} − ρ_{j}r_{j} + ρ_{j}r_{0} = (v^{T}, e_{max} − ρ_{j}e_{j})^{T} ∈ R,

In both cases, as ρ_{j} > 0 and e_{j} < 0, e_{max} − ρ_{j}e_{j} > e_{max}. contradicting the maximality of e_{max}. Thus we must have e_{j} = 0 so that r_{j} ∈ G_{R}. As the choice of 1 ≤ j ≤ r was arbitrary, {r_{1}, …, r_{r}} ⊆ G_{R}.

For all 1 ≤ i ≤ p, let p_{i} = (vi^{T}, e_{i})^{T}. Suppose that, for some 1 ≤ j ≤ p, we have e_{j} < 0. Then, as R is an ϵ-polyhedron, by condition (3) of Definition 5.2, p_{0} = (vj^{T}, 0)^{T} ∈ R. Replacing the point p_{j} by p_{0} in (11), we would obtain

(v^{T}, e_{max})^{T} − π_{j}p_{j} + π_{j}p_{0} = (v^{T}, e_{max} − π_{j}e_{j})^{T} ∈ R,

where, since π_{j} > 0, e_{max} − π_{j}e_{j} > e_{max}, contradicting the maximality of e_{max}. Hence, for all 1 ≤ i ≤ p, we have e_{i} ≥ 0. Now suppose that, for some 1 ≤ j ≤ p, we have e_{j} = 0 and there exists e_{j}^{+} > 0 such that p_{j}^{+} = (vj^{T}, e_{j}^{+})^{T} ∈ R. Replacing the point p_{j} by p_{j}^{+} in (11), we would obtain

(v^{T}, e_{max})^{T} − π_{j}p_{j} + π_{j}p_{j}^{+} = (v^{T}, e_{max} + π_{j}e_{j}^{+})^{T} ∈ R,

where, since π_{j} > 0, e_{max} + π_{j}e_{j}^{+} > e_{max}, again contradicting the maximality of e_{max}. It follows that, for all 1 ≤ i ≤ p, the point p_{i} ∈ G_{P}, if e_{i} > 0, and p_{i} ∈ C′, otherwise. Thus, (v^{T}, e_{max})^{T} ∈ gen((G_{R}, G_{P} ∪ C′)).

Proof of Proposition 5.5 on page 10. Let G = (R, P) and gen enc(G) = (R_{1}, P_{1}, C_{1}) be the corresponding extended generator system, where R_{1} = {r_{1}, …, r_{r}}, P_{1} = {p_{1}, …, p_{p}}, and C_{1} = {c_{1}, …, c_{c}}.

Suppose first that [[R]] = ∅. Then, by Definition 5.4, con(con enc(C)) = ∅. Also, by Definition 5.1, R ⊆ con({ϵ ≤ 0}) so that, by Definition 5.4, P_{1} = ∅ and gen((R_{1}, P_{1}, C_{1})) = ∅. Thus (5) holds.

Suppose now that [[R]] ≠ ∅. We will first prove that con(con enc(C)) ⊆ [[R]] and gen(gen enc(G)) ⊆ [[R]]. To this end, we assume that one of the following holds:

v ∈ con(con enc(C)),  (12)
v ∈ gen(gen enc(G)),  (13)

and, in each case, we show that there exists e_{v} > 0 such that (v^{T}, e_{v})^{T} ∈ R.

Suppose that (12) holds. By Definition 5.2, the set C_{>} ∪ C_{ϵ} is non-empty so that, as the value of the ϵ coefficient in each constraint in the set is non-zero, the set

{ e ∈ ℝ | e = −s^{−1}(⟨a, v⟩ − b), (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{>} ∪ C_{ϵ} }

is also non-empty. Let e_{v} be the least element of this set. Suppose β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{>} ∪ C_{ϵ}. By Definition 5.4, if β ∈ C_{>}, then (⟨a, x⟩ > b) ∈ con enc(C) so that, as (12) holds, ⟨a, v⟩ > b. On the other hand, if β ∈ C_{ϵ} then a = 0 and, as [[R]] is non-empty, by Definition 5.2, b < 0. Thus, in both cases ⟨a, v⟩−b > 0 so that, as s < 0, −s^{−1}(⟨a, v⟩−b) > 0. It follows that e_{v} > 0. For each (⟨a, x⟩+0·ϵ ≥ b) ∈ C_{≥}, for some ▷◁ ∈ {≥, >}, the constraint (⟨a, x⟩ ▷◁ b) ∈ con enc(C) so that, by (12), ⟨a, v⟩ ≥ b holds. Hence (v^{T}, e_{v})^{T} satisfies all the constraints in C_{≥}. It follows that (v^{T}, e_{v})^{T} satisfies every constraint in C_{>} ∪ C_{≥} ∪ C_{ϵ}. Reasoning toward a contradiction, suppose that (v^{T}, e_{v})^{T} ∉ R. As [[R]] ≠ ∅, by Definition 5.1, there exists (w^{T}, e_{w})^{T} ∈ R such that e_{w} > 0; in particular, (w^{T}, e_{w})^{T} satisfies all constraints in C. Thus there exists a point (w0^{T}, e_{0})^{T} ∈ R which lies on the line segment joining (w^{T}, e_{w})^{T} and (v^{T}, e_{v})^{T} and saturates a constraint

β′ = (⟨a′, x⟩ + s′ · ϵ ≥ b′) ∈ C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}).

Thus ⟨a′, w_{0}⟩+s′·e_{0} = b′. However, since s′ > 0 and e_{0} > 0, ⟨a′, w_{0}⟩ < b′ so that (w0^{T}, 0)^{T} ∉ R, contradicting condition (3) of Definition 5.2. Thus (v^{T}, e_{v})^{T} ∈ R.

Suppose next that (13) holds. By definition of function ‘gen’ in Theorem 4.4,

v = ∑_{i=1}^{r} ρ_{i}r_{i} + ∑_{i=1}^{p} π_{i}p_{i} + ∑_{i=1}^{c} γ_{i}c_{i}

where p > 0, {r_{1}, …, r_{r}} ⊆ R_{1}, {p_{1}, …, p_{p}} ⊆ P_{1}, {c_{1}, …, c_{c}} ⊆ C_{1}, ρ ∈ ℝr_{+}, π ∈ ℝp_{+} \ {0}, γ ∈ ℝc_{+} and

∑_{i=1}^{p} π_{i} + ∑_{i=1}^{c} γ_{i} = 1. By Definition 5.4, for some e_{1}, …, e_{p} > 0,

{(r1^{T}, 0)^{T}, …, (rr^{T}, 0)^{T}} ⊆ R, {(p1^{T}, e_{1})^{T}, …, (pp^{T}, e_{p})^{T}} ∪ {(c1^{T}, 0)^{T}, …, (cc^{T}, 0)^{T}} ⊆ P.

Thus, letting

(v^{T}, e_{v})^{T} = ∑_{i=1}^{r} ρ_{i}(ri^{T}, 0)^{T} + ∑_{i=1}^{p} π_{i}(pi^{T}, e_{i})^{T} + ∑_{i=1}^{c} γ_{i}(ci^{T}, 0)^{T}

we obtain (v^{T}, e_{v})^{T} ∈ gen(G) = R. Since p > 0 and π ≠ 0, we also obtain e_{v} > 0.

We now prove that [[R]] ⊆ con(con enc(C)) and [[R]] ⊆ gen(gen enc(G)). To this end, let (v^{T}, e)^{T} ∈ R, where e > 0; since R is an ϵ-polyhedron, by condition (2) of Definition 5.2, the ϵ dimension is bounded from above and thus there exists a value e_{max} > 0 such that (v^{T}, e_{max})^{T} ∈ R and, for all e′ > e_{max}, (v^{T}, e′)^{T} ∉ R. We show that both (12) and (13) hold.

Suppose that β′ = (⟨a, x⟩ ▷◁ b) ∈ con enc(C), where ▷◁ ∈ {≥, >}. Then, by Definition 5.4, there exists s ≤ 0 such that β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C. Since (v^{T}, e_{max})^{T} ∈ R, then ⟨a, v⟩ + s · e_{max} ≥ b so that, as e_{max} > 0 holds, we obtain ⟨a, v⟩ ≥ b. Moreover, if ▷◁ ∈ {>}, then s < 0 and we obtain ⟨a, v⟩ > b. Thus, for any ▷◁ ∈ {≥, >}, v satisfies β′. As β′ ∈ con enc(C) was chosen arbitrarily, (12) holds.

We next prove (13). Since e_{max} was chosen to be maximal for v, we can apply Lemma A.4, so that (v^{T}, e_{max})^{T} ∈ gen((G_{R}, G_{P} ∪ C′)), where

C′ = { (c^{T}, 0)^{T} ∈ G_{C} | ∀e′ ∈ ℝ : (c^{T}, e′)^{T} ∉ G_{P} }.

By definition of ‘gen’, we obtain

(v^{T}, e_{max})^{T} = ∑_{i=1}^{r} ρ_{i}(ri^{T}, 0)^{T} + ∑_{i=1}^{p} π_{i}(pi^{T}, e_{i})^{T} + ∑_{i=1}^{c} γ_{i}(ci^{T}, 0)^{T};

where

{(r1^{T}, 0)^{T}, …, (rr^{T}, 0)^{T}} ⊆ G_{R}, {(p1^{T}, e_{1})^{T}, …, (pp^{T}, e_{p})^{T}} ⊆ G_{P} , {(c1^{T}, 0)^{T}, …, (cc^{T}, 0)^{T}} ⊆ C′,

ρ ∈ ℝr_{+}, π ∈ ℝp_{+}, γ ∈ ℝc_{+} and ∑_{i=1}^{p} π_{i} + ∑_{i=1}^{c} γ_{i} = 1. As e_{max} > 0, we obtain p > 0 and π ≠ 0. By

Definition 5.4, {r_{1}, …, r_{r}} ⊆ R_{1}, {p_{1}, …, p_{p}} ⊆ P_{1} and {c_{1}, …, c_{c}} ⊆ C_{1} so that

v = ∑_{i=1}^{r} ρ_{i}r_{i} + ∑_{i=1}^{p} π_{i}p_{i} + ∑_{i=1}^{c} γ_{i}c_{i}

and hence v ∈ gen((R_{1}, P_{1}, C_{1})). Thus (13) holds.

A.3. Proofs of the Results Stated in Section 5.1

Proof of Proposition 5.10 on page 12. To prove item (1), we first show that, for any Y ∈ {C, G},

con(C) = con(con enc(con repr_{Y} (C))). (14)

Let C_{1} = con repr_{Y} (C) and C_{2} = con enc(C_{1}). Let β = (⟨a, x⟩ ▷◁ b) ∈ C, for some ▷◁ ∈ {≥, >}. If ▷◁ ∈ {>}, then, by Definitions 5.7 and 5.9, (⟨a, x⟩ − 1 · ϵ ≥ b) ∈ C_{1} and hence, by Definition 5.4, (⟨a, x⟩ > b) ∈ C_{2}. If otherwise ▷◁ ∈ {≥}, then, by Definitions 5.7 and 5.9, (⟨a, x⟩ + 0 · ϵ ≥ b) ∈ C_{1} and hence, by Definition 5.4, either (⟨a, x⟩ ≥ b) ∈ C_{2} or (⟨a, x⟩ > b) ∈ C_{2}. Thus β is satisfied by all the points in con(C_{2}). As β was an arbitrary constraint in C, we obtain con(C_{2}) ⊆ con(C).

Now let β = (⟨a, x⟩ ▷◁ b) ∈ C_{2}, for some ▷◁ ∈ {≥, >}. If ▷◁ ∈ {>}, then (⟨a, x⟩ + s · ϵ ≥ b) ∈ C_{1}, where s < 0. By Definitions 5.7 and 5.9, (⟨a, x⟩ > b) ∈ C. If ▷◁ ∈ {≥}, then, by Definition 5.4, (⟨a, x⟩+0·ϵ ≥ b) ∈ C_{1}. Thus, by Definitions 5.7 and 5.9, either (⟨a, x⟩ ≥ b) ∈ C or (⟨a, x⟩ > b) ∈ C. Thus β is satisfied by all the points in con(C). As β was an arbitrary constraint in C_{2}, we obtain the other inclusion con(C) ⊆ con(C_{2}). Thus (14) holds. As a consequence, by Proposition 5.5, we have con(C_{1}) ⇛_{ϵ} con(C).

Suppose now that Y = C. Then, by Definition 5.7, con(C_{1}) ⊆ con({ϵ ≥ 0}) so that, by Definition 5.6, con(C_{1}) is a C-ϵ-polyhedron. Otherwise, suppose that Y = G. If con(C_{1}) = ∅ then, by Definition 5.8, it is a G-ϵ-polyhedron. Otherwise, let (v^{T}, e)^{T} ∈ con(C_{1}) and consider β′ ∈ C_{1}. By Definition 5.9, either β′ = (ϵ ≤ 1) or, for some a ∈ ℝ^{n} \ {0}, b ∈ ℝ and s ∈ {0, −1}, β′ = (⟨a, x⟩ + s · ϵ ≥ b). Thus, for all ρ ∈ ℝ_{+}, (v^{T}, e′)^{T} = (v^{T}, e)^{T} + ρ(−e_{ϵ}) satisfies β′, so that −e_{ϵ} is a ray in con({β′}). As the choice of β′ was arbitrary, −e_{ϵ} ∈ rays(con(C_{1})) so that, by Definition 5.8, con(C_{1}) is a G-ϵ-polyhedron. Therefore the proof of item (1) is complete.

To prove item (2), we show that for any Y ∈ {C, G},

gen(G) = gen(gen enc(gen repr_{Y} (G))). (15)

Let G = (R, P, C), G_{1} = gen repr_{Y} (G) = (R_{1}, P_{1}) and G_{2} = gen enc(G_{1}) = (R_{2}, P_{2}, C_{2}). Suppose first that v ∈ R ∪P ∪C. If v ∈ R, then, by Definitions 5.7 and 5.9, (v^{T}, 0)^{T} ∈ R_{1} and hence, by Definition 5.4, v ∈ R_{2}. If v ∈ P, then, by Definitions 5.7 and 5.9, (v^{T}, 1)^{T} ∈ P_{1} and hence, by Definition 5.4, v ∈ P_{2}. If v ∈ C, then, by Definitions 5.7 and 5.9, (v^{T}, 0)^{T} ∈ P_{1} and hence, by Definition 5.4, v ∈ P_{2} ∪ C_{2}. Therefore, by definition of ‘gen’, we obtain gen(G) ⊆ gen(G_{2}).

Now suppose v ∈ R_{2} ∪ P_{2} ∪ C_{2}. If v ∈ R_{2}, then, by Definition 5.4, (v^{T}, 0)^{T} ∈ R_{1}. By Definitions 5.7 and 5.9, v ∈ R. If v ∈ P_{2}, then, by Definition 5.4, (v^{T}, e)^{T} ∈ P_{1}, for some e > 0. Thus, by Definitions 5.7 and 5.9, v ∈ P. If v ∈ C_{2}, then, by Definition 5.4, (v^{T}, e)^{T} ∈ P_{1}, for some e ≥ 0. Thus, by Definitions 5.7 and 5.9, v ∈ P ∪ C. Thus, by definition of ‘gen’, we obtain the other inclusion gen(G_{2}) ⊆ gen(G) and (15) holds. As a consequence, by Proposition 5.5, we have gen(G_{1}) ⇛_{ϵ} gen(G).

Suppose now that Y = G. Then, by Definition 5.9, −e_{ϵ} ∈ R_{1} so that, by Definition 5.8, gen(G_{1}) is a G-ϵ-polyhedron. Otherwise, suppose that Y = C. By Definition 5.7, for each vector (v1^{T}, e_{1})^{T} ∈ R_{1} ∪ P_{1}, we have e_{1} ≥ 0; this implies that, for any point (v^{T}, e)^{T} ∈ gen(G_{1}), we still have e ≥ 0. Thus gen(G_{1}) ⊆ con({ϵ ≥ 0}) so that, by Definition 5.6, gen(G_{1}) is a C-ϵ-polyhedron. This completes the proof of item (2).

We are now ready to provide the formal proof of the generalization of Minkowski and Weyl’s theorems for the domain of NNC polyhedra.

Proof of Theorem 4.4 on page 6. 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 G = (∅, ∅, ∅). Otherwise, let P ≠ ∅. By definition of NNC polyhedron, there exists a mixed constraint system C such that P = con(C). Let R ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P. Note that we can always find such an ϵ-polyhedron for P; e.g., by Proposition 5.10, we can consider con(con repr_{C}(C)) or con(con repr_{G}(C)). By Theorem 3.2, there exists a (standard) generator system G′ = (R′, P′) such that R = gen(G′). By defining G = gen enc(G′), the thesis P = [[R]] = gen(G) follows from Proposition 5.5.

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 ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P. As said above, we can always find such an ϵ-polyhedron for P; e.g., by Proposition 5.10, we can consider gen(gen repr_{C}(G)) or gen(gen repr_{G}(G)). By Theorem 3.2, there exists a constraint system C′, containing non-strict linear inequalities only, such that R = con(C′). By defining C = con enc(C′), the thesis P = [[R]] = con(C) follows from Proposition 5.5.

A.4. Proofs of the Results Stated in Section 5.2

The proof of Proposition 5.11 on page 12 requires a number of additional preliminary results.

For any ϵ-polyhedron, closure points in the NNC polyhedron are represented by points lying on the hyperplane defined by ϵ = 0.

Lemma A.5. Let R ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P ≠ ∅. Then ℂ(P) = { v ∈ ℝ^{n} | (v^{T}, 0)^{T} ∈ R }.

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

First, we show that P′ ⊆ ℂ(P). Let v ∈ P′, so that (v^{T}, 0)^{T} ∈ R, and consider any point p ∈ P (note that such a point exists by hypothesis). Then, since R ⇛_{ϵ} P, there exists e > 0 such that (p^{T}, e)^{T} ∈ R. Since R is a convex set, for all σ ∈ ℝ such that 0 < σ < 1 we have

σ(p^{T}, e)^{T} + (1 − σ)(v^{T}, 0)^{T} = (σp^{T} + (1 − σ)v^{T}, σe)^{T} ∈ R.

Since σe > 0, by Definition 5.1, we obtain σp + (1 − σ)v ∈ P. As the choices of p ∈ P and σ were both arbitrary, we can apply Proposition 4.3 and conclude v ∈ ℂ(P).

Now we show that ℂ(P) ⊆ P′. Let v ∈ ℂ(P) and, for all i ∈ ℕ such that i > 1, define σ_{i} = \frac{1}{i}, so that 0 < σ_{i} < 1. Then, by Proposition 4.3, for all p ∈ P we have v_{i} = σ_{i}p + (1 − σ_{i})v ∈ P. Since R ⇛_{ϵ} P, by applying the fact that P = [[R]] and then property (3) of Definition 5.2, we obtain (vi^{T}, 0)^{T} ∈ R. If p = v, then v_{i} = v, so that the thesis holds. Otherwise, let p ≠ v. For any open ball of ℝ^{n+1} centered in (v^{T}, 0)^{T} and having radius δ > 0, there exists j ∈ ℕ such that σ_{j} < δ; thus, (vj^{T}, 0)^{T} ∈ R belongs to the ball and, as the choice of δ is arbitrary, (v^{T}, 0)^{T} ∈ ℂ(R). However, R ∈ ℂℙ_{n+1} is a topologically closed set, so that R = ℂ(R) and (v^{T}, 0)^{T} ∈ R. Hence, v ∈ P′, completing the proof.

Lemma A.6. Let R ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P ≠ ∅. Then r ∈ rays(P) if and only if (r^{T}, 0)^{T} ∈ rays(R).

Proof. Assuming that r ∈ rays(P), let v ∈ P and ρ ∈ ℝ_{+}. Then v + ρr ∈ P. By Definition 5.1, for some e_{1}, e_{2} > 0, we have (v^{T}, e_{1})^{T} ∈ R and ((v + ρr)^{T}, e_{2})^{T} ∈ R and hence, by condition (2) of Definition 5.2, (v^{T}, 0)^{T} ∈ R and ((v + ρr)^{T}, 0)^{T} ∈ R. Thus (v^{T}, 0)^{T} + ρ(r^{T}, 0)^{T} ∈ R. As this holds for all ρ ∈ ℝ_{+}, (r^{T}, 0)^{T} is a ray of R.

To prove the other direction, assume that (r^{T}, 0)^{T} is a ray of R. Let v ∈ P and ρ ∈ ℝ_{+}. By Definition 5.1, for some e > 0, we have (v^{T}, e)^{T} ∈ R; by assumption, (v^{T}, e)^{T} + ρ(r^{T}, 0)^{T} ∈ R and hence, by Definition 5.1, v + ρr ∈ P, proving that r ∈ rays(P).

Lemma A.7. Let R = gen((R, P)) ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P ≠ ∅. Let also

R′ = { (r^{T}, 0)^{T} | (r^{T}, e)^{T} ∈ R, r ≠ 0 } ∪ { −e_{ϵ} | (r^{T}, e)^{T} ∈ R, e < 0 }

and R′ = gen((R′, P)). Then R′ ⇛_{ϵ} P.

Proof. Suppose that for all (r^{T}, e)^{T} ∈ R we have e = 0. Then, the result holds by observing that, in such a case, we obtain R′ = R and thus R′ = R. Otherwise, suppose that there exists (r^{T}, e)^{T} ∈ R such that e ≠ 0. By Lemma A.3, it holds e < 0. It follows from the hypothesis that (−e_{ϵ}) ∈ R′.

We first show that [[R′]] = P by proving the two inclusions separately.

Consider a ray (r^{T}, e)^{T} ∈ R. If e = 0, then r ≠ 0 so that, by hypothesis, (r^{T}, e)^{T} ∈ R′. If e < 0 and r = 0, then we can write (r^{T}, e)^{T} = −e(−e_{ϵ}), where (−e_{ϵ}) ∈ R′ and −e > 0 is a positive factor. Otherwise, if e < 0 and r ≠ 0, then, by the hypothesis, {(r^{T}, 0)^{T}, −e_{ϵ}} ⊆ R′ and we can write (r^{T}, e)^{T} = (r^{T}, 0)^{T} − e(−e_{ϵ}). Thus, each element of R can be obtained as a non-negative combination of elements of R′, therefore proving that R ⊆ R′ and, by monotonicity, P ⊆ [[R′]].

To prove the other inclusion, let R′′ = R′ \ {−e_{ϵ}} and R′′ = gen((R′′, P)). For each ray (r^{T}, 0)^{T} ∈ R′′, by hypothesis, we have (r^{T}, e)^{T} ∈ R so that, by Lemma A.2, (r^{T}, 0)^{T} is also a ray of R. Hence, R′′ ⊆ R. By the above observations, we obtain

∀(p^{T}, e)^{T} ∈ R′ : ∃(p^{T}, e_{0})^{T} ∈ R, ρ ∈ ℝ_{+} . (p^{T}, e)^{T} = (p^{T}, e_{0})^{T} + ρ(−e_{ϵ}). (16)

Let now p ∈ [[R′]], so that there exists (p^{T}, e)^{T} ∈ R′ such that e > 0. By applying (16), we obtain that (p^{T}, e_{0})^{T} ∈ R, where e_{0} = e + ρ > 0, proving that p ∈ [[R]] = P. As the choice of p was arbitrary, [[R′]] ⊆ P.

To complete the proof, we have to show that R′ is an ϵ-polyhedron. Condition (2) of Definition 5.2 easily follows from (16), because R is an ϵ-polyhedron: namely, we can consider the same ϵ upper bound constraint ϵ ≤ δ used for R. To prove condition (3) of Definition 5.2, let (p^{T}, e)^{T} ∈ R′. By (16), there exist (p^{T}, e_{0})^{T} ∈ R and ρ ∈ ℝ_{+} such that (p^{T}, e)^{T} = (p^{T}, e_{0})^{T} + ρ(−e_{ϵ}). As R is an ϵ-polyhedron, we also have (p^{T}, 0)^{T} ∈ R. Since we already observed that R ⊆ R′, this completes the proof.

Lemma A.8. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}, R_{1} ⇛_{Y} P_{1} and R_{2} ⇛_{Y} P_{2}. Then R_{1} ∩ R_{2} ⇛_{Y} P_{1} ∩ P_{2}.

Proof. We first prove condition (2) of Definition 5.2. Since both R_{1} and R_{2} are ϵ-polyhedra there exist δ_{1} > 0 and δ_{2} > 0 such that R_{1} ⊆ con({ϵ ≤ δ_{1}}) and R_{2} ⊆ con({ϵ ≤ δ_{2}}). Letting δ = min{δ_{1}, δ_{2}}, we have R_{1} ∩ R_{2} ⊆ con({ϵ ≤ δ}).

To prove condition (3) of Definition 5.2, let (v^{T}, e)^{T} ∈ R_{1} ∩ R_{2}. Then, as R_{1} and R_{2} are ϵ-polyhedra, (v^{T}, 0)^{T} ∈ R_{1} and (v^{T}, 0)^{T} ∈ R_{2}. Hence (v^{T}, 0)^{T} ∈ R_{1} ∩ R_{2}.

Having shown that R_{1} ∩ R_{2} is an ϵ-polyhedron, we next show that [[R_{1} ∩ R_{2}]] = P_{1} ∩ P_{2}. By hypothesis, R_{1} ⇛_{ϵ} P_{1} and R_{2} ⇛_{ϵ} P_{2}, so that, by Definition 5.2, P_{1} = [[R_{1}]] and P_{2} = [[R_{2}]]. By Definition 5.1, we have to show that v ∈ P_{1} ∩ P_{2} if and only if there exists e > 0 such that (v^{T}, e)^{T} ∈ R_{1} ∩ R_{2}. First, let v ∈ P_{1} ∩ P_{2}. Hence, by Definition 5.1, there exist e_{1}, e_{2} > 0 such that (v^{T}, e_{1})^{T} ∈ R_{1} and (v^{T}, e_{2})^{T} ∈ R_{2}. Suppose, without loss of generality, that e_{1} ≤ e_{2}. By condition (3) of Definition 5.2, (v^{T}, 0)^{T} ∈ R_{2}. Thus, since R_{2} is a convex set, (v^{T}, e_{1})^{T} ∈ R_{2}. Hence (v^{T}, e_{1})^{T} ∈ R_{1} ∩ R_{2}. Secondly, suppose that there exists e > 0 such that (v^{T}, e)^{T} ∈ R_{1} ∩ R_{2}. Then (v^{T}, e)^{T} ∈ R_{1} and (v^{T}, e)^{T} ∈ R_{2}. By Definition 5.1, v ∈ P_{1} and v ∈ P_{2}, so that v ∈ P_{1} ∩ P_{2}. It follows that [[R_{1} ∩ R_{2}]] = P_{1} ∩ P_{2}. By Definition 5.2, R_{1} ∩ R_{2} ⇛_{ϵ} P_{1} ∩ P_{2}.

We now prove that R_{1} ∩ R_{2} is a C-ϵ-polyhedron when R_{1} and R_{2} are C-ϵ-polyhedra. By Definition 5.6, for j ∈ {1, 2} we have R_{j} ⊆ con({ϵ ≥ 0}). Thus R_{1} ∩ R_{2} ⊆ con({ϵ ≥ 0}) so that, by Definition 5.6, R_{1} ∩ R_{2} is a C-ϵ-polyhedron.

To prove that R_{1} ∩R_{2} is a G-ϵ-polyhedron when R_{1} and R_{2} are G-ϵ-polyhedra, we consider two subcases. If R_{1} ∩ R_{2} = ∅, then there is nothing to prove. Suppose instead that R_{1} ∩ R_{2} ≠ ∅. Then, by Definition 5.8, −e_{ϵ} ∈ rays(R_{1}) and −e_{ϵ} ∈ rays(R_{2}). Let v′ ∈ R_{1} ∩ R_{2} and consider, for any ρ ∈ ℝ_{+}, v′_{ρ} = v′ + ρ(−e_{ϵ}). As v′ ∈ R_{1}, v′_{ρ} ∈ R_{1} and, as v′ ∈ R_{2}, v′_{ρ} ∈ R_{2}; hence v′_{ρ} ∈ R_{1} ∩ R_{2}. As this holds for any ρ ∈ ℝ_{+}, −e_{ϵ} ∈ rays(R_{1} ∩ R_{2}). Thus, by Definition 5.8, R_{1} ∩ R_{2} is a G-ϵ-polyhedra.

Lemma A.9. For j ∈ {1, 2}, let P_{j} = gen((R_{j}, P_{j}, C_{j})) be a non-empty NNC polyhedron. Then x ∈ P_{1}⊎P_{2} if and only if there exist r_{1} ∈ {0} ∪ rays(P_{1}), r_{2} ∈ {0} ∪ rays(P_{2}), x_{1} ∈ ℂ(P_{1}), x_{2} ∈ ℂ(P_{2}), and 0 ≤ σ ≤ 1 such that x = r_{1} + r_{2} + σx_{1} + (1 − σ)x_{2}, where (x_{1} ∈ P_{1} ∧ σ > 0) ∨ (x_{2} ∈ P_{2} ∧ σ < 1).

Proof. For j ∈ {1, 2}, let r_{j}, p_{j} and c_{j} be the cardinalities of R_{j}, P_{j} and C_{j}, respectively. By definition of the poly-hull operation, 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 r, p and c, respectively. (In general, we have r ≤ r_{1} + r_{2}, p ≤ p_{1} + p_{2} and c ≤ c_{1} + c_{2}, since there may be generators that occur in both generator systems.)

Suppose first that x ∈ P_{1} ⊎ P_{2}. Then, by the definition of function ‘gen’,

x = Rρ + P π + Cγ

where ρ ∈ ℝr_{+}, π ∈ ℝp_{+}, γ ∈ ℝc_{+}, ∑ π + ∑ γ = 1 and π ≠ 0. Therefore, we can also rewrite it as

x = R_{1}ρ_{1} + R_{2}ρ_{2} + P_{1}π_{1} + P_{2}π_{2} + C_{1}γ_{1} + C_{2}γ_{2}
= R_{1}ρ_{1} + R_{2}ρ_{2} + (P_{1}π_{1} + C_{1}γ_{1}) + (P_{2}π_{2} + C_{2}γ_{2}),

where ρ_{j} ∈ ℝr_{j}_{+}, π_{j} ∈ ℝp_{j}_{+} and γ_{j} ∈ ℝc_{j}_{+}, for j ∈ {1, 2}, ∑ π_{1}+∑ π_{2}+∑ γ_{1}+∑ γ_{2} = 1 and ∑ π_{1}+∑ π_{2} > 0.

It follows that either π_{1} ≠ 0 or π_{2} ≠ 0.

For each j ∈ {1, 2}, let r_{j} = R_{j}ρ_{j}, so that r_{j} is a non-negative combination of the rays of P_{j}. Note that either r_{j} = 0 (e.g., if ρ_{j} = 0) or r_{j} ∈ rays(P_{j}). If ∑ π_{1} + ∑ γ_{1} = 1 (so that π_{2} = γ_{2} = 0 and π_{1} ≠ 0), then, by the definition of function ‘gen’, we obtain x_{1} = P_{1}π_{1} + C_{1}γ_{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} = P_{2}π_{2} + C_{2}γ_{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} = \frac{1}{σ} (P_{1}π_{1} + C_{1}γ_{1}) and x_{2} = \frac{1}{1−σ} (P_{2}π_{2} + C_{2}γ_{2}). Thus x_{1} ∈ ℂ(P_{1}) and x_{2} ∈ ℂ(P_{2}). Moreover, by the definition of function ‘gen’, as π_{1} ≠ 0 or π_{2} ≠ 0, either x_{1} ∈ P_{1} or x_{2} ∈ P_{2}. Thus, in all cases we obtain

x = r_{1} + r_{2} + σx_{1} + (1 − σ)x_{2},

with r_{j} ∈ {0} ∪ rays(P_{j}) and 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 r_{j} ∈ {0} ∪ rays(P_{j}) and x_{j} ∈ ℂ(P_{j}), for j ∈ {1, 2}, and there exists 0 ≤ σ ≤ 1 such that

x = r_{1} + r_{2} + σx_{1} + (1 − σ)x_{2}, where either x_{1} ∈ P_{1} and σ > 0 or x_{2} ∈ P_{2} and σ < 1.

For j ∈ {1, 2}, there exists ϱ_{j} ∈ ℝr_{j}_{+} such that r_{j} = R_{j}ϱ_{j}; moreover, since x_{j} ∈ ℂ(P_{j}), there exist

ρ_{j} ∈ ℝr_{j}_{+}, π_{j} ∈ ℝp_{j}_{+} and γ_{j} ∈ ℝc_{j}_{+} such that x_{j} = R_{j}ρ_{j} + P_{j}π_{j} + C_{j}γ_{j}, where ∑ π_{j} + ∑ γ_{j} = 1. Thus,

x = R_{1}ϱ_{1} + R_{2}ϱ_{2} + σ(R_{1}ρ_{1} + P_{1}π_{1} + C_{1}γ_{1}) + (1 − σ)(R_{2}ρ_{2} + P_{2}π_{2} + C_{2}γ_{2})
= R_{1}(ϱ_{1} + σρ_{1}) + R_{2}(ϱ_{2} + (1 − σ)ρ_{2}) + P_{1}σπ_{1} + P_{2}(1 − σ)π_{2} + C_{1}σγ_{1} + C_{2}(1 − σ)γ_{2}.

Note that ϱ_{1} + σρ_{1} ∈ ℝr_{1}_{+}, ϱ_{2} + (1 − σ)ρ_{2} ∈ ℝr_{2}_{+}, and σ∑ π_{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 ρ ∈ ℝr_{+}, π ∈ ℝp_{+} and γ ∈ ℝc_{+} such that ∑ π + ∑ γ = 1, π ≠ 0, and x = Rρ + P π + Cγ. Then, by the definition of function ‘gen’, x ∈ P_{1} ⊎ P_{2}, completing the proof.

Lemma A.10. Letting ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}, suppose that R_{1} ⇛_{Y} P_{1} ≠ ∅ and R_{2} ⇛_{Y} P_{2} ≠ ∅. Then R_{1} ⊎ R_{2} ⇛_{Y} P_{1} ⊎ P_{2}.

Proof. For j ∈ {1, 2}, let P_{j} = gen((R_{j}, P_{j}, C_{j})), where the three components of the extended generator system have cardinalities r_{j}, p_{j} and c_{j}, respectively; similarly, let R_{j} = gen((R′_{j}, P′_{j})), with cardinalities r′_{j} and p′_{j}, respectively. Note that each R_{j} ∈ ℂℙ_{n+1} is also an NNC polyhedron in ℙ_{n+1}. Thus, we can write R_{j} = gen((R′_{j}, P′_{j}, ∅)) and observe that R_{j} = ℂ(R_{j}). By applying Lemma A.9, if (v^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, then for some r′_{1} = (r1^{T}, e′_{1})^{T} ∈ {0} ∪ rays(R_{1}), r′_{2} = (r2^{T}, e′_{2})^{T} ∈ {0} ∪ rays(R_{2}), v′_{1} = (v_{1}^{T}, e_{1})^{T} ∈ R_{1}, v′_{2} = (v_{2}^{T}, e_{2})^{T} ∈ R_{2}, and 0 ≤ σ ≤ 1, we have

(\begin{matrix}v \\ e \end{matrix}) = r′_{1} + r′_{2} + σv′_{1} + (1 − σ)v′_{2} = (\begin{matrix}r & 1 \\ e′_{1} \end{matrix}) + (\begin{matrix}r & 2 \\ e′_{2} \end{matrix}) + (\begin{matrix}σv_{1} + (1 − σ)v_{2} \\ σe_{1} + (1 − σ)e_{2} \end{matrix}) . (17)

For each j ∈ {1, 2}, since r′_{j} ∈ {0} ∪ rays(R_{j}), by Lemma A.3 we obtain e′_{j} ≤ 0.

We first show that R_{1}⊎R_{2} is an ϵ-polyhedron. As R_{1}, R_{2} are ϵ-polyhedra, by condition (2) of Definition 5.2 there exist δ_{1}, δ_{2} > 0 such that R_{1} ⊆ con({ϵ ≤ δ_{1}}) and R_{2} ⊆ con({ϵ ≤ δ_{2}}). Suppose that (v^{T}, e)^{T} ∈ R_{1}⊎R_{2} and rewrite it according to (17). By letting δ = max{δ_{1}, δ_{2}}, we obtain e_{1} ≤ δ and e_{2} ≤ δ. Since e′_{1} ≤ 0 and e′_{2} ≤ 0, we obtain e = σe_{1} + (1 − σ)e_{2} + e′_{1} + e′_{2} ≤ δ, so that R_{1} ⊎ R_{2} satisfies condition (2) of Definition 5.2.

To prove condition (3) of Definition 5.2, suppose that (v^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, so that we can rewrite it according to (17). For each j ∈ {1, 2}, as R_{j} is an ϵ-polyhedron, by Lemma A.2, (rj^{T}, 0)^{T} ∈ {0} ∪ rays(R_{j}); also, by condition (3) of Definition 5.2, (vj^{T}, 0)^{T} ∈ R_{j}. Thus, by applying again Lemma A.9, we obtain

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

Having shown that R_{1} ⊎ R_{2} is an ϵ-polyhedron, we next show that it represents P_{1} ⊎ P_{2}. By hypothesis, R_{1} ⇛_{ϵ} P_{1} and R_{2} ⇛_{ϵ} P_{2}, so that, by Definition 5.2, P_{1} = [[R_{1}]] and P_{2} = [[R_{2}]]. By Definition 5.1, we have to prove that v ∈ P_{1} ⊎ P_{2} if and only if there exists e > 0 such that (v^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}. First suppose that v ∈ P_{1} ⊎ P_{2}. Then, by Lemma A.9, there exist r_{j} ∈ {0} ∪ rays(P_{j}) and v_{j} ∈ ℂ(P_{j}), for each j ∈ {1, 2}, and 0 ≤ σ ≤ 1 such that v = r_{1} + r_{2} + σv_{1} + (1 − σ)v_{2}, where v_{1} ∈ P_{1} and σ > 0 or v_{2} ∈ P_{2} and σ < 1. Suppose, without loss of generality, that v_{1} ∈ P_{1} and σ > 0. By Definition 5.1, there exists e_{1} > 0 such that (v1^{T}, e_{1})^{T} ∈ R_{1}. As R_{2} ⇛_{ϵ} P_{2} and v_{2} ∈ ℂ(P_{2}), by Lemma A.5, we obtain (v2^{T}, 0)^{T} ∈ R_{2}. Moreover, by Lemma A.6, for j ∈ {1, 2} we have (rj^{T}, 0)^{T} ∈ {0} ∪ rays(R_{j}). Therefore, by letting

(\begin{matrix}v \\ e_{1} \end{matrix}) = (\begin{matrix}r & 1 \\ 0 \end{matrix}) + (\begin{matrix}r & 2 \\ 0 \end{matrix}) + σ (\begin{matrix}v & 1 \\ e_{1} \end{matrix}) + (1 − σ) (\begin{matrix}v & 2 \\ 0 \end{matrix}) ,

we obtain, again by Lemma A.9, (v^{T}, e_{1})^{T} ∈ R_{1} ⊎R_{2}, where e_{1} > 0 as required. Secondly, suppose that there exists e > 0 such that (v^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, so that we can rewrite it according to (17). 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. By Definition 5.1, we have v_{1} ∈ P_{1}. By hypothesis, R_{2} ⇛_{ϵ} P_{2}. Thus, as (v2^{T}, e_{2})^{T} ∈ R_{2} for some e_{2} ∈ ℝ, by condition (3) of Definition 5.2, (v2^{T}, 0)^{T} ∈ R_{2}. Therefore, by Lemma A.5, v_{2} ∈ ℂ(P_{2}). Thus, by Lemma A.9, v = σv_{1} + (1 − σ)v_{2} + r_{1} + r_{2} ∈ P_{1} ⊎ P_{2}. Therefore R_{1} ⊎ R_{2} ⇛_{ϵ} P_{1} ⊎ P_{2}.

To prove that R_{1} ⊎ R_{2} is a C-ϵ-polyhedron when R_{1} and R_{2} are C-ϵ-polyhedra, we have to show that R_{1} ⊎ R_{2} ⊆ con({ϵ ≥ 0}). Let (v^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, so that we can rewrite it according to (17). As R_{1} and R_{2} are both C-ϵ-representations, we obtain e_{1} ≥ 0 and e_{2} ≥ 0; moreover, by Lemma A.3 we have e′_{1} = 0 and e′_{2} = 0. Thus e = σe_{1} + (1 − σ)e_{2} + e′_{1} + e′_{2} satisfies e ≥ 0.

To prove that R_{1} ⊎ R_{2} is a G-ϵ-polyhedron when R_{1} and R_{2} are G-ϵ-polyhedra, since R_{1} ⊎ R_{2} ≠ ∅, we have to show that −e_{ϵ} is a ray in R_{1} ⊎ R_{2}. To this end, it is sufficient to observe that all the rays of R_{1} are also rays of R_{1} ⊎ R_{2} and −e_{ϵ} is a ray of R_{1}, because R_{1} is a non-empty G-ϵ-polyhedron.

Lemma A.11. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}} and suppose that R ⇛_{Y} P. Let also f =^{def} λx ∈ ℝ^{n} . Ax + b be any affine transformation defined on ℙ_{n} and define

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})

to be the corresponding affine transformation on ℂℙ_{n+1}. Then g(R) ⇛_{Y} f(P).

Proof. Observe that, by definition of g, for any (v^{T}, e)^{T} ∈ R we have g((v^{T}, e)^{T}) = (f(v)^{T}, e)^{T}. Thus the coefficient of the ϵ coordinate is not affected at all by the affine transformation, so that conditions (2) and (3) of Definition 5.2 and f(P) = [[g(R)]] follow trivially from the hypothesis. Thus, g(R) ⇛_{ϵ} f(P).

To complete the proof, we have to consider the cases when ⇛_{Y} ∈ {⇛_{C}, ⇛_{G}}. First note that, if R = ∅, then also g(R) = ∅ and there is nothing to prove. Now assume R ≠ ∅. If R is a C-ϵ-polyhedron, then all the points in R satisfy the constraint ϵ ≥ 0. Since the ϵ coordinates are unaffected by the affine transformation, all the points in g(R) satisfy the constraint ϵ ≥ 0, so that g(R) is a C-ϵ-polyhedron too. Otherwise, R is a non-empty G-ϵ-polyhedron, so that −e_{ϵ} ∈ rays(R). We have g(R) ≠ ∅ and the ray is unaffected by the affine transformation, so that −e_{ϵ} ∈ rays(g(R)).

Proof of Proposition 5.11 on page 12. Items (1), (2) and (3) follow from Lemmas A.8, A.10 and A.11, respectively.

A.5. Proofs of the Results Stated in Section 6

The proof of Proposition 6.3 requires a few preliminary lemmas.

Lemma A.12. Let R = con(C) ∈ ℂℙ_{n+1} be a non-empty ϵ-polyhedron. Then −e_{ϵ} ∈ rays(R) if and only if C = C_{>} ∪ C_{≥} ∪ C_{ϵ}.

Proof. Suppose that −e_{ϵ} ∈ rays(R). Let (v^{T}, e)^{T} ∈ R. Then, for all ρ ∈ ℝ_{+}, (v^{T}, e)^{T} + ρ(−e_{ϵ}) ∈ R. If β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C, we have ⟨a, v⟩ + s · (e − ρ) ≥ b for all ρ ∈ ℝ_{+}. Thus s ≤ 0. Since our choice of β ∈ C was arbitrary, we obtain C = C_{>} ∪ C_{≥} ∪ C_{ϵ}.

Now suppose C = C_{>} ∪ C_{≥} ∪ C_{ϵ}. This means that, if β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C, then s ≤ 0. As R is nonempty, there exists a point p = (v^{T}, e)^{T} ∈ R. Also, since s ≤ 0, for all ρ ∈ ℝ_{+} we have ⟨a, v⟩ + s · (e − ρ) ≥ b. As our choice of β ∈ C is arbitrary, p + ρ(−e_{ϵ}) satisfies all the constraints in C and is therefore in R. Thus −e_{ϵ} ∈ rays(R), because also the choice of p ∈ R was arbitrary.

Lemma A.13. Let R = con(C) ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P ≠ ∅. Let also C′ = C_{>} ∪ C_{≥} ∪ C_{ϵ} ∪ {ϵ ≥ 0} and C′′ = C ∪ {ϵ ≥ 0}. Then con(C′) ⇛_{ϵ} P and con(C′) = con(C′′).

Proof. Let R′ = con(C′), R′′ = con(C′′), and C^{∗} = C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}). Note that, by Definition 1, we have P = [[R]] = [[R′′]]. Moreover, by Proposition 5.3, since R is an ϵ-polyhedron, R′′ is also an ϵ-polyhedron. It remains for us to prove that R′ = R′′. Observe that, since C′ ⊆ C′′, R′′ ⊆ R′.

We now show that R′ ⊆ R′′. Let p = (v^{T}, e)^{T} ∈ R′ so that e ≥ 0. By hypothesis, P ≠ ∅ so that, as P = [[R]]′′, by Definition 5.1, there exists a point q = (w^{T}, e_{w})^{T} ∈ R′′ such that e_{w} > 0. By hypothesis, both p and q must satisfy every constraint in C′ = C_{>} ∪ C_{≥} ∪ C_{ϵ} ∪ {ϵ ≥ 0}. We show that p also satisfies all the constraints in C^{∗}, so that p ∈ R′′. Suppose, by contraposition, that p does not satisfy a constraint in C^{∗}. Let { σp + (1 − σ)q | 0 ≤ σ ≤ 1 } be the set of points lying on the segment between p and q. As p ∉ R′′ and q ∈ R′′, there must exists a minimum value 0 ≤ τ < 1 such that p′ = (v_{τ} , e_{τ}) = τp + (1 − τ)q ∈ R′′, so that p′ saturates some constraint β^{∗} = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C^{∗}. Note that, as e ≥ 0, e_{w} > 0 and τ < 1, we have e_{τ} > 0. Also, by definition of C^{∗}, we have s > 0. As a consequence, (vτ^{T}, 0)^{T} does not satisfy β^{∗}, which implies (vτ^{T}, 0)^{T} ∉ R′′. However, since R′′ is an ϵ-polyhedron, this contradicts condition (3) of Definition 5.2. Thus p ∈ R′′. As the choice of p ∈ R′ was arbitrary, R′ ⊆ R′′.

Lemma A.14. Let R = con(C) ∈ ℂℙ_{n+1} be an ϵ-polyhedron. Let p ∈ R be such that p = (v^{T}, e)^{T}, where e > 0, and consider p_{0} = (v^{T}, 0)^{T}. Then sat con(p_{0}, C_{>} ∪ C_{≥} ∪ C_{ϵ}) = sat con(p, C_{≥}).

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

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

Lemma A.15. Let (C, G) ≡ R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. Let β ∈ C_{>} be such that β = (⟨a, x⟩+s·ϵ ≥ b) and consider β_{0} = (⟨a, x⟩ + 0 · ϵ ≥ b). Then sat gen(β_{0}, (G_{R}, G_{C})) = sat gen(β, (G_{R}, G_{C})).

Proof. If p = (v^{T}, e)^{T} ∈ G_{R} ∪ G_{C}, then e = 0. Thus ⟨a, v⟩ + s · e = 0 if and only if ⟨a, v⟩ + 0 · e = 0. Similarly, ⟨a, v⟩ + s · e = b if and only if ⟨a, v⟩ + 0 · e = b. Thus, if p is a ray encoding or p is a closure point encoding, p saturates β if and only if it saturates β_{0}. As p is an arbitrary ray or closure point encoding in G_{R} ∪ G_{C}, we have the required result.

Lemma A.16. Let (C, G) ≡ R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. Let also β ∈ C_{>} be saturated by the point (v^{T}, 0)^{T} ∈ R. Then (v^{T}, 0)^{T} ∈ gen((G_{R}, G_{C})).

Proof. Let G = (R, P) and β = (⟨a, x⟩ + s · ϵ ≥ b). Then, as β ∈ C_{>}, s < 0. Since (v^{T}, 0)^{T} ∈ R saturates β, it holds ⟨a, v⟩ = b, so that for all e > 0 we have (v^{T}, e)^{T} ∉ R. Therefore we can apply Lemma A.4, taking e_{max} = 0, so that we obtain (v^{T}, 0)^{T} ∈ gen((G_{R}, G_{P} ∪ G_{C})). By definition of ‘gen’, we conclude (v^{T}, 0)^{T} ∈ gen((G_{R}, G_{C})).

Lemma A.17. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}. Let (C, G) ≡ R ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{Y} P ≠ ∅. If β is a strongly ϵ-redundant constraint in C, then con(C′) ⇛_{Y} P, where C′ = (C \ {β}) ∪ {ϵ ≤ 1}.

Proof. Suppose that β = (⟨a, x⟩ + s · ϵ ≥ b) is strongly ϵ-redundant in C so that, by Definition 6.2, we have β ∈ C_{>}, a ≠ 0 and s < 0. Let R′ = con(C′). As P ≠ ∅, by Definition 5.1, there exists (w^{T}, e′_{w})^{T} ∈ R for some e′_{w} > 0. As R is an ϵ-polyhedron, by condition (3) of Definition 5.2, (w^{T}, 0)^{T} ∈ R. Thus, as R is a convex set, for some 0 < e_{w} ≤ 1, (w^{T}, e_{w})^{T} ∈ R. Since e_{w} ≤ 1, we also have (w^{T}, e_{w})^{T} ∈ R′.

We show that, for all (v^{T}, e)^{T} ∈ R′ \ R,

e ≥ 0,  (18)
(v^{T}, 0)^{T} ∈ R,  (19)
(v^{T}, 0)^{T} does not saturate β.  (20)

We first prove (18). To do this we assume that e < 0 and derive a contradiction. Consider the line segment between (v^{T}, e)^{T} ∈ R′ \ R and (w^{T}, 0)^{T} ∈ R′ ∩ R. Then there must be a point (v1^{T}, e_{1})^{T} ∈ R on this segment that saturates β. As (w^{T}, e_{w})^{T} satisfies β, e_{w} > 0 and s < 0, (w^{T}, 0)^{T} does not saturate β so that v_{1} ≠ w and e_{1} < 0. Thus (v1^{T}, 0)^{T} does not satisfy β and hence (v1^{T}, 0)^{T} ∉ R; contradicting condition (3) of Definition 5.2. Therefore (18) holds.

We next show that (19) and (20) hold. Consider the closed segment between (v^{T}, e)^{T} ∈ R′ \ R and (w^{T}, e_{w})^{T} ∈ R′ ∩ R. As R′ is a convex set, for each 0 ≤ σ ≤ 1, we have (vσ^{T}, e_{σ})^{T} ∈ R′, where

(vσ^{T}, e_{σ})^{T} = σ(v^{T}, e)^{T} + (1 − σ)(w^{T}, e_{w})^{T}.  (21)

Let τ be the maximum value between 0 and 1 such that (vτ^{T}, 0)^{T} ∈ R. Observe that, as e_{w} > 0 and, by (18), e ≥ 0, e_{τ} ≥ 0. However, when e_{τ} = 0, we have e = 0 and τ = 1 contradicting the assumption that (v^{T}, e)^{T} ∉ R. It follows that e_{τ} > 0. Suppose that (vτ^{T}, 0)^{T} saturates β. Then, by Lemma A.16, (vτ^{T}, 0)^{T} ∈ gen((G_{R}, G_{C})) so that sat gen(β, (G_{R}, G_{C})) ⋢ (G_{R}, ∅). As a consequence, since by hypothesis β is strongly ϵ-redundant in C, by Definition 6.2 there exists β′ = (⟨a′, x⟩ + s′ · ϵ ≥ b′) ∈ C′_{>} such that

sat gen(β, (G_{R}, G_{C})) ⊑ sat gen(β′, G).

Thus the point (vτ^{T}, 0)^{T} also saturates β′. Since, by (21), (v^{T}, e)^{T} and (w^{T}, e_{w})^{T} both satisfy β′, (vτ^{T}, e_{τ})^{T}, also satisfies β′ so that, as s′ < 0, we have e_{τ} ≤ 0 which is a contradiction. Thus (vτ^{T}, 0)^{T} does not saturate β. For all τ < σ ≤ 1, (vσ^{T}, 0)^{T} ∉ R so that, as R is an ϵ-polyhedron, by condition (3) of Definition 5.2, (vσ^{T}, e_{σ})^{T} ∉ R. Thus, as (vτ^{T}, 0)^{T} ∈ R does not saturate β, we must have τ = 1. Hence, by (21), (v^{T}, 0)^{T} = (vτ^{T}, 0)^{T} and therefore (19) and (20) hold.

To prove R′ ⇛_{ϵ} P, we show that R′ is an ϵ-polyhedron and [[R]] = [[R′]].

By taking δ = 1, the inclusion R′ ⊆ con({ϵ ≤ δ}) holds trivially, because the constraint ϵ ≤ 1 has been explicitly added in C′. Thus condition (2) of Definition 5.2 holds. By (19), if (v^{T}, e)^{T} is an arbitrary point in R′, we have (v^{T}, 0)^{T} ∈ R. Since (v^{T}, 0)^{T} obviously satisfies the constraint ϵ ≤ 1, we have (v^{T}, 0)^{T} ∈ R′, so that condition (3) of Definition 5.2 also holds and R′ is an ϵ-polyhedron.

To prove the inclusion [[R]] ⊆ [[R′]], let v ∈ [[R]]. Thus, there exists e > 0 such that (v^{T}, e)^{T} ∈ R. By condition (3) of Definition 5.2, we also have (v^{T}, 0)^{T} ∈ R so that, as R is a convex set, there exists 0 < e′ ≤ 1 such that (v^{T}, e′)^{T} ∈ R. Note that (v^{T}, e′)^{T} satisfies all the constraints in C and it also satisfies the constraint ϵ ≤ 1; as a consequence, (v^{T}, e′)^{T} ∈ 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′. By (19) and (20), we know that ⟨a, v⟩ > b. Thus, by letting e′ = min(\{e, \frac{b−⟨a,v⟩}{s}\}), we obtain e′ > 0 and (v^{T}, e′)^{T} ∈ R. Thus v ∈ [[R]].

Suppose next that R ⇛_{C} P. Thus R ⊆ con({ϵ ≥ 0}). By the first part of the proof, R′ ⇛_{ϵ} P so that it remains to show that R′ ⊆ con({ϵ ≥ 0}). Suppose (u^{T}, e_{u})^{T} ∈ R′. If (u^{T}, e_{u})^{T} ∈ R, then, as R is a C-ϵ-polyhedron, e_{u} ≥ 0. On the other hand, if (u^{T}, e_{u})^{T} ∈ R′ \ R, then, by (18), we again have e_{u} ≥ 0. Thus con(C′) ⊆ con({ϵ ≥ 0}) and R′ ⇛_{C} P.

Finally, suppose that R ⇛_{G} P. By the first part of the proof R′ ⇛_{ϵ} P. Note that, since P ≠ ∅, we also have R ≠ ∅ and R′ ≠ ∅. Thus, by Definition 5.8, −e_{ϵ} ∈ rays(R) and, to complete the proof, we need to show that −e_{ϵ} ∈ rays(R′). By Lemma A.12, C = C_{>} ∪ C_{≥} ∪ C_{ϵ}. Since (ϵ ≤ 1) ∈ C′_{ϵ}, we also have C′ = C′_{>} ∪ C′_{≥} ∪ C′_{ϵ} so that, again by Lemma A.12, −e_{ϵ} ∈ rays(R′). Thus, R′ ⇛_{G} P.

Lemma A.18. Let (C, G) ≡ R ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P ≠ ∅ and {p, p′} ⊆ G_{P}, where sat con(p, C_{≥}) ⊆ sat con(p′, C_{≥}). Let also G = (R, P), G′ = (R, P \ {p}) and R′ = gen(G′). Then

R ∩ con({ϵ = 0}) = R′ ∩ con({ϵ = 0}).

Proof. Since G′ ⊏ G, we have R′ ⊆ R. To prove R ⊆ R′, we assume that q = (w^{T}, 0)^{T} ∈ R and show that q is also in R′.

Let p = (v^{T}, e_{v})^{T} and p′ = (y^{T}, e_{y})^{T} so that, since they are both in G_{P}, we obtain e_{v} > 0 and e_{y} > 0. Consider p_{0} = (v^{T}, 0)^{T} and p′_{0} = (y^{T}, 0)^{T}. As R is an ϵ-polyhedron, by condition (3) of Definition 5.2, we have {p_{0}, p′_{0}} ⊆ R. Thus, p_{0} can be rewritten as p_{0} = σp + (1 − σ)p_{−}, where 0 ≤ σ ≤ 1 and the point p_{−} = (v^{T}, e_{−})^{T} is such that p_{−} ∈ gen(G′) = R′. Since e_{v} > 0, we obtain e_{−} ≤ 0. Since p′ ∈ R′, which is a convex set, then R′ contains the whole segment [p_{−}, p′] and, in particular, by taking q_{1} = (w1^{T}, 0)^{T} to be the point on this segment having a zero ϵ coordinate, we obtain q_{1} ∈ R′ (note that there exists exactly one such a q_{1}, because e_{y} > 0). Thus, by applying Lemma A.14 to p and p′ we obtain sat con(p_{0}, C_{≥}) = sat con(p, C_{≥}) and sat con(p′_{0}, C_{≥}) = sat con(p′, C_{≥}) so that, by hypothesis, sat con(p_{0}, C_{≥}) ⊆ sat con(p′_{0}, C_{≥}). Thus, as q_{1} lies on the segment [p_{0}, p′_{0}], we obtain sat con(p_{0}, C_{≥}) ⊆ sat con(q_{1}, C_{≥}) and hence,

sat con(p, C_{≥}) ⊆ sat con(q_{1}, C_{≥}). (22)

Let r = q − q_{1}. If r = 0, then q = q_{1} ∈ R′. Otherwise, let r ≠ 0. By hypothesis, rays(R) = rays(R′). Thus, if r ∈ rays(R), we also have r ∈ rays(R′) so that q = q_{1} + r ∈ R′.

Suppose now that r ≠ 0 and that r ∉ rays(R). Then there must exist a minimum value 0 < ρ_{2} < 1 such that, for all ρ > ρ_{2}, we have q_{1} + ρr ∉ R. Thus let q_{2} = q_{1} + ρ_{2}r = (w2^{T}, 0)^{T} ∈ R. Note that, as ρ_{2} > 0, q_{2} ≠ q_{1}. Thus, by choice of ρ_{2}, there must exist a constraint β ∈ C that saturates q_{2} but not q_{1}. Since no constraint in C_{ϵ} can be saturated by q_{2}, we have β ∉ C_{ϵ}. Suppose that β ∈ C_{>}. Then, by Lemma A.16, q_{2} ∈ gen((G_{R}, G_{C})); since (G_{R}, G_{C}) ⊑ G′, we obtain q_{2} ∈ R′. Suppose now that β ∈ C_{≥}; then, as β ∉ sat con(q_{1}, C_{≥}), by (22), we obtain β ∉ sat con(p, C_{≥}). Similarly, supposing now β ∈ C \(C_{>} ∪C_{≥} ∪C_{ϵ}), then s > 0 so that, as p_{0} ∈ R, β ∉ sat con(p, C). In both cases, as β ∈ sat con(q_{2}, C), q_{2} is generated by sat gen(β, (G_{R}, G_{C})), so that q_{2} ∈ gen(G′) = R′. Thus in all cases q_{2} ∈ R′. As q lies on the segment [q_{1}, q_{2}] and R′ is a convex set, we have q ∈ R′ as required.

Lemma A.19. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}. Let (C, G) ≡ R ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{Y} P ≠ ∅. If p is a strongly ϵ-redundant generator in G = (R, P), then gen(G′) ⇛_{Y} P, where G′ = (R, P \ {p}).

Proof. Let R′ = gen(G′) and P′ = P \{p}, so that G′ = (R, P′). Note that G′ ⊑ G and hence, as the function ‘gen’ is monotonic, R′ ⊆ R.

Suppose that p = (v^{T}, e)^{T} is strongly ϵ-redundant in G so that, by Definition 6.2, p ∈ P, e > 0 and there exists a point p′ = (y^{T}, e′)^{T} such that p′ ∈ P′, e′ > 0 and

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

Note that p′ ∈ R′. Letting p_{0} = (v^{T}, 0)^{T} and p′_{0} = (y^{T}, 0)^{T}, by condition (3) of Definition 5.2, we have {p_{0}, p′_{0}} ⊆ R.

As (23) holds, we can use Lemma A.18, to obtain that, for all w ∈ ℝ^{n},

(w^{T}, 0)^{T} ∈ R ⟺ (w^{T}, 0)^{T} ∈ R′. (24)

In order to show that R′ ⇛_{ϵ} P, we first prove that R′ is an ϵ-polyhedron. Consider condition (2) of Definition 5.2. As R′ ⊆ R, R′ satisfies condition (2) by taking the same value δ used for R. Consider now condition (3) of Definition 5.2. Let (w^{T}, e_{w})^{T} ∈ R′. Since R′ ⊆ R, we have (w^{T}, e_{w})^{T} ∈ R; since R is an ϵ-polyhedron, (w^{T}, 0)^{T} ∈ R. Then, by (24), we obtain (w^{T}, 0)^{T} ∈ R′. Thus R′ is an ϵ-polyhedron.

To show that R′ is an ϵ-polyhedron for P, it remains to prove that [[R]] = [[R′]]. Since R′ ⊆ R, the inclusion [[R′]] ⊆ [[R]] holds by monotonicity of function [[·]]. To prove the other inclusion, suppose that w ∈ [[R]]. Then, by Definition 5.1, there exists e_{w} > 0 such that q = (w^{T}, e_{w})^{T} ∈ R. By condition (3) of Definition 5.2, we obtain q_{0} = (w^{T}, 0)^{T} ∈ R and hence, by (24), q_{0} ∈ R′. As q ∈ R, by Theorem 4.4 there exist 0 ≤ π ≤ 1 and p_{1} ∈ R′ such that q = πp + (1 − π)p_{1}. If π = 0, then q = p_{1} ∈ R′; by Definition 5.1, w ∈ [[R′]] as required. Suppose now that π > 0; then sat con(q, C) ⊆ sat con(p, C). Thus, by (23), we obtain sat con(q, C_{≥}) ⊆ sat con(p′, C). By applying Lemma A.14 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).  (25)

Now let β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ (C_{>} ∪ C_{≥} ∪ C_{ϵ}) \ sat con(q, C). Then ⟨a, w⟩ > b. Let

ρ_{c} = \begin{cases}\frac{⟨a,y⟩−⟨a,w⟩}{⟨a,y⟩−b} & if ⟨a, y⟩ > ⟨a, w⟩; \\ 1 & otherwise; \end{cases}  q_{c} = (1 + ρ_{c})q_{0} − ρ_{c}p′_{0}.

Then 0 < ρ_{c} ≤ 1 and q_{c} = (wc^{T}, 0)^{T} satisfies β. Let β vary in the set of constraints (C_{>}∪C_{≥}∪C_{ϵ})\sat con(q, C) and take ρ > 0 to be the minimum of all the ρ_{c} obtained as above. Consider the affine combination

q_{ρ} = (1 + ρ)q_{0} − ρp′_{0}.

Then q_{ρ} = (wρ^{T}, 0)^{T} satisfies all the constraints in (C_{>} ∪C_{≥} ∪C_{ϵ})\sat con(q, C). As q_{ρ} is an affine combination of q_{0} and p′_{0}, it is on the line passing through these two points and therefore, by (25), saturates every constraint in sat con(q, C). Thus sat con(q_{ρ}, C_{>} ∪C_{≥} ∪C_{ϵ}) = sat con(q, C) so that q_{ρ} satisfies every constraint in sat con(q, C). By Lemma A.13, q_{ρ} also satisfies every constraint in C \(C_{>} ∪C_{≥} ∪C_{ϵ}). Therefore q_{ρ} satisfies every constraint in C so that q_{ρ} ∈ R and hence, by (24), q_{ρ} ∈ R′. Letting σ = \frac{1}{1+ρ} we obtain 0 < σ < 1 and w = σw_{ρ} + (1 − σ)y. Thus (w^{T}, (1 − σ)e′)^{T} = σq_{ρ} + (1 − σ)p′ ∈ R′. As e′ > 0 and σ < 1, we have (1 − σ)e′ > 0 and hence, by Definition 5.1, w ∈ [[R′]] as required.

Suppose next that R ⇛_{C} P. By the first part of the proof R′ ⇛_{ϵ} P. By Definition 5.6, R ⊆ con({ϵ ≥ 0}). Since R′ ⊆ R, we also obtain R′ ⊆ con({ϵ ≥ 0}), so that, by Definition 5.6, R′ ⇛_{C} P.

Finally, suppose that R ⇛_{G} P. By the first part of the proof, R′ ⇛_{ϵ} P. By hypothesis, G′ = (R, P \{p}) so that rays(R) = rays(R′). Since R ≠ ∅, by Definition 5.8, we have that −e_{ϵ} ∈ rays(R). Thus −e_{ϵ} ∈ rays(R′) and R′ ⇛_{G} P, as required.

Proof of Proposition 6.3 on page 16. Properties (6) and (7) follow from Lemmas A.17 and A.19, respectively.

Proof of Proposition 6.4 on page 16. Since, by hypothesis P ≠ ∅, we can apply Lemma A.5 twice to obtain

(v^{T}, 0)^{T} ∈ R ⟺ v ∈ ℂ(P) ⟺ (v^{T}, 0)^{T} ∈ R′. (26)

To prove property (8), let β = (⟨a, x⟩+0·ϵ ≥ b) be a non-strict inequality encoding in C and q = (v^{T}, e)^{T} be any point of R′. By condition (3) of Definition 5.2, q_{0} = (v^{T}, 0)^{T} ∈ R′ so that, by (26), we have q_{0} ∈ R. In particular, q_{0} satisfies β and, since the coefficient of ϵ in β is 0, q also satisfies β. As the choice of q ∈ R′ is arbitrary, R′ ⊆ con({β}).

To prove property (9), let r = (s^{T}, 0)^{T} ∈ G_{R}. By hypothesis, R is not empty; thus, considering any q = (v^{T}, e)^{T} ∈ R, by condition (3) of Definition 5.2, we obtain q_{0} = (v^{T}, 0)^{T} ∈ R. Since r ∈ rays(R), for all ρ ∈ ℝ_{+} we also have

q_{ρ} = q_{0} + 2ρr = ((v + 2ρs)^{T}, 0)^{T} ∈ R.

By (26), we have q_{0} ∈ R′ and q_{ρ} ∈ R′, for all ρ ∈ ℝ_{+}. Thus, for all ρ ∈ ℝ_{+},

q′_{ρ} = q + ρr = 0.5q + 0.5q_{ρ} ∈ R.

Thus r ∈ rays(R′).

To prove property (10), let p ∈ G_{C}, so that p = (v^{T}, 0)^{T} ∈ R. Then, by (26), p ∈ R′ as required.

The proof of Proposition 6.5 is based on some preliminary lemmas. In the following proofs, for each (strict or non-strict) linear constraint β = (⟨a, x⟩ ▷◁ b), where a ∈ ℝ^{n} \ {0} and ▷◁ ∈ {≥, >}, the corresponding

non-strict constraint is denoted by geq(β) =^{def} (⟨a, x⟩ ≥ b). Similarly, for each constraint system C, we define

geq(C) =^{def} { geq(β) | β ∈ C }.

Lemma A.20. Let con(C) = R ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P ≠ ∅. Then the constraint (⟨a, x⟩ + s · ϵ ≥ b) ∈ C is singular for R if and only if s = 0 and (⟨a, x⟩ ≥ b) ∈ con enc(C) is singular for P.

Proof. Suppose that β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C is singular for R. Then every point in R must saturate β. As P ≠ ∅, by Definition 5.1, there exists a point (w^{T}, e)^{T} ∈ R with e ≠ 0; by condition (3) of Definition 5.2, we also have (w^{T}, 0)^{T} ∈ R; since both these points saturate β, it must be s = 0. By Definition 5.4, we have β_{1} = (⟨a, x⟩ ≥ b) ∈ con enc(C). Let v ∈ P so that, by Definition 5.1 and 5.2, (v^{T}, 0)^{T} ∈ R; as β is singular, (v^{T}, 0)^{T} saturates β so that v saturates β_{1}. As v ∈ P was arbitrary, every point in P saturates β_{1}; and hence β_{1} is singular for P.

Conversely, suppose there is a constraint β_{1} ∈ con enc(C) that is singular for P ≠ ∅; thus, β_{1} must be nonstrict so that, for some a ∈ ℝ^{n} and b ∈ ℝ, β_{1} = (⟨a, x⟩ ≥ b). By Definition 5.4, β = (⟨a, x⟩ + 0 · ϵ ≥ b) ∈ C. As β_{1} is singular for P, every point v ∈ ℂ(P) saturates β_{1}; thus every point (v^{T}, 0)^{T} ∈ R saturates β. By condition (3) of Definition 5.2, (v^{T}, e)^{T} ∈ R only if (v^{T}, 0)^{T} ∈ R; thus every point in R saturates β; and hence β is singular for R.

Lemma A.21. Let R = con(C) ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P ≠ ∅ and suppose that C is in minimal and orthogonal form, but not in ϵ-minimal form. Then C contains a strongly ϵ-redundant constraint.

Proof. Suppose R = gen(G), where G = (R, P). Let C_{1} = con enc(C) and G_{1} = (R_{1}, P_{1}, C_{1}) = gen enc(G). It follows from Proposition 5.5 that P = con(C_{1}) = gen(G_{1}); also, ℂ(P) = con(geq(C_{1})) = gen((R_{1}, P_{1} ∪ C_{1})).

Let eq(C) = eq(R) ∩ C and eq(C_{1}) = eq(P) ∩ C_{1} so that, by Lemma A.20, eq(C_{1}) = con enc(eq(C)). Let also ineq(C) = C \ eq(C) and ineq(C_{1}) = C_{1} \ eq(C_{1}). As P ≠ ∅, eq(C_{1}) contains no strict constraints so that, by Definition 5.4, we also have ineq(C_{1}) = con enc(ineq(C)). Since C is in orthogonal form, for all β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ eq(C) and β′ = (⟨a′, x⟩ + s′ · ϵ ≥ b′) ∈ ineq(C) we have ⟨slope(β), slope(β′)⟩ = 0; by Lemma A.20, s = 0 and hence ⟨a, a′⟩ = 0, so that C_{1} is in orthogonal form too.

As C is not in ϵ-minimal form, by Definition 6.1, C_{1} is not in minimal form. Thus there exists a constraint η = (⟨a, x⟩ ▷◁ b) ∈ C_{1}, where ▷◁ ∈ {≥, >}, which is redundant for C_{1}. By Definition 5.4, there exists s ≤ 0 such that β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C. We distinguish two main cases:

Case 1. geq(η) is saturated by none of the closure points of P; Case 2. geq(η) is saturated by at least one closure point of P.

Consider first Case 1. By the assumption for this case, we obtain sat gen(geq(η), (R_{1}, P_{1}∪C_{1})) ⊑ (R_{1}, ∅). It is easy to observe that η is non-singular for P, because any singular constraint has to be saturated by all the points of ℂ(P) ≠ ∅, including those in P_{1} ∪ C_{1}. We now show that η is a strict constraint. To do this we assume by contraposition η is non-strict. Thus η = geq(η) and, by Definition 5.4, s = 0. Since no point in P_{1} ∪ C_{1} saturates η, then no point in P saturates β. Thus β is redundant in C, contradicting the hypothesis that C is in minimal form. Therefore, η is a strict constraint, so that, by Definition 5.4, s < 0 and β ∈ C_{>}. The above saturation assumption implies sat gen(β, (G_{R}, G_{C})) ⊑ (G_{R}, ∅) and hence, by Definition 6.2, β is strongly ϵ-redundant in C.

Consider now Case 2. As η is redundant in C_{1} and geq(η) is saturated by at least one closure point of P, there exists k > 0 such that a = ∑_{i=1}^{k} ρ_{i}a_{i} and b = ∑_{i=1}^{k} ρ_{i}b_{i} where, for 1 ≤ i ≤ k, we have ρ_{i} > 0, η_{i} = (⟨a_{i}, x⟩ ▷◁_{i} b_{i}) ∈ C_{1} \ {η} and ▷◁_{i} ∈ {≥, >}. Therefore, for 1 ≤ i ≤ k, we have

sat gen(geq(η), (R_{1}, P_{1} ∪ C_{1})) ⊑ sat gen(geq(η_{i}), (R_{1}, P_{1} ∪ C_{1})). (27)

By Definition 5.4, for 1 ≤ i ≤ k, there exists s_{i} ≤ 0 such that β_{i} = (⟨a_{i}, x⟩ + s_{i} · ϵ ≥ b_{i}) ∈ C \ {β}.

Suppose first that {η_{1}, …, η_{k}} ⊆ eq(C_{1}) so that η ∈ eq(C_{1}). By Lemma A.20, β ∈ eq(C), s = 0 and, for each 1 ≤ i ≤ k, β_{i} ∈ eq(C) \ {β} and s_{i} = 0. As a consequence, slope(β) = ∑_{i=1}^{k}(ρ_{i} slope(β_{i})) so that β is redundant in eq(C); contradicting the hypothesis that C is in minimal form. Thus {η_{1}, …, η_{k}} \ eq(C_{1}) ≠ ∅.

It follows that {η_{1}, …, η_{k}} ∩ ineq(C_{1}) ≠ ∅, so that η ∈ ineq(C_{1}) and hence, by Lemma A.20, β ∈ ineq(C). Since, by the hypothesis for this case, geq(η) is saturated by at least one closure point of P, if η is a strict constraint, then at least one constraint in {η_{1}, …, η_{k}}∩ineq(C_{1}) must be strict. Thus we will assume, without losing generality, that η_{k} ∈ ineq(C_{1}) and η_{k} is strict if η is strict. By Lemma A.20, we have β_{k} ∈ ineq(C)\{β}.

We show that η is a strict constraint. To do this we assume by contraposition η is non-strict. Thus η = geq(η) and, by Definition 5.4, s = 0. Let β′_{k} = (⟨a_{k}, x⟩ + 0 · ϵ ≥ b_{k}); by Proposition 5.3, R ⊆ con({β′_{k}}), so that β′_{k} is a valid constraint for R. Consider the generator systems H = (R_{β}, P_{β}) = sat gen(β, G) and H′_{k} = (R′_{k}, P′_{k}) = sat gen(β′_{k}, G) defined by the saturators of β and β′_{k}; we now prove that H ⊑ H′_{k}. Let r = (v^{T}, e_{v})^{T} ∈ R_{β}. As s = 0, v saturates η. If v = 0, then we trivially obtain r ∈ R′_{k}. Suppose now that v ≠ 0; thus, by Lemma A.2, we have (v^{T}, 0)^{T} ∈ rays(R) and, by Lemma A.6, v ∈ rays(P), which also implies v ∈ rays(ℂ(P)). Since v saturates η, it can also be obtained as a non-negative combination of the rays in R_{1} that saturate η so that, by (27), v also saturates geq(η_{k}). As a consequence, r saturates β′_{k} and hence r ∈ R′_{k}. Now let p = (v^{T}, e_{v})^{T} ∈ P_{β}. By Definition 5.2, p_{0} = (v^{T}, 0)^{T} ∈ R so that, by Lemma A.5, v ∈ ℂ(P). As s = 0, v saturates η. Thus, by (27), v also saturates geq(η_{k}), so that p saturates β′_{k} and p ∈ P′_{k}. Hence H ⊑ H′_{k}. Note that, as β′_{k} is non-singular, C is in minimal form and β ∈ C, we cannot have H ⊏ H′_{k}, so that H = H′_{k}. Since C is also in orthogonal form, β = β′_{k}. Therefore, by Definition 5.4, as {η, η_{k}} ⊆ C_{1} = con enc(C), η = η_{k}; a contradiction. It follows that η must be a strict constraint.

By construction, since η is strict, η_{k} is also strict so that, by Definition 5.4, we have s < 0 and s_{k} < 0; hence {β, β_{k}} ⊆ C_{>}. Suppose that the constraint β is saturated by a ray encoding r = (v^{T}, 0)^{T} ∈ G_{R}. Then, v ∈ R_{1} saturates geq(η); by (27), v also saturates geq(η_{k}) and hence, r saturates β_{k}. Similarly, suppose that β is saturated by a closure point encoding p_{0} = (v^{T}, 0)^{T} ∈ G_{C}. By Definition 5.4, either v ∈ C_{1} or v ∈ P_{1}; in both cases, v saturates geq(η) and, by (27), v also saturates geq(η_{k}); hence, the closure point encoding p_{0} saturates β_{k}. Thus we obtain sat gen(β, (G_{R}, G_{C})) ⊑ sat gen(β_{k}, G) so that, by Definition 6.2, β is strongly ϵ-redundant in C.

Lemma A.22. Let R = gen(G) ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P ≠ ∅ and suppose that G is in minimal and orthogonal form, but not in ϵ-minimal form. Then G contains a strongly ϵ-redundant generator.

Proof. Let C_{1} = con enc(C). Observe that, by Definition 5.4, for each constraint (⟨a, x⟩ + s · ϵ ≥ b) ∈ C where a ≠ 0 ∈ ℝ^{n} and s, b ∈ ℝ, we have (⟨a, x⟩ ≥ b) ∈ geq(C_{1}). Let G = (R, P) and suppose that G_{1} = (R_{1}, P_{1}, C_{1}) = gen enc(G). It follows from Proposition 5.5 that P = con(C_{1}) = gen(G_{1}); moreover, ℂ(P) = con(geq(C_{1})) = gen((R_{1}, P_{1} ∪ C_{1})). By hypothesis, P ≠ ∅ so that, by Definition 5.1, there exists a point in R having an ϵ coordinate strictly greater than 0. Since G is not in ϵ-minimal form, by Definition 6.1, the generator system G_{1} is not in minimal form. Thus there exists a redundant generator v in G_{1}. To prove the thesis, we will show that v ∈ P_{1} and, for some e_{v} > 0, (v^{T}, e_{v})^{T} ∈ G_{P} is strong ϵ-redundant in G.

We first show that v ∉ R_{1}. To do this we assume by contraposition v ∈ R_{1}. Since it is redundant in G_{1}, then v is a non-negative combination of the rays in R_{1} \ {v}. By Definition 5.4, for each w ∈ R_{1} there exists (w^{T}, 0)^{T} ∈ R. As a consequence (v^{T}, 0)^{T} ∈ R is a non-negative combination of the rays in R \ {(v^{T}, 0)^{T}}, so that (v^{T}, 0)^{T} ∈ R is redundant in G; contradicting the hypothesis that G is in minimal form.

It follows that v ∈ P_{1} ∪ C_{1}. By Definition 5.4, P_{1} ∩ C_{1} = ∅. Thus, since v is redundant in G_{1}, there must exist another vector w ∈ (P_{1} ∪ C_{1}) \ {v} such that

sat con(v, geq(C_{1})) ⊆ sat con(w, geq(C_{1})). (28)

By Definition 5.4, there exist e_{v}, e_{w} ∈ ℝ_{+} such that p = (v^{T}, e_{v})^{T}, q = (w^{T}, e_{w})^{T} and {p, q} ⊆ P.

We next show that v ∉ C_{1}. To do this we assume by contraposition v ∈ C_{1} so that, by Definition 5.4, e_{v} = 0. Let q_{0} = (w^{T}, 0)^{T} so that, by condition (3) of Definition 5.2, q_{0} ∈ R. Consider ℓ ∈ lines(R). Since G is in orthogonal form and q ∈ P, we have ⟨q, ℓ⟩ = 0. Since {ℓ, −ℓ} ⊆ rays(R), by applying Lemma A.3 twice we obtain ℓ = (ℓ1^{T}, 0)^{T}. Thus ⟨w, ℓ_{1}⟩ = 0, so that ⟨q_{0}, ℓ⟩ = ⟨w, ℓ_{1}⟩ + 0 · 0 = 0. As this holds for all vectors in lines(R), we obtain q_{0} ∈ lines(R)^{⊥}. Consider now β = (⟨a, x⟩ + s · ϵ ≥ b) ∈ sat con(p, C). Suppose first that a ≠ 0. Then, by Definition 5.4, there exists η ∈ C_{1} such that geq(η) = (⟨a, x⟩ ≥ b) ∈ geq(C_{1}). Since p saturates β and e_{v} = 0, then v saturates geq(η). Thus, by (28), w saturates geq(η). Then β ∈ sat con(q_{0}, C). On the other hand, if a = 0, since p saturates β and e_{v} = 0, we obtain ⟨0, v⟩ + s · 0 = b. Thus b = 0 and again β ∈ sat con(q_{0}, C). Therefore we obtain sat con(p, C) ⊆ sat con(q_{0}, C). From this property, since q_{0} ∈ lines(R)^{⊥} and G is a generator system in minimal form, we obtain p = q_{0} and hence v = w, which is a contradiction.

It follows that v ∈ P_{1} so that, by Definition 5.4, e_{v} > 0 and p ∈ G_{P}. Consider the constraint system

C′_{1} = con enc(sat con(p, C_{≥})) = { ⟨a, x⟩ ≥ b | (⟨a, x⟩ + 0 · ϵ ≥ b) ∈ sat con(p, C_{≥}) }.

Then v saturates all the constraints in C′_{1}. As p ∈ R and e_{v} > 0, for all (⟨a, x⟩ + 0 · ϵ ≥ b) ∈ sat con(p, C_{≥}) and all s < 0, we have (⟨a, x⟩ + s · ϵ ≥ b) ∉ C. Thus, by Definition 5.4, C′_{1} ⊆ C_{1} and hence P ⊆ con(C′_{1}). Let G′ = (R, P \ {p}) and G′_{1} = gen enc(G′) = (R_{1}, P_{1} \ {v}, C_{1}). As v ∈ P is redundant in G_{1}, we have gen(G_{1}) = gen(G′_{1}) and, in particular, v ∈ gen(G′_{1}). Thus v = σy + (1 − σ)z where 0 < σ < 1, y ∈ P_{1} \ {v} and z ∈ ℂ(P). This implies that sat con(v, C_{1}) ⊆ sat con(y, C_{1}); in particular, since C′_{1} ⊆ C_{1}, we obtain sat con(v, C′_{1}) ⊆ sat con(y, C′_{1}). By Definition 5.4, p′ = (y^{T}, e_{y})^{T} ∈ P \ {p}, where e_{y} > 0, so that p′ ∈ G′_{P}. Observe that, as y saturates every constraint in C′_{1}, p′ saturates every constraint in sat con(p, C_{≥}). It follows that sat con(p, C_{≥}) ⊆ sat con(p′, C_{≥}) and, by Definition 6.2, p is strongly ϵ-redundant in G.

Proof of Proposition 6.5 on page 16. Items (1) and (2) follow from Lemmas A.21 and A.22, respectively.