Loop Termination and Generalized Collatz Sequences

Carelli, Mishel

doi:10.4230/LIPIcs.ICALP.2026.175

Loop Termination and Generalized Collatz Sequences

Mishel Carelli

CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Abstract

Linear-constraint loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an infinite computation. Decidability of termination remains open for linear-constraint loops over integers, rationals, and reals. We focus on loops over integers and show that they are tightly connected to generalized Collatz sequences – integer sequences generated by maps that are linear on each residue class modulo a fixed natural number. We prove that termination of one-variable linear-constraint loops is decidable in polynomial time, provided a long-standing conjecture about generalized Collatz sequences holds. Conversely, we show that any decision procedure for one-variable loops would prove or refute specific instances of this conjecture, which remain open. Moreover, we show that if a one-variable loop has a cyclic trace, then it also has a cyclic trace of length at most two.

Keywords and phrases:

Program Verification, Loop Termination, Generalized Collatz Sequences, Linear-Constraint Loops

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Funding:

Mishel Carelli: This work was supported by the European Research Council (ERC) Grant HYPER (No. 101055412).

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification

Related Version:

Full Version: https://arxiv.org/abs/2605.15094

Acknowledgements:

I want to thank Arkadiy Aliev, Bernd Finkbeiner, and Joël Ouaknine for the useful discussions.

DOI:

10.4230/LIPIcs.ICALP.2026.175

Event:

53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Editors:

Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Termination analysis is a long-standing topic in theoretical computer science. The Halting Problem – deciding whether a Turing machine halts on a given input – is undecidable, going back to Turing’s original work. Nevertheless, termination can become decidable when restricted to certain classes of programs.

In this paper, we analyze the open problem of termination for Single-Path Linear-Constraint Loops (SLC). This problem originates in program analysis and verification, where incomplete but efficient approaches such as ranking functions [22] and transition invariants [21] are used as building blocks in verification tools to prove termination and other liveness properties [8, 21, 10] and in Horn Clauses solvers [5, 27].

SLCs are loops of the form

\textbf{while}\ (C\boldsymbol{x}\leq d)\ \textbf{do}\ A\left(\begin{array}[]{c% }\boldsymbol{x}\\ \boldsymbol{x}^{\prime}\end{array}\right)\leq b.

(1)

Here, $\boldsymbol{x}$ is the vector of values of the program variables in the current step, and $\boldsymbol{x}^{\prime}$ denotes their values in the next step. Moreover, $A$ and $C$ are matrices with rational coefficients, and $b$ and $d$ are rational vectors. Later in the paper, we introduce an equivalent definition with the loop guard omitted. The decision problem is: given such a loop, does there exist an infinite computation with program variables taking values in $\mathbb{Z}$ from some initial state?

The question of whether this problem is decidable was posed two decades ago [7], and remains open to this day, not only for loops over $\mathbb{Z}$ , but also over $\mathbb{Q}$ and $\mathbb{R}$ . Recently, decidability over $\mathbb{R}$ has been established in the two-variable case [9].

Decidability of termination varies across loop classes. We now discuss two additional classes of linear loops to illustrate the current landscape.

On the positive side, a prominent decidable class of linear loops called affine SLCs, in which the transition is deterministic and has the form

\mathbf{while}\ (C\boldsymbol{x}\leq d)\ \mathbf{do}\ \boldsymbol{x}^{\prime}:% =A\boldsymbol{x}+b.

Termination of affine SLCs has been proved decidable over $\mathbb{R}$ [26] – via spectral analysis of $A$ – over $\mathbb{Q}$ [7], by symbolic reasoning about matrix powers through eigenvalues, and over $\mathbb{Z}$ [11], using different tools from geometry of numbers, such as the Khachiyan–Porkolab result on deciding whether a convex semi-algebraic set contains an integer point.

On the negative side, another relevant class of linear loops called Multi-Path Linear-Constraint Loops, which allows conditional choice among several linear updates:

\mathbf{while}\ (\text{true})\ \mathbf{do}\ \boldsymbol{x}^{\prime}:=\begin{% cases}A_{1}\boldsymbol{x}+b_{1}&\text{if }C_{1}\boldsymbol{x}\leq d_{1},\\ \vdots\\ A_{k}\boldsymbol{x}+b_{k}&\text{if }C_{k}\boldsymbol{x}\leq d_{k}.\end{cases}

Termination of such multi-path loops is undecidable over $\mathbb{R}$ and $\mathbb{Q}$ [6] and over $\mathbb{Z}$ [1], even for $k=2$ , via encodings of counter machines.

In [7], Braverman asked: “How much nondeterminism can be introduced in a linear loop with no initial conditions before termination becomes undecidable?” Motivated by this question and in light of the subsequent results, SLCs occupy an intriguing middle ground between deterministic, decidable affine SLCs and highly expressive, undecidable multi-path loops. Because nondeterminism in SLCs is convex, it does not allow for modeling the unstructured nondeterminism of counter machines, at least not in a straightforward way.

In [2], the authors show that allowing a single irrational coefficient makes SLC termination undecidable over $\mathbb{Z}$ , and they describe the SLC termination problem as “the most intriguing” among loop-termination problems.

For a complete explanation of these results and further references, we refer the reader to the recent survey on linear loop termination [3].

In this work, we study the SLC termination problem for the case of one variable. While this restriction may seem severe, we show that this problem is deeply non-trivial even for one-variable loops, connecting it with a long-standing number theoretic conjecture about generalized Collatz sequences.

The study of Generalized Collatz sequences is a long-standing topic in number theory [18, 17, 15, 19, 13, 16]. These integer sequences are generated by generalized Collatz mappings of the form

T(x)=\frac{m_{i}x-r_{i}}{d},\ \ \ \ \text{if }x\equiv i\text{ (mod }d)

The Uniform Distribution conjecture [18] asserts that every unbounded generalized Collatz sequence is uniformly distributed modulo $d^{\alpha}$ for every $\alpha\in\mathbb{N}$ . We formulate a weaker statement, the Reachability Conjecture, which posits that every sequence generated by generalized Collatz mappings of a certain type called weak Collatz mappings, reaches a certain residue class modulo $d$ at least once. We prove the Reachability Conjecture for $d=2$ .

Our main result shows that, if the Reachability Conjecture holds, then termination of one-variable SLCs is decidable in polynomial time.

For the other direction, we show that any algorithm deciding termination of one-variable SLCs would, given a weak Collatz mapping, determine whether the Reachability Conjecture holds for all sequences generated by that mapping. All cases with modulus $d>2$ remain open. This suggests that further progress on SLC decidability will require a deeper understanding of generalized Collatz sequences.

Let us give the high-level explanation of the results of this paper and its structure.

Section 2 introduces the basic definitions and notation. In particular, we define the SLC termination problem and split it into two subproblems: deciding the existence of cycles (finite traces from some state to itself), and deciding the existence of self-avoiding traces (infinite traces that never repeat a state).

Section 3 studies cycles. We show that deciding the existence of a cycle of a bounded length can be reduced to an instance of Integer Linear Programming problem. The main result of this section is that for a one-variable loop, the existence of any cycle implies the existence of a cycle of length at most two; hence cycle-detection problem is decidable for one-variable loops.

Section 4 introduces generalized Collatz sequences, and states the Uniform Distribution and Reachability Conjectures. We prove the Reachability conjecture for the case $d=2$ , and we prove that a one-variable SLC termination-checking algorithm, if it existed, could verify specific open instances of this conjecture.

Section 5 analyzes self-avoiding traces and shows that, assuming the Reachability Conjecture, termination of one-variable SLCs is decidable in polynomial time. The proof is geometric in nature. We view the transition relation as a polyhedron in $\mathbb{R}^{2}$ and analyze its Minkowski-Weyl decomposition. Intuitively, we identify where the transition polyhedron “points to”. Simplifying, the self-avoiding trace exists if the polyhedron points in the direction where the absolute value of the variable grows. However, several corner cases arise, in one of which, the trace of SLC forms a weak Collatz sequence, which avoids a certain residue class modulo $d$ . If the Reachability conjecture holds, we can conclude that this kind of execution needs to terminate. Otherwise, the presented approach results in a semi-algorithm, which does not give an answer in these specific cases.

Section 6 presents the formal proofs of the results from Sections 3, 4, and 5.

Section 7 summarizes the results.

2 Preliminaries

2.1 Notation

We denote the sets of natural numbers, integers, rationals, and reals by $\mathbb{N},\mathbb{Z},\mathbb{Q}$ , and $\mathbb{R}$ , respectively. The sets of positive, negative, and nonnegative real numbers are denoted by $\mathbb{R}_{+}$ , $\mathbb{R}_{-}$ , and $\mathbb{R}_{\geq 0}$ .

Given $S\subseteq\mathbb{R}^{n}$ , we write $S_{\mathbb{Z}}:=S\cap\mathbb{Z}^{n}$ for its set of integer points.

Given $T\subseteq\mathbb{R}^{2n}$ and $z\in\mathbb{R}^{n}$ , define the slice $T_{z}:=\{x_{2}\in\mathbb{R}^{n}\mid(z,x_{2})\in T\}$ .

Vectors $v_{1},v_{2}\in\mathbb{R}^{n}$ are collinear if there exists $r\in\mathbb{R}$ such that $v_{1}=rv_{2}$ ; we write $v_{1}\parallel v_{2}$ . If $v_{1}$ and $v_{2}$ are not collinear, we write $v_{1}\nparallel v_{2}$ .

For $p,q\in\mathbb{Z}$ , $\gcd(p,q)$ denotes the greatest natural number that divides both $p$ and $q$ .

For $x\in\mathbb{R}$ define

\operatorname{sign}(x):=\begin{cases}1&\text{if }x>0,\\ -1&\text{if }x<0,\\ 0&\text{if }x=0.\end{cases}

2.2 Convex sets and the Minkowski–Weyl theorem

Given $S_{1},S_{2}\subseteq\mathbb{R}^{n}$ , the Minkowski sum is

S_{1}+S_{2}:=\{\,y+z\mid y\in S_{1},\,z\in S_{2}\}.

A set $K\subseteq\mathbb{R}^{n}$ is convex if for all $x,y\in K$ and all $\lambda\in[0,1]$ , we have $\lambda x+(1-\lambda)y\in K$ .

The topological closure of $S\subseteq\mathbb{R}^{n}$ is denoted $\operatorname{cl}(S)$ (the set of limits of the sequences of elements of $S$ ). A set $S$ is closed if $S=\operatorname{cl}(S)$ .

Intersections of families of closed sets are closed, and intersections of families of convex sets are convex.

Definition 1.

Let $S\subseteq\mathbb{R}^{n}$ .

1.

A convex hull of $S$ is defined by

$\operatorname{conv}(S)=\{\sum_{i=1}^{k}\alpha_{i}v_{i}\mid k\in\mathbb{N},\ % \alpha_{i}\in[0;1],\ v_{i}\in S,\ \sum_{i=1}^{k}\alpha_{i}=1\}$
2.

A nonnegative (conic) hull is defined by

$\operatorname{nonneg}(S)=\{\sum_{i=1}^{k}\alpha_{i}v_{i}\mid k\in\mathbb{N},\ % \alpha_{i}\in\mathbb{R}_{\geq 0},\ v_{i}\in S\}$

A convex cone is a set $C\subseteq\mathbb{R}^{n}$ such that for every $c_{1},c_{2}\in C$ and every $\lambda\in\mathbb{R}_{\geq 0}$ , we have $\lambda c_{1}\in C$ and $c_{1}+c_{2}\in C$ . Every convex cone is a convex set.

Definition 2.

Let $K\subseteq\mathbb{R}^{n}$ be a nonempty convex set. The recession cone of $K$ is

