Advertisement

Termination of Triangular Integer Loops is Decidable

  • Florian Frohn
  • Jürgen GieslEmail author
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11562)

Abstract

We consider the problem whether termination of affine integer loops is decidable. Since Tiwari conjectured decidability in 2004 [15], only special cases have been solved [3, 4, 14]. We complement this work by proving decidability for the case that the update matrix is triangular.

1 Introduction

We consider affine integer loops of the form
$$\begin{aligned} \mathbf{while}\ \varphi \ \mathbf{do}\ \overline{x}\ \leftarrow A\, \overline{x}+\overline{a}. \end{aligned}$$
(1)
Here, \(A \in \mathbb {Z}^{d \times d}\) for some dimension \(d \ge 1\), \(\overline{x}\) is a column vector of pairwise different variables \(x_1,\ldots ,x_d\), \(\overline{a} \in \mathbb {Z}^d\), and \(\varphi \) is a conjunction of inequalities of the form \(\alpha > 0\) where \(\alpha \in \mathbb {A}\mathbbm {f}[\overline{x}]\) is an affine expression with rational coefficients1 over \(\overline{x}\) (i.e., \(\mathbb {A}\mathbbm {f}[\overline{x}] = \{\overline{c}^T\, \overline{x} + c \mid \overline{c} \in \mathbb {Q}^d, c \in \mathbb {Q}\}\)). So \(\varphi \) has the form \(B\,\overline{x} + \overline{b} > \overline{0}\) where \(\overline{0}\) is the vector containing k zeros, \(B \in \mathbb {Q}^{k \times d}\), and \(\overline{b} \in \mathbb {Q}^k\) for some \(k \in \mathbb {N}\). Definition 1 formalizes the intuitive notion of termination for such loops.

Definition 1

(Termination). Let \(f:\mathbb {Z}^d \rightarrow \mathbb {Z}^d\) with \(f(\overline{x}) = A\,\overline{x} + \overline{a}\). If
$$ \exists \overline{c} \in \mathbb {Z}^{d}.\ \forall n \in \mathbb {N}.\ \varphi [\overline{x} / f^n(\overline{c})], $$
then (1) is non-terminating and \(\overline{c}\) is a witness for non-termination. Otherwise, (1) terminates.

Here, \(f^n\) denotes the n-fold application of f, i.e., we have \(f^0(\overline{c}) = \overline{c}\) and \(f^{n+1}(\overline{c}) = f(f^n(\overline{c}))\). We call f the update of (1). Moreover, for any entity s, s[x / t] denotes the entity that results from s by replacing all occurrences of x by t. Similarly, if \(\overline{x} = \begin{bmatrix}x_1\\[-.15cm]\vdots \\x_m\end{bmatrix}\) and \(\overline{t} = \begin{bmatrix}t_1\\[-.15cm]\vdots \\t_m\end{bmatrix}\), then \(s[\overline{x} / \overline{t}]\) denotes the entity resulting from s by replacing all occurrences of \(x_i\) by \(t_i\) for each \(1 \le i \le m\).

Example 2

Consider the loop
$$\begin{aligned} \mathbf{while}\,\, {y + z > 0}\, \,\mathbf{do}\,\, \left[ \begin{array}{c} w\\ x\\ y\\ z \end{array}\right] \leftarrow \left[ \begin{array}{c} 2\\ x + 1\\ - w - 2 \cdot y\\ x \end{array}\right] \end{aligned}$$
where the update of all variables is executed simultaneously. This program belongs to our class of affine loops, because it can be written equivalently as follows.
$$\begin{aligned} \mathbf{while}\, \,y + z > 0\, \,\mathbf{do}\,\, \left[ \begin{array}{c} w\\ x\\ y\\ z \end{array}\right] \leftarrow \left[ \begin{array}{cccc} 0&{}0&{}0&{}0\\ 0&{}1&{}0&{}0\\ -1&{}0&{}-2&{}0\\ 0&{}1&{}0&{}0 \end{array}\right] \left[ \begin{array}{c} w\\ x\\ y\\ z \end{array}\right] + \left[ \begin{array}{c} 2\\ 1\\ 0\\ 0 \end{array}\right] \end{aligned}$$

While termination of affine loops is known to be decidable if the variables range over the real [15] or the rational numbers [4], the integer case is a well-known open problem [2, 3, 4, 14, 15].2 However, certain special cases have been solved: Braverman [4] showed that termination of linear loops is decidable (i.e., loops of the form (1) where \(\overline{a}\) is \(\overline{0}\) and \(\varphi \) is of the form \(B\,\overline{x} > \overline{0}\)). Bozga et al. [3] showed decidability for the case that the update matrix A in (1) has the finite monoid property, i.e., if there is an \(n > 0\) such that \(A^n\) is diagonalizable and all eigenvalues of \(A^n\) are in \(\{0,1\}.\) Ouaknine et al. [14] proved decidability for the case \(d \le 4\) and for the case that A is diagonalizable.

Ben-Amram et al. [2] showed undecidability of termination for certain extensions of affine integer loops, e.g., for loops where the body is of the form \(\mathbf {if}\ x > 0\ \mathbf {then}\ \overline{x} \leftarrow A\,\overline{x}\ \mathbf {else}\ \overline{x} \leftarrow A'\,\overline{x}\) where \(A,A' \in \mathbb {Z}^{d \times d}\) and \(x \in \overline{x}\).

In this paper, we present another substantial step towards the solution of the open problem whether termination of affine integer loops is decidable. We show that termination is decidable for triangular loops (1) where A is a triangular matrix (i.e., all entries of A below or above the main diagonal are zero). Clearly, the order of the variables is irrelevant, i.e., our results also cover the case that A can be transformed into a triangular matrix by reordering A, \(\overline{x}\), and \(\overline{a}\) accordingly.3 So essentially, triangularity means that the program variables \(x_1,\ldots ,x_d\) can be ordered such that in each loop iteration, the new value of \(x_i\) only depends on the previous values of \(x_1,\ldots ,x_{i-1},x_i\). Hence, this excludes programs with “cyclic dependencies” of variables (e.g., where the new values of x and y both depend on the old values of both x and y). While triangular loops are a very restricted subclass of general integer programs, integer programs often contain such loops. Hence, tools for termination analysis of such programs (e.g., [5, 6, 7, 8, 11, 12, 13]) could benefit from integrating our decision procedure and applying it whenever a sub-program is an affine triangular loop.

Note that triangularity and diagonalizability of matrices do not imply each other. As we consider loops with arbitrary dimension, this means that the class of loops considered in this paper is not covered by [3, 14]. Since we consider affine instead of linear loops, it is also orthogonal to [4].

To see the difference between our and previous results, note that a triangular matrix A where \(c_1,\ldots ,c_k\) are the distinct entries on the diagonal is diagonalizable iff \((A - c_1 I) \ldots (A- c_k I)\) is the zero matrix.4 Here, I is the identity matrix. So an easy example for a triangular loop where the update matrix is not diagonalizable is the following well-known program (see, e.g., [2]):
$$\begin{aligned} \mathbf{while}\,\, x > 0\,\, \mathbf{do} \,\, x \leftarrow x+y;\; y \leftarrow y-1 \end{aligned}$$
It terminates as y eventually becomes negative and then x decreases in each iteration. In matrix notation, the loop body is Open image in new window , i.e., the update matrix is triangular. Thus, this program is in our class of programs where we show that termination is decidable. However, the only entry on the diagonal of the update matrix A is \(c = 1\) and Open image in new window is not the zero matrix. So A (and in fact each \(A^n\) where \(n \in \mathbb {N}\)) is not diagonalizable. Hence, extensions of this example to a dimension greater than 4 where the loop is still triangular are not covered by any of the previous results.5

