论整数域上线性与仿射程序的终止性

Braverman 在文献中留下了整数域上仿射程序终止性问题这一未决难题。十多年来，该问题一直被视为极具挑战性的开放问题并被广泛引用。据我们所知，本文对此问题给出了最完整的解答：我们证明了在几乎对所有仿射程序都成立的假设下（除了一类测度为零的极小类外），整数域 $\mathbb{Z}$ 上仿射程序的终止性是可判定的。我们引入了“渐近非终止初始变量值”（asymptotically non-terminating initial variable values，简称 ANT）的概念，用于描述整数域 $\mathbb{Z}$ 上的线性循环程序。这些值直接对应于导致相应程序不终止的初始变量值。我们将整数域上线性仿射程序的终止性问题归约为特定 ANT 初始变量值集合的空性检查。对于此类线性或仿射程序，我们证明了相应的 ANT 集是一个半线性空间，并提供了一种强大的计算方法，能够自动生成这些 $ANT$ 集。此外，我们还能处理条件终止问题。换言之，通过取 ANT 集的补集，我们可以获得程序能够终止的输入集合的精确下近似。