1 Introduction
Termination is a central problem in program verification. In this paper we study termination of singlepath linear loops, i.e., programs of the form
where and are affine maps with integer coefficients. Here the loop body has a single control path that performs a simultaneous affine update of the program variables. Analysis of loops of this form, including acceleration and termination, is an important part of analysing more complex programs (see, e.g., [7, 14, 16]).
For a set , we say that the above loop terminates on
if it terminates on all initial vectors
. Despite the simplicity of singlepath linear loops, the question of deciding termination has proven challenging (and termination already becomes undecidable if the loop body consists of a nondeterministic choice between two different linear updates). Tiwari [25] showed that termination of singlepath linear loops is decidable over . Subsequently, Braverman [9], using a more refined analysis of the loop components, showed that termination is decidable over and noted that termination on can be reduced to termination on in the homogeneous case, i.e., when the update map and guards are linear. More recently, Ouaknine, SousaPinto, and Worrell [18] have proven that termination over is decidable in the nonhomogeneous case under the assumption that the update function has the form for a diagonalisable integer matrix. Decidability of termination for nonhomogeneous linear loops over was conjectured by Tiwari [25, Conjecture 1], but has remained open until now.In this paper we give a procedure for deciding termination of the general class of singlepath linear loops over the integers, i.e., we generalise the result of [18] by lifting the assumption of diagonalisability. Note that for this class of programs, the question of termination on a given initial value in (as opposed to termination over all of ) is equivalent to the Positivity Problem for linear recurrence sequences, i.e., the problem of whether all terms in a given integer linear recurrence sequence are positive. Decidability of the Positivity Problem is a longstanding open problem (going back at least as far as the 1970s [22, 24]), and results in [19] suggest that a solution to the problem will require significant breakthroughs in number theory. However, in considering termination over one can benefit from the freedom to choose the initial values of the loop variables. In the present paper we exploit this freedom in order to circumvent the need to solve “hard instances” of the Positivity Problem when deciding termination of linear loops. In particular, we avoid the use of sophisticated Diophantineapproximation techniques, such as the units theorem, that were employed in [19]. By eschewing such tools we lose all hope of obtaining an effective characterisation of the set of nonterminating points, as was done in the diagonalisable case in [19], but our methods nevertheless manage to solve the decision problem in the general case.
Among the tools we use are a circle of closely related results in the geometry of numbers, including Khinchine’s flatness theorem, Kronecker’s theorem on simultaneous Diophantine approximation, and the result of Khachiyan and Porkolab that it is decidable whether a convex semialgebraic set contains an integer point. In tandem with these, from algebraic number theory, we use a result of Masser that allows to compute all algebraic relations among the eigenvalues of the update matrix of a given loop. Using this last result, we define a semialgebraic subset of “nontermination candidates” such that the loop is nonterminating if and only if this set contains an integer point.
In this paper we focus on the foundational problem of providing complete methods to solve termination. Much effort has been devoted to scalable and pragmatic methods to prove termination for classes of programs that subsume linear loops. In particular, techniques to prove termination via synthesis of linear ranking functions [4, 5, 8, 10, 11, 20, 21] and their extension, multiphase linear ranking functions [6, 3], have been developed. Many of these techniques have been implemented in software verification tools, such as Microsoft’s Terminator [12]. Although these methods are capable of handling nondeterministic linear loops, they can only guarantee termination whenever ranking functions of a certain form exist.
2 Background
2.1 Convexity
The affine hull of is the smallest affine set that contains , where an affine set is the translation of a vector subspace of . The affine hull of can be characterised as follows:
The convex hull of is the smallest convex set that contains . The convex hull of can be characterised as follows:
Clearly . The relative interior of a convex set is its interior with respect to the restriction of the Euclidean topology to . We have the following easy proposition, characterising the relative interior.
Let . If lies in the relative interior of then there exist such that and .
Proof.
Since lies in the relative interior of , for sufficiently small we have that
For such an there exist such that and . But then . Defining for , the proposition is proved. ∎
A lattice of rank in is a set
where
are linearly independent vectors in
. Given a convex set , define the width of along a vector to beFurthermore the lattice width of is the infimum over all nonzero vectors of the width of along .
The following result (see [2, Theorem 7.2.1]) captures the intuition that a convex set that contains no lattice point in its interior must be “thin” in some direction. [Flatness Theorem] Given a fullrank lattice in there exists such that any convex set of lattice width at least contains a lattice point.
Recall that is said to be semialgebraic if it is definable by a boolean combination of polynomial constraints , where .
[Khachiyan and Porkolab [15]] It is decidable whether a given convex semialgebraic set contains an integer point, that is, whether .
2.2 Groups of Multiplicative Relations
In this subsection we will introduce some concepts concerning groups of multiplicative relations among algebraic numbers.
Let . We define the dimensional torus to be , considered as a group under componentwise multiplication. Given a tuple of algebraic numbers , the orbit is a subset of . In the following we characterise the topological closure of the orbit as an algebraic subset of .
The group of multiplicative relations of is defined as the following additive subgroup of :
where is defined to be for , that is, exponentiation acts coordinatewise. Since is a subgroup of , it is a free Abelian group and hence has a finite basis. The following powerful theorem of Masser [17] gives bounds on the magnitude of the components of such a basis.
[Masser] The free Abelian group has a basis for which
where and bound respectively the heights and degrees of all the .
Membership of a tuple in can be computed in polynomial space, using a decision procedure for the existential theory of the reals. In combination with Theorem 2.2, it follows that we can compute a basis for in polynomial space by bruteforce search.
Corresponding to , we consider the following multiplicative subgroup of :
If is a basis of , we can equivalently characterise as . Crucially, this finitary characterisation allows us to represent as an algebraic set in .
We will use the following classical lemma of Kronecker on simultaneous Diophantine approximation to show that the orbit is a dense subset of .
Let . Suppose that for all , if then also , i.e., all integer relations among the coordinates of also hold among those of (modulo ). Then, for each , there exist and a nonnegative integer such that
We now arrive at the main result of the section: Let . Then the orbit is a dense subset of .
Proof.
Let be such that (with exponentiation operating coordinatewise). Notice that if and only if . If , we can likewise define to be such that . Then the premises of Kronecker’s lemma apply to and . Thus, given , there exist a nonnegative integer and such that . Whence
∎
3 Termination Analysis via Spectral Theory
The general form of a simple linear loop in dimension is as follows:
where and are affine functions. We assume that and have integer coefficients, that is, for and , and for , and .
Note that
(1) 
for all . We say that is nondegenerate if no quotient of two distinct eigenvalues of the update matrix is a root of unity.
The termination problem for simple linear loops on integers is reducible to the special case of the problem for nondegenerate update functions.
Proof.
Consider a simple linear loop, as described above, whose update matrix has distinct eigenvalues . Let be the least common multiple of the orders of the roots of unity appearing among the quotients for . It is known that [13, Subsection 1.1.9]. The update matrix corresponding to the affine map has eigenvalues and hence is nondegenerate. Moreover the original loop terminates if and only if the following loop terminates:
This concludes the proof. ∎
In the rest of this section and in the next section we focus on the case of a loop
(2) 
with a single guard function and with nondegenerate update function
, with both maps having integer coefficients. We show that a spectral analysis of the matrix underlying the loop update function suffices to classify almost all initial values of the loop as either terminating or eventually nonterminating. Towards the end of the section we isolate a class of socalled
critical initial values that are not amenable to this analysis. We show how to deal with such points in Section 4.With respect to the loop P we say that is terminating if there exists such that . We say that is eventually nonterminating if the sequence is ultimately positive, i.e., there exists such that for all . Clearly there exists that is nonterminating if and only if there exists that is eventually nonterminating. Thus we can regard the problem of deciding termination on as that of searching for an eventually nonterminating point.
Let be the nonzero eigenvalues of and let be the maximum multiplicity over all these eigenvalues.
Define a linear preorder on by if either (i) or (ii) and . Write if and . Then we have
that is, the preorder characterises the asymptotic order of growth in absolute value of the terms for . This preorder moreover induces an equivalence relation on where iff and .
The following closedform expression for will be the focus of the subsequent development. There is a set of affine functions such that for all and all we have
Proof.
By the JordanChevalley decomposition we can write , where is diagonal, is nilpotent, is invertible, and commute, and all matrices have algebraic coefficients. Moreover we can write for appropriate idempotent diagonal matrices . Then for all with we have
where for the affine function is defined in Line (3). Clearly each function is a complexvalued affine function on with algebraic coefficients. ∎
Define for , that is, we obtain the by normalising the eigenvalues to have length . Recall from Section 2.2 the definition of the group of multiplicative relations that hold among , viz.,
Recall also that we have , given by
Given an equivalence class , note that for all we have and . Thus is determines a common multiplicity, which we denote , and a set of eigenvalues that all have the same absolute value, which we denote .
Given an equivalence class , define by^{1}^{1}1That the function is realvalued follows from the fact that if eigenvalues and are complex conjugates then and are also complex conjugates, as are and (see the proof of Proposition 3).
(4) 
From the above definition of we have
(5) 
for all and all .
We say that an equivalence class of is dominant for if is the equivalence class of the maximal indices for which is nonzero. Equivalently, is dominant for if is the maximal equivalence class such that is not identically zero on . (The equivalence of these two characterisations follows from the linear independence of the functions for .)
The following proposition shows how information about termination of the loop P on an initial value can be derived from properties of .
Consider the loop P in (2). Let and let be an equivalence class that is dominant for . Then