Our proof that termination is decidable for triangular loops proceeds in three steps. We first prove that termination of triangular loops is decidable iff termination of non-negative triangular loops (nnt-loops) is decidable, cf. Sect. 2. A loop is non-negative if the diagonal of A does not contain negative entries. Second, we show how to compute closed forms for nnt-loops, i.e., vectors \(\overline{q}\) of d expressions over the variables \(\overline{x}\) and n such that \(\overline{q}[n/c] = f^c(\overline{x})\) for all \(c\ge 0\), see Sect. 3. Here, triangularity of the matrix A allows us to treat the variables step by step. So for any \(1 \le i \le d\), we already know the closed forms for \(x_1,\ldots ,x_{i-1}\) when computing the closed form for \(x_i\). The idea of computing closed forms for the repeated updates of loops was inspired by our previous work on inferring lower bounds on the runtime of integer programs [10]. But in contrast to [10], here the computation of the closed form always succeeds due to the restricted shape of the programs. Finally, we explain how to decide termination of nnt-loops by reasoning about their closed forms in Sect. 4. While our technique does not yield witnesses for non-termination, we show that it yields witnesses for eventual non-termination, i.e., vectors \(\overline{c}\) such that \(f^n(\overline{c})\) witnesses non-termination for some \(n \in \mathbb {N}\). Detailed proofs for all lemmas and theorems can be found in [9].

2 From Triangular to Non-Negative Triangular Loops

To transform triangular loops into nnt-loops, we define how to chain loops. Intuitively, chaining yields a new loop where a single iteration is equivalent to two iterations of the original loop. Then we show that chaining a triangular loop always yields an nnt-loop and that chaining is equivalent w.r.t. termination.

Definition 3

(Chaining).Chaining the loop (1) yields:
$$\begin{aligned} \mathbf{while}\,\, \varphi \wedge \varphi [\overline{x} / A\,\overline{x} + \overline{a}] \,\,\mathbf{do}\,\, \overline{x} \leftarrow A^2\,\overline{x} + A\,\overline{a} + \overline{a} \end{aligned}$$
(2)

Example 4

Chaining Example 2 yields
$$\begin{aligned} \begin{array}{l} \mathbf{while}\,\, y + z> 0 \wedge - w - 2 \cdot y + x > 0 \,\,\mathbf{do}\\ \qquad \left[ \begin{array}{c} w\\ x\\ y\\ z \end{array}\right] \leftarrow \left[ \begin{array}{cccc} 0&{}0&{}0&{}0\\ 0&{}1&{}0&{}0\\ -1&{}0&{}-2&{}0\\ 0&{}1&{}0&{}0 \end{array}\right] ^2 \left[ \begin{array}{c} w\\ x\\ y\\ z \end{array}\right] + \left[ \begin{array}{cccc} 0&{}0&{}0&{}0\\ 0&{}1&{}0&{}0\\ -1&{}0&{}-2&{}0\\ 0&{}1&{}0&{}0 \end{array}\right] \left[ \begin{array}{c} 2\\ 1\\ 0\\ 0 \end{array}\right] + \left[ \begin{array}{c} 2\\ 1\\ 0\\ 0 \end{array}\right] \end{array} \end{aligned}$$
which simplifies to the following nnt-loop:
$$\begin{aligned} \mathbf{while}\,\, y + z> 0 \wedge - w - 2 \cdot y + x > 0 \,\,\mathbf{do}\,\, \left[ \begin{array}{c} w\\ x\\ y\\ z \end{array}\right] \leftarrow \left[ \begin{array}{cccc} 0&{}0&{}0&{}0\\ 0&{}1&{}0&{}0\\ 2&{}0&{}4&{}0\\ 0&{}1&{}0&{}0 \end{array}\right] \left[ \begin{array}{c} w\\ x\\ y\\ z \end{array}\right] + \left[ \begin{array}{c} 2\\ 2\\ -2\\ 1 \end{array}\right] \end{aligned}$$

Lemma 5 is needed to prove that (2) is an nnt-loop if (1) is triangular.

Lemma 5

(Squares of Triangular Matrices). For every triangular matrix A, \(A^2\) is a triangular matrix whose diagonal entries are non-negative.

Corollary 6

(Chaining Loops). If (1) is triangular, then (2) is an nnt-loop.

Proof

Immediate consequence of Definition 3 and Lemma 5.    \(\square \)

Lemma 7

(Equivalence of Chaining). (1) terminates \(\iff \) (2) terminates.

Proof

By Definition 1, (1) does not terminate iff
$$ \begin{array}{lll} &{}\exists \overline{c} \in \mathbb {Z}^{d}.\ \forall n \in \mathbb {N}.\ \varphi [\overline{x} / f^n(\overline{c})] &{} \\ \iff &{}\exists \overline{c} \in \mathbb {Z}^{d}.\ \forall n \in \mathbb {N}.\ \varphi [\overline{x} / f^{2 \cdot n}(\overline{c})] \wedge \varphi [\overline{x} / f^{2 \cdot n + 1}(\overline{c})]\\ \iff &{}\exists \overline{c} \in \mathbb {Z}^{d}.\ \forall n \in \mathbb {N}.\ \varphi [\overline{x} / f^{2 \cdot n}(\overline{c})] \wedge \varphi [\overline{x} / A\,f^{2 \cdot n}(\overline{c}) + \overline{a}] &{} (\text {by Definition of } f), \end{array} $$
i.e., iff (2) does not terminate as \(f^2(\overline{x}) = A^2\,\overline{x} + A\,\overline{a} + \overline{a}\) is the update of (2).    \(\square \)

Theorem 8

(Reducing Termination to nnt-Loops). Termination of triangular loops is decidable iff termination of nnt-loops is decidable.

Proof

Immediate consequence of Corollary 6 and Lemma 7.    \(\square \)

Thus, from now on we restrict our attention to nnt-loops.

3 Computing Closed Forms

The next step towards our decidability proof is to show that \(f^n(\overline{x})\) is equivalent to a vector of poly-exponential expressions for each nnt-loop, i.e., the closed form of each nnt-loop can be represented by such expressions. Here, equivalence means that two expressions evaluate to the same result for all variable assignments.

Poly-exponential expressions are sums of arithmetic terms where it is always clear which addend determines the asymptotic growth of the whole expression when increasing a designated variable n. This is crucial for our decidability proof in Sect. 4. Let \(\mathbb {N}_{\ge 1} = \{b \in \mathbb {N}\mid b \ge 1\}\) (and \(\mathbb {Q}_{>0}\), \(\mathbb {N}_{>1}\), etc. are defined analogously). Moreover, \(\mathbb {A}\mathbbm {f}[\overline{x}]\) is again the set of all affine expressions over \(\overline{x}\).

Definition 9