\operatorname{rec}(K):=\{\,v\in\mathbb{R}^{n}\mid K+\mathbb{R}_{\geq 0}v% \subseteq K\,\}.

For every nonempty convex $K$ , $\operatorname{rec}(K)$ is a closed convex cone. A cone $K$ is pointed if $K\cap(-K)=0$ .

The following classical result appears in §8.9 of [24].

Theorem 3 (Minkowski–Weyl Theorem).

Let $P\subseteq\mathbb{R}^{n}$ . The following are equivalent:

1.

$P$ is a polyhedron, i.e., $P=\{x\in\mathbb{R}^{n}\mid Ax\leq b\}$ for some $A\in\mathbb{R}^{k\times n}$ and $b\in\mathbb{R}^{k}$ .
2.

There exist $w_{1},\dots w_{l}\in P$ and $v_{1},\dots,v_{m}\in\mathbb{R}^{n}$ , such that

$P=\operatorname{conv}(w_{1},\dots,w_{l})+\operatorname{rec}(P)=\operatorname{% conv}(w_{1},\dots,w_{l})+\operatorname{nonneg}(v_{1},\dots,v_{m})$

Moreover, if $P$ is given by linear inequalities with rational coefficients, then $w_{i}$ and $v_{i}$ can be chosen with rational entries.

Note that any polyhedron $P\subseteq\mathbb{R}^{n}$ is closed and convex, because every linear inequality defines a closed half-space in $\mathbb{R}^{n}$ and $P$ is an intersection of finitely many half-spaces.

The following result trivially follows from basic results in convex geometry, but we present the proof of this exact formulation for the sake of completeness.

Proposition 4.

The following statements hold for closed convex cones $C\subseteq\mathbb{R}^{2}$ .

1.

$C$ can be represented as $\operatorname{nonneg}(v_{1},\dots,v_{m})$ for some $v_{i}\in\mathbb{R}^{2}$ with $m\leq 3$ .
2.

If $v_{1},v_{2}\in\mathbb{R}^{2}$ and $v_{1}\nparallel v_{2}$ , then $\operatorname{nonneg}(v_{1},v_{2})$ contains no line in $\mathbb{R}^{2}$ .
3.

If $C$ cannot be generated by two vectors, then $C$ is either a half-plane or the whole plane.

Proof.

By §8.9 of [24], $C$ decomposes as $C=C^{\prime}+\operatorname{lin}(C)$ , where $\operatorname{lin}(C):=C\cap(-C)$ is the lineality space and $C^{\prime}$ is a pointed cone.

If $\operatorname{lin}(C)=\mathbb{R}^{2}$ , then $C=\mathbb{R}^{2}=\operatorname{nonneg}((0,1),(1,0),(-1,-1))$ .

Assume $\operatorname{lin}(C)$ is a line, say $\operatorname{nonneg}(v,-v)$ , and $C\neq\mathbb{R}^{2}$ . Then $\mathbb{R}^{2}=H_{1}\cup H_{2}\cup\operatorname{lin}(C)$ , where $H_{1}$ and $H_{2}$ are the open half-planes with boundary $\operatorname{lin}(C)$ . If $C^{\prime}\cap H_{i}\neq\emptyset$ for some $i\in{1,2}$ , then $H_{i}\subseteq C$ . Hence $C$ is either the line $\operatorname{nonneg}(v,-v)$ or, if there exists $v^{\prime}\in C^{\prime}\setminus\operatorname{lin}(C)$ , a half-plane $\operatorname{nonneg}(v,-v,v^{\prime})$ .

Finally, if $\operatorname{lin}(C)={0}$ , then $C=C^{\prime}$ is pointed and therefore generated by two vectors (see, e.g., Example 2.39 in [25]); in this case, it cannot contain a line by definition of pointedness. $\hfill\blacktriangleleft$

The next statement is Corollary 8.3.3 in [23].

Proposition 5 (Recession cone of an intersection).

If $P_{1}$ and $P_{2}$ are closed convex sets with $P_{1}\cap P_{2}\neq\emptyset$ , then $\operatorname{rec}(P_{1}\cap P_{2})=\operatorname{rec}(P_{1})\cap\operatorname% {rec}(P_{2})$ .

2.3 Loops

We consider Single-Path Linear-Constraint Loops (SLC). Throughout, SLCs are over the integers.

The vector of variables is $\boldsymbol{x}=(x_{1},\dots,x_{n})^{T}$ . A state is a valuation over integers, i.e., a vector in $\mathbb{Z}^{n}$ . The vector of variables at the next step is $\boldsymbol{x}^{\prime}=(x_{1}^{\prime},\dots,x_{n}^{\prime})^{T}$ . An SLC is specified by a system of linear inequalities

A\left(\begin{array}[]{c}\boldsymbol{x}\\ \boldsymbol{x}^{\prime}\end{array}\right)\leq b,

(2)

where $A\in\mathbb{Z}^{k\times 2n}$ and $b\in\mathbb{Z}^{k}$ .

$\blacktriangleright$ Remark 6.

This definition differs from (1) in the Introduction because it omits an explicit loop guard. The two forms are expressively equivalent, since the guard can be encoded in the transition relation.

The transition polyhedron is the set $\mathcal{R}\subseteq\mathbb{R}^{2n}$ of vectors satisfying (2).

$\blacktriangleright$ Remark 7.

Since we study integer-valued loops, the actual transitions between states are elements of $\mathcal{R}_{\mathbb{Z}}$ . We nevertheless work over the reals when convenient for proofs.

We identify an SLC with its transition polyhedron $\mathcal{R}\subseteq\mathbb{R}^{2n}$ , and denote it by $\mathcal{R}$ . We denote the size of the binary encoding of $A$ and $b$ as $|\mathcal{R}|$ .

A trace is a sequence of states $s_{1},s_{2},\dots$ such that $(s_{i},s_{i+1})\in\mathcal{R}_{\mathbb{Z}}$ for all $i\geq 1$ .

The SLC termination problem is to decide, for a given SLC, whether it has an infinite trace.

2.4 Cycles and Self-avoiding Traces

We divide the termination problem into two problems for two different types of infinite traces.

For an SLC, a cycle of length $k$ is a finite trace $s_{1},\dots,s_{k},s_{1}$ . The existence of a cycle implies the existence of an infinite trace. The converse need not hold:

Example 8.

The SLC $x^{\prime}=x+1$ has no cycle but admits an infinite trace.

An infinite trace $s_{1},s_{2},\dots$ is self-avoiding if $s_{i}\neq s_{j}$ for all $i\neq j$ .

Observation 9.

An SLC has an infinite trace if and only if it has a cycle or a self-avoiding trace.

In the remainder of the paper, we analyze the problems of deciding the existence of a cycle and the existence of a self-avoiding trace separately for a given SLC.

3 Cycles

3.1 Bound on a cycle length

Although cycles are finite objects (unlike self-avoiding traces), deciding their existence for an SLC remains nontrivial, since a cycle can have arbitrary length. By contrast, deciding the existence of a cycle whose length is bounded is decidable.

Proposition 10.

Given an SLC $\mathcal{R}$ and $M\in\mathbb{N}$ , deciding whether $\mathcal{R}$ has a cycle of length at most $M$ is in $\mathsf{NP}$ with respect to $|\mathcal{R}|\cdot M$ .

Proof.

It is known that the feasibility problem for Integer Linear Programming (ILP) – deciding whether a rational polyhedron contains an integer point – is $\mathsf{NP}$ -complete [20]. We give a polynomial-time reduction from our problem to ILP.

Given $\mathcal{R}$ and $M$ , for each $m\in\{1,\dots,M\}$ we construct an ILP instance encoding the existence of a cycle of length exactly $m$ :

P_{m}=\bigl\{(\boldsymbol{x}_{1},\dots,\boldsymbol{x}_{m})\mid(\boldsymbol{x}_% {m},\boldsymbol{x}_{1})\in\mathcal{R}\wedge\forall i<m:(\boldsymbol{x}_{i},% \boldsymbol{x}_{i+1})\in\mathcal{R}\bigr\}.

Then $\mathcal{R}$ has a cycle of length at most $M$ iff one of the polyhedra $P_{m}$ contains an integer point. Each ILP instance has size $\mathcal{O}(|\mathcal{R}|\cdot M)$ . $\hfill\blacktriangleleft$

Proposition 26 of [9] shows that for Linear-Constraint Loops over $\mathbb{Q}$ or $\mathbb{R}$ , the existence of a bounded infinite sequence is equivalent to the existence of a cycle of length one. The next proposition shows that this equivalence fails over $\mathbb{Z}$ .

Proposition 11.

For every $n$ , there exists an SLC over $n$ variables that has a cycle of length $2^{n}$ and no cycles of smaller length.

Proof.

Fix $n$ and consider the set of states $S:=\{0,1\}^{n}$ . Take any cycle $C$ on $S$ , so that each $s\in S$ appears exactly once; $|C|=2^{n}$ . Let $T$ be the set of transitions of $C$ , so $T\subseteq\{0,1\}^{2n}$ . Let $\mathcal{R}:=\operatorname{conv}(T)$ , which as a convex hull of a finite set of integer points, can be defined as an SLC. We claim that $\mathcal{R}_{\mathbb{Z}}=T$ , i.e., $\operatorname{conv}(T)$ has no integer points other than its vertices in $T$ . This implies that the minimal cycle length of $\operatorname{conv}(T)$ is $2^{n}$ .

Suppose, to the contrary, that there exists $p\in\mathcal{R}_{\mathbb{Z}}\setminus T$ . Enumerate $T=\{t^{1},\dots,t^{2^{n}}\}$ and write $p=\sum_{i=1}^{2^{n}}\alpha_{i}t^{i}$ with $\alpha_{i}\in[0,1]$ and $\sum_{i}\alpha_{i}=1$ . Without loss of generality, assume $\alpha_{1}>0$ and choose a coordinate $j$ such that $t^{1}_{j}\neq p_{j}$ (such a $j$ exists since $t^{1}\neq p$ ). Because $p_{j}=\sum_{i=1}^{2^{n}}\alpha_{i}t^{i}_{j}$ is an integer and each $t^{i}_{j}\in\{0,1\}$ , the only way the convex combination can be an integer is if all $t^{i}_{j}$ with $\alpha_{i}>0$ are equal. This contradicts $t^{1}_{j}\neq p_{j}$ . Hence, no such $p$ exists. $\hfill\blacktriangleleft$

Since there is no universal bound on the minimal cycle length, it is natural to ask whether a bound depending on the number of variables exists.

Question 12.

For every $n\in\mathbb{N}$ , does there exist a constant $M(n)$ such that every loop over $n$ variables that has a cycle also has a cycle of length at most $M(n)$ ?

If the answer to Question 12 is positive, then cycle detection reduces to checking for cycles of length at most $M(n)$ . If $M(n)$ is computable, this yields decidability of cycle detection.

There exist convex sets that are not polyhedra (e.g., convex sets defined by quadratic inequalities). We now show that a positive answer to Question 12 extends from polyhedral relations to arbitrary convex relations.

Proposition 13.

Suppose that every SLC $\mathcal{R}\subseteq\mathbb{R}^{2n}$ with a cycle also has a cycle of length at most $M(n)$ . Then any convex relation $\mathcal{T}\subseteq\mathbb{R}^{2n}$ with a cycle also has a cycle of length at most $M(n)$ .

Proof.

If $\mathcal{T}$ has a cycle represented by the set of transitions $\{t_{1},\dots,t_{m}\}\subseteq\mathcal{T}$ , then $\operatorname{conv}(t_{1},\dots,t_{m})\subseteq\mathcal{T}$ by convexity. The polyhedron $\operatorname{conv}(t_{1},\dots,t_{m})$ has a cycle and therefore, by hypothesis, has one of length at most $M(n)$ . This cycle is contained in $\mathcal{T}$ . $\hfill\blacktriangleleft$

