Polynomial Loops: Beyond Termination

Abstract

In the last years, several works were concerned with identifying classes of programs where termination is decidable. We consider triangular weakly non-linear loops (twn-loops) over a ring Z ≤ S ≤ R_A , where R_A is the set of all real algebraic numbers. Essentially, the body of such a loop is a single assignment (x_1, ..., x_d) ← (c_1 · x_1 + pol_1, ..., c_d · x_d + pol_d) where each x_i is a variable, c_i ∈ S, and each pol_i is a (possibly non-linear) polynomial over S and the variables x_{i+1}, ..., x_d. Recently, we showed that termination of such loops is decidable for S = R_A and non-termination is semi-decidable for S = Z and S = Q. In this paper, we show that the halting problem is decidable for twn-loops over any ring Z ≤ S ≤ R_A. In contrast to the termination problem, where termination on all inputs is considered, the halting problem is concerned with termination on a given input. This allows us to compute witnesses for non-termination. Moreover, we present the first computability results on the runtime complexity of such loops. More precisely, we show that for twn-loops over Z one can always compute a polynomial f such that the length of all terminating runs is bounded by f( || (x_1, ..., x_d) || ), where || · || denotes the 1-norm. As a corollary, we obtain that the runtime of a terminating triangular linear loop over Z is at most linear.

Topics & Concepts