Termination of Triangular Integer Loops is Decidable

We consider affine integer loops of the formHere, \(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 coefficients¹ 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.

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

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‐4, 14, 15].² 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.³ 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‐8, 11‐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.⁴ 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]):It terminates as y eventually becomes negative and then x decreases in each iteration. In matrix notation, the loop body is , 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 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.⁵

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

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

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

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

As n ranges over \(\mathbb {N}\), we use as syntactic sugar for . 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 is equivalent to either 0 or .

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.

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.

The proof of Lemma 12 gives rise to a corresponding algorithm.

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

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

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.

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

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.

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

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 from the closed form \(\overline{q}\). Assume that \(\overline{q}\) has at least one factor where \(\psi \) is non-empty (otherwise, all factors are equivalent to 1) and let c be the maximal constant that occurs in such a factor. Then all addends 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 can be eliminated when checking eventual non-termination.

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

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

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

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

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.

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.

The following algorithm summarizes our decision procedure.

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

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.