A New Encoding and Implementation of Not Necessarily Closed Convex Polyhedra^{⋆}

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

1 Department of Mathematics, University of Parma, Italy

               {bagnara,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK

                    hill@comp.leeds.ac.uk

Abstract. Convex polyhedra, commonly employed for the analysis and verification of both hardware and software, may be defined either by a finite set of linear inequality constraints or by finite sets of generating points and rays of the polyhedron. 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 vector space having one extra dimension and reuse the tools and techniques already available for closed polyhedra. Previously, this embedding has been designed so that a constant number of constraints and a linear number of generators have to be added to the original NNC specification of the polyhedron. In this paper we explore an alternative approach: while still using an extra dimension to represent the NNC polyhedron by a closed polyhedron, the new embedding adds a linear number of constraints and a constant number of generators. As far as the issue of providing a non-redundant description of the NNC polyhedron is concerned, we generalize the results established in a previous paper so that they apply to both encodings.

1 Introduction

Many applications of static analysis and verification compute on some abstract domain based on convex polyhedra [5]. Traditionally, most of these applications are restricted to convex polyhedra that are topologically closed. When adopting the Double Description (DD) method [10], 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.

⋆ This work has been partly supported by MURST project “Aggregate- and numberreasoning for computing: from decision algorithms to constraint programming with multisets, sets, and maps”.

Some applications of static analysis and verification, including recent proposals such as [4], 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. 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 [7] and also described in [8], proved to be quite effective, its direct application results in a low-level user interface where most of the geometric intuition of the DD method gets lost under the “implementation details”.^{3}

A much cleaner approach was proposed in [1, 2], where the concept of generator of an NNC polyhedron is extended to also account for the closure points of the polyhedron. In particular, it is shown 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 [7, 8]: easier generalizations and a natural, implementation-independent interface.

Easier generalizations. Several complex 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 [7, 8] and the generators-based widening of [3]. The notion of extended generator system proved to be very effective in the definition and justification of these generalizations. As an example, let us consider a very basic operator: the inclusion test between two polyhedra. The usual implementation for closed polyhedra is based on the following specification in terms of their constraint and generator systems. Let P_{1} and P_{2} be closed polyhedra such that P_{1} is defined by the generator system G_{1} and P_{2} by the constraint system C_{2}. Then we have P_{1} ⊆ P_{2} if and only if all the generators in G_{1} satisfy all the constraints in C_{2}. In order to test whether or not a generator g satisfies a constraint ⟨a, x⟩ ≥ b, it is sufficient to determine if the scalar product s = ⟨a, g⟩ is such that s ≥ b, when g is a point, or such that s ≥ 0, when g is a ray. Consider now the generalization to two polyhedra P_{1} and P_{2} that are not necessarily closed. With the high-level interface proposed in [2], the inclusion test can be easily specified using the same approach described above: we only need to generalize the case analysis of the satisfaction test to also cover the combinations provided by the additional constraint and generator types (i.e., strict inequalities and closure points), as shown in Table 1. The elegance of this generalization is better appreciated if contrasted with the specification of the inclusion test on the low-level implementation of [7], informally described in the same paper, which appears to be much more tricky

3 This has a direct, negative impact on the usability of the resulting software: on this subject, see [2, Section 4.1, page 218], [6, Section 4.5, pp. 10–11], and [9, Section 1.1.4, page 10].

and obscure. The reason is that in [7] the reader has no high-level interpretation of the generators occurring in the low-level encoding.

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

Table 1. Checking whether a constraint is satisfied by a generator.

A natural, implementation-independent interface. The combination of mixed constraint systems and extended generator systems offers another improvement over the proposal in [7, 8]: 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 the strong minimization procedures [2]. On the other hand, by relying on the highlevel 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 exploit the latter possibility by introducing an alternative class of closed polyhedra for implementing the NNC polyhedra. The basis of this representation is a simple generalization of the class of polyhedra used in [7, 8] and also in [2]. 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 given in [2] 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 [2] while the other, which is biased for the use of the generator representation, is new to this paper. Moreover, we generalize the notion of strong minimal form [2] so that it is applicable to all the above classes of closed polyhedra.

One interesting and potentially useful consequence of having the option of these alternative implementations is that, depending on the number of strict constraints in the constraint system compared with the number of closure points that are also points in the generator system, the choice of representation will affect the efficiency of the polyhedral operations. The Parma Polyhedra Library^{4},

4 Publicly available at URI http://www.cs./unipr.it/ppl/. The implementation described in this paper is available in the alt nnc branch of the PPL’s CVS repository.

a modern C^{++} library for the manipulation of convex polyhedra, has been extended so as to implement both approaches, so that it will be possible to perform experiments to compare their efficiencies.

The paper is structured as follows: Section 2 recalls the required concepts and notations; Section 3 presents a general class and two special subclasses of the set of closed polyhedra that are appropriate for the representation of NNC polyhedra; Section 4 generalizes, to all the above classes of closed polyhedra, the notion of strong minimal form introduced in [2]; Section 5 concludes.

2 Preliminaries

We first define some necessary terminology and notation.

The set of non-negative reals is denoted by ℝ_{+}. In the paper, all topological arguments refer to the Euclidean topological space ℝ^{n}, for n ∈ ℕ. If S ⊆ ℝ^{n}, then the topological closure ℂ(S) is defined as ⋂{ 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). For each vector a ∈ ℝ^{n} and scalar b ∈ ℝ, where a ≠ 0, the linear inequality constraint ⟨a, x⟩ ≥ b (resp., ⟨a, x⟩ > b) defines a topologically closed (resp., open) affine half-space of ℝ^{n}. 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.

A subset P of ℝ^{n} is called a closed polyhedron if either P can be expressed as the intersection of a finite number of closed affine half-spaces of ℝ^{n} or n = 0 and P = ∅. The set of all closed polyhedra on ℝ^{n} is denoted by ℂℙ_{n}. A subset P of ℝ^{n} is called an NNC polyhedron if either P can be expressed as the intersection of a finite number of (not necessarily closed) affine half-spaces of ℝ^{n} or n = 0 and P = ∅. The set of all NNC polyhedra on ℝ^{n} is denoted by ℙ_{n}. The set ℙ_{n}, when partially ordered by subset inclusion, is a lattice and ℂℙ_{n} is a sublattice of ℙ_{n} (note that ℂℙ_{n} = ℙ_{n} if and only if n = 0). The binary meet operation is given by set-intersection, whereas the binary join operation, denoted ⊎, is called convex polyhedral hull, poly-hull for short. In this paper, we only consider polyhedra in ℙ_{n} when n > 0.

A mixed constraint system C is a finite set of linear inequality constraints and we write con(C) to denote the polyhedron described by C.

Suppose that P ∈ ℙ_{n} is non-empty. A vector p ∈ ℝ^{n} is a point of P if p ∈ P; a vector r ∈ ℝ^{n} such that r ≠ 0 is a ray of P if, for every point p ∈ P and every ρ ∈ ℝ_{+}, we have p + ρr ∈ P; a vector c ∈ ℝ^{n} is a closure point of P if c ∈ ℂ(P). Given three finite sets of vectors R, P, C ⊆ ℝ^{n}, where R = {r_{1}, …, r_{r}} and 0 ∉ R, P = {p_{1}, …, p_{p}} and C = {c_{1}, …, c_{c}}, then the triple G = (R, P, C) is called an extended generator system [2] for the NNC polyhedron

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

The polyhedron gen(G) is empty if and only if P = ∅. For a non-empty polyhedron P, vectors in R, P, and C are rays, points and closure points of P, respectively. We define an ordering ⊑ on extended generator systems such that, for any generator systems G_{1} = (R_{1}, P_{1}, C_{1}) and G_{2} = (R_{2}, P_{2}, C_{2}), G_{1} ⊑ G_{2} if and only if R_{1} ⊆ R_{2}, P_{1} ⊆ P_{2} and C_{1} ⊆ C_{2}; if, in addition, G_{1} ≠ G_{2}, we write G_{1} ⊏ G_{2}. When C = ∅, we will omit it from the generator system and simply write G = (R, P). In this case, the system G that defines the closed polyhedron P = gen(G), is called a (standard) generator system for P.

Consider a mixed constraint system C, an extended generator system G, and a polyhedron P. 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 con(G′) = P;

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

3 Representing NNC Polyhedra

The idea underlying the proposal of [7, 8] 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 1. (Represented NNC polyhedron.) Let R ∈ ℂℙ_{n+1} be a closed polyhedron. R 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 corresponding operators on the domain of NNC polyhedra. For instance, one would like to 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.

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

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

Definition 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 1. 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 1 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 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 2. For instance, even though R ∈ R_{5}, we have R′ ∉ R_{5}.

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 1. Then, it is worth noting that any facet that is parallel to the ϵ axis, such as the segment [I, L], 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 [L, 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 3. (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) =^{def} 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) =^{def} (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 2. Let (C, G) ≡ R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. Then

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

Figure 2, which shows the poly-hulls of some of the polyhedra in Figure 1, provides a graphical and informal justification for the two conditions stated in Definition 2. Suppose we do not enforce condition (2) of Definition 2, thus admitting polyhedra such as R_{1}, and consider the poly-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 2, thus allowing for polyhedra such as R_{5}, and

O  x ϵ  A  D R_{1}  R_{2} R_{1} ⊎ R_{2}  R_{4}  R_{5} M  N  Q R_{4} ⊎ R_{5}

Fig. 2. R_{1} ⊎ R_{2} does not represent the NNC polyhedron P_{1} ⊎ P_{2}; similarly, R_{4} ⊎ R_{5} does not represent the NNC polyhedron P_{4} ⊎ P_{5}.

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

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

Definition 4. (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 [7, 8]. This is also the same class considered in [2], where these polyhedra were called ϵ-representations. Thus many of the definitions and results below concerning C-ϵ-polyhedra and the embedding of the NNC polyhedra in them are taken from [2].

In [2], we have shown how a C-ϵ-polyhedron for an NNC polyhedron P may be constructed directly from the constraint and generator systems for P.

Definition 5. (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, 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 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 all the non-empty ϵ-polyhedra have the ray −e_{ϵ} =^{def} (0^{T}, −1)^{T} so that there is no lower bound for the ϵ dimension.

Definition 6. (G-ϵ-polyhedron.) An ϵ-polyhedron R = gen((R, P)) ∈ ℂℙ_{n+1} is said to be generator-biased and called a G-ϵ-polyhedron if and only if

R ⊇ gen(({−e_{ϵ}}, P )).

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 the constraint and generator systems for P.

Definition 7. (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} {0 ≤ ϵ ≤ 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′ = {−e_{ϵ}} ∪ { (r^{T}, 0)^{T} | r ∈ R },
P′ = { (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 and, by virtue of Proposition 1, ensures that condition (3) of Definition 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”.

Returning to Figure 1, it can be observed that R_{2} is a constraint-biased ϵpolyhedron, R_{4} is a generator-biased ϵ-polyhedron, whereas the ϵ-polyhedron R_{3} is neither constraint-biased nor generator-biased. By comparing R_{3} with R_{1} and R_{2} 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 computational time.

The following result formalizes the correctness of the encodings introduced in Definitions 5 and 7.

Proposition 3. 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.

The next proposition shows that most of the operators defined on the domain of NNC polyhedra ℙ_{n} can be mapped into the corresponding operators on the class of ϵ-polyhedra defined on ℂℙ_{n+1}.

Proposition 4. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}. Suppose R ⇛_{Y} P, and 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});

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 convex polyhedral 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.

4 Strong Minimization of ϵ-Polyhedra

As pointed out in [2], the usual minimization of the descriptions of a (constraintbiased) ϵ-polyhedron does not enforce the minimization of the encoded descriptions for the represented NNC polyhedron. The solution proposed in [2] is the definition of a stronger form of minimization to be applied to the descriptions of constraint-biased ϵ-polyhedra. We here define the same notion of strong minimal form, but this time for arbitrary ϵ-polyhedra, being careful that if it is constraint- or generator-biased before minimization, then it remains constraintor generator-biased, respectively, after the minimization.

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

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

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

The computation of strong minimal forms (smf’s, for short) requires the removal of non-essential constraints and generators, whose efficient detection is based on the checking of particular saturation conditions. The following notation is needed for a formal definition of these conditions.

Let R = con(C) ∈ ℂℙ_{n+1}. The set of strict and non-strict inequality encodings C_{>} and C_{≥} of C are defined as

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

We say that a constraint (⟨a, x⟩ + s · ϵ ≥ b) ∈ C is unmatched in C if s < 0 and (⟨a, x⟩ + 0 · ϵ ≥ b) ∉ C.

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

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

A point (v^{T}, e)^{T} ∈ P is said to be unmatched in G if e > 0 and (v^{T}, 0)^{T} ∉ P.

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 ∈ C | p saturates c };

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

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

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

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

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

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

Note that, according to the above definition, only the strict inequality encodings and the point encodings of an ϵ-polyhedron can be identified as ϵ-redundant constraints and generators, respectively. The following result shows that such a restriction is unconsequential, because all the redundant non-strict inequality encodings and all the redundant closure point encodings will be filtered away by the usual minimization procedure.

Proposition 5. Let R, R′ ∈ ℂℙ_{n+1} and P ∈ ℙ_{n} be such that R ⇛_{ϵ} P ≠ ∅ and R′ ⇛_{ϵ} P. Then

1. for any constraint c = (⟨a, x⟩ + 0 · ϵ ≥ b), R ⊆ con({c}) if and only if R′ ⊆ con({c});

2. for any vector p = (v^{T}, 0)^{T} ∈ ℝ^{n+1}, p ∈ R if and only if p ∈ R′.

The next proposition shows that ϵ-redundant constraints and generators can be safely removed from the descriptions of an ϵ-polyhedron without affecting the represented NNC polyhedron. Also, if the ϵ-polyhedron is constraint- or generator-biased, it remains constraint- or generator-biased, respectively.

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

1. If c is ϵ-redundant in C, then c is unmatched in C and

con(C \ {c} ∪ {ϵ ≤ 1}) ⇛_{Y} P.

2. If p is ϵ-redundant in G = (R, P), then p is unmatched in G and

gen((R, P \ {p})) ⇛_{Y} P.

If there are no ϵ-redundant constraints or generators, then the constraint or generator system, respectively, is in strong minimal form.

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

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

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

It must be stressed that the above generalizations of the results regarding strong minimal forms to any ϵ-polyhedron are extremely important from the point of view of efficiency. As a matter of fact, a lot of ϵ-redundant constraints and generators may be produced by a few applications of the usual operators, even when starting from descriptions that are in strong minimal form.

To exemplify such a possibility, in Table 2 we report the results obtained for a rather simple experimental evaluation, for which we have adopted the new generator-biased implementation made available by the Parma Polyhedra Library [1, 2]. The table has twelve rows in four groups of three. For each triple of rows, we considered four NNC polyhedra P_{i} defined by an extended generator system G_{i} = (∅, P_{i}, C_{i}). All four G_{i}, which are in minimal form, have the same cardinalities for the P_{i} and the C_{i} and these are given in the 1st column. The goal is to compute the NNC polyhedron P = (P_{1} ∩ P_{2}) ⊎ (P_{3} ∩ P_{4}) and each row in the triple achieves this by following a different evaluation strategy.

# P_{i} + # C_{i} eval Inters (# C_{i}) Poly-hull (# G_{ij})  Final result (# C)
1st arg 2nd arg 1st arg 2nd arg res smf time time-smf
a  48  48  131  77 356 56 0.91  0.01
4 + 8  b  32  32  40  17 156 56 0.08  0.00
c  48  32  132  17 251 56 0.16  0.00
a  62  62  209  125 537 59 2.29  0.01
8 + 8  b  36  36  50  21 308 59 0.25  0.00
c  62  36  190  21 332 59 0.37  0.00
a  132  132  414  305 2794 227 118.64  0.45
8 + 10  b  68  68  58  25 1084 227 1.42  0.06
c  132  68  261  25 1423 227 3.96  0.08
a  178  178  697  657 5078 235 932.72  2.07
16 + 10 b  80  80  78  29 1775 235 5.24  0.14
c  178  80  418  29 1238 235 9.48  0.08

Table 2. Exploiting smf’s to improve the efficiency of the computation.

For all evaluation strategies, in order to compute the two intersections, we first obtain the constraint systems C_{i}; the 3rd and 4th columns of the table give the cardinalities of each C_{i}, where the column labeled ‘1st arg’ indicates # C_{1} and # C_{3} (which are always the same) while that labeled ‘2nd arg’ indicates # C_{2} and # C_{4} (which are also always the same). We then compute the two intersections and obtain the generator systems G_{12} and G_{34}, whose cardinalities are reported in the 5th and 6th columns. Then, we compute the poly-hull P. In the last four columns we report: the cardinality of the constraint system obtained for P; the same, but after the removal of the ϵ-redundant constraints; the time spent by the overall computation; the time spent to compute the final smf. Rows labeled ‘a’ correspond to the usual evaluation strategy, where no smf is computed. In this case, the two intersections are computed incrementally: namely, we start from the DD pair of the first argument and incrementally add the constraints of the second argument, keeping the generator system of the result up-to-date so that it will be ready for the following poly-hull computation. Then, we compute the poly-hull, again incrementally. In the rows labeled ‘b’ we report the outcomes of an evaluation strategy that exploits the possibility of obtaining the smf’s of both arguments before each operation (in the table, the cardinalities computed after the application of strong minimization are shown in boldface). Note that, in our current implementation, such a strategy does not fit very well with the adoption of the incremental approach, because after the computation of the smf for one description we no longer have a DD pair [2]. Therefore, after computing the smf of the first argument of each operation, the corresponding dual description has to be recomputed from scratch. The rows labeled ‘c’ report the outcomes of an intermediate evaluation strategy, where we only compute the smf’s of the second argument of each operation, so that the incremental approach can still be adopted. For the examples considered, the latter strategy results in slightly smaller, but still impressive, performance improvements.

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. There may be many ϵ-redundant constraints/generators, and their removal can lead to dramatic speed-ups. Moreover, the identification of ϵ-redundant constraints/generators has a negligible cost (see the last column in Table 2) so that the number of ϵ-redundant elements contained in a description can be efficiently computed at run time; based on this, it is always possible to dynamically select the evaluation strategy that is likely to result in a more efficient computation. We believe that the third strategy, by preserving incrementality, is a safe and generally rewarding choice.

5 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 a previous paper we 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 this work we have shown that the standard implementation of NNC polyhedra, which happens to be biased for constraint-intensive computations, has a dual. We have completely defined this new, previously unknown, implementation and showed that it is biased for generator-intensive computations. Moreover, we have provided a generalization of a notion of strong minimal form that is applicable to both constraint- and generator-biased implementations. We have also shown that this general notion of strong minimization can have a dramatic effect on the size of the representations and, thus, on the efficiency of the algorithms operating upon them.

The encoding based on G-ϵ-polyhedra has dual properties with respect to the one based on C-ϵ-polyhedra. In particular, using a C-ϵ-polyhedron, the encoding of an NNC polyhedron may require a similar number of constraints but as many as twice the number of generators, while, using a G-ϵ-polyhedron, it may require a similar number of generators but as many as twice the number of constraints. We have extended the Parma Polyhedra Library [1, 2], a modern C^{++} library for the manipulation of convex polyhedra, so as to implement NNC polyhedra both with the constraint- and the generator-biased encodings. This enabled us to perform some very preliminary experiments on purely synthetic benchmarks. 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.

References

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

2. 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.

3. 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.

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

5. 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.

6. 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.

7. 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.

8. 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.

9. 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.

10. 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.

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

A Proofs

For each set S ⊆ ℝ^{n} of finite cardinality m, we denote by matrix(S) ⊆ ℝ^{n×m} the set of all matrices having S as the set of their columns.

In the proofs below we assume the following simple consequence of well known theorems by Minkowski and Weyl [11].

Theorem 1. 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, for any matrices K ∈ ℝ^{n×r} and L ∈ ℝ^{n×p} where K ∈ matrix(R) and L ∈ matrix(P),

P = { Kρ + Lπ ∈ ℝ^{n} | ρ ∈ ℝr_{+}, π ∈ ℝp_{+}, ∑_{i=1}^{p} π_{i} = 1 }.

Proof (Proof of Proposition 1 on page 6). Let R = con(C). We first assume that (4) holds for any constraint c ∈ C and show that R is an ϵ-polyhedron. Condition (2) of Definition 2 holds by hypothesis. We prove condition (3) holds. Let c = (⟨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 c. As c 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 c = (⟨a, x⟩+s·ϵ ≥ b) and that R ⊆ con({c}). Then, any point (v^{T}, e)^{T} ∈ R satisfies c. By condition (3) of Definition 2, (v^{T}, 0)^{T} ∈ R and therefore satisfies c. Thus we have ⟨a, v⟩ ≥ b. Hence, if c_{0} = (⟨a, x⟩ + 0 · ϵ ≥ b), (v^{T}, e)^{T} satisfies c_{0}. As (v^{T}, e)^{T} was an arbitrary point in R, R ⊆ con({c_{0}}). ⊓ ⊔

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

Lemma 1. If R ∈ ℂℙ_{n+1} is an ϵ-polyhedron and (r^{T}, e)^{T} is a ray of R, where r ≠ 0, then (r^{T}, 0)^{T} is a ray of R.

Proof. Since R has a ray, it is not empty. Thus, let (v^{T}, e′)^{T} ∈ R. By condition (3) of Definition 2, we also have (v^{T}, 0)^{T} ∈ R.

Since (r^{T}, e)^{T} is a ray of R, for all ρ ∈ ℝ_{+} we have that

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

From this, again by condition (3) of Definition 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 2. If R ∈ ℂℙ_{n+1} is an ϵ-polyhedron and (r^{T}, e)^{T} is a ray of R, then e ≤ 0.

Proof. Since R is an ϵ-polyhedron, condition (2) of Definition 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 2, e_{ρ} = e_{0} + ρe ≤ δ. Therefore, as this holds for all ρ ∈ ℝ_{+}, we have e ≤ 0. ⊓ ⊔

Lemma 3. 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((R′, P′ ∪ C′)), where

R′ = { (r^{T}, e)^{T} ∈ R | e = 0 },
P′ = { (v^{T}, e)^{T} ∈ P | e > 0 },
C′ = { (v^{T}, e)^{T} ∈ P | e = 0, ∀e′ ∈ ℝ : (v^{T}, e′)^{T} ∉ P′ }.

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

(v^{T}, e_{max})^{T} = (r^{T}, e_{r})^{T} + π_{1}(p1^{T}, e_{1})^{T} + ⋯ + π_{p}(pp^{T}, e_{p})^{T}  (6)

where (r^{T}, e_{r})^{T} is a ray in R, {p_{1}, …, p_{p}} ⊆ P, π_{1}, …, π_{p} > 0 and ∑_{i=1}^{p} π_{i} = 1.

By Lemma 2, e_{r} ≤ 0. Note that it cannot be r = 0, since this would also entail e_{r} < 0, so that

(v^{T}, e′)^{T} = π_{1}(p1^{T}, e_{1})^{T} + ⋯ + π_{p}(pp^{T}, e_{p})^{T} ∈ R,

where e′ = e_{max} − e_{r} > e_{max}, therefore contradicting the maximality of e_{max}. Hence r ≠ 0 and, by Lemma 1, (r^{T}, 0)^{T} is also a ray in R. Note that it can neither be e_{r} < 0, since in this case, by replacing (r^{T}, e_{r})^{T} by (r^{T}, 0)^{T} in (6), we would obtain the same contradiction seen above. Hence e_{r} = 0. Since (r^{T}, e_{r})^{T} is a ray of R, then it can be obtained as a non-negative combination of rays in R; by Lemma 2, all of these rays must have a non-positive ϵ coordinate and hence, as e_{r} = 0, they all have a zero ϵ coordinate. As a consequence, (r^{T}, e_{r})^{T} is a non-negative combination of rays in R′, so that (v^{T}, e_{max})^{T} ∈ gen((R′, P)).

Suppose that e_{i} < 0 for some 1 ≤ i ≤ p. Then, as R is an ϵ-polyhedron, by condition (3) of Definition 2, (pi^{T}, 0)^{T} ∈ R. Replacing the point (pi^{T}, e_{i})^{T} by (pi^{T}, 0)^{T} in (6), we obtain

(v^{T}, e′)^{T} = (r^{T}, e_{r})^{T} + π_{1}(p1^{T}, e_{1})^{T} + ⋯ + π_{i}(pi^{T}, 0)^{T} + ⋯ + π_{p}(pp^{T}, e_{p})^{T} ∈ R

where e′ = e_{max}−e_{i} > e_{max}, again contradicting the maximality of e_{max}. Suppose now that, for some 1 ≤ i ≤ p, e_{i} = 0 and there exists e′_{i} > 0, such that (pi^{T}, e′_{i})^{T} ∈ P. Replacing the point (pi^{T}, e_{i})^{T} by (pi^{T}, e′_{i})^{T} in (6), we obtain

(v^{T}, e′)^{T} = (r^{T}, e_{r})^{T} + π_{1}(p1^{T}, e_{1})^{T} + ⋯ + π_{i}(pi^{T}, e′_{i})^{T} + ⋯ + π_{p}(pp^{T}, e_{p})^{T} ∈ R

where e′ = e_{max} + e′_{i} > e_{max}, which again contradicts the maximality of e_{max}. It follows that, for all 1 ≤ i ≤ p, the point (pi^{T}, e_{i})^{T} is in P′ if e_{i} > 0 and it is in C′ otherwise. Thus, (v^{T}, e_{max})^{T} ∈ gen((R′, P′ ∪ C′)). ⊓ ⊔

Proof (Proof of Proposition 2 on page 7). Let con enc(C) be as specified in Definition 3. Let also G = (R, P), so that gen enc(G) = (R′, P′, C′), where R′ = {r_{1}, …, r_{r}}, P′ = {p_{1}, …, p_{p}}, and C′ = {c_{1}, …, c_{c}}.

Suppose first that [[R]] = ∅. Then, by Definition 3, con(con enc(C)) = ∅. Also, by Definition 1, R ⊆ con({ϵ ≤ 0}) so that, by Definition 3, P′ = ∅ and gen((R′, P′, C′)) = ∅. 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)),  (7)
v ∈ gen(gen enc(G)),  (8)

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

Suppose that (7) holds. If c = (⟨a, x⟩ + 0 · ϵ ≥ b) ∈ C, then, by Definition 3, there exists (⟨a, x⟩ ▷◁ b) ∈ con enc(C), for some ▷◁ ∈ {≥, >}. Thus ⟨a, v⟩ ≥ b and hence (v^{T}, e)^{T} satisfies c for all e ∈ ℝ. If (⟨a, x⟩ + s · ϵ ≥ b) ∈ C, for some s < 0 and a ≠ 0, then, by Definition 3, (⟨a, x⟩ > b) ∈ con enc(C). Thus, as (7) holds, ⟨a, v⟩ > b. If (⟨0, x⟩ + s · ϵ ≥ b) ∈ C, for some s < 0, then, as [[R]] is non-empty, by Definition 2, b < 0. By condition (2) of Definition 2, the set

{ (⟨a, v⟩ − b) ∈ ℝ | ∃s < 0 . (⟨a, x⟩ + s · ϵ ≥ b) ∈ C }

is non-empty. Let e_{min} be its smallest element. It follows that e_{min} > 0 and the point (v^{T}, e_{min})^{T} satisfies every constraint (⟨a, x⟩ + s · ϵ ≥ b) ∈ C such that s ≤ 0. Reasoning towards a contradiction, suppose that (v^{T}, e_{min})^{T} ∉ R.

As [[R]] ≠ ∅, by Definition 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_{min})^{T} that saturates a constraint (⟨a′, x⟩+s′·ϵ ≥ b′) ∈ C where s′ > 0. Thus ⟨a′, w_{0}⟩+ s′ · e_{0} = b′. However, as e_{0} > 0, ⟨a′, w_{0}⟩ < b′ so that (w0^{T}, 0)^{T} ∉ R, contradicting condition (3) of Definition 2. Thus (v^{T}, e_{min})^{T} ∈ R.

Suppose next that (8) holds. By Theorem 1

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

where ρ ∈ ℝr_{+}, π ∈ ℝp_{+}, γ ∈ ℝc_{+}, π ≠ 0 and ∑_{i=1}^{p} π_{i} + ∑_{i=1}^{c} γ_{i} = 1. By

Definition 3, {(r1^{T}, 0)^{T}, …, (rr^{T}, 0)^{T}} ⊆ R, {(p1^{T}, e_{1})^{T}, …, (pp^{T}, e_{p})^{T}} ⊆ P, for

some e_{1}, …, e_{p} > 0, and {(c1^{T}, 0)^{T}, …, (cc^{T}, 0)^{T}} ⊆ P. Letting

(v^{T}, e)^{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)^{T} ∈ gen(G) = R. Since π ≠ 0, we also obtain e > 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 2, the ϵ dimension is bounded from above and thus there exists a value e_{max} ≥ e such that (v^{T}, e_{max})^{T} ∈ R and, for all e′ > e_{max}, (v^{T}, e′)^{T} ∉ R. We show that both (7) and (8) hold.

Suppose that c′ = (⟨a, x⟩ ▷◁ b) ∈ con enc(C), where ▷◁ ∈ {≥, >}. Then, by Definition 3, there exists s ≤ 0 such that c = (⟨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 c′. As c′ ∈ con enc(C) was chosen arbitrarily, (7) holds.

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

R′′ = { (r^{T}, e)^{T} ∈ R | e = 0 } = {(r1^{T}, 0)^{T}, …, (rr^{T}, 0)^{T}},
P′′ = { (p^{T}, e)^{T} ∈ P | e > 0 } = {(p1^{T}, e_{1})^{T}, …, (pp^{T}, e_{p})^{T}},
C′′ = { (c^{T}, e)^{T} ∈ P | e = 0, ∀e′ > 0 : (c^{T}, e′)^{T} ∉ P′′ }

= {(c1^{T}, 0)^{T}, …, (cc^{T}, 0)^{T}}.

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 ρ ∈ ℝr_{+}, π ∈ ℝp_{+} and γ ∈ ℝc_{+} such that π ≠ 0 and ∑_{i=1}^{p} π_{i} + ∑_{i=1}^{c} γ_{i} = 1.

By Definition 3, for each 1 ≤ i ≤ r, r_{i} ∈ R′; for 1 ≤ i ≤ p, p_{i} ∈ P′; and, for 1 ≤ i ≤ c, c_{i} ∈ C′, 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′, P′, C′)). Thus (8) holds. ⊓ ⊔

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

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

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

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

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

