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.

翻译：线性约束循环是转换关系由线性不等式系统指定的程序。终止问题询问给定循环是否存在无限计算。对于整数、有理数和实数上的线性约束循环，终止的可判定性仍是一个开放问题。我们专注于整数上的循环，并证明它们与广义科拉茨序列——由在模固定自然数的每个剩余类上呈线性的映射生成的整数序列——紧密相连。我们证明，如果关于广义科拉茨序列的一个长期存在的猜想成立，则单变量线性约束循环的终止可在多项式时间内判定。反过来，我们表明，任何针对单变量循环的判定程序都将证明或反驳该猜想的特定实例，而这些实例目前仍是开放的。此外，我们还证明，如果单变量循环存在循环轨迹，则其长度至多为二。