{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:54Z","timestamp":1776305394985,"version":"3.50.1"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In the last years, several works were concerned with identifying classes of programs<\/jats:p><jats:p>where termination is decidable. We consider triangular weakly non-linear loops<\/jats:p><jats:p>(twn-loops) over a ring Z \u2264 S \u2264 R_A , where R_A is the set of all real algebraic<\/jats:p><jats:p>numbers. Essentially, the body of such a loop is a single assignment<\/jats:p><jats:p>(x_1, ..., x_d) \u2190 (c_1 \u00b7 x_1 + pol_1, ..., c_d \u00b7 x_d + pol_d)<\/jats:p><jats:p>where each x_i is a variable, c_i \u2208 S, and each pol_i is a (possibly non-linear)<\/jats:p><jats:p>polynomial over S and the variables x_{i+1}, ..., x_d. Recently, we showed that<\/jats:p><jats:p>termination of such loops is decidable for S = R_A and non-termination is<\/jats:p><jats:p>semi-decidable for S = Z and S = Q.<\/jats:p><jats:p>In this paper, we show that the halting problem is decidable for twn-loops over any<\/jats:p><jats:p>ring Z \u2264 S \u2264 R_A. In contrast to the termination problem, where termination on all<\/jats:p><jats:p>inputs is considered, the halting problem is concerned with termination on a given<\/jats:p><jats:p>input. This allows us to compute witnesses for non-termination.<\/jats:p><jats:p>Moreover, we present the first computability results on the runtime complexity of<\/jats:p><jats:p>such loops. More precisely, we show that for twn-loops over Z one can always<\/jats:p><jats:p>compute a polynomial f such that the length of all terminating runs is bounded<\/jats:p><jats:p>by f( || (x_1, ..., x_d) || ), where || \u00b7 || denotes the 1-norm. As a corollary, we<\/jats:p><jats:p>obtain that the runtime of a terminating triangular linear loop over Z is<\/jats:p><jats:p>at most linear.<\/jats:p>","DOI":"10.29007\/nxv1","type":"proceedings-article","created":{"date-parts":[[2020,5,27]],"date-time":"2020-05-27T22:10:11Z","timestamp":1590617411000},"page":"279-259","source":"Crossref","is-referenced-by-count":10,"title":["Polynomial Loops: Beyond Termination"],"prefix":"10.29007","volume":"73","author":[{"given":"Marcel","family":"Hark","sequence":"first","affiliation":[]},{"given":"Florian","family":"Frohn","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2020,5,27]],"date-time":"2020-05-27T22:10:22Z","timestamp":1590617422000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/Bl5n"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/nxv1","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}],"subject":[]}}