(twn-loops) over some ring $\\mathcal{S}$ like $\\mathbb{Z}$, $\\mathbb{Q}$, or

$\\mathbb{R}$. Essentially, the guard of such a loop is an arbitrary Boolean

formula over (possibly non-linear) polynomial inequations, and the body is a

single assignment $(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 present a reduction

from the question of termination to the existential fragment of the first-order

theory of $\\mathcal{S}$ and $\\mathbb{R}$. For loops over $\\mathbb{R}$, our

reduction entails 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. This transformation also allows us to prove tight complexity

bounds for the termination problem for two important classes of loops which can

always be transformed into twn-loops.

},\n}\n'