(Poly-Exponential Expressions). Let \(\mathcal {C}\) be the set of all finite conjunctions over the literals \(n = c, n \ne c\) where n is a designated variable and \(c \in \mathbb {N}\). Moreover for each formula \(\psi \) over n, let Open image in new window be the characteristic function of \(\psi \), i.e., Open image in new window if \(\psi [n/c]\) is valid and Open image in new window , otherwise. The set of all poly-exponential expressions over \(\overline{x}\) is
As n ranges over \(\mathbb {N}\), we use Open image in new window as syntactic sugar for Open image in new window . So an example for a poly-exponential expression isMoreover, note that if \(\psi \) contains a positive literal (i.e., a literal of the form “\(n = c\)” for some number \(c \in \mathbb {N}\)), then Open image in new window is equivalent to either 0 or Open image in new window .

The crux of the proof that poly-exponential expressions can represent closed forms is to show that certain sums over products of exponential and poly-exponential expressions can be represented by poly-exponential expressions, cf. Lemma 12. To construct these expressions, we use a variant of [1, Lemma 3.5]. As usual, \(\mathbb {Q}[\overline{x}]\) is the set of all polynomials over \(\overline{x}\) with rational coefficients.

Lemma 10

(Expressing Polynomials by Differences [1]). If \(q \in \mathbb {Q}[n]\) and \(c \in \mathbb {Q}\), then there is an \(r \in \mathbb {Q}[n]\) such that \(q = r - c \cdot r[n/n-1]\) for all \(n \in \mathbb {N}\).

So Lemma 10 expresses a polynomial q via the difference of another polynomial r at the positions n and \(n-1\), where the additional factor c can be chosen freely. The proof of Lemma 10 is by induction on the degree of q and its structure resembles the structure of the following algorithm to compute r. Using the Binomial Theorem, one can verify that \(q - s + c \cdot s[n/n-1]\) has a smaller degree than q, which is crucial for the proof of Lemma 10 and termination of Algorithm 1.

Example 11

As an example, consider \(q = 1\) (i.e., \(c_0 = 1\)) and \(c = 4\). Then we search for an r such that \(q = r - c \cdot r[n/n-1]\), i.e., \(1 = r - 4 \cdot r[n/n-1]\). According to Algorithm 1, the solution is \(r = \frac{c_0}{1-c} = -\frac{1}{3}\).

Lemma 12

(Closure of \(\mathbb {PE}\) under Sums of Products and Exponentials). If \(m \in \mathbb {N}\) and \(p \in \mathbb {PE}[\overline{x}]\), then one can compute a \(q \in \mathbb {PE}[\overline{x}]\) which is equivalent to \(\sum _{i=1}^{n} m^{n - i} \cdot p[n/i-1]\).

Proof