To prove item 2 of the Proposition, we show that for any Y ∈ {C, G},

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

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 and 7, (v^{T}, 0)^{T} ∈ R_{1} and hence, by Definition 3, v ∈ R_{2}. If v ∈ P, then, by Definitions 5 and 7, (v^{T}, 1)^{T} ∈ P_{1} and hence, by Definition 3, v ∈ P_{2}. If v ∈ C, then, by Definitions 5 and 7, (v^{T}, 0)^{T} ∈ P_{1} and hence, by Definition 3, 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 3, (v^{T}, 0)^{T} ∈ R_{1}. By Definitions 5 and 7, v ∈ R. If v ∈ P_{2}, then, by Definition 3, (v^{T}, e)^{T} ∈ P_{1}, for some e > 0. Thus, by Definitions 5 and 7, v ∈ P. If v ∈ C_{2}, then, by Definition 3, (v^{T}, e)^{T} ∈ P_{1}, for some e ≥ 0. Thus, by Definitions 5 and 7, v ∈ P ∪C. Therefore, by definition of gen, we obtain gen(G) ⊇ gen(G_{2}). Thus (10) holds. As a consequence, by Proposition 2, we have gen(G_{1}) ⇛_{ϵ} gen(G).

Suppose now that Y = G. Then, by Definition 7, −e_{ϵ} ∈ R_{1} so that, by Definition 6, gen(G_{1}) is a G-ϵ-polyhedron. Otherwise, suppose that Y = C. Observe that, by Definition 5, 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 4, gen(G_{1}) is a C-ϵ-polyhedron, This completes the proof of item 2. ⊓ ⊔

