We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring $\mathcal{S}$ like $\mathbb{Z}$, $\mathbb{Q}$, or $\mathbb{R}$. The guard of such a loop is an arbitrary quantifier-free Boolean formula over (possibly non-linear) polynomial inequations, and the body is a single assignment of the form $(x_1, \ldots, x_d) \longleftarrow (c_1 \cdot x_1 + p_1, \ldots, c_d \cdot x_d + p_d)$ where each $x_i$ is a variable, $c_i \in \mathcal{S}$, and each $p_i$ is a (possibly non-linear) polynomial over $\mathcal{S}$ and the variables $x_{i+1},\ldots,x_{d}$. We show that the question of termination can be reduced to the existential fragment of the first-order theory of $\mathcal{S}$. For loops over $\mathbb{R}$, our reduction implies decidability of termination. For loops over $\mathbb{Z}$ and $\mathbb{Q}$, it proves semi-decidability of non-termination. Furthermore, we present a transformation to convert certain non-twn-loops into twn-form. Then the original loop terminates iff the transformed loop terminates over a specific subset of $\mathbb{R}$, which can also be checked via our reduction. Moreover, we formalize a technique to linearize (the updates of) twn-loops in our setting and analyze its complexity. Based on these results, we prove complexity bounds for the termination problem of twn-loops as well as tight bounds for two important classes of loops which can always be transformed into twn-loops. Finally, we show that there is an important class of linear loops where our decision procedure results in an efficient procedure for termination analysis, i.e., where the parameterized complexity of deciding termination is polynomial.

翻译：我们研究在环$\mathcal{S}$（如$\mathbb{Z}$、$\mathbb{Q}$或$\mathbb{R}$）上三角弱非线性循环（twn-loops）的终止性证明问题。此类循环的守护条件是关于（可能非线性的）多项式不等式的任意无量词布尔公式，而循环体为单一赋值形式$(x_1, \ldots, x_d) \longleftarrow (c_1 \cdot x_1 + p_1, \ldots, c_d \cdot x_d + p_d)$，其中每个$x_i$为变量，$c_i \in \mathcal{S}$，且每个$p_i$是关于$\mathcal{S}$及变量$x_{i+1},\ldots,x_d$的（可能非线性）多项式。我们证明终止性问题可归约到$\mathcal{S}$的一阶理论存在性片段。对于$\mathbb{R}$上的循环，该归约蕴含终止性可判定性；对于$\mathbb{Z}$和$\mathbb{Q}$上的循环，则证明非终止性的半可判定性。此外，我们提出一种变换方法，可将特定非twn-循环转化为twn-形式。此时，原始循环终止当且仅当变换后的循环在$\mathbb{R}$的特定子集上终止，该问题同样可通过我们的归约进行验证。进一步地，我们形式化了一种在当前框架下线性化twn-循环（更新）的技术，并分析其复杂度。基于这些结果，我们证明了twn-循环终止性问题的复杂度边界，以及两类可始终转化为twn-循环的重要循环类的紧界。最后，我们证明存在一类重要的线性循环，其判定过程能产生高效的终止性分析算法，即终止性判定的参数化复杂度为多项式时间。