3.2 One variable case

The following Theorem shows that the answer to Question 12 is positive for $n=1$ with $M(1)=2$ .

Theorem 14.

If an SLC $\mathcal{R}\subseteq\mathbb{R}^{2}$ has a cycle, then it has a cycle of length at most $2$ .

Sketch of proof.

Let us informally explain the idea of the proof with an illustration from Figure 1(a). Consider the set of transitions of a cycle (the black points). The center of this set lies on the diagonal (the green point). If it has integer coordinates, then we obtain a length-one cycle. Otherwise, it lies on a unit square in the integer lattice. Two vertices of this unit square lie on the diagonal representing length-one cycles (the blue points). The other two vertices lie on the anti-diagonal, representing a length-two cycle (the red points). We then consider several cases, branching on the signs of different values, such as the largest value among the states of the cycle. In some cases, we show that $\mathcal{R}$ contains points on the diagonal below or above the blue points, yielding the existence of the length-one cycles. In the remaining cases, we show $\mathcal{R}$ contains points on the anti-diagonal on both sides of the green point, implying the existence of a length-two cycle. The formal argument is presented in Section 6. $\hfill\blacktriangleleft$

(a) Cycle intuition.

(b) SLC

\mathcal{R}^{+}

.

Figure 1:

4 Generalized Collatz sequences

The classical Collatz problem remains open. A key difficulty is its residue-class–dependent dynamics modulo $2$ . Several generalizations have been studied, replacing the modulus $2$ by other moduli and considering related piecewise-linear maps [12]. In particular, the framework proposed by Möller [19] has been investigated both theoretically and empirically [16]. In this paper, we focus on the Uniform Distribution Conjecture of Matthews and Watts [18], formulated for Möller’s generalization.

Let $d$ be a positive integer with $d\geq 2$ . Let $m_{0},\dots,m_{d-1}$ be nonzero integers such that $\gcd(m_{i},d)=1$ for every $i$ . Let $R=\{r_{0},\dots,r_{d-1}\}$ be a set of integers with the property that for each $i,$ $m_{i}i\equiv r_{i}(mod\ d)$ . Then the generalized Collatz mapping $T:\mathbb{Z}\to\mathbb{Z}$ is given by

T(x):=\frac{m_{i}x-r_{i}}{d},\ \ \ \ \text{if }x\equiv i\text{ (mod }d)

For $n\in\mathbb{Z}$ we define the sequence $\{T^{k}(n)\}_{k\in\mathbb{N}}$ recursively by

T^{k}(n):=\begin{cases}n,\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \text{if }k=0,\\ T(T^{k-1}(n)),\ \ \ \ \text{if }k>0\end{cases}

A sequence $\{s_{k}\}_{k\in\mathbb{N}}$ is called unbounded if for every $n\in\mathbb{N}$ there exists $k\in\mathbb{N}$ such that $|s_{k}|>n$ .

We recall a longstanding number-theoretic conjecture, first stated by Matthews and Watts [18] and further discussed, with empirical support, in [16].

Conjecture 15 (Uniform Distribution Conjecture).

If the sequence $\{T^{k}(n)\}_{k\in\mathbb{N}}$ is unbounded, it is uniformly distributed modulo $d^{\alpha}$ for each $\alpha\geq 1$ , i.e.

\underset{N\to\infty}{\mathrm{lim}}\;\frac{1}{N}card\{k\leq N\mid T^{k}(n)% \equiv i\ (mod\ d^{\alpha})\}=\frac{1}{d^{\alpha}}

for $i=0,\dots,d^{\alpha}-1$ .

In this paper, we state a weaker version of this conjecture. First, let us define a more restricted class of generalized Collatz mappings.

Let $d$ be a positive integer $d\geq 2$ , let $m$ be a nonzero integer with $\gcd(d,m)=1$ , and let $a$ be an integer. Then a weak Collatz mapping $T:\mathbb{Z}\rightarrow\mathbb{Z}$ is given by

T(x):=\frac{mx-(a+i)}{d},\ \ \ \ \text{where }0\leq i<d,\text{ with }mx\equiv a% +i\ (\text{mod }d).

Conjecture 16 (Reachability Conjecture).

Let $T$ be a weak Collatz mapping. Suppose for some $n\in\mathbb{Z}$ the sequence $\{T^{k}(n)\}_{k\in\mathbb{N}}$ is unbounded. Then there exists $k\geq 0$ such that $mT^{k}(n)\equiv a\ (mod\ d)$ .

The proofs of the next two propositions are presented in Section 6.

The following proposition implies that Conjecture 16 holds for mappings with $d=2$ .

Proposition 17.

Let $T$ be a generalized Collatz mapping with $d>1$ . Suppose for some $n\in\mathbb{Z}$ the sequence $\{T^{k}(n)\}_{k\in\mathbb{N}}$ is unbounded. Then it visits at least two residue classes modulo $d$ .

The next proposition links weak Collatz sequences to self-avoiding traces.

Proposition 18.

There exists a linear-time algorithm that takes as input a weak Collatz mapping $T(x)=\frac{mx-(a+i)}{d},$ with $m>d$ , and outputs two one-variable SLCs, $\mathcal{R}_{+}$ and $\mathcal{R}_{-}$ , such that:

1.

$\mathcal{R}_{+}$ has an infinite trace if and only if there exists $n\in\mathbb{Z}$ such that, for every $k\geq 0$ ,

$mT^{k}(n)\not\equiv a\pmod{d}\quad\text{and}\quad T^{k}(n)>0.$
2.

$\mathcal{R}_{-}$ has an infinite trace if and only if there exists $n\in\mathbb{Z}$ such that, for every $k\geq 0$ ,

$mT^{k}(n)\not\equiv a\pmod{d}\quad\text{and}\quad T^{k}(n)<0.$

Proposition 18 implies that any decidability procedure for one-variable SLC termination, if it existed, could, given a weak Collatz mapping, determine whether the Reachability Conjecture holds for this particular mapping. This suggests that progress on decidability requires progress in understanding the behavior of weak Collatz sequences. We conclude with an example of a mapping for which the Reachability Conjecture remains, to our knowledge, open, and we are unaware of any results that imply it.

Example 19.

Consider the weak Collatz mapping

T(x)=\frac{4x-i}{3},\ \ \ \ \text{if }4x\equiv i\ (\text{mod }3),

which can be rewritten as

T(x)=\lfloor\frac{4x}{3}\rfloor.

For this particular $T$ , it remains open whether it is true that for every $n\geq 3$ there exists $k\in\mathbb{N}$ such that $3\mid T^{k}(n)$ .

Proposition 18 implies that this question is equivalent to the termination question for the SLC defined by

\mathcal{R}^{+}:=\{(x,x^{\prime})\in\mathbb{R}^{2}\mid 4x-2\leq 3x^{\prime}% \leq 4x-1\text{ and }x\geq 3\}.

On the Figure 1(b), $\mathcal{R}^{+}$ is depicted as a red area, bounded by the two lines $x^{\prime}=\frac{4x-2}{3}$ and $x^{\prime}=\frac{4x-1}{3}$ , starting from $x=3$ , since for $3\leq x$ , $x<\lfloor\frac{4x}{3}\rfloor$ .

5 Self-avoiding Traces

The following theorem is the main result of the paper.

Theorem 20.

If the Reachability Conjecture holds, then the termination of SLCs over one variable is decidable in polynomial time.

This section is devoted to proving Theorem 20. The treatment of cycles is given in Section 3. Now we turn our attention to self-avoiding traces. To determine the existence of self-avoiding traces, we make a case analysis, based on the geometric placement of $\mathcal{R}$ in $\mathbb{R}^{2}$ , split into four Lemmas 21, 23, 24, and 25. Before stating these lemmas, we introduce an auxiliary SLC that splits $\mathbb{R}^{2}$ into different parts.

Define the following sets.

I_{+}=\{(x_{1},x_{2})\in\mathbb{R}^{2}\mid 0<x_{1}<x_{2}\},\ \ \ \ \ \ \ \ \ % \ \ I_{-}=\{(x_{1},x_{2})\in\mathbb{R}^{2}\mid x_{2}<x_{1}<0\},

\Delta_{+}=\{(x_{1},x_{2})\in\mathbb{R}^{2}\mid 0<x_{1}=x_{2}\},\ \ \ \ \ \ \ % \ \ \ \Delta_{-}=\{(x_{1},x_{2})\in\mathbb{R}^{2}\mid x_{1}=x_{2}<0\},

\Delta=\Delta_{+}\cup\Delta_{-},\ \ \ \ \ \ \ \ \ I=I_{+}\cup I_{-}.

Note that the topological closure of $I_{+}$ , $I_{-}$ and $\Delta$ are

\operatorname{cl}(I_{+})=I_{+}\cup\Delta_{+}\cup\{(0,x_{2})\in\mathbb{R}^{2}% \mid x_{2}\geq 0\},

\operatorname{cl}(I_{-})=I_{-}\cup\Delta_{-}\cup\{(0,x_{2})\in\mathbb{R}^{2}% \mid x_{2}\leq 0\},

\operatorname{cl}(\Delta)=\Delta\cup\{(0,0)\}.

Recall that any SLC $\mathcal{R}\subseteq\mathbb{R}^{2}$ can, by Theorem 3, be represented as

\mathcal{R}=\operatorname{conv}(w_{1},\dots w_{l})+\operatorname{rec}(\mathcal% {R})=\operatorname{conv}(w_{1},\dots,w_{l})+\operatorname{nonneg}(v_{1},\dots,% v_{m}),

with $m\leq 3$ . Moreover, since $\mathcal{R}$ is defined by the set of integer linear inequalities, we may assume that all $w_{i}$ and $v_{i}$ have rational coefficients.

The following case distinction, presented in four lemmas, is aimed at characterizing when a given SLC admits a self-avoiding trace, and is based on the number of generators of $\operatorname{rec}(\mathcal{R})$ and on the intersection of $\operatorname{rec}(\mathcal{R})$ with $I_{+},I_{-},\Delta_{+}$ and $\Delta_{-}$ . Each lemma treats SLCs whose recession cone has a specific number of generators.

Lemma 21.

Let $\mathcal{R}$ be an SLC. Suppose $\operatorname{rec}(\mathcal{R})=\operatorname{nonneg}(v_{1},v_{2})$ and $v_{1}\nparallel v_{2}$ . Then:

1.

If $\operatorname{rec}(\mathcal{R})\cap I\neq\emptyset$ , then the loop has a self-avoiding trace.
2.

If $\operatorname{rec}(\mathcal{R})\cap(I\cup\Delta)=\emptyset$ , then the loop does not have a self-avoiding trace.
3.

If $\operatorname{rec}(\mathcal{R})\cap\Delta_{+}\neq\emptyset$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{+}\neq\emptyset$ , then the loop has a self-avoiding trace.
4.

If $\operatorname{rec}(\mathcal{R})\cap(I\cup\Delta)\subseteq\Delta_{-}$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{-}=\emptyset$ , then the loop does not have a self-avoiding trace.
5.

If $\operatorname{rec}(\mathcal{R})\cap\Delta_{-}\neq\emptyset$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{-}\neq\emptyset$ , then the loop has a self-avoiding trace.
6.

If $\operatorname{rec}(\mathcal{R})\cap(I\cup\Delta)\subseteq\Delta_{+}$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{+}=\emptyset$ , then the loop does not have a self-avoiding trace.

Sketch of proof.