The proof of the Proposition 4 on page 10, requires a number of additional preliminary results. In [2], we have shown that when considering NNC polyhedra, closure points can be characterized by a property which is similar to the one used when defining rays.

Proposition 8. [2, Proposition 3] Let P ∈ ℙ_{n} and c ∈ ℝ^{n}. Then c ∈ ℂ(P) if and only if P ≠ ∅ and σp + (1 − σ)c ∈ P for every point p ∈ P and σ ∈ ℝ such that 0 < σ < 1.

As for a C-ϵ-polyhedron (see [2, Lemma 5]), for any ϵ-polyhedron, closure points in the NNC polyhedron are represented by points lying on the hyperplane defined by ϵ = 0.

Lemma 4. 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 1, we obtain σp + (1 − σ)v ∈ P. As the choices of p ∈ P and σ were both arbitrary, we can apply Proposition 8 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 8, 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 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 a 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 5. Let R ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P ≠ ∅ and r ∈ ℝ^{n} be a ray of the NNC polyhedron P. Then (r^{T}, 0)^{T} is a ray of R.

Proof. Suppose v ∈ P and ρ ∈ ℝ_{+}. Then v + ρr ∈ P. By Definition 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 2, (v^{T}, 0)^{T} ∈ R and ((v + ρr)^{T}, 0)^{T} ∈ R. Thus (v^{T}, 0)^{T} + ρ(r^{T}, 0)^{T} ∈ R. Therefore, as this holds for all ρ ∈ ℝ_{+}, (r^{T}, 0)^{T} is a ray of R. ⊓ ⊔