If then is eventually nonterminating for P.

If then is terminating for P.
Proof.
By Proposition 3 and Equation (5) we have that for all ,
(6)  
Moreover by the dominance of we have that
(7) 
for all such that .
We first prove Item 1. By assumption, in this case there exists such that for all . Together with Equation (7), this shows that the asymptotically dominant term in Equation (6) has positive sign. It follows that is positive for sufficiently large and hence is eventually nonterminating.
We turn now to Item 2. By assumption there exists and an open subset of such that for all . Moreover by density of in there exist infinitely many such that . Exactly as in Case 1 we can now use the dominance of to conclude that for sufficiently large such that and hence is terminating. ∎
Given , since is an algebraic subset of , the number is algebraic and its sign can be decided. Note however that Proposition 3 does not completely resolve the question of termination with respect to guard from a given initial value . Indeed, let us define to be critical if , where is the dominant equivalence class for . Then neither clause in the above proposition suffices to resolve termination of the loop P in (2) on such a . Indeed the question of whether such a point is eventually nonterminating is equivalent to the Ultimate Positivity Problem for linear recurrence sequences: a longstanding and notoriously difficult open problem in number theory, only known to be decidable up to order 4 [1, 19]. Fortunately in the setting of deciding loop termination we can sidestep such difficult questions. The following section is devoted to handling critical points. The idea is to show that if there is a critical initial value then there is another initial value that is eventually nonterminating and moreover whose eventual nontermination can be established by Proposition 3.
4 Analysis of Critical Points
In this section we continue to analyse termination of the loop P, as given in (2) in the previous section, and refer to the notation established therein.
4.1 Transition Invariance of Critical Points
Intuitively critical points are those for which it is difficult to determine eventual nontermination. One should therefore expect that if is critical then should also be critical. This, and more, follows from the following proposition.
Let and let be an equivalence class that is dominant for . Then is also dominant for and for all we have , where the product is defined pointwise.
Proof.
By definition we have , where the satisfy
(8) 
for all . Likewise we have , where the satisfy
(9) 
Combining Equations (8) and (9) we have the for all ,
Now the collection of functions for is linearly independent in the vector space (see, e.g., [23, Lemma 9.6]). Equating the coefficients of the functions for in the above equation we have for all ; likewise we have that is dominant for . The proposition follows. ∎
The next lemma shows that the existence of a critical point entails the existence of an eventually nonterminating point.
If is critical then there exists a positive integer such that for all , all points in the relative interior of are eventually nonterminating.
Proof.
Given an arbitrary we claim that there exists for which we have . If this were not the case then for all we would have . But by Theorem 2.2, the set is dense in and hence we would have that is identically on , contradicting the dominance of .
For each , the set is an open subset of . Moreover, by the analysis above, the collection is an open cover of . Thus by compactness of there exists such that is a finite cover of .
4.2 Integer NonTerminating Points from Critical Points
Lemma 4.1 shows how to derive the existence of nonterminating points from the existence of a critical point. In this subsection we refine this analysis to derive the existence of integer nonterminating points. In particular, fixing an initial value , we show that for sufficiently large, the set
contains an integer point in its relative interior.
Define and let the vector subspace be the unique translate of containing the origin. Write for the dimension of (equivalently the dimension of ).
For all nonzero integer vectors the set is unbounded.
Proof.
Consider the sequence . If this sequence were constant then would be orthogonal to , contradicting the fact that is nonzero. Since the sequence is nonconstant, integervalued, and satisfies a nondegenerate linear recurrence of order at most (see, e.g., [13, Subsection 1.1.12]), by the SkolemMahlerLech Theorem we have that is unbounded (see the discussion of growth of linear recurrence in [13, Section 2.2]).^{2}^{2}2The above argument actually establishes that diverges to infinity in absolute value. We briefly sketch a more elementary proof of mere unboundedness. If the sequence were bounded then by van der Waerden’s Theorem, for all it would contain a constant subsequence of the form for some . In particular, if then since every infinite subsequence satisfies a linear recurrence of order at most , would have an infinite constant subsequence . If then is constant and if then by [23, Lemma 9.11] is degenerate. ∎
There exists such that for all the set
contains an integer point in its relative interior.
Proof.
Since is spanned by integer vectors, is a lattice of rank in . Define and .
Let be a linear map that takes bijectively onto and whose kernel is the orthogonal complement of . Then is a lattice in of full rank. We claim that the lattice width of with respect to is infinite. Indeed for any nonzero vector we have
(10) 
where is the adjoint map of . But is a nonzero rational vector in and hence Proposition 4.2 entails that the absolute value of (10) is unbounded as runs over . This proves the claim.
By Theorem 2.1 we have that contains a point of in its relative interior and hence contains a point of (necessarily an integer point) in its relative interior. We conclude that also contains an integer point in its relative interior. ∎
We summarise Sections 3 and 4 with a theorem characterising when a loop with a single guard is terminating.
The loop P, given in (2), is nonterminating on if and only if there exists and an equivalence class such that (i) is dominating for and (ii) .
Proof.
We postpone the question of the effectiveness of the above characterisation until we handle loops with multiple guards, in Section 5.
5 Multiple Guards
Now we are ready to present our decision procedure for a general linear loop program
(11) 
with multiple guards. Associated to the loop we consider singleguard loops with a common update function:
for . Clearly Q is nonterminating if and only if there exists such that each loop is nonterminating on . As we now explain, we can decide the existence of such a point following the proof of Theorem 4.2.
Let be the distinct nonzero eigenvalues of the matrix corresponding to the update function in the loop Q. As before, write for . For , denote by the function associated to loop and equivalence class as defined by (4). Given equivalence classes , we define to be the set of such that the following hold for :

