Loop Termination and Generalized Collatz Sequences

TL;DR

This paper explores the decidability of loop termination for linear-constraint loops over integers, connecting it to generalized Collatz sequences, and provides polynomial-time results under a conjecture.

Contribution

It establishes a link between loop termination and Collatz conjecture, proving polynomial-time decidability under certain conditions and highlighting the conjecture's significance.

Findings

Termination of one-variable loops is decidable in polynomial time if a Collatz conjecture holds.

Any decision procedure for these loops could resolve open Collatz conjecture instances.

Loops with cyclic traces have cycles of length at most two.

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.