---
abstract: 'In this paper, we investigate the termination problem of a family of polynomial programs, in which all assignments to program variables are polynomials, and test conditions of loops and conditional statements are polynomial equations. Our main result is that the non-terminating inputs of such a polynomial program is algorithmically computable according to a strictly descending chain of algebraic sets, which implies that the termination problem of these programs is decidable. The complexity of the algorithm follows immediately from the length of the chain, which can be computed by Hilbert’s function and Macaulay’s theorem. To the best of our knowledge, the considered family of polynomial programs should be the largest one with a decidable termination problem so far. The experimental results indicate the efficiency of our approach.'
bibliography:
- 'LICS2016bib.bib'
title: Termination Analysis of Polynomial Programs with Equality Conditions
---

[***keywords**: Termination Analysis, Polynomial Programs, Polynomial Ideals*]{}

Introduction
============

Termination analysis plays an important role in program verification and testing, and has attracted an increasing attention recently [@cook:termination; @yang:advances]. However, the program termination problem is equivalent to the famous halting problem [@turing:computable], and hence is undecidable in general. Thus, a complete method for termination analysis for programs, even for 