Lemma 6. 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 }.

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

Proof. Let R′ = gen((R′, P)).

First, 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.

Second, suppose that there exists (r^{T}, e)^{T} ∈ R such that e ≠ 0. By Lemma 2, it holds e < 0. It follows from the hypothesis that (−e_{ϵ}) ∈ R′.

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, we have {(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 positive 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 1, (r^{T}, 0)^{T} is also a ray of R. Hence, R′′ ⊆ R. By the above observations, we obtain that

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

Let now p ∈ [[R′]], so that there exists (p^{T}, e)^{T} ∈ R′ such that e > 0. By applying (11), 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 2 easily follows from (11), because R is an ϵ-polyhedron: namely, we can consider the same upper bound constraint ϵ ≤ δ used for R. To prove condition (3) of Definition 2, let (p^{T}, e)^{T} ∈ R′. By (11), we have (p^{T}, e)^{T} = (p^{T}, e_{0})^{T} + ρ(−e_{ϵ}), where (p^{T}, e_{0})^{T} ∈ R. As R is an ϵ-polyhedron, we also have (p^{T}, 0)^{T} ∈ R. Since we already observed that R ⊆ R′, this completes the proof. ⊓ ⊔

The following Lemma is proved in [2].

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

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

x = σx_{1} + (1 − σ)x_{2} + ρ_{1}K_{1} + ρ_{2}K_{2},

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

Proof (Proof of Proposition 4 on page 10). The case when ⇛_{Y} ∈ {⇛_{C}} is proved in [2, Proposition 3]. We prove here the cases when ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{G}}.

To prove item (1), we assume that R_{1} ⇛_{Y} P_{1} and R_{2} ⇛_{Y} P_{2} and show that R_{1} ∩ R_{2} ⇛_{Y} P_{1} ∩ P_{2}.

We first prove condition (2) of Definition 2. As R_{1} and R_{2} are ϵ-polyhedra there exists δ_{1}, δ_{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 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 it represents P_{1} ∩ P_{2}. By Definition 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}. By hypothesis, R_{1} ⇛_{ϵ} P_{1} and R_{2} ⇛_{ϵ} P_{2}, so that P_{1} = [[R_{1}]] and P_{2} = [[R_{2}]]. Hence, by Definition 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 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}. As P_{1} = [[R_{1}]] and P_{2} = [[R_{2}]], v ∈ P_{1} and v ∈ P_{2}, so that v ∈ P_{1} ∩ P_{2}. Thus, R_{1} ∩ R_{2} ⇛_{ϵ} P_{1} ∩ P_{2}.

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. If otherwise R_{1} ∩ R_{2} ≠ ∅, then we have to prove that −e_{ϵ} is a ray in R_{1} ∩ R_{2}. Let v′ ∈ R_{1} ∩ R_{2} and consider, for any ρ ∈ ℝ_{+}, the vector v′_{ρ} = v′ + ρ(−e_{ϵ}). As v′ ∈ R_{1} ∩ R_{2}, v′ ∈ R_{1} and v′ ∈ R_{2}. As R_{1} and R_{2} are non-empty G-ϵ-polyhedra, −e_{ϵ} is a ray in R_{1} and R_{2} so that, for any ρ ∈ ℝ_{+}, v′_{ρ} ∈ R_{1} and v′_{ρ} ∈ R_{2}. Hence v′_{ρ} ∈ R_{1} ∩ R_{2}.

To prove item (2) of the proposition, we assume that R_{1} ⇛_{Y} P_{2} ≠ ∅ and R_{2} ⇛_{Y} P_{2} ≠ ∅ and show that R_{1} ⊎ R_{2} ⇛_{Y} P_{1} ⊎ P_{2}.

For j ∈ {1, 2}, let P_{j} = gen((R_{j}, P_{j}, C_{j})), where R_{j} has cardinality k_{j}. By Lemma 7, if (v^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, then for some 0 ≤ σ ≤ 1, (v_{1}^{T}, e_{1})^{T} ∈ R_{1}, (v_{2}^{T}, e_{2})^{T} ∈ R_{2}, e′_{1}, e′_{2} ∈ ℝ, r_{1} = ρ_{1}K_{1} and r_{2} = ρ_{2}K_{2} where K_{1} ∈ matrix(R_{1}),

K_{2} ∈ matrix(R_{2}), ρ_{1} ∈ ℝk_{1}_{+} and ρ_{2} ∈ ℝk_{2}_{+}, we have

(\begin{matrix}v \\ e \end{matrix}) = σ (\begin{matrix}v & 1 \\ e_{1} \end{matrix}) + (1 − σ) (\begin{matrix}v & 2 \\ e_{2} \end{matrix}) + (\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}) + (\begin{matrix}r_{1} \\ e′_{1} \end{matrix}) + (\begin{matrix}r_{2} \\ e′_{2} \end{matrix}) .  (12)

We first prove condition (2) of Definition 2. As R_{1}, R_{2} are ϵ-polyhedra, 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 (12). By letting δ = max{δ_{1}, δ_{2}}, we obtain e_{1} ≤ δ and e_{2} ≤ δ. Also, by Lemma 2, e′_{1}, e′_{2} ≤ 0. Thus e = σe_{1} +(1−σ)e_{2} +e′_{1} +e′_{2} satisfies e ≤ δ so that (v^{T}, e)^{T} ∈ con({ϵ ≤ δ}), as required.