This lemma handles the case where $\operatorname{rec}(\mathcal{R})$ is pointed and generated by two noncollinear vectors. In this regime, $\mathcal{R}$ is “large” in the sense that the number of integer points in its vertical slices, $|\mathcal{R}_{n}\cap\mathbb{Z}|$ , is unbounded as $n$ varies. Consequently, we can decide whether the loop admits a self-avoiding trace by inspecting the direction of this cone.

Statements 1 and 2 are the essential ones.

The case where the recession cone intersects $I$ , as in Figure 2(a), corresponds to Statement 1. In this case, it points in a direction in which the absolute value of the state increases; thus, $\mathcal{R}$ admits a self-avoiding trace.

The case where the recession cone does not intersect $I\cup\Delta$ , as in Figure 2(b), corresponds to Statement 2. In this case, it points only in directions in which the absolute value of the state decreases; thus, $\mathcal{R}$ does not admit a self-avoiding trace.

The case in which the cone intersects $\Delta$ is slightly more delicate and requires analyzing the intersection $\mathcal{R}\cap I$ , which is done in the remaining statements.

The complete proof is given in Section 6. $\hfill\blacktriangleleft$

(a) SLC that points towards

I_{+}

.

(b) SLC that does not point towards

I\cup\Delta

.

Figure 2: SLC with recession cone generated by two noncollinear vectors.

The next lemma, Lemma 23, treats the case in which $\operatorname{rec}(\mathcal{R})$ is generated by a single vector. In this situation $\mathcal{R}$ is infinite but “thin”: each vertical slice $\mathcal{R}_{n}$ is bounded. We quantify this thinness via the $0pt$ .

Definition 22.

For $T\subseteq\mathbb{R}^{2}$ and $p\in\mathbb{N}$ , define the $p$ -height of $T$ by

0pt_{p}(T):=\sup\{|T_{z}\cap(\frac{1}{p}\mathbb{Z})|\mid z\in\mathbb{Z}\}.

Lemma 23.

Let $\mathcal{R}$ be an SLC. Suppose $\operatorname{rec}(\mathcal{R})=\operatorname{nonneg}(v)$ and $v=(p,q)$ for $p\in\mathbb{Z}$ , $q\in\mathbb{Z}$ and GCD $(p,q)=1$ . Then:

1.

If $|p|<|q|$ , $\operatorname{sign}(p)=\operatorname{sign}(q)$ and $0pt_{|p|}(\mathcal{R})\geq|p|$ , then the loop has a self-avoiding trace.
2.

If $\operatorname{sign}(p)\neq\operatorname{sign}(q)$ , then the loop does not have a self-avoiding trace.
3.

If $|p|>1$ and $1<0pt_{|p|}(\mathcal{R})<|p|$ , then the loop does not have a self-avoiding trace if Conjecture 16 holds.
4.

If $|p|>1$ and $0pt_{|p|}(\mathcal{R})\leq 1$ , then the loop does not have a self-avoiding trace.
5.

If $0pt_{|p|}(\mathcal{R})=0$ , then the loop does not have a self-avoiding trace.
6.

If $|p|>|q|$ , then the loop does not have a self-avoiding trace.
7.

If $p=q=1$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{+}\neq\emptyset$ , then the loop has a self-avoiding trace.
8.

If $p=q=1$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{+}=\emptyset$ , then the loop does not have a self-avoiding trace.
9.

If $p=q=-1$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{-}\neq\emptyset$ , then the loop has a self-avoiding trace.
10.

If $p=q=-1$ and $\mathcal{R}_{\mathbb{Z}}\cap I_{-}=\emptyset$ , then the loop does not have a self-avoiding trace.

Sketch of proof.

In this case, the cone is again pointed, but it is generated by a single vector. Since the cone is not “large” as in Lemma 21, it requires a more delicate analysis.

The cases where the recession cone does not intersect $I\cup\Delta$ (Statements 2 and 6) are similar to Statement 2 of Lemma 21 and are handled in the same way.

The cases where the recession cone intersects $I$ are the essential ones and correspond to Statements 1, 3, and 4, which are the most important in this Lemma.

The case where the height of $\mathcal{R}$ is too small, as in Figure 3(a), corresponds to Statement 4. In this regime, traces correspond to a weak Collatz sequence that visits only one residue class. Thus, the non-existence of a self-avoiding trace follows from Proposition 17.

The case where the height of $\mathcal{R}$ is large enough, as in Figure 3(b), corresponds to Statement 1. This case is analogous to Statement 1 of Lemma 21. Here we show the existence of a self-avoiding trace.

The case where the height of $\mathcal{R}$ is at least $1$ but less than $|p|$ , as in Figure 1(b), corresponds to Statement 3. In this case, every trace is a weak Collatz sequence that visits fewer than $|p|$ residue classes. If the Reachability Conjecture 16 holds, then the loop does not admit a self-avoiding trace.

The complete proof is presented in Section 6. $\hfill\blacktriangleleft$

(a) Thin SLC.

(b) Thick SLC.

Figure 3: SLC with recession cone generated by one vector.

Lemma 24.

Let $\mathcal{R}$ be an SLC. Suppose $\operatorname{rec}(\mathcal{R})=\operatorname{nonneg}(v_{1},v_{2})$ and $v_{1}=-v_{2}=(p,q)$ for $p\in\mathbb{Z}_{\geq 0}$ , $q\in\mathbb{Z}$ and GCD $(p,q)=1$ . Then:

1.

If $0<p<|q|$ and $0pt_{p}(\mathcal{R})\geq p$ , then the loop has a self-avoiding trace.
2.

If $p>1$ and $1<0pt_{p}(\mathcal{R})<p$ , then the loop does not have a self-avoiding trace if Conjecture 16 holds.
3.

If $p>1$ and $0pt_{p}(\mathcal{R})\leq 1$ , then the loop does not have a self-avoiding trace.
4.

If $0pt_{|p|}(\mathcal{R})=0$ , then the loop does not have a self-avoiding trace.
5.

If $p>|q|$ , then the loop does not have a self-avoiding trace.
6.

If $p=q$ and $\mathcal{R}_{\mathbb{Z}}\cap I\neq\emptyset$ , then the loop has a self-avoiding trace.
7.

If $p=q$ and $\mathcal{R}_{\mathbb{Z}}\cap I=\emptyset$ , then the loop does not have a self-avoiding trace.
8.

If $-p=q$ and $0pt_{1}(\mathcal{R})\geq 2$ , then the loop has a self-avoiding trace.
9.

If $-p=q$ and $0pt_{1}(\mathcal{R})\leq 1$ , then the loop does not have a self-avoiding trace.
10.

If $p=0$ , then the loop does not have a self-avoiding trace.

Sketch of proof.

This lemma treats the case where $\operatorname{rec}(\mathcal{R})$ is a line (i.e., generated by vectors $v_{1}$ and $-v_{1}$ ). In this setting, $\mathcal{R}$ is unbounded but “thin”: each vertical slice $\mathcal{R}_{n}$ is bounded. Accordingly, we analyze the height $0pt_{p}(\mathcal{R})$ to determine whether a self-avoiding trace exists.

The intuition is the same as in Lemma 23, but the argument requires some additional technicalities. The complete proof is presented in Section 6. $\hfill\blacktriangleleft$

Lemma 25.

Let $\mathcal{R}$ be an SLC. The following statements hold.

1.

If $\operatorname{rec}(\mathcal{R})=\operatorname{nonneg}(v_{1},v_{2},v_{3})$ and it cannot be generated by two vectors, then the loop has a self-avoiding trace.
2.

If $\operatorname{rec}(\mathcal{R})=\{0\}$ , then the loop does not have a self-avoiding trace.

Sketch of proof.

This Lemma analyzes the remaining two cases. The complete proof is presented in Section 6. $\hfill\blacktriangleleft$

Finally, we are ready to prove the main theorem.

Proof of Theorem 20.

In fixed dimension, integer feasibility for rational polyhedra can be decided in polynomial time [14].

By Theorem 14, cycle detection for a one-variable SLC reduces to checking for cycles of length at most two. Each such check can be expressed as an ILP instance of dimension four, as in Proposition 10, and can therefore be performed in polynomial time.

Moreover, a Minkowski–Weyl decomposition of $\mathcal{R}$ can be computed in polynomial time [4]. By Lemmas 21, 23, 24, and 25, the remaining analysis consists of a constant number of two-dimensional ILP feasibility checks, obtained by intersecting $\operatorname{rec}(\mathcal{R})$ with the cones $I_{+},I_{-},\Delta_{+}$ , and $\Delta_{-}$ , and, in certain cases, by computing the height.

It remains to argue that the height checks can also be carried out in polynomial time. If $\operatorname{rec}(\mathcal{R})=\operatorname{nonneg}(v,-v)$ , then all vertical slices $\mathcal{R}_{z}$ are translates of one another; hence, the height is independent of $z$ and can be computed from any single slice.

If $\mathcal{R}=\operatorname{conv}(w_{1},\dots,w_{\ell})+\operatorname{nonneg}(v)$ with $v=(p,q)$ , $\operatorname{sign}(p)=\operatorname{sign}(q)$ , and $\gcd(p,q)=1$ , then the height of the slice $\mathcal{R}_{z}$ varies monotonically with $z$ : it increases with $z$ when $p,q>0$ and decreases with $z$ when $p,q<0$ .

Since $\operatorname{conv}(w_{1},\dots,w_{\ell})$ is bounded, there exists $M\in\mathbb{N}$ such that the absolute values of the coordinates of all points in $\operatorname{conv}(w_{1},\dots,w_{\ell})$ are bounded by $M$ .

Assume $p,q>0$ . Then for any $z_{2}\geq z_{1}$ we have $\mathcal{R}_{z_{1}}+(z_{2}-z_{1})\frac{q}{p}\ \subseteq\ \mathcal{R}_{z_{2}}.$ Moreover, if $z_{1}\geq M$ , then $\mathcal{R}_{z_{1}}+(z_{2}-z_{1})\frac{q}{p}\ =\ \mathcal{R}_{z_{2}}.$ Hence, it suffices to check the height at $z=M$ .

If $p,q<0$ , a symmetric argument shows that it suffices to check the height at $z=-M$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 26.

The algorithm in Theorem 20 can be used as a semi-algorithm without assuming that the Reachability Conjecture holds: one can repeat the case distinction from Lemmas 21, 23, 24, and 25. However, the procedure fails to return an answer in Case 3 of Lemma 23 and Case 2 of Lemma 24.

6 Proofs

6.1 Cycles

First, we state an auxiliary lemma.

Lemma 27.

Let $a,\alpha,b$ be integers. If $sign(a-\alpha)=sign(b-\alpha)\neq 0$ , then

(\frac{ba-\alpha^{2}}{a+b-2\alpha},\frac{ba-\alpha^{2}}{a+b-2\alpha})\in% \operatorname{conv}\Bigl((a,\alpha),(\alpha,b)\Bigr).

Proof.

Define $x=\frac{b-\alpha}{a+b-2\alpha}$ . Note that $0<x<1$ because $sign(a-\alpha)=sign(b-\alpha)\neq 0$ .

Hence we obtain

x(a,\alpha)+(1-x)(\alpha,b)\in\operatorname{conv}\Bigl((a,\alpha),(\alpha,b)% \Bigr).

Let us rewrite the expression.

	$\displaystyle x(a,\alpha)+(1-x)(\alpha,b)$	$\displaystyle=(\frac{(b-\alpha)a+(a-\alpha)\alpha}{b+a-2\alpha},\frac{(b-% \alpha)\alpha+(a-\alpha)b}{b+a-2\alpha})$
		$\displaystyle=(\frac{ba-\alpha^{2}}{b+a-2\alpha},\frac{ba-\alpha^{2}}{b+a-2% \alpha}).$

