On Termination of Polynomial Programs with Equality Conditions

TL;DR

This paper proves the decidability of termination for a broad class of polynomial programs with equality conditions, introduces an Ackermannian recursive function for analysis, and extends techniques to programs with inequalities and invariant generation.

Contribution

It establishes the largest known family of polynomial programs with decidable termination, providing explicit recursive bounds and extending methods to inequality guards and invariant generation.

Findings

Termination is decidable for the considered family of polynomial programs.

An Ackermannian recursive function computes the maximal length of polynomial ideal chains.

The methods can be extended to programs with polynomial inequalities and invariant generation.

Abstract

We investigate the termination problem of a family of multi-path polynomial programs (MPPs), in which all assignments to program variables are polynomials, and test conditions of loops and conditional statements are polynomial equalities. We show that the set of non-terminating inputs (NTI) of such a program is algorithmically computable, thus leading to the decidability of its termination. To the best of our knowledge, the considered family of MPPs is hitherto the largest one for which termination is decidable. We present an explicit recursive function which is essentially Ackermannian, to compute the maximal length of ascending chains of polynomial ideals under a control function, and thereby obtain a complete answer to the questions raised by Seidenberg. This maximal length facilitates a precise complexity analysis of our algorithms for computing the NTI and deciding termination of MPPs. We extend our method to programs with polynomial guarded commands and show how an incomplete procedure for MPPs with inequality guards can be obtained. An application of our techniques to invariant generation of polynomial programs is further presented.