To prove condition (3) of Definition 2, suppose that (v^{T}, e)^{T} ∈ R_{1} ⊎ R_{2}, so that we can rewrite it according to (12). As R_{1} and R_{2} are ϵ-polyhedra, (v1^{T}, 0)^{T} ∈ R_{1} and (v2^{T}, 0)^{T} ∈ R_{2} and, by Lemma 1, (r1^{T}, 0)^{T} is a ray in R_{1} and (r2^{T}, 0)^{T} is a ray in R_{2}, so that

(\begin{matrix}v \\ 0 \end{matrix}) = σ (\begin{matrix}v & 1 \\ 0 \end{matrix}) + (1 − σ) (\begin{matrix}v & 2 \\ 0 \end{matrix}) + (\begin{matrix}r & 1 \\ 0 \end{matrix}) + (\begin{matrix}r & 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 Definition 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 7, v = σv_{1} + (1 − σ)v_{2} + r_{1} + r_{2}, for some 0 ≤ σ ≤ 1, v_{1} ∈ ℂ(P_{1}) and v_{2} ∈ ℂ(P_{2}), where v_{1} ∈ P_{1} and σ > 0 or v_{2} ∈ P_{2} and σ < 1, and r_{1} = ρ_{1}K_{1} and r_{2} = ρ_{2}K_{2} where K_{1} ∈ matrix(R_{1}) and K_{2} ∈ matrix(R_{2}), ρ_{1} ∈ ℝk_{1}_{+} and ρ_{2} ∈ ℝk_{2}_{+}. Suppose, without loss of generality, that v_{1} ∈ P_{1} and σ > 0. As R_{1} ⇛_{ϵ} P_{1}, there exists e_{1} > 0 such that (v1^{T}, e_{1})^{T} ∈ R_{1}. As R_{2} is an ϵ-polyhedron, by Lemma 4, from v_{2} ∈ ℂ(R_{2}) we obtain (v2^{T}, 0)^{T} ∈ R_{2}. By Lemma 5, (r1^{T}, 0)^{T} is a ray in R_{1} and (r2^{T}, 0)^{T} is a ray in R_{2}. Thus, by letting

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

we obtain (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 (12). As e > 0 and σ ≥ 0, either e_{1} > 0 and σ > 0 or e_{2} > 0 and σ < 1. Without loss of generality, we assume that e_{1} > 0 and σ > 0. As R_{1} ⇛_{ϵ} P_{1}, we have v_{1} ∈ P_{1}. As R_{2} ⇛_{ϵ} P_{2}, by Lemma 4, v_{2} ∈ ℂ(P_{2}). Thus, by Lemma 7,

v = σv_{1} + (1 − σ)v_{2} + r_{1} + r_{2} ∈ P_{1} ⊎ P_{2}.

Thus, R_{1} ⊎ R_{2} ⇛_{ϵ} P_{1} ⊎ P_{2}.

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.

To prove item (3) of the proposition, we assume that R ⇛_{Y} P and show that g(R) ⇛_{Y} f(P). 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 2 and f(P) = [[g(R)]] follow trivially from the hypothesis. To complete the proof, we have to show that if R is a G-ϵ-polyhedron then g(R) is a G-ϵ-polyhedron. If R = ∅, then also g(R) = ∅ and there is nothing to prove. If otherwise R ≠ ∅, then −e_{ϵ} is a ray in R. We have g(R) ≠ ∅ and the ray is unaffected by the affine transformation, so that −e_{ϵ} is also a ray in g(R). ⊓ ⊔

Proof (Proof of Proposition 5 on page 12). We first prove item 2, which easily follows from two applications of Lemma 4, since P ≠ ∅. Namely

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

We now prove the only if part of item 1. Thus, let c = (⟨a, x⟩ + 0 · ϵ ≥ b) and suppose that R ⊆ con({c}). Consider a point q = (v^{T}, e)^{T} ∈ R′; by condition (3) of Definition 2, (v^{T}, 0)^{T} ∈ R′ so that, by the previous paragraph, we have (v^{T}, 0)^{T} ∈ R. Thus, the vector (v^{T}, 0)^{T} satisfies c and, since the coefficient of ϵ in c is 0, q also satisfies c. As the choice of q ∈ R′ is arbitrary, R′ ⊆ con({c}). The if part follows by the same reasoning as above, after swapping R and R′.

⊓ ⊔

The proof of Proposition 6 requires some additional notation and a few preliminary lemmas.

Let R = con(C) ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P ≠ ∅. Then, the set of ϵ-upper-bounds of the constraint system C is defined as

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

A constraint c ∈ C_{ϵ} will be usually denoted as ϵ ≤ δ. Note that, since P ≠ ∅, we have δ > 0.

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

Proof. Suppose that −e_{ϵ} is a ray of R. Let (v^{T}, e)^{T} ∈ R. Then, for all ρ ∈ ℝ_{+}, (v^{T}, e)^{T}+ρ(−e_{ϵ}) ∈ R. Thus, if (⟨a, x⟩+s·ϵ ≥ b) ∈ C, we have ⟨a, v⟩+s·(e−ρ) ≥ b for all ρ ∈ ℝ_{+}. Thus s ≤ 0 so that 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 non-empty, there exists a point (v^{T}, e)^{T} ∈ R. Also, for all ρ ∈ ℝ_{+}, ⟨a, v⟩ + s · (e − ρ) ≥ b. As our choice of constraint in C is arbitrary, (v^{T}, e)^{T} + ρ(−e_{ϵ}) satisfies all constraints in C and is therefore in R. Thus −e_{ϵ} is a ray in R. ⊓ ⊔

Lemma 9. 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 1, since R is an ϵ-polyhedron, R′′ is also an ϵ-polyhedron. To complete the proof, we show that R′ = R′′.

Observe that R′′ ⊆ R′, because C′ ⊆ C′′. We now show the other inclusion R′ ⊆ R′′. Let p = (v^{T}, e)^{T} ∈ R′, so that e ≥ 0. By hypothesis, P ≠ ∅ so that 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′_{>} ∪C′_{≥} ∪C′_{ϵ}. We show that p also satisfies all the constraints in C^{∗}, so that p ∈ R′′, completing the proof. 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 c^{∗} = (⟨a, x⟩ + s · ϵ ≥ b) ∈ C^{∗}. Note that e_{τ} > 0 and, by definition of C^{∗}, we have s > 0. As a consequence, (vτ^{T}, 0)^{T} does not satisfy c^{∗}, which implies (vτ^{T}, 0)^{T} ∉ R′′. However, since R′′ is an ϵpolyhedron, this contradics condition (3) of Definition 2. ⊓ ⊔

Lemma 10. 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. Consider c ∈ C_{≥}, so that c = (⟨a, x⟩ + 0 · ϵ ≥ b); then c ∈ sat con(p, C_{≥}) if and only if c ∈ sat con(p_{0}, C_{≥}), so that sat con(p_{0}, C_{≥}) = sat con(p, C_{≥}). Consider now c ∈ C_{>}, so that c = (⟨a, x⟩ + s · ϵ ≥ b) where s < 0; since e > 0, we obtain ⟨a, v⟩ > b, so that p_{0} satisfies but does not saturate c; thus sat con(p_{0}, C_{>}) = ∅. Consider now c ∈ C_{ϵ}, so that c = (ϵ ≤ δ) for some δ > 0; then it follows that sat con(p_{0}, C_{ϵ}) = ∅. By all the above relations, 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 11. Let (C, G) ≡ R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. Let also c ∈ C_{>} be such that c = (⟨a, x⟩ + s · ϵ ≥ b) and consider c_{0} = (⟨a, x⟩ + 0 · ϵ ≥ b). Then

sat gen(c_{0}, (G_{R}, G_{C})) = sat gen(c, (G_{R}, G_{C})).

Proof. If p = (v^{T}, e)^{T} ∈ G_{C} ∪ G_{R}, then e = 0. Thus, ⟨a, v⟩ + s · e = b if and only if ⟨a, v⟩ + 0 · e = b. Similarly, ⟨a, v⟩ + s · e = 0 if and only if ⟨a, v⟩ + 0 · e = 0. Thus, if p is a point or p is a ray, p saturates c if and only if it saturates c_{0}. As p is an arbitrary point or ray in G_{C} ∪ G_{R}, we have the required result. ⊓ ⊔ Lemma 12. Let (C, G) ≡ R ∈ ℂℙ_{n+1} be an ϵ-polyhedron. Let also c ∈ 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 c = (⟨a, x⟩ + s · ϵ ≥ b). Then, as c ∈ C_{>}, s < 0. Since (v^{T}, 0)^{T} ∈ R saturates c, it holds ⟨a, v⟩ = b, so that for all e > 0 we have (v^{T}, e)^{T} ∉ R. Therefore we can apply Lemma 3, 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 13. Let R ∈ ℂℙ_{n+1} be an ϵ-polyhedron and (C, G) ≡ R be a DD pair in minimal form. Then, if c is ϵ-redundant in C, c is unmatched in C.

Proof. Let G = (R, P). Suppose that c = (⟨a, x⟩ + s · ϵ ≥ b) is ϵ-redundant in C. Let also c_{0} = (⟨a, x⟩ + 0 · ϵ ≥ b) be the constraint matching c. We suppose that c_{0} ∈ C and derive a contradiction. As c is ϵ-redundant, by Definition 9, c ∈ C_{>} and there are two cases to consider.

First suppose that

sat gen(c, (G_{R}, G_{C})) ⊑ (G_{R}, ∅).  (13)

Then, for all (v^{T}, 0)^{T} ∈ G_{C}, ⟨a, v⟩ + s · 0 > b. Thus, by Lemma 12, for all (v^{T}, 0)^{T} ∈ R, ⟨a, v⟩ + s · 0 > b. However, by condition (3) of Definition 2, for all (v^{T}, e)^{T} ∈ R, the point (v^{T}, 0)^{T} ∈ R. Thus, for all (v^{T}, e)^{T} ∈ R, we must have ⟨a, v⟩ + 0 · e > b so that c_{0} is not saturated by any points in R. As C is minimal, c_{0} ∉ C which is a contradiction.

Secondly, we assume that (13) does not hold so that, by Definition 9, there exists c′ = (⟨a′, x⟩ + s′ · ϵ ≥ b′) ∈ C_{>} \ {c} such that

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

Let c′_{0} = (⟨a′, x⟩ + 0 · ϵ ≥ b′). As c and c′ are in C_{>}, we have both s < 0 and s′ < 0. By Lemma 11, we have

sat gen(c_{0}, (G_{R}, G_{C})) = sat gen(c, (G_{R}, G_{C})),
sat gen(c′_{0}, (G_{R}, G_{C})) = sat gen(c′, (G_{R}, G_{C}))

so that, by (14),

sat gen(c_{0}, (G_{R}, G_{C})) ⊑ sat gen(c′_{0}, (G_{R}, G_{C})).  (15)

We show that

sat gen(c_{0}, G) ⊑ sat gen(c′_{0}, G).  (16)

Let (H_{R}, H_{P}) = sat gen(c_{0}, (G_{R}, G_{C})) and (H′_{R}, H′_{P}) = sat gen(c′_{0}, (G_{R}, G_{C})). Suppose that p = (v^{T}, e)^{T} ∈ P ∪ R saturates c_{0} so that ⟨a, v⟩ = b. Then, to prove (16), we show that p is a point or ray in sat gen(c′_{0}, G). Let p_{0} = (v^{T}, 0)^{T} so that p_{0} saturates c_{0} and hence, c. Suppose first that p ∈ P. By condition (3) of Definition 2, p_{0} = (v^{T}, 0)^{T} ∈ R. By Lemma 12, p_{0} ∈ gen((H_{R}, H_{C})). Therefore, by (15), p_{0} ∈ gen((H′_{R}, H′_{C})) so that p_{0} saturates c′_{0}. Thus ⟨a′, v⟩ = b′ and p saturates c′_{0}. Thus p is a point in sat gen(c′_{0}, G). Suppose next that that p ∈ R. By Lemma 1, p_{0} = (v^{T}, 0)^{T} is a ray in R. By Lemma 2, every ray in R has a non-positive value for the ϵ coordinate so that as p_{0} is a linear combination of rays in R that saturate c_{0}, p_{0} must be a linear combination of rays in G_{R} that saturate c_{0}. Thus p_{0} is a linear combination of rays in H_{R}. Therefore, by (15), p_{0} must be a linear combination of rays in H′_{R} so that p_{0} saturates c′_{0}. Thus ⟨a′, v⟩ = b′ and p saturates c′_{0}. Thus p is a ray in sat gen(c′_{0}, G).

If c′_{0} and c_{0} are distinct constraints, then c′_{0} is a linear combination of constraints including c′′ ∈ C \ {c_{0}} such that sat gen(c′_{0}, G) ⊑ sat gen(c′′, G). By (16), sat gen(c_{0}, G) ⊑ sat gen(c′′, G) contradicting the hypothesis that C is minimal. On the other hand, if c′_{0} and c_{0} are the same, then c′ = (⟨a, x⟩ + s′ · ϵ ≥ b). As c ≠ c′, either s > s′ or s < s′. If s > s′, every point that satisfies c′ also satisfies c so that c is redundant and similarly, if s < s′, c′ is redundant; both cases contradicting the hypothesis that C is minimal. ⊓ ⊔

Lemma 14. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}. Let R ∈ ℂℙ_{n+1} be such that (C, G) ≡ R is a DD pair in minimal form and R ⇛_{Y} P ≠ ∅. If c is an ϵ-redundant constraint in C, then c is unmatched in C and con(C′) ⇛_{Y} P, where C′ = C \ {c} ∪ {ϵ ≤ 1}.

Proof. By Lemma 13, c is unmatched in C. By Definition 9, we have c ∈ C_{>}; thus c = (⟨a, x⟩ + s · ϵ ≥ b), where a ≠ 0 and s < 0.

Let R′ = con(C′) and consider (v^{T}, e)^{T} ∈ R′ \ R. We first show that

(v^{T}, 0)^{T} ∈ R,  (17)
(v^{T}, 0)^{T} does not saturate c.  (18)

As P ≠ ∅, by Definition 1, there exists (w^{T}, e′_{w})^{T} ∈ R for some e′_{w} > 0. As R is an ϵ-polyhedron, (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 that (w^{T}, e_{w})^{T} ∈ R′. Consider the 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}.  (19)

Letting σ = 0, we obtain v_{0} = w so that, by condition (3) of Definition 2, (v0^{T}, 0)^{T} ∈ R. Now let τ be the maximum value between 0 and 1 such that (vτ^{T}, 0)^{T} ∈ R. Then, for all σ ∈ ℝ such that τ < σ ≤ 1, (vσ^{T}, 0)^{T} ∉ R. Thus, again by condition (3) of Definition 2, (vσ^{T}, e′)^{T} ∉ R for all e′ ∈ ℝ and all σ ∈ ℝ such that τ < σ ≤ 1.

Suppose first that τ < 1. Then, it follows that the only point in R on the line joining (v^{T}, e)^{T} and (vτ^{T}, 0)^{T} is the end point (vτ^{T}, 0)^{T}. As every point on this line is in R′, this implies that (vτ^{T}, 0)^{T} saturates constraint c. Thus, by Lemma 12, (vτ^{T}, 0)^{T} ∈ gen((G_{R}, G_{C})) so that sat gen(c, (G_{R}, G_{C})) ⋢ (G_{R}, ∅). As a consequence, since by hypothesis c is ϵ-redundant in C, by Definition 9 there exists a constraint c′ = (⟨a′, x⟩ + s′ · ϵ ≥ b′) ∈ C′_{>} such that

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

By (20), the point (vτ^{T}, 0)^{T} also saturates c′. As already observed before, for all σ ∈ ℝ such that τ < σ ≤ 1, we have (vσ^{T}, e_{σ})^{T} ∈ R′ \ R, so that (vσ^{T}, e_{σ})^{T} does not satisfy c but does satisfy c′. As s < 0, e_{τ} ≥ 0. Hence, as s′ < 0, the point (vτ^{T}, e_{τ})^{T} either saturates c′ or it does not satisfy c′; in both cases, for all σ ∈ ℝ such that τ < σ ≤ 1, the point (vσ^{T}, e_{σ})^{T} ∈ R′ does not satisfy c′ ∈ C′, which is a contradiction. Thus it must hold τ = 1 and, by (19),

(vτ^{T}, 0)^{T} = (v^{T}, 0)^{T} ∈ R′ ∩ R

so that (17) holds. Suppose now that (18) does not hold, so that (v^{T}, 0)^{T} saturates c. As (v^{T}, e)^{T} ∈ R′ \ R, it does not satisfy c. Thus, since s < 0, we must have e > 0. By (20), (v^{T}, 0)^{T} also saturates c′. Hence, as s′ < 0, (v^{T}, e)^{T} does not satisfy c′, contradicting the assumption that (v^{T}, e)^{T} ∈ R′. Therefore (18) holds.

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 2 holds. By (17), 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 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 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 (17) and (18), ⟨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 so that R is a C-ϵ-polyhedron. By the first part of the proof, R′ ⇛_{ϵ} P. We show that con(C′) ⊆ con({ϵ ≥ 0}). By contraposition, suppose that there exists (u^{T}, e_{u})^{T} ∈ R′ where e_{u} < 0. As [[R′]] ≠ ∅, there exists (w^{T}, e_{w})^{T} ∈ R′ where e_{w} > 0. By condition (2) of Definition 2, (w^{T}, 0)^{T} ∈ R′. Let σ = \frac{e_{w}}{2(e_{w}−e_{u})} so that, as e_{u} < 0 and e_{w} > 0, we have 0 < σ < 1. Then, if

(wσ^{T}, e_{σ})^{T} = σ(u^{T}, e_{u})^{T} + (1 − σ)(w^{T}, e_{w})^{T},
(wσ^{T}, e′_{σ})^{T} = σ(u^{T}, e_{u})^{T} + (1 − σ)(w^{T}, 0)^{T},

we obtain e_{σ} > 0 and e′_{σ} < 0 and both (wσ^{T}, e_{σ})^{T} ∈ R′ and (wσ^{T}, e′_{σ})^{T} ∈ R′. As e_{σ} > 0, w_{σ} ∈ [[R′]] = [[R]]. Thus, by Definition 1 and condition (2) of Definition 2, (wσ^{T}, 0)^{T} ∈ R and hence satisfies c. Thus, as s · e′_{σ} > 0, (wσ^{T}, e′_{σ})^{T} also satisfies c and, as it is in R′ = con(C′), it satisfies all the constraints in C. Thus (wσ^{T}, e′_{σ})^{T} ∈ R. However, as R is a C-ϵ-polyhedron, by Definition 4, R ⊆ con({ϵ ≥ 0}) which contradicts e′_{σ} < 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 6, −e_{ϵ} is a ray of R and we need to show that it is also a ray of R′. By Lemma 8, C = C_{>} ∪ C_{≥} ∪ C_{ϵ}. As c ∈ C_{>} and (ϵ ≤ 1) ∈ C′_{ϵ}, we also have C′ = C′_{>} ∪ C′_{≥} ∪ C′_{ϵ} so that, again by Lemma 8, −e_{ϵ} is a ray of R′. Thus, R′ ⇛_{G} P. ⊓ ⊔

Lemma 15. Let R ∈ ℂℙ_{n+1} be an ϵ-polyhedron and (C, G) ≡ R be a DD pair in minimal form. Then, if p is ϵ-redundant in G, p is unmatched in G.

Proof. Let G = (R, P) and suppose that p = (v^{T}, e)^{T} is ϵ-redundant in G. Then, by Definition 9, p ∈ G_{P} and there exists p′ = (y^{T}, e′)^{T} ∈ G_{P} \ {p} such that

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

As p and p′ are in G_{P}, we have both e > 0 and e′ > 0. Let p_{0} = (v^{T}, 0)^{T} and p′_{0} = (y^{T}, 0)^{T}; as R is an ϵ-polyhedron, by condition (3) of Definition 2, we have both p_{0} ∈ R and p′_{0} ∈ R. Also note that, since G is in minimal form, then v ≠ y.

To prove the result, we assume that p is matched (i.e., p_{0} ∈ P) and derive a contradiction. By Lemma 10, we have

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

so that, by (21),

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

Suppose first that e ≤ e′ and let σ = \frac{e}{e′}, so that 0 < σ ≤ 1. Consider the point q_{e} = σp′ + (1 − σ)p_{0} = (w^{T}, e)^{T}. Being a convex combination of p′ and p_{0}, we have q_{e} ∈ R. Let also r = p − q_{e}; then r cannot be a ray of R, since otherwise we would have p ∈ gen((R, {p′, p_{0}})), contradicting the hypothesis that G is in minimal form. For each ρ ∈ ℝ_{+}, let p_{ρ} = p_{0} + ρr = (s^{T}, 0)^{T}. Since r is not a ray of R, there must exist ρ′ ∈ ℝ_{+} such that p_{ρ′} ∈ R but p_{ρ} ∉ R, for all ρ > ρ′. If ρ′ > 0, then p_{ρ′} ≠ p_{0}; thus, p_{0} can be expressed as a convex combination of p_{ρ′} and p′_{0}, contradicting the hypothesis that G is in minimal form. Therefore, it must hold ρ′ = 0 (i.e., p_{ρ′} = p_{0}). Since for all ρ > 0 we have p_{ρ} = (s^{T}, 0)^{T} ∉ R and R is an ϵ-polyhedron, then (s^{T}, e′′)^{T} ∉ R for all e′′ ∈ ℝ. As a consequence, there must exist a constraint c ∈ C such that c is saturated by all the points lying on the segment identified by p and p_{0}. As a consequence, c ∈ C_{≥} and c is not saturated by p′_{0}. However, this contradicts the condition (22) established above, so that we cannot have e ≤ e′.

Secondly suppose that e > e′ and let p_{e′} = (v^{T}, e′)^{T}. Being a convex combination of p and p_{0}, we have p_{e′} ∈ R. Let also r′ = p′ −p_{e′}; then r′ cannot be a ray of R, since otherwise we would have p′ ∈ gen((R, {p, p_{0}})), contradicting the hypothesis that G is in minimal form. Consider now the vector r = −r′. Again, r cannot be a ray of R, since otherwise p_{0} could be obtained by combining p′_{0} and r. Thus, we are in the same situation identified before and a contradiction can be derived by the same argument. As a consequence, p_{0} ∈ P cannot hold, so that p is unmatched in G, completing the proof. ⊓ ⊔

Lemma 16. Let R ∈ ℂℙ_{n+1} be such that R ⇛_{ϵ} P ≠ ∅, (C, G) ≡ R 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. Therefore, to prove the lemma, we need to show that any point q = (w^{T}, 0)^{T} ∈ R is also in R′. Note that any ray in R is also a ray 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 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 10 to p and p′ we obtain

sat con(p_{0}, C_{≥}) = sat con(p, C_{≥}),  (23)
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, using again (23),

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

Let r = q − q_{1}. If r = 0, then q = q_{1} ∈ R′. Otherwise, let r ≠ 0. If r is a ray in R, then it is also a ray in R′ and there exists ρ ∈ ℝ_{+} such that q = q_{1} + ρr ∈ R′. Suppose therefore that r ≠ 0 is not a ray of R. Then there must exist a minimum value ρ_{2} > 0 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 ∈ C that saturates q_{2} but not q_{1}. Since no constraint in C_{ϵ} can be saturated by q_{2}, we have c ∉ C_{ϵ}. Suppose that c ∈ C_{>}. Then, by Lemma 12, q_{2} ∈ gen((G_{R}, G_{C})); since (G_{R}, G_{C}) ⊑ G′, we obtain q_{2} ∈ R′. Suppose now that c ∈ C_{≥}; then, as c ∉ sat con(q_{1}, C_{≥}), by (24), we obtain c ∉ sat con(p, C_{≥}). Similarly, supposing now c ∈ C \ (C_{>} ∪ C_{≥} ∪ C_{ϵ}), we obtain again c ∉ sat con(p, C), because otherwise we would have p_{0} ∉ R. In both cases, as q_{2} saturates constraint c, then q_{2} can be obtained as a combination of generators in G all of which saturate c, i.e., a combination where p has a zero coefficient, so that q_{2} ∈ gen(G′) = R′.

Thus, in all cases q_{2} ∈ R′ so that, as q lies on the segment [q_{1}, q_{2}] and R′ is a convex set, we have q ∈ R′ as required. ⊓ ⊔

Lemma 17. Let ⇛_{Y} ∈ {⇛_{ϵ}, ⇛_{C}, ⇛_{G}}. Let R ∈ ℂℙ_{n+1} be such that (C, G) ≡ R is a DD pair in minimal form and R ⇛_{Y} P. If p is ϵ-redundant in G = (R, P), then p is unmatched in G and 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. Also note that any ray in R is also a ray in R′.

Suppose that p = (v^{T}, e)^{T} is ϵ-redundant in G so that, by Definition 9, 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).  (25)