$\hfill\blacktriangleleft$

Proof of Theorem 14.

Suppose $\mathcal{R}$ has a cycle $C=\{s_{1},\dots,s_{m}\}$ , where all $s_{i}$ are different states (otherwise we can take a smaller cycle) and $m>2$ . Then for every $1\leq i<m$ : $(s_{i},s_{i+1})\in\mathcal{R}$ and $(s_{m},s_{1})\in\mathcal{R}$ , so

(\frac{\sum_{i=1}^{m}s_{i}}{m},\frac{\sum_{i=1}^{m}s_{i}}{m})\in\mathcal{R}.

Denote $z:=\frac{\sum_{i=1}^{m}s_{i}}{m}$ . Consider the translated relation $\mathcal{R}^{\prime}:=\{(x-\lfloor z\rfloor,y-\lfloor z\rfloor)\mid(x,y)\in% \mathcal{R}\}$ and translated states $s_{i}^{\prime}:=s_{i}-\lfloor z\rfloor$ . Then $\mathcal{R}^{\prime}$ has a cycle $(s_{1}^{\prime},\dots,s_{m}^{\prime})$ , and the corresponding average satisfies $0\leq z-\lfloor z\rfloor<1$ . Thus, without loss of generality, we may assume $0\leq z<1$ . If $z=0$ , then there is a cycle of length $1$ . Suppose this is not the case.

Let $\alpha$ denote the state of $C$ with the largest absolute value, and let $a$ and $b$ be the neighboring states of $\alpha$ in $C$ . Hence, $(a,\alpha)$ and $(\alpha,b)$ are in $\mathcal{R}$ . Since $|a|,|b|\leq|\alpha|$ and all $s_{i}$ are different, we have $sign(a-\alpha)=sign(b-\alpha)\neq 0$ . Now we can apply Lemma 27 and obtain

(\frac{ba-\alpha^{2}}{a+b-2\alpha},\frac{ba-\alpha^{2}}{a+b-2\alpha})\in% \operatorname{conv}\Bigl((a,\alpha),(\alpha,b)\Bigr)\subseteq\mathcal{R}.

Denote $\beta:=\frac{ba-\alpha^{2}}{a+b-2\alpha}$ and consider the following cases.

Case 1: $\beta\leq 0$ or $1\leq\beta$ .

In this case, since $0\leq z<1$ , either $(0,0)$ or $(1,1)$ can be expressed as a convex combination of $(z,z)$ and $(\beta,\beta)$ , yielding a cycle of length one.

Case 2: $\alpha\leq 0$ .

Note that $\alpha\leq a,b\leq-\alpha$ and $a, b$ and $\alpha$ are distinct. Thus, $a+b-2\alpha>0$ , and $ba-\alpha^{2}<0$ , which implies $\beta<0$ . Hence, the statement follows from Case 1.

Case 3: $0<\alpha$ and $0<\beta<1$ .

Since $2\alpha>a+b$ , rewriting $\beta<1$ , we obtain

a+b-2\alpha<ab-\alpha^{2},

\alpha^{2}-2\alpha<ab-a-b,

(\alpha-1)^{2}<(a-1)(b-1).

If, for some $i$ , $s_{i}=-\alpha$ , then we can take $-\alpha$ instead of $\alpha$ and the statement follows from Case 2. Thus, we can assume that for every $i$ we have $-\alpha<s_{i}$ . Therefore,

|a|,|b|<\alpha,

-\alpha<a,b<\alpha,

-\alpha-1<a-1,b-1<\alpha-1.

Hence inequality $(\alpha-1)^{2}<(a-1)(b-1)$ can be satisfied only if $a=-\alpha+1$ and $b=-\alpha+2$ or $a=-\alpha+2$ and $b=-\alpha+1$ . Without loss of generality, assume the first case.

Then $a$ is the smallest value in $C$ . Let $c$ denote the predecessor of $a$ in $C$ .

All states in $C$ are different, and the length of $C$ is at least $3$ , hence $-\alpha+2\leq c<\alpha$ . Since $sign(\alpha-a)=sign(c-a)=1$ , then we can apply Lemma 27 to get

(\frac{\alpha c-a^{2}}{c+\alpha-2a},\frac{\alpha c-a^{2}}{c+\alpha-2a})\in% \operatorname{conv}\Bigl((a,\alpha),(c,a)\Bigr)\subseteq\mathcal{R},

(\frac{\alpha c-(\alpha-1)^{2}}{c+3\alpha-2},\frac{\alpha c-(\alpha-1)^{2}}{c+% 3\alpha-2})\in\mathcal{R}.

If $c<\alpha-1$ , then $\frac{\alpha c-(\alpha-1)^{2}}{c+3\alpha-2}\leq 0$ , hence $(0,0)\in\operatorname{conv}\Bigl((\frac{\alpha c-(\alpha-1)^{2}}{c+3\alpha-2},% \frac{\alpha c-(\alpha-1)^{2}}{c+3\alpha-2}),(z,z)\Bigr)\subseteq\mathcal{R}$ .

It remains to prove the statement for $c=\alpha-1$ . Since $(\alpha-1,1-\alpha)$ and $(\alpha,2-\alpha)$ are in $\mathcal{R}$ we get that

(\alpha-\frac{1}{2},\frac{3}{2}-\alpha)\in\mathcal{R}

It is easy to see that points $(1,0)$ and $(0,1)$ lie on the interval

[(\alpha-\frac{1}{2},\frac{3}{2}-\alpha);(1-\alpha,\alpha)]\subseteq\mathcal{R},

because $(\alpha-\frac{1}{2},\frac{3}{2}-\alpha)=(\frac{1}{2},\frac{1}{2})+(\alpha-1,1-\alpha)$ and $(1-\alpha,\alpha)=(\frac{1}{2},\frac{1}{2})+(\frac{1}{2}-\alpha,\alpha-\frac{1% }{2})$ . Hence, $\mathcal{R}$ has a cycle of length 2. $\hfill\blacktriangleleft$

6.2 Generalized Collatz Sequences

Proof of Proposition 17.

Assume the contrary, there exist $T$ , $n$ and $i$ such that $T^{k}(n)\equiv i\text{ (mod }d)$ for every $k\geq 0$ . Hence,

T^{k+1}(n)=\frac{m_{i}T^{k}(n)-r_{i}}{d}.

We prove by induction on $k$ , that for every $k\geq 1$

T^{k}(n)=\frac{nm_{i}^{k}-r_{i}\sum_{j=0}^{k-1}m_{i}^{j}d^{k-1-j}}{d^{k}}.

For $k=1$ we get $T(n)=\frac{nm_{i}-r_{i}}{d}$ . Assuming the formula for $k$ let us prove it for $k+1$ ,

	$\displaystyle T^{k+1}(n)$	$\displaystyle=\frac{m_{i}T^{k}(n)-r_{i}}{d}=\frac{m_{i}(nm_{i}^{k}-r_{i}\sum_{% j=0}^{k-1}m_{i}^{j}d^{k-1-j})-r_{i}d^{k}}{d^{k+1}}$
		$\displaystyle=\frac{nm_{i}^{k+1}-r_{i}\sum_{j=0}^{k}m_{i}^{j}d^{k-j}}{d^{k+1}}.$

Hence, for every $k\geq 1$ ,

nm_{i}^{k}-r_{i}\sum_{j=0}^{k-1}m_{i}^{j}d^{k-1-j}\equiv 0\text{ (mod }d^{k}).

Multiplying it by $m_{i}-d$ yields

(m_{i}-d)(nm_{i}^{k}-r_{i}\sum_{j=0}^{k-1}m_{i}^{j}d^{k-1-j})=nm_{i}^{k+1}-ndm% _{i}^{k}-r_{i}(m_{i}^{k}-d^{k})\equiv 0\text{ (mod }d^{k}).

Since $d^{k}\equiv 0\text{ (mod }d^{k})$ and $\gcd(m_{i},d)=1$ , we obtain for every $k$ that

nm_{i}-nd-r_{i}\equiv 0\text{ (mod }d^{k}).

As this holds for all $k$ and $d>1$ , it follows that $nm_{i}-nd-r_{i}=0$ . Thus $n=\frac{nm_{i}-r_{i}}{d}$ . Therefore $T^{k}(n)=n$ for all $k$ , contradicting unboundedness. $\hfill\blacktriangleleft$

Proof of Proposition 18.

Recall that $T$ has the form

T(x)=\frac{mx-(a+i)}{d},\ \ \ \ \text{if }mx\equiv a+i\ (\text{mod }d)

Define

\mathcal{R}^{+}:=\{(x,x^{\prime})\in\mathbb{R}^{2}\mid mx-a-d+1\leq dx^{\prime% }\leq mx-a-1\text{ and }0<x<x^{\prime}\}

Note that,

\mathcal{R}^{+}_{\mathbb{Z}}=\{(n,T(n))\in\mathbb{Z}^{2}\mid 0<n<T(n)\text{ % and }mn\not\equiv a\ (\text{mod }d)\}.

Therefore every infinite trace of $\mathcal{R}^{+}$ is self-avoiding and corresponds to the unbounded sequence $\{mT^{k}(n)\}_{k\in\mathbb{N}}$ with $mT^{k}(n)\not\equiv a\ (\text{mod }d)$ , and $T^{k}(n)>0$ , for every $k\geq 0$ .

For the other direction, if there exists an infinite unbounded sequence $\{T^{k}(n)\}_{k\in\mathbb{N}}$ of positive values, then, since $m>d$ , from some step it takes values large enough to have $T^{k}(n)<T^{k+1}(n)$ . It implies the existence of a self-avoiding trace of $\mathcal{R}^{+}$ .

The proof for

\mathcal{R}^{-}:=\{(x,x^{\prime})\in\mathbb{R}^{2}\mid mx-a-d+1\leq dx^{\prime% }\leq mx-a-1\text{ and }0>x>x^{\prime}\}

is symmetric. $\hfill\blacktriangleleft$

6.3 Self-avoiding Traces

Let us formulate an auxiliary notation and an auxiliary lemma.

C_{+}=\{(x_{1},x_{2})\in\mathbb{R}^{2}\mid x_{1}\geq 0\geq x_{2}\}\ \ \ \ \ \ % \ \ \ \ C_{-}=\{(x_{1},x_{2})\in\mathbb{R}^{2}\mid x_{2}\geq 0\geq x_{1}\}

Lemma 28.

Let $v_{1},v_{2},w,u\in\mathbb{R}^{2}$ be nonzero vectors with $v_{1}\nparallel v_{2}$ , $w\in C_{+}$ , $u\in C_{-}$ and $w,u\in\operatorname{nonneg}(v_{1},v_{2})$ . Then $\operatorname{nonneg}(v_{1},v_{2})\cap\Delta\neq\emptyset$ and $\operatorname{nonneg}(v_{1},v_{2})\cap I\neq\emptyset$ .

Proof.

If $w\parallel u$ , then $nonneg(w,u)$ is a line contained in the closed cone $nonneg(v_{1},v_{2})$ , contradicting Proposition 4, since $v_{1}\nparallel v_{2}$ . Thus $w\nparallel u$ .

