add isl_pw_qpolynomial_fold_insert_dims
[isl.git] / doc / implementation.tex
blob758d27ee128a4907cf9742582cc1f2be1f353130
1 \section{Sets and Relations}
3 \begin{definition}[Polyhedral Set]
4 A {\em polyhedral set}\index{polyhedral set} $S$ is a finite union of basic sets
5 $S = \bigcup_i S_i$, each of which can be represented using affine
6 constraints
7 $$
8 S_i : \Z^n \to 2^{\Z^d} : \vec s \mapsto
9 S_i(\vec s) =
10 \{\, \vec x \in \Z^d \mid \exists \vec z \in \Z^e :
11 A \vec x + B \vec s + D \vec z + \vec c \geq \vec 0 \,\}
14 with $A \in \Z^{m \times d}$,
15 $B \in \Z^{m \times n}$,
16 $D \in \Z^{m \times e}$
17 and $\vec c \in \Z^m$.
18 \end{definition}
20 \begin{definition}[Parameter Domain of a Set]
21 Let $S \in \Z^n \to 2^{\Z^d}$ be a set.
22 The {\em parameter domain} of $S$ is the set
23 $$\pdom S \coloneqq \{\, \vec s \in \Z^n \mid S(\vec s) \ne \emptyset \,\}.$$
24 \end{definition}
26 \begin{definition}[Polyhedral Relation]
27 A {\em polyhedral relation}\index{polyhedral relation}
28 $R$ is a finite union of basic relations
29 $R = \bigcup_i R_i$ of type
30 $\Z^n \to 2^{\Z^{d_1+d_2}}$,
31 each of which can be represented using affine
32 constraints
34 R_i = \vec s \mapsto
35 R_i(\vec s) =
36 \{\, \vec x_1 \to \vec x_2 \in \Z^{d_1} \times \Z^{d_2}
37 \mid \exists \vec z \in \Z^e :
38 A_1 \vec x_1 + A_2 \vec x_2 + B \vec s + D \vec z + \vec c \geq \vec 0 \,\}
41 with $A_i \in \Z^{m \times d_i}$,
42 $B \in \Z^{m \times n}$,
43 $D \in \Z^{m \times e}$
44 and $\vec c \in \Z^m$.
45 \end{definition}
47 \begin{definition}[Parameter Domain of a Relation]
48 Let $R \in \Z^n \to 2^{\Z^{d+d}}$ be a relation.
49 The {\em parameter domain} of $R$ is the set
50 $$\pdom R \coloneqq \{\, \vec s \in \Z^n \mid R(\vec s) \ne \emptyset \,\}.$$
51 \end{definition}
53 \begin{definition}[Domain of a Relation]
54 Let $R \in \Z^n \to 2^{\Z^{d+d}}$ be a relation.
55 The {\em domain} of $R$ is the polyhedral set
56 $$\domain R \coloneqq \vec s \mapsto
57 \{\, \vec x_1 \in \Z^{d_1} \mid \exists \vec x_2 \in \Z^{d_2} :
58 (\vec x_1, \vec x_2) \in R(\vec s) \,\}
61 \end{definition}
63 \begin{definition}[Range of a Relation]
64 Let $R \in \Z^n \to 2^{\Z^{d+d}}$ be a relation.
65 The {\em range} of $R$ is the polyhedral set
67 \range R \coloneqq \vec s \mapsto
68 \{\, \vec x_2 \in \Z^{d_2} \mid \exists \vec x_1 \in \Z^{d_1} :
69 (\vec x_1, \vec x_2) \in R(\vec s) \,\}
72 \end{definition}
74 \begin{definition}[Composition of Relations]
75 Let $R \in \Z^n \to 2^{\Z^{d_1+d_2}}$ and
76 $S \in \Z^n \to 2^{\Z^{d_2+d_3}}$ be two relations,
77 then the composition of
78 $R$ and $S$ is defined as
80 S \circ R \coloneqq
81 \vec s \mapsto
82 \{\, \vec x_1 \to \vec x_3 \in \Z^{d_1} \times \Z^{d_3}
83 \mid \exists \vec x_2 \in \Z^{d_2} :
84 \vec x_1 \to \vec x_2 \in R(\vec s) \wedge
85 \vec x_2 \to \vec x_3 \in S(\vec s)
86 \,\}
89 \end{definition}
91 \begin{definition}[Difference Set of a Relation]
92 Let $R \in \Z^n \to 2^{\Z^{d+d}}$ be a relation.
93 The difference set ($\Delta \, R$) of $R$ is the set
94 of differences between image elements and the corresponding
95 domain elements,
97 \Delta \, R \coloneqq
98 \vec s \mapsto
99 \{\, \vec \delta \in \Z^{d} \mid \exists \vec x \to \vec y \in R :
100 \vec \delta = \vec y - \vec x
101 \,\}
103 \end{definition}
105 \section{Simple Hull}\label{s:simple hull}
107 It is sometimes useful to have a single
108 basic set or basic relation that contains a given set or relation.
109 For rational sets, the obvious choice would be to compute the
110 (rational) convex hull. For integer sets, the obvious choice
111 would be the integer hull.
112 However, {\tt isl} currently does not support an integer hull operation
113 and even if it did, it would be fairly expensive to compute.
114 The convex hull operation is supported, but it is also fairly
115 expensive to compute given only an implicit representation.
117 Usually, it is not required to compute the exact integer hull,
118 and an overapproximation of this hull is sufficient.
119 The ``simple hull'' of a set is such an overapproximation
120 and it is defined as the (inclusion-wise) smallest basic set
121 that is described by constraints that are translates of
122 the constraints in the input set.
123 This means that the simple hull is relatively cheap to compute
124 and that the number of constraints in the simple hull is no
125 larger than the number of constraints in the input.
126 \begin{definition}[Simple Hull of a Set]
127 The {\em simple hull} of a set
128 $S = \bigcup_{1 \le i \le v} S_i$, with
130 S : \Z^n \to 2^{\Z^d} : \vec s \mapsto
131 S(\vec s) =
132 \left\{\, \vec x \in \Z^d \mid \exists \vec z \in \Z^e :
133 \bigvee_{1 \le i \le v}
134 A_i \vec x + B_i \vec s + D_i \vec z + \vec c_i \geq \vec 0 \,\right\}
136 is the set
138 H : \Z^n \to 2^{\Z^d} : \vec s \mapsto
139 S(\vec s) =
140 \left\{\, \vec x \in \Z^d \mid \exists \vec z \in \Z^e :
141 \bigwedge_{1 \le i \le v}
142 A_i \vec x + B_i \vec s + D_i \vec z + \vec c_i + \vec K_i \geq \vec 0
143 \,\right\}
146 with $\vec K_i$ the (component-wise) smallest non-negative integer vectors
147 such that $S \subseteq H$.
148 \end{definition}
149 The $\vec K_i$ can be obtained by solving a number of
150 LP problems, one for each element of each $\vec K_i$.
151 If any LP problem is unbounded, then the corresponding constraint
152 is dropped.
154 \section{Coalescing}\label{s:coalescing}
156 See \shortciteN{Verdoolaege2009isl}, for now.
157 More details will be added later.
159 \section{Transitive Closure}
161 \subsection{Introduction}
163 \begin{definition}[Power of a Relation]
164 Let $R \in \Z^n \to 2^{\Z^{d+d}}$ be a relation and
165 $k \in \Z_{\ge 1}$
166 a positive number, then power $k$ of relation $R$ is defined as
167 \begin{equation}
168 \label{eq:transitive:power}
169 R^k \coloneqq
170 \begin{cases}
171 R & \text{if $k = 1$}
173 R \circ R^{k-1} & \text{if $k \ge 2$}
175 \end{cases}
176 \end{equation}
177 \end{definition}
179 \begin{definition}[Transitive Closure of a Relation]
180 Let $R \in \Z^n \to 2^{\Z^{d+d}}$ be a relation,
181 then the transitive closure $R^+$ of $R$ is the union
182 of all positive powers of $R$,
184 R^+ \coloneqq \bigcup_{k \ge 1} R^k
187 \end{definition}
188 Alternatively, the transitive closure may be defined
189 inductively as
190 \begin{equation}
191 \label{eq:transitive:inductive}
192 R^+ \coloneqq R \cup \left(R \circ R^+\right)
194 \end{equation}
196 Since the transitive closure of a polyhedral relation
197 may no longer be a polyhedral relation \shortcite{Kelly1996closure},
198 we can, in the general case, only compute an approximation
199 of the transitive closure.
200 Whereas \shortciteN{Kelly1996closure} compute underapproximations,
201 we, like \shortciteN{Beletska2009}, compute overapproximations.
202 That is, given a relation $R$, we will compute a relation $T$
203 such that $R^+ \subseteq T$. Of course, we want this approximation
204 to be as close as possible to the actual transitive closure
205 $R^+$ and we want to detect the cases where the approximation is
206 exact, i.e., where $T = R^+$.
208 For computing an approximation of the transitive closure of $R$,
209 we follow the same general strategy as \shortciteN{Beletska2009}
210 and first compute an approximation of $R^k$ for $k \ge 1$ and then project
211 out the parameter $k$ from the resulting relation.
213 \begin{example}
214 As a trivial example, consider the relation
215 $R = \{\, x \to x + 1 \,\}$. The $k$th power of this map
216 for arbitrary $k$ is
218 R^k = k \mapsto \{\, x \to x + k \mid k \ge 1 \,\}
221 The transitive closure is then
223 \begin{aligned}
224 R^+ & = \{\, x \to y \mid \exists k \in \Z_{\ge 1} : y = x + k \,\}
226 & = \{\, x \to y \mid y \ge x + 1 \,\}
228 \end{aligned}
230 \end{example}
232 \subsection{Computing an Approximation of $R^k$}
233 \label{s:power}
235 There are some special cases where the computation of $R^k$ is very easy.
236 One such case is that where $R$ does not compose with itself,
237 i.e., $R \circ R = \emptyset$ or $\domain R \cap \range R = \emptyset$.
238 In this case, $R^k$ is only non-empty for $k=1$ where it is equal
239 to $R$ itself.
241 In general, it is impossible to construct a closed form
242 of $R^k$ as a polyhedral relation.
243 We will therefore need to make some approximations.
244 As a first approximations, we will consider each of the basic
245 relations in $R$ as simply adding one or more offsets to a domain element
246 to arrive at an image element and ignore the fact that some of these
247 offsets may only be applied to some of the domain elements.
248 That is, we will only consider the difference set $\Delta\,R$ of the relation.
249 In particular, we will first construct a collection $P$ of paths
250 that move through
251 a total of $k$ offsets and then intersect domain and range of this
252 collection with those of $R$.
253 That is,
254 \begin{equation}
255 \label{eq:transitive:approx}
256 K = P \cap \left(\domain R \to \range R\right)
258 \end{equation}
259 with
260 \begin{equation}
261 \label{eq:transitive:path}
262 P = \vec s \mapsto \{\, \vec x \to \vec y \mid
263 \exists k_i \in \Z_{\ge 0}, \vec\delta_i \in k_i \, \Delta_i(\vec s) :
264 \vec y = \vec x + \sum_i \vec\delta_i
265 \wedge
266 \sum_i k_i = k > 0
267 \,\}
268 \end{equation}
269 and with $\Delta_i$ the basic sets that compose
270 the difference set $\Delta\,R$.
271 Note that the number of basic sets $\Delta_i$ need not be
272 the same as the number of basic relations in $R$.
273 Also note that since addition is commutative, it does not
274 matter in which order we add the offsets and so we are allowed
275 to group them as we did in \eqref{eq:transitive:path}.
277 If all the $\Delta_i$s are singleton sets
278 $\Delta_i = \{\, \vec \delta_i \,\}$ with $\vec \delta_i \in \Z^d$,
279 then \eqref{eq:transitive:path} simplifies to
280 \begin{equation}
281 \label{eq:transitive:singleton}
282 P = \{\, \vec x \to \vec y \mid
283 \exists k_i \in \Z_{\ge 0} :
284 \vec y = \vec x + \sum_i k_i \, \vec \delta_i
285 \wedge
286 \sum_i k_i = k > 0
287 \,\}
288 \end{equation}
289 and then the approximation computed in \eqref{eq:transitive:approx}
290 is essentially the same as that of \shortciteN{Beletska2009}.
291 If some of the $\Delta_i$s are not singleton sets or if
292 some of $\vec \delta_i$s are parametric, then we need
293 to resort to further approximations.
295 To ease both the exposition and the implementation, we will for
296 the remainder of this section work with extended offsets
297 $\Delta_i' = \Delta_i \times \{\, 1 \,\}$.
298 That is, each offset is extended with an extra coordinate that is
299 set equal to one. The paths constructed by summing such extended
300 offsets have the length encoded as the difference of their
301 final coordinates. The path $P'$ can then be decomposed into
302 paths $P_i'$, one for each $\Delta_i$,
303 \begin{equation}
304 \label{eq:transitive:decompose}
305 P' = \left(
306 (P_m' \cup \identity) \circ \cdots \circ
307 (P_2' \cup \identity) \circ
308 (P_1' \cup \identity)
309 \right) \cap
310 \{\,
311 \vec x' \to \vec y' \mid y_{d+1} - x_{d+1} = k > 0
312 \,\}
314 \end{equation}
315 with
317 P_i' = \vec s \mapsto \{\, \vec x' \to \vec y' \mid
318 \exists k \in \Z_{\ge 1}, \vec \delta \in k \, \Delta_i'(\vec s) :
319 \vec y' = \vec x' + \vec \delta
320 \,\}
323 Note that each $P_i'$ contains paths of length at least one.
324 We therefore need to take the union with the identity relation
325 when composing the $P_i'$s to allow for paths that do not contain
326 any offsets from one or more $\Delta_i'$.
327 The path that consists of only identity relations is removed
328 by imposing the constraint $y_{d+1} - x_{d+1} > 0$.
329 Taking the union with the identity relation means that
330 that the relations we compose in \eqref{eq:transitive:decompose}
331 each consist of two basic relations. If there are $m$
332 disjuncts in the input relation, then a direct application
333 of the composition operation may therefore result in a relation
334 with $2^m$ disjuncts, which is prohibitively expensive.
335 It is therefore crucial to apply coalescing (\autoref{s:coalescing})
336 after each composition.
338 Let us now consider how to compute an overapproximation of $P_i'$.
339 Those that correspond to singleton $\Delta_i$s are grouped together
340 and handled as in \eqref{eq:transitive:singleton}.
341 Note that this is just an optimization. The procedure described
342 below would produce results that are at least as accurate.
343 For simplicity, we first assume that no constraint in $\Delta_i'$
344 involves any existentially quantified variables.
345 We will return to existentially quantified variables at the end
346 of this section.
347 Without existentially quantified variables, we can classify
348 the constraints of $\Delta_i'$ as follows
349 \begin{enumerate}
350 \item non-parametric constraints
351 \begin{equation}
352 \label{eq:transitive:non-parametric}
353 A_1 \vec x + \vec c_1 \geq \vec 0
354 \end{equation}
355 \item purely parametric constraints
356 \begin{equation}
357 \label{eq:transitive:parametric}
358 B_2 \vec s + \vec c_2 \geq \vec 0
359 \end{equation}
360 \item negative mixed constraints
361 \begin{equation}
362 \label{eq:transitive:mixed}
363 A_3 \vec x + B_3 \vec s + \vec c_3 \geq \vec 0
364 \end{equation}
365 such that for each row $j$ and for all $\vec s$,
367 \Delta_i'(\vec s) \cap
368 \{\, \vec \delta' \mid B_{3,j} \vec s + c_{3,j} > 0 \,\}
369 = \emptyset
371 \item positive mixed constraints
373 A_4 \vec x + B_4 \vec s + \vec c_4 \geq \vec 0
375 such that for each row $j$, there is at least one $\vec s$ such that
377 \Delta_i'(\vec s) \cap
378 \{\, \vec \delta' \mid B_{4,j} \vec s + c_{4,j} > 0 \,\}
379 \ne \emptyset
381 \end{enumerate}
382 We will use the following approximation $Q_i$ for $P_i'$:
383 \begin{equation}
384 \label{eq:transitive:Q}
385 \begin{aligned}
386 Q_i = \vec s \mapsto
387 \{\,
388 \vec x' \to \vec y'
389 \mid {} & \exists k \in \Z_{\ge 1}, \vec f \in \Z^d :
390 \vec y' = \vec x' + (\vec f, k)
391 \wedge {}
394 A_1 \vec f + k \vec c_1 \geq \vec 0
395 \wedge
396 B_2 \vec s + \vec c_2 \geq \vec 0
397 \wedge
398 A_3 \vec f + B_3 \vec s + \vec c_3 \geq \vec 0
399 \,\}
401 \end{aligned}
402 \end{equation}
403 To prove that $Q_i$ is indeed an overapproximation of $P_i'$,
404 we need to show that for every $\vec s \in \Z^n$, for every
405 $k \in \Z_{\ge 1}$ and for every $\vec f \in k \, \Delta_i(\vec s)$
406 we have that
407 $(\vec f, k)$ satisfies the constraints in \eqref{eq:transitive:Q}.
408 If $\Delta_i(\vec s)$ is non-empty, then $\vec s$ must satisfy
409 the constraints in \eqref{eq:transitive:parametric}.
410 Each element $(\vec f, k) \in k \, \Delta_i'(\vec s)$ is a sum
411 of $k$ elements $(\vec f_j, 1)$ in $\Delta_i'(\vec s)$.
412 Each of these elements satisfies the constraints in
413 \eqref{eq:transitive:non-parametric}, i.e.,
415 \left[
416 \begin{matrix}
417 A_1 & \vec c_1
418 \end{matrix}
419 \right]
420 \left[
421 \begin{matrix}
422 \vec f_j \\ 1
423 \end{matrix}
424 \right]
425 \ge \vec 0
428 The sum of these elements therefore satisfies the same set of inequalities,
429 i.e., $A_1 \vec f + k \vec c_1 \geq \vec 0$.
430 Finally, the constraints in \eqref{eq:transitive:mixed} are such
431 that for any $\vec s$ in the parameter domain of $\Delta$,
432 we have $-\vec r(\vec s) \coloneqq B_3 \vec s + \vec c_3 \le \vec 0$,
433 i.e., $A_3 \vec f_j \ge \vec r(\vec s) \ge \vec 0$
434 and therefore also $A_3 \vec f \ge \vec r(\vec s)$.
435 Note that if there are no mixed constraints and if the
436 rational relaxation of $\Delta_i(\vec s)$, i.e.,
437 $\{\, \vec x \in \Q^d \mid A_1 \vec x + \vec c_1 \ge \vec 0\,\}$,
438 has integer vertices, then the approximation is exact, i.e.,
439 $Q_i = P_i'$. In this case, the vertices of $\Delta'_i(\vec s)$
440 generate the rational cone
441 $\{\, \vec x' \in \Q^{d+1} \mid \left[
442 \begin{matrix}
443 A_1 & \vec c_1
444 \end{matrix}
445 \right] \vec x' \,\}$ and therefore $\Delta'_i(\vec s)$ is
446 a Hilbert basis of this cone \shortcite[Theorem~16.4]{Schrijver1986}.
448 Existentially quantified variables can be handled by
449 classifying them into variables that are uniquely
450 determined by the parameters, variables that are independent
451 of the parameters and others. The first set can be treated
452 as parameters and the second as variables. Constraints involving
453 the other existentially quantified variables are removed.
455 \begin{example}
456 Consider the relation
459 n \to \{\, x \to y \mid \exists \, \alpha_0, \alpha_1: 7\alpha_0 = -2 + n \wedge 5\alpha_1 = -1 - x + y \wedge y \ge 6 + x \,\}
462 The difference set of this relation is
464 \Delta = \Delta \, R =
465 n \to \{\, x \mid \exists \, \alpha_0, \alpha_1: 7\alpha_0 = -2 + n \wedge 5\alpha_1 = -1 + x \wedge x \ge 6 \,\}
468 The existentially quantified variables can be defined in terms
469 of the parameters and variables as
471 \alpha_0 = \floor{\frac{-2 + n}7}
472 \qquad
473 \text{and}
474 \qquad
475 \alpha_1 = \floor{\frac{-1 + x}5}
478 $\alpha_0$ can therefore be treated as a parameter,
479 while $\alpha_1$ can be treated as a variable.
480 This in turn means that $7\alpha_0 = -2 + n$ can be treated as
481 a purely parametric constraint, while the other two constraints are
482 non-parametric.
483 The corresponding $Q$~\eqref{eq:transitive:Q} is therefore
485 \begin{aligned}
486 n \to \{\, (x,z) \to (y,w) \mid
487 \exists\, \alpha_0, \alpha_1, k, f : {} &
488 k \ge 1 \wedge
489 y = x + f \wedge
490 w = z + k \wedge {} \\
492 7\alpha_0 = -2 + n \wedge
493 5\alpha_1 = -k + x \wedge
494 x \ge 6 k
495 \,\}
497 \end{aligned}
499 Projecting out the final coordinates encoding the length of the paths,
500 results in the exact transitive closure
502 R^+ =
503 n \to \{\, x \to y \mid \exists \, \alpha_0, \alpha_1: 7\alpha_1 = -2 + n \wedge 6\alpha_0 \ge -x + y \wedge 5\alpha_0 \le -1 - x + y \,\}
506 \end{example}
508 \subsection{Checking Exactness}
510 The approximation $T$ for the transitive closure $R^+$ can be obtained
511 by projecting out the parameter $k$ from the approximation $K$
512 \eqref{eq:transitive:approx} of the power $R^k$.
513 Since $K$ is an overapproximation of $R^k$, $T$ will also be an
514 overapproximation of $R^+$.
515 To check whether the results are exact, we need to consider two
516 cases depending on whether $R$ is {\em cyclic}, where $R$ is defined
517 to be cyclic if $R^+$ maps any element to itself, i.e.,
518 $R^+ \cap \identity \ne \emptyset$.
519 If $R$ is acyclic, then the inductive definition of
520 \eqref{eq:transitive:inductive} is equivalent to its completion,
521 i.e.,
523 R^+ = R \cup \left(R \circ R^+\right)
525 is a defining property.
526 Since $T$ is known to be an overapproximation, we only need to check
527 whether
529 T \subseteq R \cup \left(R \circ T\right)
532 This is essentially Theorem~5 of \shortciteN{Kelly1996closure}.
533 The only difference is that they only consider lexicographically
534 forward relations, a special case of acyclic relations.
536 If, on the other hand, $R$ is cyclic, then we have to resort
537 to checking whether the approximation $K$ of the power is exact.
538 Note that $T$ may be exact even if $K$ is not exact, so the check
539 is sound, but incomplete.
540 To check exactness of the power, we simply need to check
541 \eqref{eq:transitive:power}. Since again $K$ is known
542 to be an overapproximation, we only need to check whether
544 \begin{aligned}
545 K'|_{y_{d+1} - x_{d+1} = 1} & \subseteq R'
547 K'|_{y_{d+1} - x_{d+1} \ge 2} & \subseteq R' \circ K'|_{y_{d+1} - x_{d+1} \ge 1}
549 \end{aligned}
551 where $R' = \{\, \vec x' \to \vec y' \mid \vec x \to \vec y \in R
552 \wedge y_{d+1} - x_{d+1} = 1\,\}$, i.e., $R$ extended with path
553 lengths equal to 1.
555 All that remains is to explain how to check the cyclicity of $R$.
556 Note that the exactness on the power is always sound, even
557 in the acyclic case, so we only need to be careful that we find
558 all cyclic cases. Now, if $R$ is cyclic, i.e.,
559 $R^+ \cap \identity \ne \emptyset$, then, since $T$ is
560 an overapproximation of $R^+$, also
561 $T \cap \identity \ne \emptyset$. This in turn means
562 that $\Delta \, K'$ contains a point whose first $d$ coordinates
563 are zero and whose final coordinate is positive.
564 In the implementation we currently perform this test on $P'$ instead of $K'$.
565 Note that if $R^+$ is acyclic and $T$ is not, then the approximation
566 is clearly not exact and the approximation of the power $K$
567 will not be exact either.
569 \subsection{Decomposing $R$ into strongly connected components}
571 If the input relation $R$ is a union of several basic relations
572 that can be partially ordered
573 then the accuracy of the approximation may be improved by computing
574 an approximation of each strongly connected components separately.
575 For example, if $R = R_1 \cup R_2$ and $R_1 \circ R_2 = \emptyset$,
576 then we know that any path that passes through $R_2$ cannot later
577 pass through $R_1$, i.e.,
578 \begin{equation}
579 \label{eq:transitive:components}
580 R^+ = R_1^+ \cup R_2^+ \cup \left(R_2^+ \circ R_1^+\right)
582 \end{equation}
583 We can therefore compute (approximations of) transitive closures
584 of $R_1$ and $R_2$ separately.
585 Note, however, that the condition $R_1 \circ R_2 = \emptyset$
586 is actually too strong.
587 If $R_1 \circ R_2$ is a subset of $R_2 \circ R_1$
588 then we can reorder the segments
589 in any path that moves through both $R_1$ and $R_2$ to
590 first move through $R_1$ and then through $R_2$.
592 This idea can be generalized to relations that are unions
593 of more than two basic relations by constructing the
594 strongly connected components in the graph with as vertices
595 the basic relations and an edge between two basic relations
596 $R_i$ and $R_j$ if $R_i$ needs to follow $R_j$ in some paths.
597 That is, there is an edge from $R_i$ to $R_j$ iff
598 \begin{equation}
599 \label{eq:transitive:edge}
600 R_i \circ R_j
601 \not\subseteq
602 R_j \circ R_i
604 \end{equation}
605 The components can be obtained from the graph by applying
606 Tarjan's algorithm \shortcite{Tarjan1972}.
608 In practice, we compute the (extended) powers $K_i'$ of each component
609 separately and then compose them as in \eqref{eq:transitive:decompose}.
610 Note, however, that in this case the order in which we apply them is
611 important and should correspond to a topological ordering of the
612 strongly connected components. Simply applying Tarjan's
613 algorithm will produce topologically sorted strongly connected components.
614 The graph on which Tarjan's algorithm is applied is constructed on-the-fly.
615 That is, whenever the algorithm checks if there is an edge between
616 two vertices, we evaluate \eqref{eq:transitive:edge}.
617 The exactness check is performed on each component separately.
618 If the approximation turns out to be inexact for any of the components,
619 then the entire result is marked inexact and the exactness check
620 is skipped on the components that still need to be handled.
622 It should be noted that \eqref{eq:transitive:components}
623 is only valid for exact transitive closures.
624 If overapproximations are computed in the right hand side, then the result will
625 still be an overapproximation of the left hand side, but this result
626 may not be transitively closed. If we only separate components based
627 on the condition $R_i \circ R_j = \emptyset$, then there is no problem,
628 as this condition will still hold on the computed approximations
629 of the transitive closures. If, however, we have exploited
630 \eqref{eq:transitive:edge} during the decomposition and if the
631 result turns out not to be exact, then we check whether
632 the result is transitively closed. If not, we recompute
633 the transitive closure, skipping the decomposition.
634 Note that testing for transitive closedness on the result may
635 be fairly expensive, so we may want to make this check
636 configurable.
638 \begin{figure}
639 \begin{center}
640 \begin{tikzpicture}[x=0.5cm,y=0.5cm,>=stealth,shorten >=1pt]
641 \foreach \x in {1,...,10}{
642 \foreach \y in {1,...,10}{
643 \draw[->] (\x,\y) -- (\x,\y+1);
646 \foreach \x in {1,...,20}{
647 \foreach \y in {5,...,15}{
648 \draw[->] (\x,\y) -- (\x+1,\y);
651 \end{tikzpicture}
652 \end{center}
653 \caption{The relation from \autoref{ex:closure4}}
654 \label{f:closure4}
655 \end{figure}
656 \begin{example}
657 \label{ex:closure4}
658 Consider the relation in example {\tt closure4} that comes with
659 the Omega calculator~\shortcite{Omega_calc}, $R = R_1 \cup R_2$,
660 with
662 \begin{aligned}
663 R_1 & = \{\, (x,y) \to (x,y+1) \mid 1 \le x,y \le 10 \,\}
665 R_2 & = \{\, (x,y) \to (x+1,y) \mid 1 \le x \le 20 \wedge 5 \le y \le 15 \,\}
667 \end{aligned}
669 This relation is shown graphically in \autoref{f:closure4}.
670 We have
672 \begin{aligned}
673 R_1 \circ R_2 &=
674 \{\, (x,y) \to (x+1,y+1) \mid 1 \le x \le 9 \wedge 5 \le y \le 10 \,\}
676 R_2 \circ R_1 &=
677 \{\, (x,y) \to (x+1,y+1) \mid 1 \le x \le 10 \wedge 4 \le y \le 10 \,\}
679 \end{aligned}
681 Clearly, $R_1 \circ R_2 \subseteq R_2 \circ R_1$ and so
683 \left(
684 R_1 \cup R_2
685 \right)^+
687 \left(R_2^+ \circ R_1^+\right)
688 \cup R_1^+
689 \cup R_2^+
692 \end{example}
694 \begin{figure}
695 \newcounter{n}
696 \newcounter{t1}
697 \newcounter{t2}
698 \newcounter{t3}
699 \newcounter{t4}
700 \begin{center}
701 \begin{tikzpicture}[>=stealth,shorten >=1pt]
702 \setcounter{n}{7}
703 \foreach \i in {1,...,\value{n}}{
704 \foreach \j in {1,...,\value{n}}{
705 \setcounter{t1}{2 * \j - 4 - \i + 1}
706 \setcounter{t2}{\value{n} - 3 - \i + 1}
707 \setcounter{t3}{2 * \i - 1 - \j + 1}
708 \setcounter{t4}{\value{n} - \j + 1}
709 \ifnum\value{t1}>0\ifnum\value{t2}>0
710 \ifnum\value{t3}>0\ifnum\value{t4}>0
711 \draw[thick,->] (\i,\j) to[out=20] (\i+3,\j);
712 \fi\fi\fi\fi
713 \setcounter{t1}{2 * \j - 1 - \i + 1}
714 \setcounter{t2}{\value{n} - \i + 1}
715 \setcounter{t3}{2 * \i - 4 - \j + 1}
716 \setcounter{t4}{\value{n} - 3 - \j + 1}
717 \ifnum\value{t1}>0\ifnum\value{t2}>0
718 \ifnum\value{t3}>0\ifnum\value{t4}>0
719 \draw[thick,->] (\i,\j) to[in=-20,out=20] (\i,\j+3);
720 \fi\fi\fi\fi
721 \setcounter{t1}{2 * \j - 1 - \i + 1}
722 \setcounter{t2}{\value{n} - 1 - \i + 1}
723 \setcounter{t3}{2 * \i - 1 - \j + 1}
724 \setcounter{t4}{\value{n} - 1 - \j + 1}
725 \ifnum\value{t1}>0\ifnum\value{t2}>0
726 \ifnum\value{t3}>0\ifnum\value{t4}>0
727 \draw[thick,->] (\i,\j) to (\i+1,\j+1);
728 \fi\fi\fi\fi
731 \end{tikzpicture}
732 \end{center}
733 \caption{The relation from \autoref{ex:decomposition}}
734 \label{f:decomposition}
735 \end{figure}
736 \begin{example}
737 \label{ex:decomposition}
738 Consider the relation on the right of \shortciteN[Figure~2]{Beletska2009},
739 reproduced in \autoref{f:decomposition}.
740 The relation can be described as $R = R_1 \cup R_2 \cup R_3$,
741 with
743 \begin{aligned}
744 R_1 &= n \mapsto \{\, (i,j) \to (i+3,j) \mid
745 i \le 2 j - 4 \wedge
746 i \le n - 3 \wedge
747 j \le 2 i - 1 \wedge
748 j \le n \,\}
750 R_2 &= n \mapsto \{\, (i,j) \to (i,j+3) \mid
751 i \le 2 j - 1 \wedge
752 i \le n \wedge
753 j \le 2 i - 4 \wedge
754 j \le n - 3 \,\}
756 R_3 &= n \mapsto \{\, (i,j) \to (i+1,j+1) \mid
757 i \le 2 j - 1 \wedge
758 i \le n - 1 \wedge
759 j \le 2 i - 1 \wedge
760 j \le n - 1\,\}
762 \end{aligned}
764 The figure shows this relation for $n = 7$.
765 Both
766 $R_3 \circ R_1 \subseteq R_1 \circ R_3$
768 $R_3 \circ R_2 \subseteq R_2 \circ R_3$,
769 which the reader can verify using the {\tt iscc} calculator:
770 \begin{verbatim}
771 R1 := [n] -> { [i,j] -> [i+3,j] : i <= 2 j - 4 and i <= n - 3 and
772 j <= 2 i - 1 and j <= n };
773 R2 := [n] -> { [i,j] -> [i,j+3] : i <= 2 j - 1 and i <= n and
774 j <= 2 i - 4 and j <= n - 3 };
775 R3 := [n] -> { [i,j] -> [i+1,j+1] : i <= 2 j - 1 and i <= n - 1 and
776 j <= 2 i - 1 and j <= n - 1 };
777 (R1 . R3) - (R3 . R1);
778 (R2 . R3) - (R3 . R2);
779 \end{verbatim}
780 $R_3$ can therefore be moved forward in any path.
781 For the other two basic relations, we have both
782 $R_2 \circ R_1 \not\subseteq R_1 \circ R_2$
784 $R_1 \circ R_2 \not\subseteq R_2 \circ R_1$
785 and so $R_1$ and $R_2$ form a strongly connected component.
786 By computing the power of $R_3$ and $R_1 \cup R_2$ separately
787 and composing the results, the power of $R$ can be computed exactly
788 using \eqref{eq:transitive:singleton}.
789 As explained by \shortciteN{Beletska2009}, applying the same formula
790 to $R$ directly, without a decomposition, would result in
791 an overapproximation of the power.
792 \end{example}
794 \subsection{Partitioning the domains and ranges of $R$}
796 The algorithm of \autoref{s:power} assumes that the input relation $R$
797 can be treated as a union of translations.
798 This is a reasonable assumption if $R$ maps elements of a given
799 abstract domain to the same domain.
800 However, if $R$ is a union of relations that map between different
801 domains, then this assumption no longer holds.
802 In particular, when an entire dependence graph is encoded
803 in a single relation, as is done by, e.g.,
804 \shortciteN[Section~6.1]{Barthou2000MSE}, then it does not make
805 sense to look at differences between iterations of different domains.
806 Now, arguably, a modified Floyd-Warshall algorithm should
807 be applied to the dependence graph, as advocated by
808 \shortciteN{Kelly1996closure}, with the transitive closure operation
809 only being applied to relations from a given domain to itself.
810 However, it is also possible to detect disjoint domains and ranges
811 and to apply Floyd-Warshall internally.
813 \linesnumbered
814 \begin{algorithm}
815 \caption{The modified Floyd-Warshall algorithm of
816 \protect\shortciteN{Kelly1996closure}}
817 \label{a:Floyd}
818 \SetKwInput{Input}{Input}
819 \SetKwInput{Output}{Output}
820 \Input{Relations $R_{pq}$, $0 \le p, q < n$}
821 \Output{Updated relations $R_{pq}$ such that each relation
822 $R_{pq}$ contains all indirect paths from $p$ to $q$ in the input graph}
824 \BlankLine
825 \SetVline
826 \dontprintsemicolon
828 \For{$r \in [0, n-1]$}{
829 $R_{rr} \coloneqq R_{rr}^+$ \nllabel{l:Floyd:closure}\;
830 \For{$p \in [0, n-1]$}{
831 \For{$q \in [0, n-1]$}{
832 \If{$p \ne r$ or $q \ne r$}{
833 $R_{pq} \coloneqq R_{pq} \cup \left(R_{rq} \circ R_{pr}\right)
834 \cup \left(R_{rq} \circ R_{rr} \circ R_{pr}\right)$
835 \nllabel{l:Floyd:update}
840 \end{algorithm}
842 Let the input relation $R$ be a union of $m$ basic relations $R_i$.
843 Let $D_{2i}$ be the domains of $R_i$ and $D_{2i+1}$ the ranges of $R_i$.
844 The first step is to group overlapping $D_j$ until a partition is
845 obtained. If the resulting partition consists of a single part,
846 then we continue with the algorithm of \autoref{s:power}.
847 Otherwise, we apply Floyd-Warshall on the graph with as vertices
848 the parts of the partition and as edges the $R_i$ attached to
849 the appropriate pairs of vertices.
850 In particular, let there be $n$ parts $P_k$ in the partition.
851 We construct $n^2$ relations
853 R_{pq} \coloneqq \bigcup_{i \text{ s.t. } \domain R_i \subseteq P_p \wedge
854 \range R_i \subseteq P_q} R_i
857 apply \autoref{a:Floyd} and return the union of all resulting
858 $R_{pq}$ as the transitive closure of $R$.
859 Each iteration of the $r$-loop in \autoref{a:Floyd} updates
860 all relations $R_{pq}$ to include paths that go from $p$ to $r$,
861 possibly stay there for a while, and then go from $r$ to $q$.
862 Note that paths that ``stay in $r$'' include all paths that
863 pass through earlier vertices since $R_{rr}$ itself has been updated
864 accordingly in previous iterations of the outer loop.
865 In principle, it would be sufficient to use the $R_{pr}$
866 and $R_{rq}$ computed in the previous iteration of the
867 $r$-loop in Line~\ref{l:Floyd:update}.
868 However, from an implementation perspective, it is easier
869 to allow either or both of these to have been updated
870 in the same iteration of the $r$-loop.
871 This may result in duplicate paths, but these can usually
872 be removed by coalescing (\autoref{s:coalescing}) the result of the union
873 in Line~\ref{l:Floyd:update}, which should be done in any case.
874 The transitive closure in Line~\ref{l:Floyd:closure}
875 is performed using a recursive call. This recursive call
876 includes the partitioning step, but the resulting partition will
877 usually be a singleton.
878 The result of the recursive call will either be exact or an
879 overapproximation. The final result of Floyd-Warshall is therefore
880 also exact or an overapproximation.
882 \begin{figure}
883 \begin{center}
884 \begin{tikzpicture}[x=1cm,y=1cm,>=stealth,shorten >=3pt]
885 \foreach \x/\y in {0/0,1/1,3/2} {
886 \fill (\x,\y) circle (2pt);
888 \foreach \x/\y in {0/1,2/2,3/3} {
889 \draw (\x,\y) circle (2pt);
891 \draw[->] (0,0) -- (0,1);
892 \draw[->] (0,1) -- (1,1);
893 \draw[->] (2,2) -- (3,2);
894 \draw[->] (3,2) -- (3,3);
895 \draw[->,dashed] (2,2) -- (3,3);
896 \draw[->,dotted] (0,0) -- (1,1);
897 \end{tikzpicture}
898 \end{center}
899 \caption{The relation (solid arrows) on the right of Figure~1 of
900 \protect\shortciteN{Beletska2009} and its transitive closure}
901 \label{f:COCOA:1}
902 \end{figure}
903 \begin{example}
904 Consider the relation on the right of Figure~1 of
905 \shortciteN{Beletska2009},
906 reproduced in \autoref{f:COCOA:1}.
907 This relation can be described as
909 \begin{aligned}
910 \{\, (x, y) \to (x_2, y_2) \mid {} & (3y = 2x \wedge x_2 = x \wedge 3y_2 = 3 + 2x \wedge x \ge 0 \wedge x \le 3) \vee {} \\
911 & (x_2 = 1 + x \wedge y_2 = y \wedge x \ge 0 \wedge 3y \ge 2 + 2x \wedge x \le 2 \wedge 3y \le 3 + 2x) \,\}
913 \end{aligned}
915 Note that the domain of the upward relation overlaps with the range
916 of the rightward relation and vice versa, but that the domain
917 of neither relation overlaps with its own range or the domain of
918 the other relation.
919 The domains and ranges can therefore be partitioned into two parts,
920 $P_0$ and $P_1$, shown as the white and black dots in \autoref{f:COCOA:1},
921 respectively.
922 Initially, we have
924 \begin{aligned}
925 R_{00} & = \emptyset
927 R_{01} & =
928 \{\, (x, y) \to (x+1, y) \mid
929 (x \ge 0 \wedge 3y \ge 2 + 2x \wedge x \le 2 \wedge 3y \le 3 + 2x) \,\}
931 R_{10} & =
932 \{\, (x, y) \to (x_2, y_2) \mid (3y = 2x \wedge x_2 = x \wedge 3y_2 = 3 + 2x \wedge x \ge 0 \wedge x \le 3) \,\}
934 R_{11} & = \emptyset
936 \end{aligned}
938 In the first iteration, $R_{00}$ remains the same ($\emptyset^+ = \emptyset$).
939 $R_{01}$ and $R_{10}$ are therefore also unaffected, but
940 $R_{11}$ is updated to include $R_{01} \circ R_{10}$, i.e.,
941 the dashed arrow in the figure.
942 This new $R_{11}$ is obviously transitively closed, so it is not
943 changed in the second iteration and it does not have an effect
944 on $R_{01}$ and $R_{10}$. However, $R_{00}$ is updated to
945 include $R_{10} \circ R_{01}$, i.e., the dotted arrow in the figure.
946 The transitive closure of the original relation is then equal to
947 $R_{00} \cup R_{01} \cup R_{10} \cup R_{11}$.
948 \end{example}
950 \subsection{Incremental Computation}
951 \label{s:incremental}
953 In some cases it is possible and useful to compute the transitive closure
954 of union of basic relations incrementally. In particular,
955 if $R$ is a union of $m$ basic maps,
957 R = \bigcup_j R_j
960 then we can pick some $R_i$ and compute the transitive closure of $R$ as
961 \begin{equation}
962 \label{eq:transitive:incremental}
963 R^+ = R_i^+ \cup
964 \left(
965 \bigcup_{j \ne i}
966 R_i^* \circ R_j \circ R_i^*
967 \right)^+
969 \end{equation}
970 For this approach to be successful, it is crucial that each
971 of the disjuncts in the argument of the second transitive
972 closure in \eqref{eq:transitive:incremental} be representable
973 as a single basic relation, i.e., without a union.
974 If this condition holds, then by using \eqref{eq:transitive:incremental},
975 the number of disjuncts in the argument of the transitive closure
976 can be reduced by one.
977 Now, $R_i^* = R_i^+ \cup \identity$, but in some cases it is possible
978 to relax the constraints of $R_i^+$ to include part of the identity relation,
979 say on domain $D$. We will use the notation
980 ${\cal C}(R_i,D) = R_i^+ \cup \identity_D$ to represent
981 this relaxed version of $R^+$.
982 \shortciteN{Kelly1996closure} use the notation $R_i^?$.
983 ${\cal C}(R_i,D)$ can be computed by allowing $k$ to attain
984 the value $0$ in \eqref{eq:transitive:Q} and by using
986 P \cap \left(D \to D\right)
988 instead of \eqref{eq:transitive:approx}.
989 Typically, $D$ will be a strict superset of both $\domain R_i$
990 and $\range R_i$. We therefore need to check that domain
991 and range of the transitive closure are part of ${\cal C}(R_i,D)$,
992 i.e., the part that results from the paths of positive length ($k \ge 1$),
993 are equal to the domain and range of $R_i$.
994 If not, then the incremental approach cannot be applied for
995 the given choice of $R_i$ and $D$.
997 In order to be able to replace $R^*$ by ${\cal C}(R_i,D)$
998 in \eqref{eq:transitive:incremental}, $D$ should be chosen
999 to include both $\domain R$ and $\range R$, i.e., such
1000 that $\identity_D \circ R_j \circ \identity_D = R_j$ for all $j\ne i$.
1001 \shortciteN{Kelly1996closure} say that they use
1002 $D = \domain R_i \cup \range R_i$, but presumably they mean that
1003 they use $D = \domain R \cup \range R$.
1004 Now, this expression of $D$ contains a union, so it not directly usable.
1005 \shortciteN{Kelly1996closure} do not explain how they avoid this union.
1006 Apparently, in their implementation,
1007 they are using the convex hull of $\domain R \cup \range R$
1008 or at least an approximation of this convex hull.
1009 We use the simple hull (\autoref{s:simple hull}) of $\domain R \cup \range R$.
1011 It is also possible to use a domain $D$ that does {\em not\/}
1012 include $\domain R \cup \range R$, but then we have to
1013 compose with ${\cal C}(R_i,D)$ more selectively.
1014 In particular, if we have
1015 \begin{equation}
1016 \label{eq:transitive:right}
1017 \text{for each $j \ne i$ either }
1018 \domain R_j \subseteq D \text{ or } \domain R_j \cap \range R_i = \emptyset
1019 \end{equation}
1020 and, similarly,
1021 \begin{equation}
1022 \label{eq:transitive:left}
1023 \text{for each $j \ne i$ either }
1024 \range R_j \subseteq D \text{ or } \range R_j \cap \domain R_i = \emptyset
1025 \end{equation}
1026 then we can refine \eqref{eq:transitive:incremental} to
1028 R_i^+ \cup
1029 \left(
1030 \left(
1031 \bigcup_{\shortstack{$\scriptstyle\domain R_j \subseteq D $\\
1032 $\scriptstyle\range R_j \subseteq D$}}
1033 {\cal C} \circ R_j \circ {\cal C}
1034 \right)
1035 \cup
1036 \left(
1037 \bigcup_{\shortstack{$\scriptstyle\domain R_j \cap \range R_i = \emptyset$\\
1038 $\scriptstyle\range R_j \subseteq D$}}
1039 \!\!\!\!\!
1040 {\cal C} \circ R_j
1041 \right)
1042 \cup
1043 \left(
1044 \bigcup_{\shortstack{$\scriptstyle\domain R_j \subseteq D $\\
1045 $\scriptstyle\range R_j \cap \domain R_i = \emptyset$}}
1046 \!\!\!\!\!
1047 R_j \circ {\cal C}
1048 \right)
1049 \cup
1050 \left(
1051 \bigcup_{\shortstack{$\scriptstyle\domain R_j \cap \range R_i = \emptyset$\\
1052 $\scriptstyle\range R_j \cap \domain R_i = \emptyset$}}
1053 \!\!\!\!\!
1055 \right)
1056 \right)^+
1059 If only property~\eqref{eq:transitive:right} holds,
1060 we can use
1062 R_i^+ \cup
1063 \left(
1064 \left(
1065 R_i^+ \cup \identity
1066 \right)
1067 \circ
1068 \left(
1069 \left(
1070 \bigcup_{\shortstack{$\scriptstyle\domain R_j \subseteq D $}}
1071 R_j \circ {\cal C}
1072 \right)
1073 \cup
1074 \left(
1075 \bigcup_{\shortstack{$\scriptstyle\domain R_j \cap \range R_i = \emptyset$}}
1076 \!\!\!\!\!
1078 \right)
1079 \right)^+
1080 \right)
1083 while if only property~\eqref{eq:transitive:left} holds,
1084 we can use
1086 R_i^+ \cup
1087 \left(
1088 \left(
1089 \left(
1090 \bigcup_{\shortstack{$\scriptstyle\range R_j \subseteq D $}}
1091 {\cal C} \circ R_j
1092 \right)
1093 \cup
1094 \left(
1095 \bigcup_{\shortstack{$\scriptstyle\range R_j \cap \domain R_i = \emptyset$}}
1096 \!\!\!\!\!
1098 \right)
1099 \right)^+
1100 \circ
1101 \left(
1102 R_i^+ \cup \identity
1103 \right)
1104 \right)
1108 It should be noted that if we want the result of the incremental
1109 approach to be transitively closed, then we can only apply it
1110 if all of the transitive closure operations involved are exact.
1111 If, say, the second transitive closure in \eqref{eq:transitive:incremental}
1112 contains extra elements, then the result does not necessarily contain
1113 the composition of these extra elements with powers of $R_i$.
1115 \subsection{An {\tt Omega}-like implementation}
1117 While the main algorithm of \shortciteN{Kelly1996closure} is
1118 designed to compute and underapproximation of the transitive closure,
1119 the authors mention that they could also compute overapproximations.
1120 In this section, we describe our implementation of an algorithm
1121 that is based on their ideas.
1122 Note that the {\tt Omega} library computes underapproximations
1123 \shortcite[Section 6.4]{Omega_lib}.
1125 The main tool is Equation~(2) of \shortciteN{Kelly1996closure}.
1126 The input relation $R$ is first overapproximated by a ``d-form'' relation
1128 \{\, \vec i \to \vec j \mid \exists \vec \alpha :
1129 \vec L \le \vec j - \vec i \le \vec U
1130 \wedge
1131 (\forall p : j_p - i_p = M_p \alpha_p)
1132 \,\}
1135 where $p$ ranges over the dimensions and $\vec L$, $\vec U$ and
1136 $\vec M$ are constant integer vectors. The elements of $\vec U$
1137 may be $\infty$, meaning that there is no upper bound corresponding
1138 to that element, and similarly for $\vec L$.
1139 Such an overapproximation can be obtained by computing strides,
1140 lower and upper bounds on the difference set $\Delta \, R$.
1141 The transitive closure of such a ``d-form'' relation is
1142 \begin{equation}
1143 \label{eq:omega}
1144 \{\, \vec i \to \vec j \mid \exists \vec \alpha, k :
1145 k \ge 1 \wedge
1146 k \, \vec L \le \vec j - \vec i \le k \, \vec U
1147 \wedge
1148 (\forall p : j_p - i_p = M_p \alpha_p)
1149 \,\}
1151 \end{equation}
1152 The domain and range of this transitive closure are then
1153 intersected with those of the input relation.
1154 This is a special case of the algorithm in \autoref{s:power}.
1156 In their algorithm for computing lower bounds, the authors
1157 use the above algorithm as a substep on the disjuncts in the relation.
1158 At the end, they say
1159 \begin{quote}
1160 If an upper bound is required, it can be calculated in a manner
1161 similar to that of a single conjunct [sic] relation.
1162 \end{quote}
1163 Presumably, the authors mean that a ``d-form'' approximation
1164 of the whole input relation should be used.
1165 However, the accuracy can be improved by also trying to
1166 apply the incremental technique from the same paper,
1167 which is explained in more detail in \autoref{s:incremental}.
1168 In this case, ${\cal C}(R_i,D)$ can be obtained by
1169 allowing the value zero for $k$ in \eqref{eq:omega},
1170 i.e., by computing
1172 \{\, \vec i \to \vec j \mid \exists \vec \alpha, k :
1173 k \ge 0 \wedge
1174 k \, \vec L \le \vec j - \vec i \le k \, \vec U
1175 \wedge
1176 (\forall p : j_p - i_p = M_p \alpha_p)
1177 \,\}
1180 In our implementation we take as $D$ the simple hull
1181 (\autoref{s:simple hull}) of $\domain R \cup \range R$.
1182 To determine whether it is safe to use ${\cal C}(R_i,D)$,
1183 we check the following conditions, as proposed by
1184 \shortciteN{Kelly1996closure}:
1185 ${\cal C}(R_i,D) - R_i^+$ is not a union and for each $j \ne i$
1186 the condition
1188 \left({\cal C}(R_i,D) - R_i^+\right)
1189 \circ
1191 \circ
1192 \left({\cal C}(R_i,D) - R_i^+\right)
1196 holds.