is dominant for x in loop , that is, and for all .

.
Loop is nonterminating if and only if there exist equivalence classes such that contains an integer point.
Proof.
Suppose that fails to terminate on . Then each loop also fails to terminate on . Thus if is the dominant equivalence class for in program , for , applying Proposition 3(2) we get that .
Proposition 5 leads to the following procedure for deciding termination of a given linear loop , as shown in (11).

Compute the eigenvalues of the matrix corresponding to the loop update function, as given in (1).

Compute the dominance preorder among eigenvalues.

Compute a basis of the group of multiplicative relations .

Return “nonterminating” if some set contains an integer point and otherwise return “terminating”.
In terms of effectiveness, Steps 1 and 2 can be accomplished via standard symbolic computations with algebraic numbers. (We refer to [18] for a detailed treatment in a very similar setting.) By Theorem 2.2, computing a basis of reduces to checking a finite collection of multiplicative relations among algebraic numbers. Given a basis of we can directly obtain representations of each set as semialgebraic subsets of . Finally, since is convex, we can decide the existence of an integer point in each set using Theorem 2.1.
We have thus established the main result of the paper: There is a procedure to decide termination of singlepath linear loops (of the form specified in (11)) over the integers.
References
 [1] Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, and James Worrell. Effective divergence analysis for linear recurrence sequences. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 47, 2018, Beijing, China, pages 42:1–42:15, 2018.
 [2] Alexander I. Barvinok. Lattice points and lattice polytopes. In Handbook of Discrete and Computational Geometry, Second Edition., pages 153–176. Chapman and Hall/CRC, 2004.
 [3] Amir M. BenAmram, Jesús Doménech, and Samir Genaim. Multiphaselinear ranking functions and their relation to recurrent sets. CoRR, abs/1811.07340, 2018.
 [4] Amir M. BenAmram and Samir Genaim. On the linear ranking problem for integer linearconstraint loops. In The 40th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy  January 23  25, 2013, pages 51–62, 2013.
 [5] Amir M. BenAmram and Samir Genaim. Ranking functions for linearconstraint loops. J. ACM, 61(4):26:1–26:55, 2014.
 [6] Amir M. BenAmram and Samir Genaim. On multiphaselinear ranking functions. In Computer Aided Verification  29th International Conference, CAV 2017, Heidelberg, Germany, July 2428, 2017, Proceedings, Part II, pages 601–620, 2017.