Let us prove that there exists $\alpha\in\mathbb{R}_{+}$ , such that $\alpha w+(1-\alpha)u\in\operatorname{cl}(\Delta)$ . Denote $w=(w_{1},w_{2})$ and $u=(u_{1},u_{2})$ . Define $\alpha:=\frac{u_{2}-u_{1}}{w_{1}-w_{2}+u_{2}-u_{1}}$ . Since $w\in C_{+}$ and $u\in C_{-}$ , we obtain $w_{1}-w_{2}\geq 0$ , $u_{2}-u_{1}\geq 0$ and since $w\nparallel u$ they cannot be both equal to $0$ . Hence denominator of $\alpha$ is nonzero and $\alpha\geq 0$ . A direct computation gives

	$\displaystyle\alpha w+(1-\alpha)u$	$\displaystyle=w\frac{u_{2}-u_{1}}{w_{1}-w_{2}+u_{2}-u_{1}}+u\frac{w_{1}-w_{2}}% {w_{1}-w_{2}+u_{2}-u_{1}}$
		$\displaystyle=(\frac{w_{1}(u_{2}-u_{1})+u_{1}(w_{1}-w_{2})}{w_{1}-w_{2}+u_{2}-% u_{1}},\frac{w_{2}(u_{2}-u_{1})+u_{2}(w_{1}-w_{2})}{w_{1}-w_{2}+u_{2}-u_{1}})$
		$\displaystyle=(\frac{w_{1}u_{2}-u_{1}w_{2}}{w_{1}-w_{2}+u_{2}-u_{1}},\frac{w_{% 1}u_{2}-u_{1}w_{2}}{w_{1}-w_{2}+u_{2}-u_{1}})\in\operatorname{cl}(\Delta).$

Since $w\nparallel u$ we have $\alpha w+(1-\alpha)u\neq(0,0)$ , thus $\alpha w+(1-\alpha)u\in\Delta$ . Recall that $u,w\in nonneg(v_{1},v_{2})$ , hence $\alpha w+(1-\alpha)u\in\Delta$ .

Since $\alpha w+(1-\alpha)u\nparallel v_{1}$ , and $\alpha w+(1-\alpha)u\nparallel v_{2}$ , we get that $\alpha w+(1-\alpha)u$ is in the interior of $\operatorname{nonneg}(v_{1},v_{2})$ , thus, some open neighborhood of $\alpha w+(1-\alpha)u$ is contained in $\operatorname{nonneg}(v_{1},v_{2})$ , but any such neighborhood intersects $I$ , since $\Delta\subseteq\operatorname{cl}(I)$ . Hence, the statement follows. $\hfill\blacktriangleleft$

Proof of Lemma 21.

1.

Without loss of generality assume $\operatorname{nonneg}(v_{1},v_{2})\cap I_{+}\neq\emptyset$ . The case when $\operatorname{nonneg}(v_{1},v_{2})\cap I_{-}\neq\emptyset$ follows from the considered one applied to $-\mathcal{R}$ .

The set $\operatorname{nonneg}(v_{1},v_{2})\cap I_{+}$ is a (possibly nonclosed) convex cone as the intersection of two convex cones. Let us prove that it contains at least two noncollinear vectors. Indeed, for the contradiction, suppose there exists a vector $v$ , such that every vector in $\operatorname{nonneg}(v_{1},v_{2})\cap I_{+}$ is collinear to $v$ . Thus, $\operatorname{nonneg}(v_{1},v_{2})\cap I_{+}\subseteq\operatorname{nonneg}(v)$ .

Informally, $\operatorname{nonneg}(v_{1},v_{2})$ contains “half of a neighborhood of $v$ ”. Formally, for angles $-\pi<\epsilon_{1}<\epsilon_{2}<\pi$ , let $rot_{v}(\epsilon_{1},\epsilon_{2})$ be the set of vectors $v_{\mathrm{rot}}\in\mathbb{R}^{2}$ such that there exists an angle $\theta$ with $\epsilon_{1}<\theta<\epsilon_{2}$ and $v_{\mathrm{rot}}$ is the image of $v$ under rotation by $\theta$ around the origin. Equivalently, $rot_{v}(\epsilon_{1},\epsilon_{2})=\{R_{\theta}v\mid\epsilon_{1}<\theta<% \epsilon_{2}\}$ , where $R_{\theta}$ is the rotation matrix.

Since $v\in\operatorname{nonneg}(v_{1},v_{2})$ and $v_{1}\nparallel v_{2}$ , there exists $\epsilon\in(0,\pi)$ such that either $rot_{v}(0,\epsilon)\subseteq\operatorname{nonneg}(v_{1},v_{2})$ or $rot_{v}(-\epsilon,0)\subseteq\operatorname{nonneg}(v_{1},v_{2})$ .

Moreover, since $I_{+}$ is open and $v\in I_{+}$ , we can choose $\epsilon>0$ small enough such that $rot_{v}(-\epsilon,\epsilon)\subseteq I_{+}$ . Consequently, one of the sets $rot_{v}(0,\epsilon)$ or $rot_{v}(-\epsilon,0)$ is contained in $\operatorname{nonneg}(v_{1},v_{2})\cap I_{+}$ , contradicting the assumption that $\operatorname{nonneg}(v_{1},v_{2})\cap I_{+}\subseteq\operatorname{nonneg}(v)$ .

Hence, there are two non-collinear vectors $w,u\in\operatorname{nonneg}(v_{1},v_{2})\cap I_{+}$ . Then

$|(\operatorname{nonneg}(v_{1},v_{2})\cap I_{+})_{n}\cap\mathbb{Z}|\geq|% \operatorname{nonneg}(w,u)_{n}\cap\mathbb{Z}|\geq n|\frac{w}{|w|}-\frac{u}{|u|% }|\xrightarrow[n\rightarrow\infty]{}\infty.$

Hence, for sufficiently large $n$ , there always exists a transition from $n$ to a larger value, thus the loop has a self-avoiding trace.
2.

Suppose there is a self-avoiding trace $\{s_{i}\}_{i\in\mathbb{N}}$ . If there are infinitely many negative and infinitely many positive states, then infinitely many indices $i$ satisfy $s_{i}<0<s_{i+1}$ and infinitely many satisfy $s_{i}>0>s_{i+1}$ . Thus, sets $\mathcal{R}\cap C_{+}$ and $\mathcal{R}\cap C_{-}$ are unbounded. In that case, their recession cones are non-empty, thus, by Proposition 5, there are non-zero vectors $w\in\operatorname{rec}(\mathcal{R})\cap C_{+}$ and $u\in\operatorname{rec}(\mathcal{R})\cap C_{-}$ . Hence, by Lemma 28, $\operatorname{rec}(\mathcal{R})\cap\Delta\neq\emptyset$ . Contradiction.

Suppose instead there are only finitely many negative $s_{i}$ . The case when there are only finitely many positive $s_{i}$ follows from the considered one for $-\mathcal{R}$ .

Then there are infinitely many $i$ such that $s_{i+1}>s_{i}>0$ . By Theorem 3, $\mathcal{R}=\operatorname{conv}(w_{1},\dots,w_{l})+\operatorname{rec}(\mathcal% {R})$ . Hence, for every $i$ , there are $w^{i}\in\operatorname{conv}(w_{1},\dots,w_{l})$ and $v^{i}\in\operatorname{rec}(\mathcal{R})$ , such that $(s_{i},s_{i+1})=w^{i}+v^{i}$ . Consider the normalized vectors $\frac{v^{i}}{\lVert v^{i}\rVert}$ along the infinite subsequence with $s_{i+1}>s_{i}>0$ . Since it is an infinite sequence on a compact sphere, it must have a converging subsequence $\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}$ . Since for every $j$ holds $\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}\in\operatorname{rec}(\mathcal{R})$ this sequence must converge to $v\in\operatorname{rec}(\mathcal{R})$ and $\lVert v\rVert=1$ . Let us prove that $v\in\operatorname{cl}(I_{+})$ .

Assume that $v\notin\operatorname{cl}(I_{+})$ . Since $\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}$ converges to $v$ , for every $\epsilon$ there exists $N$ , such that for every $j>N$ , $\lVert\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}-v\rVert\leq\epsilon$ . Let us take $\epsilon<\operatorname{dist}(v,\operatorname{cl}(I_{+}))$ . Thus, $\operatorname{nonneg}(v^{\prime}\in\mathbb{R}^{2}\mid\lVert v-v^{\prime}\rVert% \leq\epsilon)\cap\operatorname{cl}(I_{+})=\emptyset$ , hence by Proposition 5 $\operatorname{rec}(\operatorname{nonneg}(v^{\prime}\in\mathbb{R}^{2}\mid\lVert v% -v^{\prime}\rVert\leq\epsilon))\cap\operatorname{rec}(\operatorname{conv}(-w_{% 1},\dots,-w_{l})+I_{+})=\emptyset$ , which implies that $\operatorname{nonneg}(v^{\prime}\in\mathbb{R}^{2}\mid\lVert v-v^{\prime}\rVert% \leq\epsilon)\cap(\operatorname{conv}(-w_{1},\dots,-w_{l})+I_{+})$ is bounded by Theorem 3. For every $j>N$ , $(s_{i_{j}},s_{i_{j}+1})-w^{i_{j}}=v^{i_{j}}\in\operatorname{nonneg}(v^{\prime}% \in\mathbb{R}^{2}\mid\lVert v-v^{\prime}\rVert\leq\epsilon)$ , but $(s_{i_{j}},s_{i_{j}+1})\in I_{+}$ , hence $v^{i_{j}}\in\operatorname{conv}(-w_{1},\dots,-w_{l})+I_{+}$ . Since the sequence $s_{i_{j}}$ is unbounded and the set $\operatorname{conv}(w_{1},\dots,w_{l})$ is bounded, the sequence $v^{i_{j}}$ is also unbounded, but it is contained in a bounded set. Thus $v\in\operatorname{cl}(I_{+})$ by contradiction.

Since $v\in\operatorname{cl}(I_{+})\cap\operatorname{rec}(\mathcal{R})$ and $\operatorname{rec}(\mathcal{R})\cap(I_{+}\cup\Delta_{+})=\emptyset$ we obtain $v\in\{(0,x_{2})\in\mathbb{R}^{2}\mid x_{2}>0\}$ , hence $v=(0,1)$ . There exists $N$ , such that for every $j>N$ holds $|\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}-(0,1)|<0.1$ , hence $\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}\in\{(x_{1},x_{2})\mid x_{1}\leq 0\}$ , because otherwise $\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}\in I_{+}$ , which is impossible, since $\frac{v^{i_{j}}}{\lVert v^{i_{j}}\rVert}\in\operatorname{rec}(\mathcal{R})$ . Since the set $\operatorname{conv}(w_{1},\dots,w_{l})$ is bounded, the supremum $\sup\{x_{1}\in\mathbb{R}\mid\exists x_{2}\in\mathbb{R}:(x_{1},x_{2})\in% \operatorname{conv}(w_{1},\dots,w_{l})\}$ is finite, denote it as $K$ . Since $s_{i_{j}}=w^{i_{j}}+v^{i_{j}}$ from the proven above, for every $j>N$ , $0<s_{i_{j}}<K$ . That contradicts the distinctness of $s_{i}$ and the assumption that there are only finitely many negative $s_{i}$ .
3.

If $\operatorname{rec}(\mathcal{R})\cap\Delta_{+}\neq\emptyset$ , then $\Delta_{+}\subseteq\operatorname{rec}(\mathcal{R})$ . If $(a,b)\in\mathcal{R}_{\mathbb{Z}}\cap I_{+}$ , then $(a,b)+\Delta_{+}\subseteq\mathcal{R}$ , hence for any $n\geq a$ it is always possible to make a transition to $n-a+b$ . Thus, the loop has a self-avoiding trace.
4.