Note that p′ ∈ R′. By Lemma 15, p is unmatched in G. Letting p_{0} = (v^{T}, 0)^{T} and p′_{0} = (y^{T}, 0)^{T}, by condition (3) of Definition 2, we have {p_{0}, p′_{0}} ⊆ R.

As (25) holds, we can use Lemma 16, to obtain that, for all w ∈ ℝ^{n},

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

In order to show that R′ ⇛_{ϵ} P, we first prove that R′ is an ϵ-polyhedron. Consider condition (2) of Definition 2. As R′ ⊆ R, R′ satisfies condition (2) by taking the same value δ used for R. Consider now condition (3) of Definition 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 (26), we obtain (w^{T}, 0)^{T} ∈ R′.

Thus, R′ is an ϵ-polyhedron. To show that it is indeed an ϵ-polyhedron for P, we have to prove that [[R]] = [[R′]]. The inclusion [[R′]] ⊆ [[R]] holds by monotonicity of function [[·]], since R′ ⊆ R. To prove the other inclusion, suppose that w ∈ [[R]]. Then there exists e_{w} > 0 such that q = (w^{T}, e_{w})^{T} ∈ R. By condition (3) of Definition 2, we obtain q_{0} = (w^{T}, 0)^{T} ∈ R and hence, by (26), q_{0} ∈ R′. As q ∈ R, by definition of ‘gen’ there exist 0 ≤ π ≤ 1 and p_{1} ∈ gen(G′) such that q = πp+(1−π)p_{1}. If π = 0, then q ∈ R′, so that w ∈ [[R′]] as required. Suppose now that π > 0; then sat con(q, C) ⊆ sat con(p, C). Thus, by (25), we obtain

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