Let Open image in new window . We have:As \(\mathbb {PE}[\overline{x}]\) is closed under addition, it suffices to show that we can compute an equivalent poly-exponential expression for any expression of the formWe first regard the case \(m=0\). Here, the expression (4) can be simplified toClearly, there is a \(\psi ' \in \mathcal {C}\) such that Open image in new window is equivalent to Open image in new window . Moreover, \(\alpha \cdot b^{n-1} = \tfrac{\alpha }{b} \cdot b^n\) where \(\tfrac{\alpha }{b} \in \mathbb {A}\mathbbm {f}[\overline{x}]\). Hence, due to the Binomial Theoremwhich is a poly-exponential expression as \(\tfrac{\alpha }{b}\cdot \left( {\begin{array}{c}a\\ i\end{array}}\right) \cdot (-1)^i \in \mathbb {A}\mathbbm {f}[\overline{x}]\).
From now on, let \(m \ge 1\). If \(\psi \) contains a positive literal \(n = c\), then we getThe step marked with \((\dagger )\) holds as we have Open image in new window for all \(i \in \{1,\ldots ,n\}\) and the step marked with \((\dagger \dagger )\) holds since \(i \ne c+1\) implies Open image in new window . If \(\psi \) does not contain a positive literal, then let c be the maximal constant that occurs in \(\psi \) or \(-1\) if \(\psi \) is empty. We get:Again, the step marked with \((\dagger )\) holds since we have Open image in new window for all \(i \in \{1,\ldots ,n\}\). The last step holds as \(i \ge c+2\) implies Open image in new window . Similar to the case where \(\psi \) contains a positive literal, we can compute a poly-exponential expression which is equivalent to the first addend. We havewhich is a poly-exponential expression as \(\tfrac{1}{m^{i}}\cdot \alpha \cdot (i-1)^a \cdot b^{i-1} \in \mathbb {A}\mathbbm {f}[\overline{x}]\). For the second addend, we have:Lemma 10 ensures \(r \in \mathbb {Q}[n]\), i.e., we have \(r = \sum _{i=0}^{d_r} m_i \cdot n^i\) for some \(d_r \in \mathbb {N}\) and \(m_i \in \mathbb {Q}\). Thus, \(r[n/c+1] \cdot \left( \frac{b}{m}\right) ^{c+1} \cdot \frac{\alpha }{b} \in \mathbb {A}\mathbbm {f}[\overline{x}]\) which implies Open image in new window . It remains to show that the addend Open image in new window is equivalent to a poly-exponential expression. As \(\frac{\alpha }{b} \cdot m_i \in \mathbb {A}\mathbbm {f}[\overline{x}]\), we have   \(\square \)
The proof of Lemma 12 gives rise to a corresponding algorithm.

Example 13

We compute an equivalent poly-exponential expression forwhere w is a variable. (It will later on be needed to compute a closed form for Example 4, see Example 18.) According to Algorithm 2 and (3), we getwith Open image in new window , Open image in new window , and \(p_3 = \sum _{i=1}^{n} 4^{n-i} \cdot (- 2)\). We search for \(q_1, q_2, q_3 \in \mathbb {PE}[w]\) that are equivalent to \(p_1, p_2, p_3\), i.e., \(q_1 + q_2 + q_3\) is equivalent to (12). We only show how to compute \(q_2\)(and omit the computation of Open image in new window ). Analogously to (8), we get:The next step is to rearrange the first sum as in (9). In our example, it directly simplifies to 0 and hence we obtainFinally, by applying the steps from (10) we get:The step marked with \((\dagger )\) holds by Lemma 10 with \(q = 1\) and \(c = 4\). Thus, we have \(r = -\tfrac{1}{3}\), cf. Example 11.
Recall that our goal is to compute closed forms for loops. As a first step, instead of the n-fold update function \(h(n,\overline{x}) = f^n(\overline{x})\) of (1) where f is the update of (1), we consider a recursive update function for a single variable \(x \in \overline{x}\):
$$ \textstyle g(0,\overline{x}) = x \quad \text {and} \quad g(n,\overline{x}) = m \cdot g(n-1, \overline{x}) + p[n/n-1] \quad \text {for all n > 0} $$
Here, \(m \in \mathbb {N}\) and \(p \in \mathbb {PE}[\overline{x}]\). Using Lemma 12, it is easy to show that g can be represented by a poly-exponential expression.

Lemma 14

(Closed Form for Single Variables). If \(x \in \overline{x}\), \(m \in \mathbb {N}\), and \(p \in \mathbb {PE}[\overline{x}]\), then one can compute a \(\,q \in \mathbb {PE}[\overline{x}]\) which satisfies
$$ \textstyle q\,[n/0] = x \quad \text {and} \quad q = (m \cdot q + p)\;[n/n-1] \quad \text {for all } n > 0. $$

Proof

It suffices to find a \(q \in \mathbb {PE}[\overline{x}]\) that satisfies
$$\begin{aligned} \textstyle q = m^n \cdot x + \sum _{i=1}^{n} m^{n-i} \cdot p[n/i-1]. \end{aligned}$$
(13)
To see why (13) is sufficient, note that (13) implies
$$ \textstyle q[n/0] \quad = \quad m^0 \cdot x + \sum \nolimits _{i=1}^{0} m^{0-i} \cdot p[n/i-1] \quad =\quad x $$
and for \(n > 0\), (13) implies
$$ \begin{array}{llll} q &{}=&{} m^{n} \cdot x + \mathop {\sum }\nolimits _{i=1}^{n} m^{n-i} \cdot p[n/i-1]\\ &{}=&{} m^{n} \cdot x + \left( \mathop {\sum }\nolimits _{i=1}^{n-1} m^{n-i} \cdot p[n/i-1]\right) + p[n/n-1]\\ &{}=&{} m \cdot \left( m^{n-1} \cdot x + \mathop {\sum }\nolimits _{i=1}^{n-1} m^{n-i-1} \cdot p[n/i-1]\right) + p[n/n-1]\\ &{}=&{} m \cdot q[n/n-1] + p[n/n-1]\\ &{}=&{} (m \cdot q + p)[n/n-1]. \end{array} $$
By Lemma 12, we can compute a \(q' \in \mathbb {PE}[\overline{x}]\) such that
$$ \textstyle m^n \cdot x + \mathop {\sum }\nolimits _{i=1}^{n} m^{n-i} \cdot p[n/i-1] \quad = \quad m^n \cdot x + q'. $$
Moreover,So both addends are equivalent to poly-exponential expressions.    \(\square \)

Example 15

We show how to compute the closed forms for the variables w and x from Example 4. We first consider the assignment \(w \leftarrow 2\), i.e., we want to compute a \(q_w \in \mathbb {PE}[w,x,y,z]\) with \(q_w [n/0] = w\) and \(q_w = (m_w \cdot q_w + p_w)\,[n/n-1]\) for \(n > 0\), where \(m_w = 0\) and \(p_w = 2\). According to (13) and (14), \(q_w\) isFor the assignment \(x \leftarrow x + 2\), we search for a \(q_x\) such that \(q_x[n/0] = x\) and \(q_x = (m_x \cdot q_x + p_x)\,[n/n-1]\) for \(n > 0\), where \(m_x = 1\) and \(p_x = 2\). By (13), \(q_x\) is
$$\textstyle m_x^n \cdot x + \sum _{i=1}^{n} m_x^{n-i} \cdot p_x[n/i-1] = 1^n \cdot x + \sum _{i=1}^{n} 1^{n-i} \cdot 2 = x + 2 \cdot n. $$
The restriction to triangular matrices now allows us to generalize Lemma 14 to vectors of variables. The reason is that due to triangularity, the update of each program variable \(x_i\) only depends on the previous values of \(x_1,\ldots ,x_{i}\). So when regarding \(x_i\), we can assume that we already know the closed forms for \(x_1,\ldots ,x_{i-1}\). This allows us to find closed forms for one variable after the other by applying Lemma 14 repeatedly. In other words, it allows us to find a vector \(\overline{q}\) of poly-exponential expressions that satisfies
$$ \textstyle \overline{q}\,[n/0] = \overline{x}\quad \text {and} \quad \overline{q} = A\, \overline{q}[n/n-1] + \overline{a} \quad \text {for all } n > 0. $$
To prove this claim, we show the more general Lemma 16. For all \(i_1,\ldots ,i_k \in \{1, \ldots , m\}\), we define \([z_1,\ldots ,z_m]_{i_1,\ldots ,i_k} = [z_{i_1},\ldots ,z_{i_k}]\) (and the notation \(\overline{y}_{i_1,\ldots ,i_k}\) for column vectors is defined analogously). Moreover, for a matrix A, \(A_{i}\) is A’s \(i^{th}\) row and \(A_{i_1,\ldots ,i_n;j_1,\ldots ,j_k}\) is the matrix with rows \((A_{i_1})_{j_1,\ldots ,j_k}, \ldots , (A_{i_n})_{j_1,\ldots ,j_k}\). So for \(A = \begin{bmatrix} a_{1,1}&a_{1,2}&a_{1,3}\\ a_{2,1}&a_{2,2}&a_{2,3}\\ a_{3,1}&a_{3,2}&a_{3,3} \end{bmatrix}\), we have \(A_{1,2;1,3} = \begin{bmatrix} a_{1,1}&a_{1,3}\\ a_{2,1}&a_{2,3} \end{bmatrix}\).

Lemma 16

(Closed Forms for Vectors of Variables). If \(\overline{x}\) is a vector of at least \(d \ge 1\) pairwise different variables, \(A \in \mathbb {Z}^{d \times d}\) is triangular with \(A_{i;i} \ge 0\) for all \(1 \le i \le d\), and \(\overline{p} \in \mathbb {PE}[\overline{x}]^d\), then one can compute \(\overline{q} \in \mathbb {PE}[\overline{x}]^d\) such that:
$$\begin{aligned} \overline{q}\,[n/0]&= \overline{x}_{1,\ldots ,d}\quad \text {and}\end{aligned}$$
(16)
$$\begin{aligned} \overline{q}&= (A\, \overline{q} + \overline{p})\;[n/n-1] \quad \text {for all } n > 0 \end{aligned}$$
(17)

Proof

Assume that A is lower triangular (the case that A is upper triangular works analogously). We use induction on d. For any \(d \ge 1\) we have:
$$ \begin{array}{llllll} &{}\overline{q} &{}=&{} (A\, \overline{q} + \overline{p})\;[n/n-1]\\ \iff &{} \overline{q}_j &{}=&{} (A_{j} \cdot \overline{q} + \overline{p}_j)\;[n/n-1] &{} \text {for all } 1 \le j \le d\\ \iff &{} \overline{q}_j &{}=&{} (A_{j;2,\ldots ,d} \cdot \overline{q}_{2,\ldots ,d} + A_{j;1} \cdot \overline{q}_1 + \overline{p}_j)\;[n/n-1] &{} \text {for all } 1 \le j \le d\\ \iff &{} \overline{q}_1 &{}=&{} (A_{1;2,\ldots ,d} \cdot \overline{q}_{2,\ldots ,d} + A_{1;1} \cdot \overline{q}_1 + \overline{p}_1)\;[n/n-1] &{} \wedge \\ &{} \overline{q}_j &{}=&{} (A_{j;2,\ldots ,d} \cdot \overline{q}_{2,\ldots ,d} + A_{j;1} \cdot \overline{q}_1 + \overline{p}_j)\;[n/n-1] &{} \text {for all } 1< j \le d\\ \iff &{} \overline{q}_1 &{}=&{} (A_{1;1} \cdot \overline{q}_1 + \overline{p}_1)\;[n/n-1] &{} \wedge \\ &{} \overline{q}_j &{}=&{} (A_{j;2,\ldots ,d} \cdot \overline{q}_{2,\ldots ,d} + A_{j;1} \cdot \overline{q}_1 + \overline{p}_j)\;[n/n-1] &{} \text {for all } 1 < j \le d \end{array} $$
The last step holds as A is lower triangular. By Lemma 14, we can compute a \(\overline{q}_1 \in \mathbb {PE}[\overline{x}]\) that satisfies
$$ \textstyle \overline{q}_1[n/0] = \overline{x}_1 \quad \text {and} \quad \overline{q}_1 = (A_{1;1} \cdot \overline{q}_1 + \overline{p}_1)\;[n/n-1] \quad \text {for all } n > 0. $$
In the induction base (\(d = 1\)), there is no j with \(1 < j \le d\). In the induction step (\(d > 1\)), it remains to show that we can compute \(\overline{q}_{2,\ldots ,d}\) such that
$$ \textstyle \overline{q}_j[n/0] = \overline{x}_j \quad \text {and} \quad \overline{q}_j = (A_{j;2,\ldots ,d} \cdot \overline{q}_{2,\ldots ,d} + A_{j;1} \cdot \overline{q}_1 + \overline{p}_j)\;[n/n-1] $$
for all \(n > 0\) and all \(1 < j \le d\), which is equivalent to
$$\begin{aligned} \overline{q}_{2,\ldots ,d}[n/0]&= \overline{x}_{2,\ldots ,d} \quad \text {and}\\[-1.3em] \overline{q}_{2,\ldots ,d}&= (A_{2,\ldots ,d;2,\ldots ,d} \cdot \overline{q}_{2,\ldots ,d} + \begin{bmatrix}A_{2;1}\\\vdots \\A_{d;1}\end{bmatrix} \cdot \overline{q}_1 + \overline{p}_{2,\ldots ,d})\;[n/n-1] \end{aligned}$$
for all \(n>0\). As \(A_{j;1} \cdot \overline{q}_1 + \overline{p}_j \in \mathbb {PE}[\overline{x}]\) for each \(2 \le j \le d\), the claim follows from the induction hypothesis.    \(\square \)
Together, Lemmas 14 and 16 and their proofs give rise to the following algorithm to compute a solution for (16) and (17). It computes a closed form \(\overline{q}_1\) for \(\overline{x}_1\) as in the proof of Lemma 14, constructs the argument \(\overline{p}\) for the recursive call based on A, \(\overline{q}_1\), and the current value of \(\overline{p}\) as in the proof of Lemma 16, and then determines the closed form for \(\overline{x}_{2, \ldots , d}\) recursively.

We can now prove the main theorem of this section.

Theorem 17

(Closed Forms for nnt-Loops). One can compute a closed form for every nnt-loop. In other words, if \(f:\mathbb {Z}^d \rightarrow \mathbb {Z}^d\) is the update function of an nnt-loop with the variables \(\overline{x}\), then one can compute a \(\overline{q} \in \mathbb {PE}[\overline{x}]^d\) such that \(\overline{q}[n/c] = f^c(\overline{x})\) for all \(c \in \mathbb {N}\).

Proof

Consider an nnt-loop of the form (1). By Lemma 16, we can compute a \(\overline{q} \subseteq \mathbb {PE}[\overline{x}]^d\) that satisfies
$$ \textstyle \overline{q}[n/0] = \overline{x} \quad \text {and} \quad \overline{q} = (A\, \overline{q} + \overline{a})\;[n/n-1] \quad \text {for all } n > 0. $$
We prove \(f^c(\overline{x}) = \overline{q}[n/c]\) by induction on \(c \in \mathbb {N}\). If \(c=0\), we get
$$ f^c(\overline{x}) = f^0(\overline{x}) = \overline{x} = \overline{q}[n/0] = \overline{q}[n/c]. $$
$$ \begin{array}{l@{}llll} \text{ If } c>0\text{, } \text{ we } \text{ get: }&{} f^c(\overline{x}) &{}=&{} A\, f^{c-1}(\overline{x}) + \overline{a} &{} \text {by definition of } f\\ &{}&{}=&{} A\, \overline{q}[n/c-1] + \overline{a} &{} \text {by the induction hypothesis}\\ &{}&{}=&{} (A\, \overline{q} + \overline{a})\;[n/c-1] &{} \text {as } \overline{a} \in \mathbb {Z}^d \text { does not contain } n\\ &{}&{}=&{} \overline{q}[n/c] &{} \end{array}$$
   \(\square \)

So invoking Algorithm 3 on \(\overline{x}, A\), and \(\overline{a}\) yields the closed form of an nnt-loop (1).

Example 18

We show how to compute the closed form for Example 4. For
$$ y \leftarrow 2 \cdot w + 4 \cdot y - 2, $$
we obtainwhere \(q_0 = y \cdot 4^n\). For \(z \leftarrow x + 1\), we getSo the closed form of Example 4 for the values of the variables after n iterations is:

4 Deciding Non-Termination of nnt-Loops

Our proof uses the notion of eventual non-termination [4, 14]. Here, the idea is to disregard the condition of the loop during a finite prefix of the program run.

Definition 19

(Eventual Non-Termination). A vector \(\overline{c} \in \mathbb {Z}^d\) witnesses eventual non-termination of (1) if
$$ \exists n_0 \in \mathbb {N}.\ \forall n \in \mathbb {N}_{>n_0}.\ \varphi [\overline{x} / f^{n}(\overline{c})]. $$
If there is such a witness, then (1) is eventually non-terminating.

Clearly, (1) is non-terminating iff (1) is eventually non-terminating [14]. Now Theorem 17 gives rise to an alternative characterization of eventual non-termination in terms of the closed form \(\overline{q}\) instead of \(f^{n}(\overline{c})\).

Corollary 20

(Expressing Non-Termination with \(\mathbb {PE}\)). If \(\overline{q}\) is the closed form of (1), then \(\overline{c} \in \mathbb {Z}^d\) witnesses eventual non-termination iff
$$\begin{aligned} \exists n_0 \in \mathbb {N}.\ \forall n \in \mathbb {N}_{>n_0}.\ \varphi [\overline{x} / \overline{q}][\overline{x} / \overline{c}]. \end{aligned}$$
(18)

Proof

Immediate, as \(\overline{q}\) is equivalent to \(f^n(\overline{x})\).    \(\square \)

So to prove that termination of nnt-loops is decidable, we will use Corollary 20 to show that the existence of a witness for eventual non-termination is decidable. To do so, we first eliminate the factors Open image in new window from the closed form \(\overline{q}\). Assume that \(\overline{q}\) has at least one factor Open image in new window where \(\psi \) is non-empty (otherwise, all factors Open image in new window are equivalent to 1) and let c be the maximal constant that occurs in such a factor. Then all addends Open image in new window where \(\psi \) contains a positive literal become 0 and all other addends become \(\alpha \cdot n^{a} \cdot b^n\) if \(n > c\). Thus, as we can assume \(n_0 > c\) in (18) without loss of generality, all factors Open image in new window can be eliminated when checking eventual non-termination.

Corollary 21

Removing Open image in new window from \(\mathbb {PE}\)s). Let \(\overline{q}\) be the closed form of an nnt-loop (1). Let \(\overline{q}_{norm}\) result from \(\overline{q}\) by removing all addends Open image in new window where \(\psi \) contains a positive literal and by replacing all addends Open image in new window where \(\psi \) does not contain a positive literal by \(\alpha \cdot n^{a} \cdot b^n\). Then \(\overline{c} \in \mathbb {Z}^d\) is a witness for eventual non-termination iff
$$\begin{aligned} \exists n_0 \in \mathbb {N}.\ \forall n \in \mathbb {N}_{>n_0}.\ \varphi [\overline{x} / \overline{q}_{norm}][\overline{x} / \overline{c}]. \end{aligned}$$
(19)

By removing the factors Open image in new window from the closed form \(\overline{q}\) of an nnt-loop, we obtain normalized poly-exponential expressions.

Definition 22

(Normalized \(\mathbb {PE}\)s). We call \(p \in \mathbb {PE}[\overline{x}]\) normalized if it is inW.l.o.g., we always assume \((b_i,a_i) \ne (b_j,a_j)\) for all \(i,j \in \{1,\ldots ,\ell \}\) with \(i \ne j\). We define \(\mathbb {NPE}= \mathbb {NPE}[\varnothing ]\), i.e., we have \(p \in \mathbb {NPE}\) if \(\alpha _j \in \mathbb {Q}\) for all \(1 \le j \le \ell \).

Example 23

We continue Example 18. By omitting the factors Open image in new window ,and \(q_x = x + 2 \cdot n, q_0 = y \cdot 4^n\), and \(q_3 = \tfrac{2}{3} - \frac{2}{3} \cdot 4^{n}\) remain unchanged. Moreover,Thus, \(q_y = q_0 + q_1 + q_2 + q_3\) becomes
$$ \textstyle y \cdot 4^n + \frac{1}{2} \cdot w \cdot 4^{n} - \frac{4}{3} + \frac{1}{3}\cdot 4^{n} + \tfrac{2}{3}- \frac{2}{3} \cdot 4^{n} = 4^n \cdot \left( y - \frac{1}{3} + \frac{1}{2} \cdot w\right) - \frac{2}{3}. $$
Let \(\sigma = \left[ w/2,\, x/x+ 2 \cdot n, \, y/4^n \cdot \left( y - \frac{1}{3} + \frac{1}{2} \cdot w\right) - \frac{2}{3}, \, z/x-1 + 2 \cdot n\right] \). Then we get that Example 2 is non-terminating iff there are \(w,x,y,z \in \mathbb {Z}, n_0 \in \mathbb {N}\) such that
$$ \begin{array}{l} (y + z)\;\sigma> 0 \wedge (- w - 2 \cdot y + x)\; \sigma> 0 \qquad \qquad \qquad \,\,\, \iff \\ 4^n \cdot \left( y - \frac{1}{3} + \frac{1}{2} \cdot w\right) - \frac{2}{3} + x - 1 + 2 \cdot n> 0 \wedge \\ \qquad - 2 - 2 \cdot \left( 4^n \cdot \left( y - \frac{1}{3} + \frac{1}{2} \cdot w\right) - \frac{2}{3}\right) + x + 2 {\cdot } n> 0 \iff \\ p^{\varphi }_1> 0 \wedge p^{\varphi }_2 > 0\\ \end{array} $$
holds for all \(n > n_0\) where
$$ \begin{array}{llll} p^{\varphi }_1 &{}=&{} 4^n \cdot \left( y - \frac{1}{3} + \frac{1}{2} \cdot w\right) + 2 \cdot n + x - \frac{5}{3} &{} \text {and}\\ p^{\varphi }_2 &{}=&{} 4^n \cdot \left( \frac{2}{3} - 2 \cdot y - w\right) + 2 \cdot n + x - \frac{2}{3}. \end{array} $$

Recall that the loop condition \(\varphi \) is a conjunction of inequalities of the form \(\alpha > 0\) where \(\alpha \in \mathbb {A}\mathbbm {f}[\overline{x}]\). Thus, \(\varphi [\overline{x} / \overline{q}_{norm}]\) is a conjunction of inequalities \(p > 0\) where \(p \in \mathbb {NPE}[\overline{x}]\) and we need to decide if there is an instantiation of these inequalities that is valid “for large enough n”. To do so, we order the coefficients \(\alpha _j\) of the addends \(\alpha _j \cdot n^{a_j} \cdot b_j^n\) of normalized poly-exponential expressions according to the addend’s asymptotic growth when increasing n. Lemma 24 shows that \(\alpha _2 \cdot n^{a_2} \cdot b_2^n\) grows faster than \(\alpha _1 \cdot n^{a_1} \cdot b_1^n\) iff \(b_2 > b_1\) or both \(b_2 = b_1\) and \(a_2 > a_1\).

Lemma 24

(Asymptotic Growth). Let \(b_1,b_2 \in \mathbb {N}_{\ge 1}\) and \(a_1, a_2 \in \mathbb {N}\). If \((b_2, a_2) >_{lex} (b_1, a_1)\), then \(\mathcal {O}(n^{a_1} \cdot b_1^n) \subsetneq \mathcal {O}(n^{a_2} \cdot b_2^n)\). Here, \({>_{lex}}\) is the lexicographic order, i.e., \((b_2,a_2) >_{lex} (b_1,a_1)\) iff \(b_2 > b_1\) or \(b_2 = b_1 \wedge a_2 > a_1\).

Proof

By considering the cases \(b_2 > b_1\) and \(b_2 = b_1\) separately, the claim can easily be deduced from the definition of \(\mathcal {O}\).    \(\square \)

Definition 25

(Ordering Coefficients).Marked coefficients are of the form \(\alpha ^{(b,a)}\) where \(\alpha \in \mathbb {A}\mathbbm {f}[\overline{x}], b \in \mathbb {N}_{\ge 1}\), and \(a \in \mathbb {N}\). We define \(\mathrm{unmark}(\alpha ^{(b,a)}) = \alpha \) and \(\alpha _2^{(b_2,a_2)} \succ \alpha _1^{(b_1,a_1)}\) if \((b_2,a_2) >_{lex} (b_1,a_1)\). Let
$$ \textstyle p = \sum _{j=1}^\ell \alpha _j \cdot n^{a_j} \cdot b_j^n \in \mathbb {NPE}[\overline{x}], $$
where \(\alpha _j \ne 0\) for all \(1 \le j \le \ell \). The marked coefficients of p are

Example 26

In Example 23 we saw that the loop from Example 2 is non-terminating iff there are \(w,x,y,z \in \mathbb {Z}, n_0 \in \mathbb {N}\) such that \(p^{\varphi }_1> 0 \wedge p^{\varphi }_2 > 0\) for all \(n > n_0\). We get:
$$\begin{aligned} \mathrm{coeffs}\left( p^{\varphi }_1\right)&= \left\{ \left( y - \tfrac{1}{3} + \tfrac{1}{2} \cdot w\right) ^{(4,0)}, 2^{(1,1)}, \left( x-\tfrac{5}{3}\right) ^{(1, 0)}\right\} \\ \mathrm{coeffs}\left( p^{\varphi }_2\right)&= \left\{ \left( \tfrac{2}{3} - 2 \cdot y - w\right) ^{(4,0)}, 2^{(1,1)}, \left( x-\tfrac{2}{3}\right) ^{(1,0)}\right\} \end{aligned}$$

Now it is easy to see that the asymptotic growth of a normalized poly-exponential expression is solely determined by its \(\succ \)-maximal addend.

Corollary 27

(Maximal Addend Determines Asymptotic Growth). Let \(p \in \mathbb {NPE}\) and let \(\max _{\succ }(\mathrm{coeffs}(p)) = c^{(b,a)}\). Then \(\mathcal {O}(p) = \mathcal {O}(c \cdot n^a \cdot b^n)\).

Proof

Clear, as \(c \cdot n^a \cdot b^n\) is the asymptotically dominating addend of p.    \(\square \)

Note that Corollary 27 would be incorrect for the case \(c = 0\) if we replaced \(\mathcal {O}(p) = \mathcal {O}(c \cdot n^a \cdot b^n)\) with \(\mathcal {O}(p) = \mathcal {O}(n^a \cdot b^n)\) as \(\mathcal {O}(0) \ne \mathcal {O}(1)\). Building upon Corollary 27, we now show that, for large n, the sign of a normalized poly-exponential expression is solely determined by its \(\succ \)-maximal coefficient. Here, we define \(\mathrm{sign}(c) = -1\) if \(c \in \mathbb {Q}_{<0} \cup \{-\infty \}\), \(\mathrm{sign}(0) = 0\), and \(\mathrm{sign}(c) = 1\) if \(c \in \mathbb {Q}_{>0} \cup \{\infty \}\).

Lemma 28

(Sign of \(\mathbb {NPE}\)s). Let \(p \in \mathbb {NPE}\). Then \(\lim _{n \mapsto \infty } p \in \mathbb {Q}\) iff \(p \in \mathbb {Q}\) and otherwise, \(\lim _{n \mapsto \infty } p \in \{ \infty , -\infty \}\). Moreover, we have
$$ \textstyle \mathrm{sign}\left( \lim _{n \mapsto \infty } p\right) = \mathrm{sign}(\mathrm{unmark}(\max _{\succ }(\mathrm{coeffs}(p)))). $$

Proof

If \(p \notin \mathbb {Q}\), then the limit of each addend of p is in \(\{-\infty , \infty \}\) by definition of \(\mathbb {NPE}\). As the asymptotically dominating addend determines \(\lim _{n \mapsto \infty } p\) and \(\mathrm{unmark}(\max _{\succ }(\mathrm{coeffs}(p)))\) determines the sign of the asymptotically dominating addend, the claim follows.    \(\square \)

Lemma 29 shows the connection between the limit of a normalized poly-exponential expression p and the question whether p is positive for large enough n. The latter corresponds to the existence of a witness for eventual non-termination by Corollary 21 as \(\varphi [\overline{x} / \overline{q}_{norm}]\) is a conjunction of inequalities \(p > 0\) where \(p \in \mathbb {NPE}[\overline{x}]\).

Lemma 29

(Limits and Positivity of \(\mathbb {NPE}\)s). Let \(p \in \mathbb {NPE}\). Then
$$ \textstyle \exists n_0 \in \mathbb {N}.\ \forall n \in \mathbb {N}_{>n_0}.\ p> 0 \iff \lim _{n \mapsto \infty } p > 0. $$

Proof

By case analysis over \(\lim _{n \mapsto \infty } p\).    \(\square \)

Now we show that Corollary 21 allows us to decide eventual non-termination by examining the coefficients of normalized poly-exponential expressions. As these coefficients are in \(\mathbb {A}\mathbbm {f}[\overline{x}]\), the required reasoning is decidable.

Lemma 30

(Deciding Eventual Positiveness of \(\mathbb {NPE}\)s). Validity of
$$\begin{aligned} \begin{array}{l} \exists \overline{c} \in \mathbb {Z}^{d}, n_0 \in \mathbb {N}.\ \forall n \in \mathbb {N}_{>n_0}.\ \bigwedge \nolimits _{i=1}^k p_i[\overline{x}/\overline{c}] > 0 \end{array} \end{aligned}$$
(20)
where \(p_1,\ldots ,p_k \in \mathbb {NPE}[\overline{x}]\) is decidable.

Proof

For any \(p_i\) with \(1 \le i \le k\) and any \(\overline{c} \in \mathbb {Z}^{d}\), we have \(p_i[\overline{x}/\overline{c}] \in \mathbb {NPE}\). Hence:Let \(p \in \mathbb {NPE}[\overline{x}]\) with \(\mathrm{coeffs}(p) = \left\{ \alpha _1^{(b_1,a_1)}\!,\ldots ,\alpha ^{(b_{\ell },a_{\ell })}_{\ell }\right\} \) where \(\alpha ^{(b_i,a_i)}_i \succ \alpha ^{(b_{j},a_{j})}_{j}\) for all \(1 \le i < j \le \ell \). If \(p[\overline{x}/\overline{c}] = 0\) holds, then \(\mathrm{coeffs}(p[\overline{x}/\overline{c}]) = \{ 0^{(1,0)} \}\) and thus \(\mathrm{unmark}(\max _{\succ }(\mathrm{coeffs}(p[\overline{x}/\overline{c}]))) = 0\). Otherwise, there is an \(1 \le j \le \ell \) with \(\mathrm{unmark}(\max _{\succ }(\mathrm{coeffs}(p[\overline{x}/\overline{c}]))) = \alpha _j[\overline{x}/\overline{c}] \ne 0\) and we have \(\alpha _i[\overline{x}/\overline{c}] = 0\) for all \(1 \le i \le j-1\). Hence, \(\mathrm{unmark}(\max _{\succ }(\mathrm{coeffs}(p[\overline{x}/\overline{c}]))) > 0\) holds iff \(\bigvee _{j=1}^\ell \left( \alpha _j[\overline{x}/\overline{c}] > 0 \wedge \bigwedge _{i=0}^{j-1} \alpha _i[\overline{x}/\overline{c}] = 0\right) \) holds, i.e., iff \([\overline{x}/\overline{c}]\) is a model for
$$\begin{aligned} \begin{array}{l} \mathrm{max\_coeff\_pos}(p) = \bigvee \nolimits _{j=1}^\ell \left( \alpha _j > 0 \wedge \bigwedge \nolimits _{i=0}^{j-1} \alpha _i = 0\right) . \end{array} \end{aligned}$$
(21)
Hence by the considerations above, (20) is valid iff
$$\begin{aligned} \begin{array}{l} \exists \overline{c} \in \mathbb {Z}^{d}. \; \bigwedge \nolimits _{i=1}^k \mathrm{max\_coeff\_pos}(p_i) [\overline{x}/\overline{c}] \end{array} \end{aligned}$$
(22)
is valid. By multiplying each (in-)equality in (22) with the least common multiple of all denominators, one obtains a first-order formula over the theory of linear integer arithmetic. It is well known that validity of such formulas is decidable.    \(\square \)

Note that (22) is valid iff \(\bigwedge _{i=1}^k \mathrm{max\_coeff\_pos}(p_i)\) is satisfiable. So to implement our decision procedure, one can use integer programming or SMT solvers to check satisfiability of \(\bigwedge _{i=1}^k \mathrm{max\_coeff\_pos}(p_i)\). Lemma 30 allows us to prove our main theorem.

Theorem 31

Termination of triangular loops is decidable.

Proof

By Theorem 8, termination of triangular loops is decidable iff termination of nnt-loops is decidable. For an nnt-loop (1) we obtain a \(\overline{q}_{norm} \in \mathbb {NPE}[\overline{x}]^{d}\) (see Theorem 17 and Corollary 21) such that (1) is non-terminating iff
$$\begin{aligned} \exists \overline{c} \in \mathbb {Z}^{d}, n_0 \in \mathbb {N}.\ \forall n \in \mathbb {N}_{>n_0}.\ \varphi [\overline{x} / \overline{q}_{norm}][\overline{x} / \overline{c}], \end{aligned}$$
(20)
where \(\varphi \) is a conjunction of inequalities of the form \(\alpha > 0\), \(\alpha \in \mathbb {A}\mathbbm {f}[\overline{x}]\). Hence,
$$\begin{array}{l} \varphi [\overline{x} / \overline{q}_{norm}][\overline{x} / \overline{c}] \; = \; \bigwedge _{i=1}^k p_i[\overline{x}/\overline{c}] > 0 \end{array}$$
where \(p_1,\ldots ,p_k \in \mathbb {NPE}[\overline{x}]\). Thus, by Lemma 30, validity of (20) is decidable.    \(\square \)
The following algorithm summarizes our decision procedure.

Example 32

In Example 26 we showed that Example 2 is non-terminating iff
$$ \textstyle \exists w,x,y,z \in \mathbb {Z},\ n_0 \in \mathbb {N}.\ \forall n \in \mathbb {N}_{>n_0}.\ p^{\varphi }_1> 0 \wedge p^{\varphi }_2 > 0 $$
is valid. This is the case iff \(\mathrm{max\_coeff\_pos}(p_1) \wedge \mathrm{max\_coeff\_pos}(p_2)\), i.e.,

is satisfiable. This formula is equivalent to \(6 \cdot y - 2 + 3 \cdot w = 0\) which does not have any integer solutions. Hence, the loop of Example 2 terminates.

Example 33 shows that our technique does not yield witnesses for non-termination, but it only proves the existence of a witness for eventual non-termination. While such a witness can be transformed into a witness for non-termination by applying the loop several times, it is unclear how often the loop needs to be applied.

Example 33

Consider the following non-terminating loop:The closed form of x is Open image in new window . Replacing x with \(q_{norm}\) in \(x > 0\) yields \(x + y + n - 1 > 0\). The maximal marked coefficient of \(x + y + n - 1\) is \(1^{(1,1)}\). So by Algorithm 4, (23) does not terminate if \(\exists x,y \in \mathbb {Z}.\ 1 > 0\) is valid. While \(1 > 0\) is a tautology, (23) terminates if \(x \le 0\) or \(x \le -y\).

However, the final formula constructed by Algorithm 4 precisely describes all witnesses for eventual non-termination.

Lemma 34

(Witnessing Eventual Non-Termination). Let (1) be a triangular loop, let \(\overline{q}_{norm}\) be the normalized closed form of (2), and let
$$ \textstyle \left( \varphi \wedge \varphi [\overline{x} / A\,\overline{x} + \overline{a}]\right) [\overline{x}/\overline{q}_{norm}] = \bigwedge _{i=1}^k p_i > 0. $$
Then \(\overline{c} \in \mathbb {Z}^d\) witnesses eventual non-termination of (1) iff \([\overline{x}/\overline{c}]\) is a model for
$$ \textstyle \bigwedge _{i=1}^k \mathrm{max\_coeff\_pos}(p_i). $$

5 Conclusion

We presented a decision procedure for termination of affine integer loops with triangular update matrices. In this way, we contribute to the ongoing challenge of proving the 15 years old conjecture by Tiwari [15] that termination of affine integer loops is decidable. After linear loops [4], loops with at most 4 variables [14], and loops with diagonalizable update matrices [3, 14], triangular loops are the fourth important special case where decidability could be proven.

The key idea of our decision procedure is to compute closed forms for the values of the program variables after a symbolic number of iterations n. While these closed forms are rather complex, it turns out that reasoning about first-order formulas over the theory of linear integer arithmetic suffices to analyze their behavior for large n. This allows us to reduce (non-)termination of triangular loops to integer programming. In future work, we plan to investigate generalizations of our approach to other classes of integer loops.

Footnotes

  1. 1.

    Note that multiplying with the least common multiple of all denominators yields an equivalent constraint with integer coefficients, i.e., allowing rational instead of integer coefficients does not extend the considered class of loops.

  2. 2.

    The proofs for real or rational numbers do not carry over to the integers since [15] uses Brouwer’s Fixed Point Theorem which is not applicable if the variables range over \(\mathbb {Z}\) and [4] relies on the density of \(\mathbb {Q}\) in \(\mathbb {R}\).

  3. 3.

    Similarly, one could of course also use other termination-preserving pre-processings and try to transform a given program into a triangular loop.

  4. 4.

    The reason is that in this case, \((x - c_1) \ldots (x- c_k)\) is the minimal polynomial of A and diagonalizability is equivalent to the fact that the minimal polynomial is a product of distinct linear factors.

  5. 5.

    For instance, consider Open image in new window .

References

  1. 1.
    Bagnara, R., Zaccagnini, A., Zolo, T.: The Automatic Solution of Recurrence Relations. I. Linear Recurrences of Finite Order with Constant Coefficients. Technical report. Quaderno 334. Dipartimento di Matematica, Università di Parma, Italy (2003). http://www.cs.unipr.it/Publications/
  2. 2.
    Ben-Amram, A.M., Genaim, S., Masud, A.N.: On the termination of integer loops. ACM Trans. Programm. Lang. Syst. 34(4), 16:1–16:24 (2012).  https://doi.org/10.1145/2400676.2400679CrossRefzbMATHGoogle Scholar
  3. 3.
    Bozga, M., Iosif, R., Konecný, F.: Deciding conditional termination. Logical Methods Comput. Sci. 10(3) (2014).  https://doi.org/10.2168/LMCS-10(3:8)2014
  4. 4.
    Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 372–385. Springer, Heidelberg (2006).  https://doi.org/10.1007/11817963_34CrossRefGoogle Scholar
  5. 5.
    Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387–393. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_22CrossRefGoogle Scholar
  6. 6.
    Chen, Y.-F., et al.: Advanced automata-based algorithms for program termination checking. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 135–150 (2018).  https://doi.org/10.1145/3192366.3192405
  7. 7.
    Chen, H.-Y., David, C., Kroening, D., Schrammel, P., Wachter, B.: Bit-precise procedure-modular termination analysis. ACM Trans. Programm. Lang. Syst. 40(1), 1:1–1:38 (2018).  https://doi.org/10.1145/3121136CrossRefGoogle Scholar
  8. 8.
    D’Silva, V., Urban, C.: Conflict-driven conditional termination. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 271–286. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21668-3_16CrossRefGoogle Scholar
  9. 9.
    Frohn, F., Giesl, J.: Termination of triangular integer loops is decidable. In: CoRR abs/1905.08664 (2019). https://arxiv.org/abs/1905.08664
  10. 10.
    Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 550–567. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-40229-1_37CrossRefGoogle Scholar
  11. 11.
    Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning 58(1), 3–31 (2017).  https://doi.org/10.1007/s10817-016-9388-yMathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: Jobstmann, B., Ray, S. (eds.) FMCAD 2013, pp. 218–225 (2013).  https://doi.org/10.1109/FMCAD.2013.6679413
  13. 13.
    Le, T.C., Qin, S., Chin, W.-N.: Termination and non-termination specification inference. In: Grove, D., Blackburn, S. (eds.) PLDI 2015, pp. 489–498 (2015).  https://doi.org/10.1145/2737924.2737993
  14. 14.
    Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: Indyk, P. (ed.) SODA 2015, pp. 957–969 (2015).  https://doi.org/10.1137/1.9781611973730.65
  15. 15.
    Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_6CrossRefGoogle Scholar

Copyright information

© The Author(s) 2019

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Max Planck Institute for InformaticsSaarbrückenGermany
  2. 2.LuFG Informatik 2, RWTH Aachen UniversityAachenGermany

Personalised recommendations