[7]
Bernard Boigelot.
On iterating linear transformations over recognizable sets of integers.
Theor. Comput. Sci., 309(13):413–468, 2003.  [8] Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination analysis of integer linear loops. In CONCUR 2005  Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 2326, 2005, Proceedings, pages 488–502, 2005.

[9]
Mark Braverman.
Termination of integer linear programs.
In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 1720, 2006, Proceedings, pages 372–385, 2006.  [10] Hong Yi Chen, Shaked Flur, and Supratik Mukhopadhyay. Termination proofs for linear simple loops. STTT, 17(1):47–57, 2015.
 [11] Michael Colón and Henny Sipma. Synthesis of linear ranking functions. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 26, 2001, Proceedings, pages 67–81, 2001.
 [12] Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 1114, 2006, pages 415–426, 2006.
 [13] Graham Everest, Alfred J. van der Poorten, Igor E. Shparlinski, and Thomas Ward. Recurrence Sequences, volume 104 of Mathematical surveys and monographs. American Mathematical Society, 2003.
 [14] Bertrand Jeannet, Peter Schrammel, and Sriram Sankaranarayanan. Abstract acceleration of general linear loops. In The 41st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 2021, 2014, pages 529–540. ACM, 2014.
 [15] Leonid Khachiyan and Lorant Porkolab. Computing integral points in convex semialgebraic sets. In 38th Annual Symposium on Foundations of Computer Science, FOCS ’97, Miami Beach, Florida, USA, October 1922, 1997, pages 162–171, 1997.
 [16] Zachary Kincaid, Jason Breck, John Cyphert, and Thomas W. Reps. Closed forms for numerical loops. PACMPL, 3(POPL):55:1–55:29, 2019.
 [17] David W Masser. Linear relations on algebraic groups. New Advances in Transcendence Theory, pages 248–262, 1988. <
Comments
There are no comments yet.