By applying Lemma 10 twice, we obtain

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

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

ρ_{c} = \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}.

Thus q_{c} = (wc^{T}, 0)^{T} is an affine combination of q_{0} and p′_{0}, therefore lying on the line passing through these two points. Note that ρ_{c} > 0 and q_{c} satisfies constraint c. Let c vary in the set of constraints C \ sat con(q_{0}, 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_{ϵ}. By Lemma 9, q_{ρ} also satisfies every constraint in C \(C_{>} ∪C_{≥} ∪C_{ϵ}), so that q_{ρ} ∈ R. Thus, by (26), q_{ρ} ∈ R′. Letting σ = \frac{1}{1+ρ} we obtain 0 < σ < 1 and w = σw_{ρ} + (1 − σ)y. Thus, we have

(w^{T}, (1 − σ)e′)^{T} = σq_{ρ} + (1 − σ)p′ ∈ R′.

As e′ > 0 and σ < 1, we have (1 − σ)e′ > 0 and hence w ∈ [[R′]] as required.

Suppose next that R ⇛_{C} P. Then, by the first part of the proof R′ ⇛_{ϵ} P. By Definition 4, R ⊆ con({ϵ ≥ 0}). Thus, if (v^{T}, e)^{T} ∈ R ∪ P, e ≥ 0. Since G′ ⊑ G, we also obtain gen(G′) ⊆ con({ϵ ≥ 0}), so that R′ ⇛_{C} P.

Finally, suppose that R ⇛_{G} P. By the first part of the proof R′ ⇛_{ϵ} P. Since R ≠ ∅, by Definition 6, we have that −e_{ϵ} is a ray of R. Thus, −e_{ϵ} is also a ray of R′ and R′ ⇛_{G} P, as required. ⊓ ⊔

Proof (Proof of Proposition 6 on page 12). Items 1 and 2 have been proved as Lemmas 14 and 17 respectively. ⊓ ⊔

The proof of Proposition 7 is based on the following lemmas.

Lemma 18. Let R ∈ ℂℙ_{n+1} be such that (C, G) ≡ R is a DD pair in minimal form and R ⇛_{ϵ} P ≠ ∅. If C has no ϵ-redundant constraint then it is in smf.

Proof. To prove the thesis, we assume that C is not in smf and show that C must contain an ϵ-redundant constraint. By Proposition 2, P = con(con enc(C)). As C is not in smf, by Definition 8, there exists a constraint system C′ ⊂ C such that con enc(C′) ⊂ con enc(C) and con(C′ ∪ {ϵ ≤ 1}) ⇛_{ϵ} P. Let R′ = con(C′) and R′_{1} = con(C′ ∪ {ϵ ≤ 1}).

Suppose that all the constraints in con enc(C) \ con enc(C′) are non-strict inequalities. Then, by Definition 3, con enc(C_{>}) = con enc(C′_{>}). Also, by Definition 3, con enc(C) = con enc(C_{>} ∪ C_{≥}) and con enc(C′) = con enc(C′_{>} ∪ C′_{≥}); so that, as con enc(C′) ≠ con enc(C), C′_{≥} ≠ C_{≥}. Thus, since C′ ⊆ C, we obtain C′_{≥} ⊂ C_{≥}. Therefore there exist a ∈ ℝ^{n} \ {0} and b ∈ ℝ such that

c = (⟨a, x⟩ + 0 · ϵ ≥ b) ∈ C \ C′.

Let R_{0} = con(C \ {c}). Then, as C′ ⊆ C \ {c} ⊂ C, R_{0} ⊆ R′ and R ⊆ R_{0}. We now show that R_{0} ⊆ R so that R = R_{0}; therefore contradicting the hypothesis that C is in minimal form. For this, consider any vector p = (v^{T}, e)^{T} ∈ R_{0}. We need to show that p ∈ R. Since R_{0} ⊆ R′, p ∈ R′. We prove that v ∈ ℂ(P) and we do this by considering the cases e ≤ 1 and e > 1 separately. If e ≤ 1, then p satisfies c_{u} = (ϵ ≤ 1) so that p ∈ R′_{1}. In this case, as R′_{1} ⇛_{ϵ} P, by condition (3) of Definition 2, p_{0} = (v^{T}, 0)^{T} ∈ R′_{1} and hence, by Lemma 4, v ∈ ℂ(P). Suppose now that e > 1; then p ∈ con(C′_{>} ∪ C′_{≥} ∪ C′_{ϵ} ∪ {c_{ℓ}}), where c_{ℓ} = (ϵ ≥ 0), and hence, (v^{T}, 1)^{T} ∈ R′′_{1} = con(C′_{>} ∪ C′_{≥} ∪ C′_{ϵ} ∪ {c_{u}, c_{ℓ}}). Since R′_{1} ⇛_{ϵ} P, it follows from Lemma 9, that R′′_{1} ⇛_{ϵ} P; hence, by Definition 2, v ∈ P. Thus in both cases we have v ∈ ℂ(P). Therefore, as R ⇛_{ϵ} P, by Lemma 4, we obtain p_{0} ∈ R so that p_{0} satisfies c. As c ∈ C_{≥}, p also satisfies c and hence p ∈ R. As p is an arbitrary point in R_{0}, R_{0} ⊆ R, as required.

Thus there must exist a constraint c_{1} ∈ con enc(C) \ con enc(C′) which is a strict inequality, so that c_{1} = (⟨a, x⟩ > b) for some a ∈ ℝ^{n} \ {0} and b ∈ ℝ. By Definition 3, for some s < 0,

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

We now show that c is ϵ-redundant in C. Letting G = (R, P), suppose first that no point in gen((R, G_{C})) saturates c; this implies that no point in G_{C} saturates c, so that sat gen(c, (G_{R}, G_{C})) ⊑ (G_{R}, ∅). It follows from Definition 9 that c is ϵ-redundant in C.

Suppose next that there exists a point p ∈ gen((R, G_{C})) saturating c and let p = (v^{T}, e_{v})^{T}. Note that, if e_{c} is the value of the ϵ coordinate of a point in G_{C}, then e_{c} = 0. Also, by Lemma 2, if e_{r} is the value of the ϵ coordinate of a ray in R, then e_{r} ≤ 0. Thus we obtain e_{v} ≤ 0. Since p ∈ R, by condition (3) of Definition 2, p_{0} = (v^{T}, 0)^{T} ∈ R. Since p saturates c and s < 0, we obtain e_{v} = 0, i.e., p = p_{0}. Thus p ∈ gen((G_{R}, G_{C})).

We show that there exist c′ ∈ C′_{>} that is saturated by p. Since s < 0, we have (v^{T}, e)^{T} ∉ R, for all e > 0. As R ⇛_{ϵ} P, by Definition 2, v ∉ P and, by Lemma 4, we have v ∈ ℂ(P). By hypothesis, R′_{1} ⇛_{ϵ} P so that, by applying again Definition 2 and Lemma 4, we obtain (v^{T}, e)^{T} ∉ R′_{1}, for all e > 0, and p ∈ R′_{1}. As a consequence, there must exist c′ = (⟨a′, x⟩ + s′ · ϵ ≥ b′) ∈ C′ such that c′ is saturated by p but not satisfied by (v^{T}, e)^{T}, for any e > 0. Thus s′ < 0 and hence, c′ ∈ C′_{>} (note that it cannot be c′ = (ϵ ≤ 0) because we have P ≠ ∅).

Let H = (H_{R}, H_{C}) = sat gen(c, (G_{R}, G_{C})) and C′_{>} = {c′_{1}, …, c′_{k}}. Suppose that, for each 1 ≤ i ≤ k, there exists a point q_{i} ∈ gen(H) that does not saturate c′_{i}. Then the convex combination \frac{1}{k} ∑_{i=1}^{k} q_{i} ∈ gen(H) saturates c, but does not saturate any constraint in C′_{>}, contradicting the previous paragraph. As a consequence, there exists a constraint c′_{j} ∈ C′_{>} that is saturated by all the points in gen(H), so that H ⊑ sat gen(c′_{j}, G). It then follows from Definition 9 that c is ϵ-redundant in C. ⊓ ⊔

Lemma 19. Let R ∈ ℂℙ_{n+1} be such that (C, G) ≡ R is a DD pair in minimal form and R ⇛_{ϵ} P ≠ ∅. If G has no ϵ-redundant generator then it is in smf.

Proof. To prove the thesis, we assume that G is not in smf and show that G must have an ϵ-redundant generator. Let (R, P) = G and (R_{1}, P_{1}, C_{1}) = gen enc(G). Since R ⇛_{ϵ} P then, by Proposition 2, we have P = gen(gen enc(G)). As G is in minimal form but not in smf, then by Definition 8, there exists G′ = (R′, P′) such that G′ ⊏ G, R′ = gen(G′) ⇛_{ϵ} P and gen enc(G′) ⊏ gen enc(G). Let (R′_{1}, P′_{1}, C′_{1}) = gen enc(G′); thus we have R′_{1} ⊂ R_{1}, or P′_{1} ⊂ P_{1}, or C′_{1} ⊂ C_{1}. Note that, again by Proposition 2, we have P = gen(gen enc(G′)).

We first suppose that there exists v ∈ R_{1} \ R′_{1} and derive a contradiction. By Definition 3, (v^{T}, 0)^{T} ∈ R \ R′. Thus v is a ray in P and hence v is the positive combination of rays in R′_{1}. By Definition 3, there is a ray r ∈ R′_{1} if and only if there is a ray (r^{T}, 0)^{T} ∈ R′. Therefore (v^{T}, 0)^{T} is the positive combination of rays in R \ {(v^{T}, 0)^{T}}; contradicting the hypothesis that G is in minimal form.

We next suppose there exists v ∈ C_{1} \ C′_{1} and derive a contradiction. By Definition 3, p_{0} = (v^{T}, 0)^{T} ∈ P and (v^{T}, e)^{T} ∉ P for all e > 0. As P′ ⊆ P, we also have that (v^{T}, e)^{T} ∉ P′ for all e > 0. As a consequence, as v ∉ C′_{1}, by Definition 3 we obtain p_{0} ∉ P′. Since P ≠ ∅, we have v ∈ ℂ(P). Thus, since R′ ⇛_{ϵ} P, we can apply Lemma 4 to obtain p_{0} ∈ R′. Let G′′ = (R, P \ {p_{0}}); then, we have G′ ⊑ G′′ ⊏ G. By the monotonicity of the function gen, we obtain p_{0} ∈ gen(G′′), so that gen(G′′) = R, contradicting the hypothesis that G is in minimal form.

Therefore there exists a vector v ∈ P_{1} \P′_{1}. By Definition 3, there exists e > 0 such that p = (v^{T}, e)^{T} ∈ P, so that p ∈ G_{P}. Moreover, since v ∉ P′_{1}, we have p ∉ G′_{P}. Let C′ = sat con(p, C_{≥}) and

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

(Note that the constraints in C′ are defined on the vector space ℝ^{n+1}, whereas those in C′_{1} are defined on ℝ^{n}.) Then v saturates all the constraints in C′_{1}. For all c = (⟨a, x⟩ + 0 · ϵ ≥ b) ∈ C′ and all s < 0, we have c_{s} = (⟨a, x⟩ + s · ϵ ≥ b) ∉ C, because otherwise we would have p ∉ R. Thus, by Definition 3, we obtain C′_{1} ⊆ con enc(C), which also implies P ⊆ con(C′_{1}).

As gen(gen enc(G′)) = P, then v can be obtained by combining the generators in (R′_{1}, P′_{1}, C′_{1}). By definition of gen, this means that there exists a point y ∈ P′_{1} that, in such a combination, has a strictly positive coefficient; this implies that sat con(v, con enc(C)) ⊆ sat con(y, con enc(C)); in particular, since C′_{1} ⊆ con enc(C), we obtain sat con(v, C′_{1}) ⊆ sat con(y, C′_{1}). By Definition 3, there exists e′ > 0 such that p′ = (y^{T}, e′)^{T} ∈ P′, so that p′ ∈ G′_{P}. Since G′ ⊏ G, we also obtain p′ ∈ G_{P} \ {p}. Observe that, as y saturates every constraint in C′_{1}, then p′ saturates every constraint in C′. It follows that sat con(p, C_{≥}) ⊆ sat con(p′, C_{≥}) and, by Definition 9, p is ϵ-redundant in G. ⊓ ⊔

Proof (Proof of Proposition 7 on page 12). Items 1 and 2 have been proved as Lemmas 18 and 19 respectively. ⊓ ⊔