Suppose there is a self-avoiding trace $\{s_{i}\}_{i\in\mathbb{N}}$ . If there are infinitely many negative and infinitely many positive states, then infinitely many indices $i$ satisfy $s_{i}<0<s_{i+1}$ and infinitely many satisfy $s_{i}>0>s_{i+1}$ . Thus, sets $\mathcal{R}\cap C_{+}$ and $\mathcal{R}\cap C_{-}$ are unbounded. In that case, their recession cones are non-empty, thus, by Proposition 5, there are non-zero vectors $w\in\operatorname{rec}(\mathcal{R})\cap C_{+}$ and $u\in\operatorname{rec}(\mathcal{R})\cap C_{-}$ . Hence, by Lemma 28, $\operatorname{rec}(\mathcal{R})\cap I\neq\emptyset$ . Contradiction.

There cannot be only finitely many negative $s_{i}$ , due to the argument identical to the argument in statement 2 of this lemma.

If it contains only finitely many positive terms, then there is some index with $0>s_{i}>s_{i+1}$ , contradicting $\mathcal{R}_{\mathbb{Z}}\cap I_{-}=\emptyset$ .
5.

This statement follows from the statement 3 applied to $-\mathcal{R}$ .
6.

This statement follows from the statement 4 applied to $-\mathcal{R}$ .

$\hfill\blacktriangleleft$

Proof of Lemma 23.

1.

Assume $0<p<q$ . The case when $q<p<0$ follows from the considered one applied to $-\mathcal{R}$ .

If $0pt_{|p|}(\mathcal{R})\geq p$ , then there exists $z\in\mathbb{Z}$ , such that

$|\mathcal{R}_{z}\cap(\frac{1}{p}\mathbb{Z})|\geq p.$

For any $z^{\prime}\geq z$ , using $(p,q)\in\operatorname{rec}(\mathcal{R})$ we can shift by $(z^{\prime}-z)/p$ along $(p,q)$ , which maps $x_{1}=z$ to $x_{1}=z^{\prime}$ and adds $\frac{q}{p}(z^{\prime}-z)$ to the second coordinate. Hence

$|\mathcal{R}_{z^{\prime}}\cap(\frac{1}{p}\mathbb{Z})|\geq|\mathcal{R}_{z}\cap(% \frac{1}{p}\mathbb{Z})+\frac{q}{p}(z^{\prime}-z)|=|\mathcal{R}_{z}\cap(\frac{1% }{p}\mathbb{Z})|\geq p.$

Since $|\mathcal{R}_{z^{\prime}}|$ is convex $|\mathcal{R}_{z^{\prime}}\cap(\frac{1}{p}\mathbb{Z})|\geq p$ implies that $\mathcal{R}_{z^{\prime}}$ contains at least $p$ consecutive points from $\frac{1}{p}\mathbb{Z}$ , hence at least one of them is an integer. Thus $|\mathcal{R}_{z^{\prime}}\cap\mathbb{Z}|\geq 1$ .

Since $0<p<q$ there exists $N\in\mathbb{N}$ , such that for every $z^{\prime}\geq N$ , $\mathcal{R}_{z^{\prime}}\subseteq I_{+}$ . Hence, $\mathcal{R}_{z^{\prime}}\cap\mathbb{Z}\subseteq[z^{\prime}+1;\infty)$ . Thus, for every $z^{\prime}>\max(N,z)$ , it is possible to make a transition to a larger value. Hence, the loop has a self-avoiding trace.
2.

Assume $p<0<q$ . The case when $q<0<p$ follows from the considered one applied to $-\mathcal{R}$ . In that case,

$\operatorname{rec}(\mathcal{R})\subseteq\mathbb{R}_{-}\times\mathbb{R}_{+}\cup% \{(0,0)\}.$

By Proposition 5 the set $\mathcal{R}\cap(\mathbb{R}^{2}\setminus(\mathbb{R}_{-}\times\mathbb{R}_{+}))$ is bounded. Therefore, any self-avoiding trace would eventually have to make transitions only from $\mathbb{R}_{-}$ to $\mathbb{R}_{+}$ , which is impossible. Hence, no self-avoiding trace exists.
3.

Assume $0<p,q$ . The case when $p,q<0$ follows from the considered one applied to $-\mathcal{R}$ . The case when $\operatorname{sign}(p)\neq\operatorname{sign}(q)$ follows from the statement 2 of this Lemma.

Denote $h=0pt_{|p|}(\mathcal{R})$ . There exists $z\in\mathbb{Z}$ , such that $|\mathcal{R}_{z}\cap(\frac{1}{p}\mathbb{Z})|=h.$ Since $\mathcal{R}$ is convex the points of $\mathcal{R}_{z}\cap(\frac{1}{p}\mathbb{Z})$ are of the form $\{\frac{qz-a-i}{p}\}_{1\leq i\leq h}$ for some $a\in\mathbb{Z}$ .

Let us prove that for all $z^{\prime}\in\mathbb{Z}$ ,

$\mathcal{R}_{z^{\prime}}\cap(\frac{1}{p}\mathbb{Z})\subseteq\mathcal{R}_{z}% \cap(\frac{1}{p}\mathbb{Z})+\frac{q}{p}(z^{\prime}-z).$ (3)

For $z^{\prime}>z$ since $(p,q)\in\operatorname{rec}(\mathcal{R})$ and $z^{\prime}-z>0$ the following holds

$\mathcal{R}_{z}\cap(\frac{1}{p}\mathbb{Z})+\frac{q}{p}(z^{\prime}-z)\subseteq% \mathcal{R}_{z^{\prime}}\cap(\frac{1}{p}\mathbb{Z}),$

but since $|\mathcal{R}_{z^{\prime}}\cap(\frac{1}{p}\mathbb{Z})|\leq h$ we get (3).

Suppose that $z^{\prime}<z$ , then for any $r\in\mathcal{R}_{z^{\prime}}\cap(\frac{1}{p}\mathbb{Z})$ , since $(p,q)\in\operatorname{rec}(\mathcal{R})$ and $z-z^{\prime}>0$ , we obtain $r+\frac{q}{p}(z-z^{\prime})\in\mathcal{R}_{z}\cap(\frac{1}{p}\mathbb{Z})$ . Thus, we get (3).

Hence $\mathcal{R}_{\mathbb{Z}}\subseteq\{(x,y)\in\mathbb{Z}^{2}\mid y=\frac{qx-a-i}{% p},\ 1\leq i\leq h\}.$

Non-existence of a self-avoiding trace follows from Conjecture 16, since $h<p$ .
4.

The proof is analogous to the proof of the statement 3, but at the end, instead of Conjecture 16, Proposition 17 needs to be applied.
5.

In that case $\mathcal{R}\cap\mathbb{Z}^{2}=\emptyset$ , so the claim is immediate.
6.

If $|p|>|q|$ , then

$\operatorname{rec}(\mathcal{R})\subseteq\{(x_{1},x_{2})\in\mathbb{R}^{2}\mid|x% _{1}|>|x_{2}|\text{ or }x_{1}=x_{2}=0\}.$

Hence, the set $\mathcal{R}\cap\{(x,y)\in\mathbb{R}^{2}\mid|x|\leq|y|\}$ is bounded. Assume there is a self-avoiding trace $\{s_{i}\}_{i\in\mathbb{N}}$ . Then there are infinitely many $i$ , such that $|s_{i}|<|s_{i+1}|$ . Contradiction.

If $p=q>0$ , then $\operatorname{rec}(\mathcal{R})=\Delta_{+}$ . If $p=q<0$ , then $\operatorname{rec}(\mathcal{R})=\Delta_{-}$ . Hence, the proofs of statements 6,7,8 and 9 are analogous to the proofs of statement 3, 4, 5 and 6 of Lemma 21 . $\hfill\blacktriangleleft$

Proof of Lemma 24.

The proofs of 1, 2, 3, 4, 5, 6, and 7 are analogous to the proofs of Lemma 23, items 1, 3, 4, 5, 6, 7, and 8, respectively.

Assume $-p=q$ . Since $\gcd(p,q)=1$ we have $p=1$ , $q=-1$ .

Denote $h=0pt_{1}(\mathcal{R})$ . Take $z\in\mathbb{Z}$ , such that $|\mathcal{R}_{z}\cap\mathbb{Z}|=h$ . For every $z^{\prime}\in\mathbb{Z}$ ,

\mathcal{R}_{z}\cap\mathbb{Z}+(z^{\prime}-z)\subseteq\mathcal{R}_{z^{\prime}}% \cap\mathbb{Z},

and since $|\mathcal{R}_{z^{\prime}}\cap\mathbb{Z}|\leq h$ , equality holds

\mathcal{R}_{z}\cap\mathbb{Z}+(z^{\prime}-z)=\mathcal{R}_{z^{\prime}}\cap% \mathbb{Z}.

Denote $\mathcal{R}_{0}\cap\mathbb{Z}=[a;b]$ , then $h=b-a+1$ . Thus $\mathcal{R}_{\mathbb{Z}}=\{(x,y)\in\mathbb{Z}\mid a\leq y+x\leq b\}$ . If $h=1$ , then for every trace $s_{1},s_{2},s_{3}$ we have $s_{1}+s_{2}=s_{2}+s_{3}=a$ , hence $s_{1}=s_{3}$ , the loop does not have a self-avoiding trace, thus statement 9 is proved.

If $h\geq 2$ , then let us define a trace $\{s_{i}\}_{i\in\mathbb{N}}$ by

s_{1}=2|a|,\qquad s_{i+1}=\begin{cases}a-s_{i},&\text{if }i\text{ is odd},\\[6% .0pt] b-s_{i},&\text{if }i\text{ is even}.\end{cases}

For every odd $i$ we get $s_{i+2}=b-a+s_{i}>s_{i}$ and $s_{i+1}=a-s_{i}<a-s_{1}<a-2|a|<0$ , hence this trace is self-avoiding. Thus, statement 8 is proved.

The statement 10 follows from the fact, that if $p=0$ , then the set $\{x\in\mathbb{Z}\mid\exists y\in\mathbb{Z}.\ (x,y)\in\mathcal{R}\}$ is bounded, thus an infinite trace can visit only the finite number of different states. $\hfill\blacktriangleleft$

Proof of Lemma 25.

1.

If $\operatorname{rec}(\mathcal{R})=\operatorname{nonneg}(v_{1},v_{2},v_{3})$ and this cone cannot be generated by two vectors, then by Proposition 4 it is either a whole plane or a (closed) affine half-plane. In the former case, $\mathcal{R}=\mathbb{R}^{2}$ . For the latter case, note that any closed affine half-plane must intersect $I$ , hence the argument of Lemma 21.1 applies and yields a self-avoiding trace.
2.

If $\operatorname{rec}(\mathcal{R})=\{0\}$ , then $\mathcal{R}$ is bounded, hence any infinite trace can visit only a finite number of states and thus cannot be self-avoiding.

$\hfill\blacktriangleleft$

7 Conclusion

In this paper, we have studied the termination problem for SLCs over $\mathbb{Z}$ . We have observed that a loop has an infinite computation iff it admits either a cycle or a self-avoiding trace.

We first analyzed cyclic traces. For one-variable SLCs, we have proved that the existence of a cycle implies the existence of a cycle of length at most two. An open question is whether, for $n>1$ , there exists a bound $K(n)$ such that any $n$ -variable loop that has a cycle also has one of length at most $K(n)$ .

Next, we have formulated the Reachability Conjecture for weak Collatz sequences – a special case of a long-standing conjecture – and proved it for modulus $d=2$ . We have shown that a decision procedure for one-variable SLC termination would verify the Reachability Conjecture for specific mappings; for most mappings (in particular, all cases with $d>2$ ), the conjecture remains open.

Finally, assuming the Reachability Conjecture, we have established that termination of one-variable SLCs is decidable in polynomial time.

References

[1] Amir M. Ben-Amram. Mortality of Iterated Piecewise Affine Functions over the Integers: Decidability and Complexity. In Natacha Portier and Thomas Wilke, editors, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013), volume 20 of Leibniz International Proceedings in Informatics (LIPIcs), pages 514–525, Dagstuhl, Germany, 2013. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.STACS.2013.514.
[2] Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. ACM Trans. Program. Lang. Syst., 34(4), 2012. doi:10.1145/2400676.2400679.
[3] Amir M. Ben-Amram, Samir Genaim, Joël Ouaknine, and James Worrell. Termination analysis of linear-constraint programs, 2025. doi:10.48550/arXiv.2509.06752.
[4] Mark de Berg, Otfried Cheong, Marc van Kreveld, and Mark Overmars. Computational Geometry: Algorithms and Applications. Springer-Verlag TELOS, Santa Clara, CA, USA, 3rd ed. edition, 2008.
[5] Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. Solving existentially quantified horn clauses. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 869–882, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. doi:10.1007/978-3-642-39799-8_61.
[6] Vincent D. Blondel, Olivier Bournez, Pascal Koiran, Christos H. Papadimitriou, and John N. Tsitsiklis. Deciding stability and mortality of piecewise affine dynamical systems. Theor. Comput. Sci., 255(1–2):687–696, March 2001. doi:10.1016/S0304-3975(00)00399-6.
[7] Mark Braverman. Termination of integer linear programs. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, pages 372–385, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. doi:10.1007/11817963_34.
[8] Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator: beyond safety. In Proceedings of the 18th International Conference on Computer Aided Verification, CAV’06, pages 415–418, Berlin, Heidelberg, 2006. Springer-Verlag. doi:10.1007/11817963_37.
[9] Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell. The 2-Dimensional Constraint Loop Problem Is Decidable. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024), volume 297 of Leibniz International Proceedings in Informatics (LIPIcs), pages 140:1–140:21, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2024.140.
[10] Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. Linear ranking for linear lasso programs. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis, pages 365–380, Cham, 2013. Springer International Publishing. doi:10.1007/978-3-319-02444-8_26.
[11] Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of Linear Loops over the Integers. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 118:1–118:13, Dagstuhl, Germany, 2019. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2019.118.
[12] Jeffrey C. Lagarias. The 3x+1 problem: An overview, 2021. arXiv:2111.02635.
[13] George M. Leigh. A markov process underlying the generalized syracuse algorithm. Acta Arithmetica, 46:125–143, 1986. URL: https://api.semanticscholar.org/CorpusID:117635633.
[14] Hendrik W. Lenstra. Integer programming with a fixed number of variables. Math. Oper. Res., 8:538–548, 1983. doi:10.1287/MOOR.8.4.538.
[15] Keith R. Matthews. Some borel measures associated with the generalized collatz mapping. Colloquium Mathematicum, 63:191–202, 1992. URL: https://api.semanticscholar.org/CorpusID:54607478.
[16] Keith R Matthews. Generalized 3x+ 1 mappings: markov chains and ergodic theory. The ultimate challenge: The 3x, 1:79–103, 2010.
[17] Keith R. Matthews and A. M. Watts. A markov approach to the generalized syracuse algorithm. Acta Arithmetica, 45:29–42, 1985. URL: https://api.semanticscholar.org/CorpusID:118600406.
[18] Watts A. Matthews K. A generalization of hasse’s generalization of the syracuse algorithm. Acta Arithmetica, 43(2):167–175, 1984. URL: http://eudml.org/doc/205897.
[19] H. Möller. Über hasses verallgemeinerung des syracuse-algorithmus (kakutanis problem). Acta Arithmetica, 34:219–226, 1978. URL: https://api.semanticscholar.org/CorpusID:117690327.
[20] Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765–768, October 1981. doi:10.1145/322276.322287.
[21] A. Podelski and A. Rybalchenko. Transition invariants. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pages 32–41, 2004. doi:10.1109/LICS.2004.1319598.
[22] Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, volume 2937, pages 239–251, January 2004. doi:10.1007/978-3-540-24622-0_20.
[23] R. Tyrrell Rockafellar. Convex Analysis. Princeton Landmarks in Mathematics and Physics. Princeton University Press, 1970.
[24] Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., USA, 1986.
[25] Simon Telen. Introduction to toric geometry, 2022. arXiv:2203.01690.
[26] A. Tiwari. Termination of linear programs. In R. Alur and D. Peled, editors, Computer-Aided Verification, CAV, volume 3114 of LNCS, pages 70–82. Springer, July 2004. doi:10.1007/978-3-540-27813-9_6.
[27] Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 742–766, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-81685-8_35.

[bib.bib1] [1] Amir M. Ben-Amram. Mortality of Iterated Piecewise Affine Functions over the Integers: Decidability and Complexity. In Natacha Portier and Thomas Wilke, editors, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013), volume 20 of Leibniz International Proceedings in Informatics (LIPIcs), pages 514–525, Dagstuhl, Germany, 2013. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.STACS.2013.514.

[bib.bib2] [2] Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. ACM Trans. Program. Lang. Syst., 34(4), 2012. doi:10.1145/2400676.2400679.

[bib.bib3] [3] Amir M. Ben-Amram, Samir Genaim, Joël Ouaknine, and James Worrell. Termination analysis of linear-constraint programs, 2025. doi:10.48550/arXiv.2509.06752.

[bib.bib4] [4] Mark de Berg, Otfried Cheong, Marc van Kreveld, and Mark Overmars. Computational Geometry: Algorithms and Applications. Springer-Verlag TELOS, Santa Clara, CA, USA, 3rd ed. edition, 2008.

[bib.bib5] [5] Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. Solving existentially quantified horn clauses. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 869–882, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. doi:10.1007/978-3-642-39799-8_61.

[bib.bib6] [6] Vincent D. Blondel, Olivier Bournez, Pascal Koiran, Christos H. Papadimitriou, and John N. Tsitsiklis. Deciding stability and mortality of piecewise affine dynamical systems. Theor. Comput. Sci., 255(1–2):687–696, March 2001. doi:10.1016/S0304-3975(00)00399-6.

[bib.bib7] [7] Mark Braverman. Termination of integer linear programs. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, pages 372–385, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. doi:10.1007/11817963_34.

[bib.bib8] [8] Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator: beyond safety. In Proceedings of the 18th International Conference on Computer Aided Verification, CAV’06, pages 415–418, Berlin, Heidelberg, 2006. Springer-Verlag. doi:10.1007/11817963_37.

[bib.bib9] [9] Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell. The 2-Dimensional Constraint Loop Problem Is Decidable. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024), volume 297 of Leibniz International Proceedings in Informatics (LIPIcs), pages 140:1–140:21, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2024.140.

[bib.bib10] [10] Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. Linear ranking for linear lasso programs. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis, pages 365–380, Cham, 2013. Springer International Publishing. doi:10.1007/978-3-319-02444-8_26.

[bib.bib11] [11] Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of Linear Loops over the Integers. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 118:1–118:13, Dagstuhl, Germany, 2019. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2019.118.

[bib.bib12] [12] Jeffrey C. Lagarias. The 3x+1 problem: An overview, 2021. arXiv:2111.02635.

[bib.bib13] [13] George M. Leigh. A markov process underlying the generalized syracuse algorithm. Acta Arithmetica, 46:125–143, 1986. URL: https://api.semanticscholar.org/CorpusID:117635633.

[bib.bib14] [14] Hendrik W. Lenstra. Integer programming with a fixed number of variables. Math. Oper. Res., 8:538–548, 1983. doi:10.1287/MOOR.8.4.538.

[bib.bib15] [15] Keith R. Matthews. Some borel measures associated with the generalized collatz mapping. Colloquium Mathematicum, 63:191–202, 1992. URL: https://api.semanticscholar.org/CorpusID:54607478.

[bib.bib16] [16] Keith R Matthews. Generalized 3x+ 1 mappings: markov chains and ergodic theory. The ultimate challenge: The 3x, 1:79–103, 2010.

[bib.bib17] [17] Keith R. Matthews and A. M. Watts. A markov approach to the generalized syracuse algorithm. Acta Arithmetica, 45:29–42, 1985. URL: https://api.semanticscholar.org/CorpusID:118600406.

[bib.bib18] [18] Watts A. Matthews K. A generalization of hasse’s generalization of the syracuse algorithm. Acta Arithmetica, 43(2):167–175, 1984. URL: http://eudml.org/doc/205897.

[bib.bib19] [19] H. Möller. Über hasses verallgemeinerung des syracuse-algorithmus (kakutanis problem). Acta Arithmetica, 34:219–226, 1978. URL: https://api.semanticscholar.org/CorpusID:117690327.

[bib.bib20] [20] Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765–768, October 1981. doi:10.1145/322276.322287.

[bib.bib21] [21] A. Podelski and A. Rybalchenko. Transition invariants. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pages 32–41, 2004. doi:10.1109/LICS.2004.1319598.

[bib.bib22] [22] Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, volume 2937, pages 239–251, January 2004. doi:10.1007/978-3-540-24622-0_20.

[bib.bib23] [23] R. Tyrrell Rockafellar. Convex Analysis. Princeton Landmarks in Mathematics and Physics. Princeton University Press, 1970.

[bib.bib24] [24] Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., USA, 1986.

[bib.bib25] [25] Simon Telen. Introduction to toric geometry, 2022. arXiv:2203.01690.

[bib.bib26] [26] A. Tiwari. Termination of linear programs. In R. Alur and D. Peled, editors, Computer-Aided Verification, CAV, volume 3114 of LNCS, pages 70–82. Springer, July 2004. doi:10.1007/978-3-540-27813-9_6.

[bib.bib27] [27] Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 742–766, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-81685-8_35.

Loop Termination and Generalized Collatz Sequences

Abstract

Keywords and phrases:

Category:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

2.1 Notation

2.2 Convex sets and the Minkowski–Weyl theorem

Definition 1.

Definition 2.

Theorem 3 (Minkowski–Weyl Theorem).

Proposition 4.

Proof.

Proposition 5 (Recession cone of an intersection).

2.3 Loops

▶ Remark 6.

▶ Remark 7.

2.4 Cycles and Self-avoiding Traces

Example 8.

Observation 9.

3 Cycles

3.1 Bound on a cycle length

Proposition 10.

Proof.

Proposition 11.

Proof.

Question 12.

Proposition 13.

Proof.

3.2 One variable case

Theorem 14.

Sketch of proof.

4 Generalized Collatz sequences

Conjecture 15 (Uniform Distribution Conjecture).

Conjecture 16 (Reachability Conjecture).

Proposition 17.

Proposition 18.

Example 19.

5 Self-avoiding Traces

Theorem 20.

Lemma 21.

Sketch of proof.

Definition 22.

Lemma 23.

Sketch of proof.

Lemma 24.

Sketch of proof.

Lemma 25.

Sketch of proof.

Proof of Theorem 20.

▶ Remark 26.

6 Proofs

6.1 Cycles

Lemma 27.

Proof.

Proof of Theorem 14.

Case 1: 𝜷≤𝟎 or 𝟏≤𝜷.

Case 2: 𝜶≤𝟎.

Case 3: 𝟎<𝜶 and 𝟎<𝜷<𝟏.

6.2 Generalized Collatz Sequences

Proof of Proposition 17.

Proof of Proposition 18.

6.3 Self-avoiding Traces

Lemma 28.

Proof.

Proof of Lemma 21.

Proof of Lemma 23.

Proof of Lemma 24.

Proof of Lemma 25.

7 Conclusion

References

$\blacktriangleright$ Remark 6.

$\blacktriangleright$ Remark 7.

$\blacktriangleright$ Remark 26.

Case 1: $\beta\leq 0$ or $1\leq\beta$ .

Case 2: $\alpha\leq 0$ .

Case 3: $0<\alpha$ and $0<\beta<1$ .