---
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 the general linear or polynomial programs, is impossible [@tiwari:terminate; @Muller-Olm; @bradley:polynomial; @braverman:terminate]. So, a practical way for termination analysis is conducted by providing sufficient conditions for termination and/or nontermination. Classical method for establishing termination of a program, either linear or polynomial, makes use of a well-founded domain together with a so-called *ranking function* that maps the state space of the program to the domain, which provides a sufficient condition for the termination of the program, e.g., [@Ben-AmramG14; @colon:synthesis; @podelski:ranking; @podelski:transition; @chen:ranking; @cousot:lagrangian]. In [@gupta:NT], the authors considered a sufficient condition for non-termination inputs, while in [@Harris10], the authors investigated sufficient conditions for termination and nontermination inputs respectively, and check the two conditions in parallel for termination analysis.

In contrast, Tiwari investigated this issue at a very fundamental level. He first noticed that the termination of a class of simple linear loops is related to the eigenvalues of assignment matrix and proved that the termination problem of these linear programs with input set $\mathbb{R}$ is decidable [@tiwari:terminate]. This theory was further developed in [@braverman:terminate; @XZ2010; @XYZZ2011].

Following this line, Bradley et al. [@bradley:polynomial] tried to investigate the termination problem of a family of polynomial programs, which are modeled as *multi-path polynomial programs* (MPPs) by using *finite difference tree* (FDT).The MPP model is an expressive class of loops with multiple paths, polynomial loop guards and assignments, that enables practical code abstraction and analysis. It was proved in [@bradley:polynomial] that the termination problem of MPPs is generally undecidable. In [@bradley:polynomial], the authors only considered a small class of MPPs, i.e., MPPs with polynomial behaviour. Similar idea was used for termination analysis of polynomial programs in [@cook:polynomial]. In [@LXZZ14], the authors considered another class of MPPs, whose loop guards are polynomial equations. According to their algebraic structures, the authors established sufficient conditions for termination and nontermination simultaneously for these MPPs, thus termination analysis can be conducted by checking these conditions in parallel, which is analogous to [@Harris10]. In [@LXZZ14], the authors raised an open problem whether the termination of this family of MPPs is decidable.

In this paper, we give a confirmative answer to the open problem raised in [@LXZZ14] that the termination problem of MPPs with equality guards is decidable. To the best of our knowledge, this family of polynomial programs should be the largest one with a decidable termination problem so far, noting that the program termination with inequality conditions is hardly to decide even for linear loops, since such problem is equivalent to the famous Skolem’s problem [@OW15]. On the other hand, inequality loop guards can be strengthened as equality guards, e.g. $f(x)\neq 0\Leftarrow f(x)z+1=0$, thus our approach can also be used to find non-terminating inputs for general MPPs.

The basic idea of our approach is as follows: Given an MPP $P$ with $\ell$ paths, for any input ${\pmb{x}}\in \mathbb{R}^d$, if at the first iteration ${\pmb{x}}$ satisfies the loop guard, then one of the paths in the loop body will be nondeterministically selected and the corresponding assignment will be used to update the value of ${\pmb{x}}$, which results in $\ell$ possible values of ${\pmb{x}}$; afterwards, the above procedure is repeated until the guard does not hold any more. Thus the execution of an MPP on input ${\pmb{x}}\in \mathbb{R}^d$ forms a tree. An input ${\pmb{x}}$ is called *non-terminating* if the execution tree on ${\pmb{x}}$ has an infinite path. Obviously, each of such paths forms an ascending chain of polynomial ideals, and an input ${\pmb{x}}$ is *non-terminating* iff ${\pmb{x}}$ is in the variety of an ascending chain in the execution tree. By using some results of polynomial algebra, we prove that there is a uniform upper bound for these ascending chains. This implies the decidability of termination problem of the family of MPPs. Similar argument is applicable to polynomial guarded commands in which all test guards are polynomial equations.

Related work {#related-work .unnumbered}
------------

In the past, various well-established work on termination analysis can only be applied to linear programs, whose guards and assignments are linear. For single-path linear programs, Colón and Sipma utilized polyhedral cones to synthesize linear ranking functions [@colon:synthesis]. Podelski and Rybalchenko, based on Farkas’ lemma, presented a complete method to find linear ranking functions if they exist [@podelski:ranking]. In [@Ben-AmramG14], Ben[-]{}Amram and Genaim considered to extend the above results in the following two aspects: firstly, they proved that synthesizing linear ranking functions for single path linear programs is still decidable if program variables are interpreted over integers, but with co-NP complexity, in contrast to PTIME complexity when program variables are interpreted over rationals or reals; secondly, they proposed the notion of *lexicographical ranking function* and a corresponding approach for synthesizing lexicographical ranking functions for dealing with linear programs with multi-path.

In recent years, the termination problem of non-linear programs attracted more attentions as they are omnipresent in safety-critical embedded systems. Bradley et al. proposed an approach to proving termination of MPPs with polynomial behaviour over $\mathbb{R}$ through finite difference trees [@bradley:polynomial]. Similar idea was used in [@cook:polynomial] for termination analysis of polynomial programs. Typically, with the development of computer algebra, more and more techniques from symbolic computation, for instance, Gröbner basis [@sank:GB; @muller:invariants], quantifier elimination [@kapur:QE] and recurrence relation [@rodriguez:simple; @kovacs:psolvable], are borrowed and successfully applied to the verification of programs. Certainly, these techniques can also be applied to polynomial programs to discover termination or non-termination proofs. Chen et al. proposed a relatively complete (w.r.t. a given template) method for generating polynomial ranking functions over $\mathbb{R}$ by reduction to semi-algebraic system solving [@chen:ranking]. Gupta et al. proposed a practical method to search for counter-examples of termination [@gupta:NT], by first generating lasso-shaped [@cook:code] candidate paths and then checking the feasibility of the “lassoes" using constraint solving. Velroyen and Rümmer applied invariants to show that terminating states of a program are unreachable from certain initial states, and then identified these “bad” initial states by constraint-solving [@Velroyen08]. Brockschmidt et al. detected non-termination and Null Pointer Exceptions for by constructing and analyzing termination graphs, and implemented a termination prover [@Brockschmidt11].

For more general programs, many other techniques, like predicate abstraction, parametric abstraction, fair assumption, Lagrangian relaxation, semidefinite programming, sum of squares, etc., have been successfully applied [@cousot:termination; @cousot:lagrangian; @cook:conditional].

The following work are more related to ours. Tiwari first identified a class of simple linear loops and proved that its termination problem is decidable over reals $\mathbb{R}$ [@tiwari:terminate]. Braverman extended Tiwari’s result by proving the termination problem is still decidable when program variables are interpreted over integers $\Bbb{Z}$ [@braverman:terminate], and Xia and Zhang investigated an extension of Tiwari’s simple linear loops by allowing a loop condition to be non-linear constraint and proved that the termination problem of the extension is still decidable over reals, and becomes undecidable over integers [@XZ2010]. In [@bradley:polynomial], Brandley et al. proved that the termination problem of MPPs with inequalities as loop conditions is not semi-decidable. Additionally, Müller-Olm and Seidl proved that the termination problem of linear guarded commands with equations and inequations as guards is undecidable [@Muller-Olm]. Thus, we believe that the class of polynomial programs, i.e., polynomial guarded commands with equalities as guards, under consideration in this paper, is the largest one with a decidable termination problem, any extension of it by allowing inequalities, or inequations in a guard will result in the termination problem undecidable.

The rest of the paper is organized as follows. In Section \[sec:nutshell\], we give an overview of our approach by a running example. In Section \[sec:pre\], some concepts and results on computational algebraic geometry are reviewed. Section \[sec:bound\] is devoted to computing the upper bound on the length of a descending chain of algebraic sets. In Section \[sec:MPP\], we introduce the model of MPPs with equality guards. In Section \[sec:Deci\], we prove the decidability of the termination problem of the MPPs by proposing an algorithm to compute the set of non-terminating inputs. Section \[sec:pgc\] extends the decidability result to polynomial guarded commands with equality guards. Section \[sec:case\] reports some experimental results with our method. A conclusion is drawn in Section \[sec:conc\].

A running example {#sec:nutshell}
=================

Consider the following polynomial program (denoted by `running`):

\[exm:running\] $$\begin{split}
&(x,y) \coloneqq (x_0,y_0);\\
&\textsc{ while}\ (x+y=0)\ \textsc{do}\\
&\quad \textsc{if ? then}\ (x,y) \coloneqq (y^2,2x+y);\\
&\quad \textsc{else}\ (x,y) \coloneqq (2x^2+y-1,x+2y+1);\\
&\textsc{ end \ while}
\end{split}$$ Here “<span style="font-variant:small-caps;">?</span>” means that the condition has been ignored by abstraction of the program, and thus in each iteration these two assignments are *nondeterministically* chosen. Our problem is to decide if or not for any initial value $(x_0,y_0)$ in a given set $V=\{(x,y)\mid x^2+y=0\}$, the program would always terminate in a finite number of iterations.

For simplicity, the polynomial of the loop guard is denoted as $G(x,y)=x+y$, and the two polynomial vectors of the assignments as ${\pmb{A}}_1(x,y)=(y^2,2x+y)$ and ${\pmb{A}}_2(x,y)=(2x^2+y-1,x+2y+1)$. Our approach is to compute the set $D$ of all possible initial values of $(x_0,y_0)$ for which the program may not terminate. Thus, the termination problem of the program on the set of inputs $X$ is easily obtained by checking if $X\cap D=\emptyset$. The detailed procedure is described step by step as follows:

1.  Consider the equation $G(x,y)=x+y=0$, and write the set of its solutions as $D_0$. Thus, $(x_0,y_0)\in D_0$ means that the body of the loop should be executed once at least w.r.t. the input.

2.  Denote by $D_{(1)}$ and $D_{(2)}$ the solution sets of equations: $$\begin{split}
    &\left\{
       \begin{aligned}
       &G(x,y)=x+y=0\\
       &G({\pmb{A}}_1(x,y))=y^2+(2x+y)=0
       \end{aligned}\right.\\
    {\rm and}&\\
    &\left\{
       \begin{aligned}
       &G(x,y)=x+y=0\\
       &G({\pmb{A}}_2(x,y))=(2x^2+y-1)+(x+2y+1)=0
       \end{aligned}\right.
    \end{split}$$ respectively. So, $(x_0,y_0)\in D_{(i)}\ (i=1,2)$ means that the loop body may be executed twice at least by correspondingly choosing ${\pmb{A}}_i$ to be the assignment in the first iteration. So $(x_0,y_0)\in D_1\triangleq D_{(1)}\cup D_{(2)}$ allows at least two iterations in the execution. It is easy to calculate that $D_{(1)}=\{(0,0),(-1,1)\}$, $D_{(2)}=\{(0,0),(1,-1)\}$, and so $D_1=\{(0,0),(1,-1),(-1,1)\}$.

3.  Similarly, the solution set $D_{(ij)}$ of equation $$\left\{
       \begin{aligned}
       &G(x,y)=0\\
       &G({\pmb{A}}_i(x,y))=0\\
       &G({\pmb{A}}_j({\pmb{A}}_i(x,y)))=0
       \end{aligned}\right.$$ is the set of inputs for which the third iteration is achievable by successively choosing ${\pmb{A}}_i$ and ${\pmb{A}}_j$ in the first and the second iterations. $D_2\triangleq D_{(11)}\cup D_{(12)}\cup D_{(21)}\cup D_{(22)}$ is the set of inputs which allow at least three iterations. By simple calculation, we obtain that $D_{(11)}=\{(0,0)\}$, $D_{(12)}=\{(0,0),(-1,1)\}$, $D_{(21)}=\{(0,0),(1,-1)\}$, $D_{(22)}=\{(1,-1)\}$, and $D_2=\{(0,0),(1,-1),(-1,1)\}$.

4.  Now we note that $D_1=D_2$. Our results reported in this paper guarantee that $D=D_1=\{(0,0),(1,-1),(-1,1)\}$, namely, $D_1$ is actually the set of inputs which make the program possibly nonterminating.

5.  Observe that $V\cap D=\{(1,-1)\}\neq\emptyset$. So the program is nonterminating on input $(x_0,y_0)=(1,-1)$.

Preliminaries {#sec:pre}
=============

In this section, we recall some basic concepts and results on computational algebraic geometry, which serve as the theoretical foundation of our discussion. For a detailed exposition to this subject, please refer to [@DJD07][@FSM27].

Polynomial rings and ideals
---------------------------

Consider a number field ${\mathbb{K}}$, which could be the field of rational numbers $\mathbb{Q}$, real numbers $\mathbb{R}$ or complex numbers $\mathbb{C}$ throughout this paper. Let ${\pmb{x}}=(x_1,x_2,\cdots,x_d)$ be a vector of variables. A monomial of ${{\pmb{x}}}$ is of the form ${\pmb{x}}^{{\pmb{\alpha}}}\triangleq x_1^{\alpha_1} x_2^{\alpha_2}\cdots x_d^{\alpha_d},$ where ${{\pmb{\alpha}}}=(\alpha_1,\alpha_2,\ldots,\alpha_d)\in\mathbb N^d$ is a vector of natural numbers, and $\sum_{i=1}^d \alpha_i$ is called the *degree* of ${\pmb{x}}^{\alpha}$, denoted by $\deg({\pmb{x}}^{{\pmb{\alpha}}})$. A polynomial $f$ of ${{\pmb{x}}}$ is a linear combination of a finite number of monomials over ${\mathbb{K}}$, i.e., $f=\sum_{i=1}^m\lambda_i{\pmb{x}}^{{\pmb{\alpha}}_i},$ where $m$ is the number of distinct monomials of $f$ and $\lambda_i\in{\mathbb{K}}$ is the nonzero coefficient of ${\pmb{x}}^{{\pmb{\alpha}}_i}$, for each $i$. The degree of $f({\pmb{x}})$ is defined as $\deg(f)=\max\{\deg{{\pmb{x}}^{{\pmb{\alpha}}_i}}\mid i=1,2,\cdots,m\}$. Denote by $\mathcal{M}[{\pmb{x}}]$ the set of monomials of ${\pmb{x}}$ and ${\mathbb{K}}[{\pmb{x}}]$ the polynomial ring of ${\pmb{x}}$ over ${\mathbb{K}}$. The degree of a finite set $X\subseteq{\mathbb{K}}[{\pmb{x}}]$ is defined as $\deg(X)=\max\{\deg(f)\mid f\in X\}$.

we introduce the lexicographic order for monomials: ${\pmb{x}}^{{\pmb{\alpha}}}\prec{\pmb{x}}^{\pmb{\beta}}$ if there exists $1\leq i\leq d$ such that $\alpha_i<\beta_i$ and $\alpha_j=\beta_j$ for all $1\leq j < i$. For every polynomial $f\in{\mathbb{K}}[{\pmb{x}}]$ we write its leading monomial (i.e., the greatest monomial under $\prec $) as $\operatorname{lm}(f)$. For any $n\in{\mathbb{N}}$, a set of monomials $M$ is called *$n$-compressed*, if for any $m\in M$, $\deg(m)=n$, then $\{m'\mid\deg(m')=n,m'\prec m\}\subseteq M.$

1.  A nonempty subset $I\subseteq{\mathbb{K}}[{\pmb{x}}]$ is called an ideal if $f,\ g\in I\Rightarrow f-g\in I$, and $f\in I,\ h\in{\mathbb{K}}[{\pmb{x}}]\Rightarrow fh\in I$.

2.  Let $P$ be a nonempty subset of ${\mathbb{K}}[{\pmb{x}}]$, the ideal generated by $P$ is defined as $\langle P\rangle\triangleq\Big\{\sum_{i=1}^n f_ih_i\mid n\in \mathbb{N},\ f_i\in P,\ h_i\in {\mathbb{K}}[{\pmb{x}}]\Big\}.$

3.  The product of two ideals $I$ and $J$ is defined as $$I\times J=\langle\{f\cdot g\mid f\in I, g\in J\}\rangle.$$

The ideal generated by $P$ is actually the minimal one of ideals that contain $P$. When $P=\{f_1,f_2,\cdots,f_n\}$ is a finite set, we simply write $\langle P\rangle$ as $\langle f_1,f_2,\cdots,f_n\rangle$. Given two polynomial sets $P$ and $Q$, we define $P\cdot Q\triangleq\{f\cdot g\mid f\in P, g\in Q\}$. Obviously, $\langle P\rangle\times\langle Q\rangle=\langle P\cdot Q\rangle$.

Every ideal $I\subseteq {\mathbb{K}}[{\pmb{x}}]$ is finitely generated, that is, $I=\langle f_1,f_2,\cdots,f_n\rangle$ for some $f_1,f_2,\cdots,f_n\in {\mathbb{K}}[{\pmb{x}}]$. Here $\{f_1,f_2,\cdots,f_n\}$ is called a basis of $I$.

We define the degree of an ideal $I$ as $$\operatorname{gdeg}(I)=\min\{\deg(P)\mid P\ \text{is a basis of}\ I\}.$$ Note that an ideal may have different bases. However, using the Buchberger’s algorithm under a fixed monomial ordering, a unique (reduced) Gröbner basis of $I$, denoted by $\operatorname{GB}(I)$, can be computed from any other basis. We also simply write $\operatorname{GB}(\langle P\rangle)$ as $\operatorname{GB}(P)$ for any basis $P$. An important property of Gröbner basis is that the remainder of any polynomial $f$ on division by $\operatorname{GB}(P)$, written as $\operatorname{Rem}(f,\operatorname{GB}(P))$, satisfies that $$f\in\langle P\rangle\Leftrightarrow\operatorname{Rem}(f,\operatorname{GB}(P))=0.$$

The Hilbert’s Basis Theorem implies that the polynomial ring ${\mathbb{K}}[{\pmb{x}}]$ is a Noetherian ring, i.e.,

\[thm:asc-chain\]For any ascending chain of ideals $$I_1\subseteq I_2\subseteq \cdots\subseteq I_n \subseteq \cdots$$ of ${\mathbb{K}}[{\pmb{x}}]$, there exists an $N\in\mathbb{N}$ such that $I_n=I_N$ for all $n\geq N$.

Algebraic sets and varieties
----------------------------

By assigning values in ${\mathbb{K}}^d$ to ${\pmb{x}}$, a polynomial $f\in{\mathbb{K}}[{\pmb{x}}]$ can be regarded as a function from the affine space ${\mathbb{K}}^d$ to ${\mathbb{K}}$. Then the set of zeros of a polynomial set $P\subset{\mathbb{K}}[{\pmb{x}}]$ can be defined as $Z(P)\triangleq\{{\pmb{x}}\in{\mathbb{K}}^d\mid\forall f\in P.\, f({\pmb{x}})=0\}$. It is easy to verify that $Z(P)=Z(\langle P\rangle)$.

A subset $X\subseteq{\mathbb{K}}^d$

1.  is algebraic, if there exists some $P\subseteq{\mathbb{K}}[{\pmb{x}}]$ such that $X=Z(P)$, and $P$ is called a set of generating polynomials of $X$;

2.  is reducible, if it has two algebraic proper subsets $X_1$ and $X_2$ such that $X=X_1\cup X_2$; otherwise it is called irreducible;

3.  is a variety, if it is a nonempty irreducible algebraic set.

The following properties on algebraic and variety can be easily verified: the union of two algebraic sets is an algebraic set, and the intersection of any family of algebraic sets is still algebraic; suppose $X_1,X_2,\cdots,X_n$ are algebraic sets and $X$ is a variety, then $$X\subseteq X_1\cup\cdots\cup X_n\Rightarrow X\subseteq X_k\ \text{for some}\ k.$$ An algebraic set is usually represented by its generating polynomials in practice. Note that an algebraic set may have different sets of generating polynomials. However, by defining $$I(X)\triangleq\{f\in{\mathbb{K}}[x]\mid\forall {\pmb{x}}\in X.\, f({\pmb{x}})=0\}$$ for any $X\subseteq {\mathbb{K}}^d$, one can easily verify that $I(Z(P))$ is the maximal set that generates $Z(P)$. So, any algebraic set $X$ can be identified by the ideal $I(X)$. The membership $f\in I(Z(P))$ for any polynomial $f$ and any finite set $P=\{f_1,\cdots,f_n\}$ of polynomials is equivalent to the unsatisfiability of $f_1=0\wedge f_2=0\wedge\cdots\wedge f_n=0\wedge f\neq0$, which is decidable [@Tarski51].

Additionally, noting that $X_1\subset X_2\Leftrightarrow I(X_1)\supset I(X_2)$ for two algebraic sets $X_1$ and $X_2$, it follows from Theorem \[thm:asc-chain\] that

\[thm:des-chain\]For any descending chain of algebraic sets $$X_1\supseteq X_2\supseteq\cdots\supseteq X_n\supseteq\cdots$$ of ${\mathbb{K}}^d$, there exists an $N\in\mathbb{N}$ such that $X_n=X_N$ for all $n\geq N$.

Monomial ideals and Hilbert’s functions
---------------------------------------

An ideal $I$ is called monomial if it can be generated by a set of monomials. A monomial ideal always has a basis $\{m_1,m_2,\dots,m_s\}$ of monomials (due to Dickson’s Lemma), and any monomial $m\in \langle m_1,m_2,\cdots,m_s\rangle$ should be a multiple of some $m_i$.

For a monomial ideal $I\subseteq{\mathbb{K}}[{\pmb{x}}]$, a function $H_I:{\mathbb{N}}\rightarrow{\mathbb{N}}$ is defined as $$H_I(n)=\dim_{\mathbb{K}}{\mathbb{K}}_n[{\pmb{x}}]/I_n=\dim_{\mathbb{K}}{\mathbb{K}}_n[{\pmb{x}}]-\dim_{\mathbb{K}}I_n,$$ where ${\mathbb{K}}_n[{\pmb{x}}]$ is the set of homogeneous polynomials of degree $n$ and $I_n=I\cap{\mathbb{K}}_n[{\pmb{x}}]$, and both of them are linear spaces over ${\mathbb{K}}$.

Note that $\dim_{\mathbb{K}}{\mathbb{K}}_n[{\pmb{x}}]=(n)_{d-1}$ is the number of monomials of degree $n$, where $$(n)_{d-1}\triangleq\binom{n+d-1}{d-1}=(n+d-1)(n+d-2)\cdots(n+1)/(d-1)!.$$ And $H_I(n)=0$ means that $I$ contains all monomials of degree $\geq n$.

We invoke the Macaulay’s theorem [@FSM27] to estimate the value of Hilbert’s function $H_I$. To this end, we define a function $\operatorname{Inc}_k:{\mathbb{N}}\rightarrow{\mathbb{N}}$ for every natural number $k\geq 1$ as follows. When $k$ is given, any number $n\in{\mathbb{N}}$ can be uniquely decomposed as $$n=(n_1)_k+(n_2)_{k-1}+\cdots+(n_r)_{k-r+1}\triangleq(n_1,n_2...,n_r)_k,$$ where $0\leq r\leq k$ and $n_1\geq n_2\geq\cdots\geq n_r\geq 0$. In fact, $0=()_k$ with $r=0$; and for $n>0$, $n_1, n_2,\cdots,n_r$ are successively determined by $$\begin{split}
(n_1)_k&\leq n<(n_1+1)_k\\
(n_2)_{k-1}&\leq n-(n_1)_k<(n_2+1)_{k-1}\\
&\cdots
\end{split}$$ until $n=(n_1,n_2...,n_r)_k$ for some $r\geq 1$. Now we define $$\operatorname{Inc}_k((n_1,\cdots,n_r)_k)=(n_1,...,n_r)_{k+1}.$$ For instance, $\operatorname{Inc}_k(0)=0$, and $\operatorname{Inc}_3(11)=\operatorname{Inc}_3((2,0)_3)=(2,0)_4=16$ (note that $11=(2,0)_3$).

\[thm:Macaulay\] For any monomial ideal $I\subseteq{\mathbb{K}}[{\pmb{x}}]$, $H_I(n+1)\leq\operatorname{Inc}_n(H_I(n))$ for all $n\geq1$. Moreover, $H_I(n+1)=\operatorname{Inc}_n(H_I(n))$ if $\operatorname{gdeg}(I)\leq n$ and $I$ is $n$-compressed.

Upper bound of the length of polynomial ascending chains {#sec:bound}
========================================================

In this section, we investigate the length of polynomial ascending chains, which plays a key role in proving the decidability of the termination problem. In addition, this problem is independently of interest in mathematics and has received many studies [@GMS92; @Seidenberg1971].

The computing is based on Moreno-Socías’s approach [@GMS92], which consists of the following three steps:

-   Reduce computing the bound on $f$-bounded polynomial ideal chains to computing the bound on $f$-generating sequences of monomials, which is obtained by Moreno-Socías’s result [@GMS92].

-   Compute the longest homogeneous $f$-generating sequence, which is achieved directly by using Hilbert’s function and Macaulay’s theorem. This step is different from Moreno-Socias’s, as his result on this step (i.e. Proposition 4.3 in [@GMS92]) is wrong.

-   Prove that the bound of $f$-generating sequences of monomials is exactly same as the length of the longest homogeneous $f$-generating sequence obtained in (ii), which is trivially achieved by introducing a fresh variable.

For any increasing function $f:{\mathbb{N}}\rightarrow{\mathbb{N}}$ (that is, $f(x)\leq f(y)$ for all $x\leq y$), an ascending chain $I_1\subseteq I_2\subseteq\cdots\subseteq I_n$ of polynomial ideals of ${\mathbb{K}}[{\pmb{x}}]$ is called $f$-bounded, if $\operatorname{gdeg}(I_i)\leq f(i)$ for all $i\geq 1$. Denote by $L(d,f)$ the greatest length of all strictly ascending chains of ${\mathbb{K}}[{\pmb{x}}]$ which are $f$-bounded.

1.  The condition of $f$-boundedness is necessary to define the greatest length, as the length of chains with unbounded degrees could be arbitrarily large (for instance, the length of $\langle x^n\rangle\subset\langle x^{n-1}\rangle\subset\cdots\subset\langle 1\rangle$ could be arbitrarily large if $n$ is unbounded).

2.  For ease of discussion, we assume $f$ is *increasing* without loss of generality. In fact, for a general $f$, consider the increasing function $F:{\mathbb{N}}\rightarrow{\mathbb{N}}$, $F(n)\triangleq\max\{f(1),f(2),\cdots,f(n)\}$. Then a $f$-bounded chain is always a $F$-bounded chain since $f(n)\leq F(n)$ for all $n$. So $L(d,f)\leq L(d,F)$, and we can use $L(d,F)$ as the upper bound of the chains.

Our aim is to compute $L(d,f)$ based on the number of variables $d$ and function $f$. To this end, we particularly consider ascending chains of a special form.

\[def:f-gener\]Given a function $f:{\mathbb{N}}\rightarrow{\mathbb{N}}$, a finite sequence of monomials $m_1,m_2,\cdots,m_n\in\mathcal{M}[{\pmb{x}}]$ is called $f$-generating, if $\deg(m_i)\leq f(i)$ and $m_{i+1}\notin\langle m_1,\cdots,m_i\rangle$ for all $i\geq 1$.

Then a $f$-generating monomial sequence $m_1,m_2,\cdots,m_n$ generates a strictly ascending chain of monomial ideals $I_1\subset I_2\subset\cdots\subset I_n$ satisfying $\operatorname{gdeg}(I_i)\leq f(i)$, by defining $I_i=\langle m_1,m_2,\cdots,m_i\rangle$. Moreno-Socías proved in [@GMS92] that in order to compute $L(d,f)$, it suffices to consider the ascending chains that are generated by $f$-generating monomial sequences. That is,

\[prop:monomial\]$L(d,f)$ is exactly the greatest number of monomials of $f$-generating sequences in $\mathcal{M}[{\pmb{x}}]$.

Hence, in the rest of this section, we construct the longest chain of this form. We first do this for a special case where the degrees of polynomial ideals are not just bounded but completely determined by a function $f$. Then we reduce the general case to this special one.

The longest chain of specified degrees
--------------------------------------

In this subsection, we only consider a special type of $f$-generating sequences $m_1,\cdots,m_n$ such that: $$\label{equ:special}\forall i\in\{1,\cdots,n\}.\, \deg(m_i)=f(i).$$

We inductively construct a $f$-generating sequence of monomials $\hat{m}_1,\hat{m}_2,\cdots,\hat{m}_N$ as follows: Initially define $\hat{m}_1=x_1^{f(1)}$; suppose $\hat{m}_1,\hat{m}_2,\cdots,\hat{m}_n$ are defined for some $n\geq 1$, then let $$\label{equ:hatm}\hat{m}_{n+1}\triangleq \min\{m|\deg(m)=f(n+1), m\notin \langle \hat{m}_1,...,\hat{m}_n\rangle\},$$ until $\{m|\deg(m)=f(N+1)\}\subseteq\langle \hat{m}_1,...,\hat{m}_N\rangle$ for some $N$.

Obviously, this sequence satisfies equation (\[equ:special\]). It follows immediately from the equation (\[equ:hatm\]) that the corresponding ideal $\hat{I}_n\triangleq\langle\hat{m}_1,\hat{m}_2,\cdots,\hat{m}_n\rangle$ is $f(n)$-compressed for every $n=1,2,\cdots,N$, and $H_{\hat{I}_N}(f(N+1))=0$ from the definition of Hilbert’s function.

\[exm:4382\] For $d=3$ and $f(n)=2\times3^{n-1}$ , we have a set $$\begin{split}
\{\hat{m}_1,\hat{m}_2,\ldots,\hat{m}_{4382}\}
=&\{x^2,xy^5,xy^4z^3,xy^3z^{50},xy^2z^{159}, xyz^{484},\\
&xz^{1457},y^{4374},y^{4373}z^{8749},\ldots,y^0z^{2\cdot3^{4381}}\}.\end{split}$$ Then $N=4382$ in this case.

Now we shall prove that the sequence we construct has the greatest number of monomials among all $f$-generating sequences that satisfies (\[equ:special\]).

If $m_1,m_2,\cdots,m_n$ is a $f$-generating sequence that satisfies equation (\[equ:special\]), then $n\leq N$.

*Proof:* We proceed by contradiction. Suppose $n\geq N+1$. Let $I_i=\langle m_1,\cdots,m_i\rangle$ for all $i\in{1,2,\cdots,n}$. For simplicity, we define $H_i(j)\triangleq H_{I_i}(j)$ and $\hat{H}_{i}(j)\triangleq H_{\hat{I}_i}(j)$, for all $i,j\geq 1$. Observe that$$\label{equ:H_exp}
H_i(j)\left\{
   \begin{aligned}
   &=H_{i-1}(j),\quad j<f(i);\\
   &=H_{i-1}(j)-1,\quad j=f(i);\\
   &\leq \operatorname{Inc}_{j-1}H_i(j-1),\quad j>f(i).
   \end{aligned}\right.$$ Indeed, the first two equalities directly follow from the definition of $I_i$, and the third inequality is from Theorem \[thm:Macaulay\]. Similarly, we have$$\label{equ:hatH_exp}
\hat{H}_i(j)\left\{
   \begin{aligned}
   &=\hat{H}_{i-1}(j),\quad j<f(i);\\
   &=\hat{H}_{i-1}(j)-1,\quad j=f(i);\\
   &=\operatorname{Inc}_{j-1}\hat{H}_i(j-1),\quad j>f(i).
   \end{aligned}\right.$$ Here, the third one becomes equality since $\hat{I_i}$ is $f(i)$-compressed and $\operatorname{gdeg}(\hat{I_i})=f(i)\leq j-1$ and so the conditions for equality in Theorem \[thm:Macaulay\] is satisfied. On the other hand, we observe that $H_1(f(1))=\hat{H}_1(f(1))=(f(1))_{d-1}-1$. Then it can be inductively proved from equations (\[equ:H\_exp\]) and (\[equ:hatH\_exp\]) that:$$\begin{split}
H_i(j)&=H_{i-1}(j)\leq \hat{H}_{i-1}(j)=\hat{H}_i(j),\quad \text{for}\ j<f(i);\\
H_i(j)&=H_{i-1}(j)-1\leq \hat{H}_{i-1}(j)-1=\hat{H}_i(j),\quad \text{for}\ j=f(i);\\
H_i(j)&\leq \operatorname{Inc}_{j-1}H_i(j-1)\leq\operatorname{Inc}_{j-1}\hat{H}_i(j)=\hat{H}_i(j),\quad \text{for}\ j>f(i).
\end{split}$$ Here, the fact that $r<t\Rightarrow\operatorname{Inc}_j(r)<\operatorname{Inc}_j(t)$ is applied. So we have proved that $H_i(j)\leq\hat{H}_i(j),$ for all $i\geq 1$ and $j\geq 1$. Then $H_N(f(N+1))\leq \hat{H}_N(f(N+1))=0$. We have $m_{N+1}\in\{m|\deg(m)=f(N+1)\}\subseteq\langle \hat{m}_1,...,\hat{m}_n\rangle$, which is contrary to the definition of $\{m_1,\cdots,m_n\}$. $\Box$

We consider to compute the greatest length $N$ using the condition $\hat{H}_N(f(N))=\hat{H}_N(f(N+1))=0$. To this end, we define $\Omega(d-1,f,t)$ to be the number $k$ such that $$\label{equ:Omega}\begin{split}\hat{H}_k(f(k))&=(d\underbrace{-2,d-2,\cdots,d-}_{f(1)-t\ \text{times}}2)_{f(k)}\\
&=(d-2)_{f(k)}+\cdots+(d-2)_{(f(k)-f(1)+t+1)}.\end{split}$$ Then from this definition $N=\Omega(d-1,f,f(1))$. Note that $$\hat{H}_1(f(1))=(f(1))_{d-1}-1=(d\underbrace{-2,d-2,\cdots,d-}_{f(1)\ \text{times}}2)_{f(1)},$$ then $\Omega(d-1,f,0)=1$. Computing $\Omega(d,f,t)$ is presented in the following theorem.

\[thm:Omega\] Given a number $d\in{\mathbb{N}}$, an increasing function $f:{\mathbb{N}}\rightarrow{\mathbb{N}}$, and a number $t\in\{0,1,\cdots,f(1)\}$, $\Omega(d,f,t)$ can be recursively calculated as follows:

1.  $\Omega(0,f,t)=1$ and $\Omega(d,f,0)=1$, for any $d\geq 1$, $f$ and $t$;

2.  Write $n_t\triangleq \Omega(d,f,t)$ for $t=0,1,\cdots,f(1)$, then they can be successively calculated by $n_0=0$ and for $t\geq 1$, $$n_t=n_{t-1}+\Omega(d-1,f_{+n_{t-1}},f(n_{t-1}+1)-f(1)+1).$$ Here $f_{+m}$ is a function defined as $f_{+m}(n)=f(m+n)$.

*Proof:* It is equivalent to show that the recursive function $\Omega$ defined by the calculation procedure above is the same as the one defined by equation (\[equ:Omega\]); namely, if we compute a number $k=\Omega(d-1,f,t)$ by the calculation, then $\hat{H}_k(f(k))$ should be as in equation (\[equ:Omega\]). On the other hand, for any $k\geq 1$, decompose $\hat{H}_k(f(k))$ as $\hat{H}_k(f(k))=(a_1,a_2,\cdots,a_r)_{f(k)}$. It can be verified by equation (\[equ:H\_exp\]) that $\hat{H}_{k+1}(f(k+1))=(a_1,a_2,\cdots,a_r)_{f(k+1)}-1$. So $\hat{H}_k(f(k))$ can also be recursively calculated from $\hat{H}_1(f(1))$. Then it is easy to prove the result by induction on $d$ and $t$.$\Box$

For instance, let $f(n)=2\times 3^{n-1}$, then $\Omega(2,f,2)=4382$ by Theorem \[thm:Omega\], which is exactly the number of monomials in Example \[exm:4382\].

Reduction from the general case
-------------------------------

Now we remove the restriction (\[equ:special\]) and consider the length of a general $f$-generating sequence of monomials $m_1,\cdots,m_n$ in $\mathcal{M}[{\pmb{x}}]$. Our method is to reduce this general case to the homogenous case. Specifically, we introduce a new variable $x_{d+1}$ (for which the lexicographic order becomes $x_1\prec \cdots \prec x_d\prec x_{d+1}$), and construct for each $m_i$ $(i=1,\cdots,n)$ a monomial $\tilde{m}_i\in\mathcal{M}[{\pmb{x}},x_{d+1}]$ such that $\tilde{m}_i=m_ix_{d+1}^{c_i}$, where $c_i=f(i)-\deg(m_i)\in{\mathbb{N}}$. So $\deg(\tilde{m}_i)=f(i)$ and thus the restriction (\[equ:special\]) is satisfied by $\tilde{m}_1,\cdots,\tilde{m}_n$. Furthermore,

$\tilde{m}_1,\cdots,\tilde{m}_n$ is a $f$-generating sequence of ${\mathbb{K}}[{\pmb{x}},x_{d+1}]$.

*Proof:* It suffices to prove that $\tilde{m}_{i+1}\notin\langle\tilde{m}_1,\cdots,\tilde{m}_{i}\rangle$ for every $i=1,2,\cdots,n-1$. In fact, if it is not the case then $\tilde{m}_{i+1}$ should be a multiple of some $\tilde{m}_j$, where $j\leq i$. It implies that $m_{i+1}$ is a multiple of $m_j$, which is contrary to $m_{i+1}\notin\{m_1,\cdots,m_i\}$. $\Box$

Then it immediately follows from the definition of $\Omega$ that $n\leq\Omega(d,f,f(1))$. Since $m_1,\cdots,m_n$ is arbitrarily chosen, we obtain $L(d,f)\leq\Omega(d,f,f(1))$ from Proposition \[prop:monomial\]. Conversely, we also show that $\Omega(d,f,f(1))\leq L(d,f)$. We consider the sequence $\hat{m}_1,\cdots,\hat{m}_N$ of ${\mathbb{K}}[{\pmb{x}},x_{d+1}]$, which is defined as in equation (\[equ:hatm\]). Then $N=\Omega(d,f,f(1))$. By putting $x_{d+1}=1$, this sequence becomes another sequence $m_1^\prime,\cdots,m_N^\prime$ of ${\mathbb{K}}[{\pmb{x}}]$.

$m_1^\prime,\cdots,m_n^\prime$ is a $f$-generating sequence.

*Proof:* Observe that $\deg(m_i^\prime)\leq\deg(\tilde{m}_i)=f(i)$ for all $i$. Then we only need to prove that $m_i^\prime\notin\{m_1^\prime,\cdots,m_{i-1}^\prime\}$ for all $i$. We assume that $m_i^\prime$ is a multiple of some $m_j^\prime$, where $j<i$. Let $\tilde{m}_i=m_i^\prime x_{d+1}^\alpha$ and $\tilde{m}_j=m_j^\prime x_{d+1}^\beta$, then $\alpha<\beta$ (otherwise $\tilde{m}_i$ would be a multiple of $\tilde{m}_j$). We also have $f(j)<f(i)$; otherwise,f(j)=f(i) and thus $\tilde{m}_i\prec\tilde{m}_j$, which is contrary to $j<i$.

Note that $\deg(m_j^\prime)=f(j)-\beta< f(j)-\alpha<f(i)-\alpha=\deg(m_j^\prime)$. Then we can find some monomial $m'\in\mathcal[{\pmb{x}}]$ such that $\deg(m')=f(j)-\alpha$, and $m'$ is simultaneously a multiple of $m_j^\prime$ and a factor of $m_i^\prime$. Put $\tilde{m}=m'x_{d+1}^\alpha\in\mathcal{M}[{\pmb{x}},x_{d+1}]$, then $\deg(\tilde{m})=f(j)=\deg(\tilde{m}_j)$ and $\tilde{m}\prec \tilde{m}_j$. So $\tilde{m}$ is also in the sequence $\tilde{m}_1,\cdots,\tilde{m}_n$. However, $\tilde{m}_i$ is a multiple of $\tilde{m}$ and thus we find contradiction. $\Box$

$\Omega(d,f,f(1))=N\leq L(d,f)$ follows immediately from this result. Therefore, we obtain the following theorem.

\[thm:bound\] $L(d,f)=\Omega(d,f,f(1))$.

\[exm:incorrect\] For $d=2 ,f(i)=1+i$, the monomial set of the longest monomial ascending chain is $$\{ m_1,m_2,...,m_{11}\}=\{x^2,xy^2,xy,x,y^6,y^5,y^4,y^3,y^2,y,1\},$$ and $L(2,f)=11$.

However, according to Moreno-Socías’s approach [@GMS92], the monomial set is $$\{x^2,xy^2,y^4,y^3,xy,y^2,x,y,1\}$$ and thus $L(2,f)=9$, which is obviously wrong.

More generally, it can be proved that for $f(i)=ai+b$, $$\label{equ:linear-length}L(d,f)=\frac{1}{a}((a+1)\uparrow^{d-2}(a+b+1)-a-b-2), a>0.$$ Here, $\uparrow$ is used to define the Ackermann’s function same as in [@GMS92]. In fact, the length of the $f$-generating sequence defined by (\[equ:hatm\]) has been correctly computed in [@GMS92] by $$N=\frac{1}{a}((a+1)\uparrow^{d-1}(a+b+1)-a-b-2).$$ Note that $\Omega(d-1,f,f(1))=N$, then (\[equ:linear-length\]) follows immediately from this result and Theorem \[thm:bound\].

Termination of multi-path polynomial programs with equality guards {#sec:MPP}
==================================================================

Multi-path polynomial programs
------------------------------

The polynomial programs considered in this paper are formally defined as follows:

\[def:mpp\] A multi-path polynomial program with equality guard has the form $$\label{equ:mpp}
\textsc{ while} \quad (G({\pmb{x}})=0)\quad
  \left\{
   \begin{aligned}
   &{\pmb{x}}\coloneqq {\pmb{A}}_{1}({\pmb{x}});\\
   \parallel\quad &{\pmb{x}}\coloneqq {\pmb{A}}_{2}({\pmb{x}}); \\
   &\vdots\\
   \parallel\quad &{\pmb{x}}\coloneqq {\pmb{A}}_{l-1}({\pmb{x}}); \\
   \parallel\quad &{\pmb{x}}\coloneqq {\pmb{A}}_{l}({\pmb{x}});
   \end{aligned}\right\},$$ where

1.  ${\pmb{x}}\in {\mathbb{K}}^d$ denotes the vector of program variables;

2.  $ G\in {\mathbb{K}}[{\pmb{x}}]$ is a polynomial and $G({{\pmb{x}}})=0$ is the equality typed loop guard;

3.  $ {\pmb{A}}_{i}\in {\mathbb{K}}^d[{\pmb{x}}]$ ($ 1\leq i\leq l$) are vectors of polynomials, describing the transformations on program variables in the loop body;

4.  $``\parallel"$ interprets as a nondeterministic choice between the $l$ transformations.

<!-- -->

1.  The loop guard of MPP (\[equ:mpp\]) can be extended to a more general form $\bigvee_{i=1}^M\bigwedge_{j=1}^{N_i} G_{ij}({\pmb{x}})=0$. However, it is essential to assume that inequalities will never occur in guards, otherwise the termination problem will become undecidable, even not semi-decidable [@bradley:polynomial].

2.  The initial value of ${\pmb{x}}$ is not specified here, and assume it is taken from $\Bbb{K}^{d}$. If the input ${\pmb{x}}$ is subject to semi-algebraic constraints, our decidability result still holds according to [@Tarski51].

\[exm1\] Consider the following MPP (named as `liu1`): $$\textsc{while} \quad (x^2+1-y=0)\quad
  \left\{
   \begin{aligned}
   (x,y) &\coloneqq (x,x^2y);  \\
   \parallel\quad (x,y) &\coloneqq (-x,y);  \\
    \end{aligned}
   \right\}.$$ We have $d=2$, $G(x,y)=x^2-y+1$, ${\pmb{A}}_1(x,y)=(x,x^2y)$ and ${\pmb{A}}_2(x,y)=(-x,y)$.

\[exa:quantum\] A nondeterministic quantum program [@LY14] is of the form: $$\label{equ:quantum}
\textsc{ while} \quad (\textit{Mea}[\rho]=0)\quad
  \left\{
   \begin{aligned}
   \rho &\coloneqq \mathcal{E}_1(\rho);  \\
   \parallel\quad \rho &\coloneqq \mathcal{E}_2(\rho);  \\
   &\vdots\\
   \parallel\quad \rho &\coloneqq \mathcal{E}_{l-1}(\rho); \\
   \parallel\quad \rho &\coloneqq \mathcal{E}_l(\rho);
    \end{aligned}
   \right\}.$$ where

1.  $\rho\in\mathbb{C}^{d^2}$ is a $d\times d$ density matrix.

2.  $\textit{Mea}=\{M_0,M_1\}$ is a two-outcome quantum measurement, where $M_0$ and $M_1$ are $d\times d$ complex matrices.

3.  $\mathcal{E}_i$ are quantum super-operators, which are linear transformations over $\mathbb{C}^{d^2}$.

In this example, ${\pmb{x}}=\rho$, $G({\pmb{x}})={\rm tr}(M_0\rho M_0^\dagger)$ and ${\pmb{A}}_i=\mathcal{E}_i$, where ${\rm tr}(M)$ is the trace of a matrix $M$, and $M^\dagger=(M^T)^*$ is the complex conjugate of the transpose of $M$. Clearly, it is a multi-path linear program over $\mathbb{C}^{d^2}$. In [@LY14], the non-terminating inputs of this program plays a key role in deciding the termination of quantum programs.

Execution of MPPs
-----------------

Given an input ${\pmb{x}}$, the behavior of MPP (\[equ:mpp\]) is determined by the choices of ${\pmb{A}}_i\ (1\leq i\leq l)$ nondeterministically, and all the possible executions form a tree.

The execution tree of MPP (\[equ:mpp\]) for an input ${\pmb{x}}\in {\mathbb{K}}^d$ is defined inductively as follows:

1.  the root is the input value of ${\pmb{x}}$;

2.  for any node $ \widetilde{{\pmb{x}}}$, it is a leaf node if $ G(\widetilde{{\pmb{x}}})\neq 0$; otherwise, $\widetilde{{\pmb{x}}}$ has $l$ children ${\pmb{A}}_{1}(\widetilde{{\pmb{x}}})$, ${\pmb{A}}_{2}(\widetilde{{\pmb{x}}}),\cdots,{\pmb{A}}_{l}(\widetilde{{\pmb{x}}})$, and there is a directed edge from $\widetilde{{\pmb{x}}}$ to ${\pmb{A}}_{i}(\widetilde{{\pmb{x}}})$, labeled by $i$, for $1\leq i\leq l$.

Now we consider the paths in the execution tree. Denote by $\Sigma=\{1,2,...,l\}$ the set of indices of the transformations ${\pmb{A}}_{i}$ ($1\leq i\leq l$). For any string $\sigma=a_1 a_2\cdots a_s\in\Sigma^*$, we write $|\sigma|=s$ for its length and $\operatorname{Pre}(\sigma)=\{a_1\cdots a_i\mid i=0,1,\cdots,s-1\}$ for the set of its proper prefixes. The concatenation of two strings $\sigma$ and $\tau=b_1\cdots b_t$ is written as $\sigma\tau=a_1\cdots a_sb_1\cdots b_t$. For simplicity, we put ${\pmb{A}}_\sigma={\pmb{A}}_{a_s}\circ\cdots\circ {\pmb{A}}_{a_2}\circ {\pmb{A}}_{a_1}$ and ${\pmb{A}}_\epsilon=\mathbf{id}$ (i.e ${\pmb{A}}_\epsilon({\pmb{x}})\equiv{\pmb{x}}$) for the empty string $\epsilon$. Then ${\pmb{A}}_{\sigma\tau}={\pmb{A}}_{\tau}\circ{\pmb{A}}_{\sigma}$. Similarly, for an infinite sequence $\sigma=a_1 a_2\cdots\in\Sigma^\omega$ we define $|\sigma|=\infty$ and $\operatorname{Pre}(\sigma)=\{a_1\cdots a_i\mid i=0,1,\cdots\}$. And the concatenation of a string $\tau=b_1\cdots b_t$ and $\sigma$ is defined as $\tau\sigma=b_1\cdots b_ta_1a_2\cdots\in\Sigma^\omega$.

Then any finite or infinite path from the root in the execution tree can be identified by a finite or infinite string over $\Sigma$. Specifically, for any $\sigma=a_1a_2\cdots\in\Sigma^*\cup\Sigma^\omega$, the corresponding execution path is as follows: $${\pmb{x}}\xrightarrow{{\pmb{A}}_{a_1}}{\pmb{A}}_{a_1}({\pmb{x}})\xrightarrow{{\pmb{A}}_{a_2}}{\pmb{A}}_{a_2}({\pmb{A}}_{a_1}({\pmb{x}}))\xrightarrow{{\pmb{A}}_{a_3}}\cdots.$$ Moreover, any node in the execution tree is of the form ${\pmb{A}}_\sigma({\pmb{x}})$, where $\sigma\in\Sigma^*$ represents the history of the execution. Its ancestor nodes are ${\pmb{A}}_\tau({\pmb{x}})$ ($\tau\in\operatorname{Pre}(\sigma)$). According to the definition of execution tree, we have $G({\pmb{A}}_\tau({\pmb{x}}))=0$. Then all the paths of the execution tree are given as follows:

The set of execution paths of MPP (\[equ:mpp\]) for an input ${\pmb{x}}\in \mathbb K^d$ is defined as $$\operatorname{Path}({\pmb{x}})=\{\sigma\in\Sigma^*\cup\Sigma^\omega\mid \forall \tau\in \operatorname{Pre}(\sigma):\ G({\pmb{A}}_\tau({\pmb{x}}))=0\}.$$

For any path $\sigma$, we write the set of corresponding polynomials as $T_\sigma^-=\{G\circ A_\tau\mid \tau\in \operatorname{Pre}(\sigma)\}$. Then it is obvious that $$\label{equ:path-Z}\sigma\in\operatorname{Path}({\pmb{x}})\Leftrightarrow {\pmb{x}}\in Z(T_\sigma^-).$$

Termination of MPPs
-------------------

Now we define the termination of MPP (\[equ:mpp\]). Intuitively, that a program will terminate means that its execution will be accomplished with a finite number of runs. It actually means that the execution tree is finite (namely, has only a finite number of nodes). Formally, we have

\[def:Termi\]

1.  For an input ${\pmb{x}}\in {\mathbb{K}}^d$, MPP (\[equ:mpp\]) is called terminating if $|\operatorname{Path}({\pmb{x}})|<\infty$ (i.e. $\operatorname{Path}({\pmb{x}})$ is a finite set); otherwise it is called non-terminating.

2.  The set of non-terminating inputs (**NTI**) of MPP (\[equ:mpp\]) is defined as $D=\{{\pmb{x}}\in{\mathbb{K}}^d\mid |\operatorname{Path}({\pmb{x}})|=\infty\}.$

By applying the König’s lemma [@koenig] we know that the execution tree is infinite if and only if it contains an infinite path, i.e., $$\label{equ:konig}|\operatorname{Path}({\pmb{x}})|=\infty \Leftrightarrow \operatorname{Path}({\pmb{x}})\cap\Sigma^\omega\neq\emptyset$$ for all ${\pmb{x}}\in{\mathbb{K}}^d$. Then the **NTI** can be expressed as $$\label{equ:D}D=\bigcup_{\sigma\in\Sigma^\omega}Z(T_\sigma^-).$$

We also figure it out when the program terminates within a fixed number of iterations of the while loop.

\[def:Termi\]$\ $

1.  MPP (\[equ:mpp\]) is called $n$-terminating for an input ${\pmb{x}}\in {\mathbb{K}}^d$, if $|\sigma|\leq n$ for all $\sigma\in\operatorname{Path}({\pmb{x}})$.

2.  The set of $n$-non-terminating inputs ($n$-**NTI**) of MPP (\[equ:mpp\]) is defined as $$D_n=\{{\pmb{x}}\in{\mathbb{K}}^d\mid \exists \sigma\in\operatorname{Path}({\pmb{x}}):\ |\sigma|>n\}.$$

The $n$-**NTI** can be expressed in a similar way to expression (\[equ:D\]). For clarity, we put $T_\sigma=T_\sigma^-\cup\{G\circ{\pmb{A}}_\sigma\}$, then it is easy to verify that $T_{\sigma a}^-=T_{\sigma}$ for any $\sigma\in\Sigma^*$ and $a\in\Sigma$. Obviously, we have

$$\label{equ:Dn}D_n=\bigcup_{|\sigma|=n}Z(T_\sigma).$$

Decidability of the termination problem {#sec:Deci}
=======================================

In this section we prove the main result of this paper, i.e., it is decidable if an MPP of form (\[equ:mpp\]) is terminating on a given input ${\pmb{x}}$. In fact we propose an algorithm to compute the NTI $D$ for an MPP. Then it suffices to decide whether ${\pmb{x}}\in D$.

Characterization of the NTI
---------------------------

We investigate the mathematical structures of the NTI first, which will imply the decidability of the termination problem.

\[thm:Dn\_D\]

1.  \[ite:algebraic\] For any $n\geq 0$, $D_n$ is an algebraic set.

2.  \[ite:chain\] The algebraic sets $D_i$s form a descending chain $$\label{equ:chain}D_0\supseteq D_1\supseteq\cdots\supseteq D_n\supseteq\cdots,$$ and there exists a least $N$ such that $$0\leq N \leq L(d,F) \wedge \forall n\in \Bbb{N}. D_N=D_{N+n},$$ where $F(i) {\hat{=}}ab^i$, in which $a = \deg(G)$, and $b=\max \{ \deg(A_1), $ $ \cdots,\deg(A_l)\}$.

3.  \[ite:D=DN\] $D=D_N$, i.e., the fixed point of the chain is exactly the NTI.

*Proof:* Clause \[ite:algebraic\] is directly from equation (\[equ:Dn\]), and clause \[ite:chain\] is directly from the definitions, Proposition \[prop:monomial\] and Theorem \[thm:bound\]. To prove clause \[ite:D=DN\], we only need to prove $D_N\subseteq D$, since $D\subseteq D_n$ ($\forall n\geq 0$) is easily verified from the definition. For any $n\geq N$ and any ${\pmb{x}}\in D_N=D_n$, we have $\exists \sigma\in\operatorname{Path}({\pmb{x}}): |\sigma|>n$. Therefore, $|\operatorname{Path}({\pmb{x}})|=\infty$ and ${\pmb{x}}\in D$. $\Box$

For any $X\subseteq {\mathbb{K}}^d$, we define its *backward subset* under MPP (\[equ:mpp\]) as $\operatorname{Back}(X)\triangleq\bigcup_{a\in\Sigma}(X\cap{{\pmb{A}}_a}^{-1}(X)),$ i.e., $\{x\in X \mid \exists a\in \Sigma.\, {\pmb{A}}_a(x)\in X\}$.

\[lem:2\] For any $n\geq 0$, $\operatorname{Back}(D_n)=D_{n+1}$.

*Proof:* First, we prove that $D_{n+1}\subseteq \operatorname{Back}(D_n)$. For any ${\pmb{x}}\in D_{n+1}$, it follows from (\[equ:Dn\]) that ${\pmb{x}}\in Z(T_\sigma)$ for some $\sigma=a_1\cdots a_{n+1}\in\Sigma^{n+1}$. Then it is easily verified from the definition that ${\pmb{A}}_{a_1}({\pmb{x}})\in Z(T_{a_2\cdots a_{n+1}})\subseteq D_n$. Noting that ${\pmb{x}}\in D_{n+1}\subseteq D_n$, we have ${\pmb{x}}\in D_n\cap{\pmb{A}}_{a_1}^{-1}(D_n)\subseteq \operatorname{Back}(D_n)$.

Conversely, to prove $\operatorname{Back}(D_n)\subseteq D_{n+1}$, suppose ${\pmb{x}}\in \operatorname{Back}(D_n)$. So, we have ${\pmb{x}}\in D_n$ and ${\pmb{x}}\in{\pmb{A}}_a^{-1}(D_n)$ for some $a\in\Sigma$. Then $G({\pmb{x}})=0$ and ${\pmb{A}}_a({\pmb{x}})\in Z(T_\sigma)$ for some $\sigma\in\Sigma^n$. As $\{G\}\cup\{f\circ {\pmb{A}}_a\mid f\in T_\sigma\}=T_{a\sigma}$, we have ${\pmb{x}}\in Z(T_{a\sigma})\subseteq D_{n+1}$. This completes the proof. $\Box$

A direct consequence of Lemma \[lem:2\] is that the descending chain (\[equ:chain\]) is strict, namely,

\[cor:strict\] $D_0\supset D_1\supset\cdots\supset D_N=D_{N+1}=\cdots$.

We say a set $X\subseteq{\mathbb{K}}^d$ is transitive under MPP (\[equ:mpp\]), if it can be finitely decomposed as $X=X_1\cup X_2\cup\cdots\cup X_n$ satisfying that for any $i\in\{1,2,\cdots,n\}$, there exists some $a\in\Sigma$ and $j\in\{1,2,\cdots,n\}$ such that ${\pmb{A}}_a(X_i)\subseteq X_j$.

\[lem:trans\] Let $X\subseteq D_0$ be transitive, then $X\subseteq D$.

*Proof:* The transitivity of $X=X_1\cup X_2\cup\cdots\cup X_n$ allows existence of two functions $a:\{1,2,\cdots,n\}\rightarrow\Sigma$ and $b:\{1,2,\cdots,n\}\rightarrow\{1,2,\cdots,n\}$ such that ${\pmb{A}}_{a(i)}(X_i)\subseteq X_{b(j)}$ for all $i\in\{1,2,\cdots,n\}$. Now for any ${\pmb{x}}\in X$, ${\pmb{x}}\in X_i$ for some $i\in\{1,\cdots,n\}$. Putting $b_k=b^k(i)$ and $a_k=a(b^k(i))$ for all $k\geq 0$, we have the path: $$X_i=X_{b_0}\xrightarrow{{\pmb{A}}_{a_0}} X_{b_1}\xrightarrow{{\pmb{A}}_{a_1}} X_{b_2}\xrightarrow{{\pmb{A}}_{a_2}}\cdots$$ satisfying ${\pmb{A}}_{a_k}(X_{b_k})\subseteq X_{b_{k+1}}$. Then for $\sigma=a_1a_2\cdots\in\Sigma^\omega$ and any $\tau\in\operatorname{Pre}(\sigma)$, we have ${\pmb{A}}_\tau(X_i)=X_{b_{|\tau|}}\subseteq X\subseteq D_0$. So ${\pmb{A}}_\tau({\pmb{x}})\in D_0=Z(\{G\})$, and thus $(G\circ{\pmb{A}}_\tau)({\pmb{x}})=0$. Therefore $\sigma\in\operatorname{Path}({\pmb{x}})$ and ${\pmb{x}}\in D$.

Moreover, we note that $\{b_0,b_1,\cdots\}\subseteq\{1,2,\cdots,n\}$ has at most $n$ elements, then there exists some $j\in\{0,1,\cdots,n-1\}$ and $p\in\{1,\cdots,n\}$ such that $b_j=b_{j+p}$. So for all $k\geq 0$ and $t\geq j$, $b_{t+kp}=b^{t+kp}(i)=b^t(i)=b_t$. We have: $$\sigma=(a_1a_2\cdots a_{j-1})(a_ja_{j+1}\cdots a_{j+p})^\omega. \, \Box$$

$D$ is the greatest transitive subset of $D_0$.

*Proof:* According to Lemma \[lem:trans\], it suffices to prove that $D$ is transitive. In fact we use the irreducible decomposition $D=Y_1\cup Y_2\cup\cdots\cup Y_n$, and prove the transitivity.

For any $i\in\{1,2,\cdots,n\}$, we have $$Y_i\subseteq D=\operatorname{Back}(D)\subseteq\bigcup_{a\in\Sigma}{{\pmb{A}}_a}^{-1}(D)=\bigcup_{a\in\Sigma}\bigcup_{j=1}^n{\pmb{A}}_a^{-1}(Y_j).$$ Note that $Y_i$ is irreducible and for any $a\in\Sigma$ and any algebraic set $X=Z(T)$, ${\pmb{A}}_a^{-1}(X)=Z(\{f\circ{\pmb{A}}_a \mid f\in T\})$ is also algebraic. Then there exists some $a\in\Sigma$ and $j\in\{1,2,\cdots,n\}$ such that $Y_i\subseteq{{\pmb{A}}_a}^{-1}(D)$, i.e., ${\pmb{A}}_a(Y_i)\subseteq Y_j$. $\Box$

For any ${\pmb{x}}\in D$, $\operatorname{Path}({\pmb{x}})$ has an infinite path with a regular form $\sigma=\sigma_0\sigma_1^\omega$, where $\sigma_0,\ \sigma_1\in\Sigma^*$.

Algorithms and complexity analysis
----------------------------------

Now we are ready to formally present algorithms for deciding the termination of MPP (\[equ:mpp\]), i.e., algorithms to compute $D$, or more precisely, compute a set $B$ of generating polynomials of $D$ (i.e., $D=Z(B)$); thus whether the program to be terminated for a given input set $X$, which is a semi-algebraic set defined by a polynomial formula $\phi({\pmb{x}})$ is equivalent to the unsatisfiability of $\bigwedge_{f\in B}(f=0) \wedge \phi({\pmb{x}})$, which is decidable [@Tarski51]. An algorithm of computing $D$ can be directly obtained from Theorem \[thm:Dn\_D\]. In fact, equation (\[equ:Dn\]) implies that $\prod_{\sigma\in\Sigma^n}T_\sigma$ is a set of generating polynomials of $D_n$ for every $n\in{\mathbb{N}}$. So, if we find the number $N=\min\, \{n\geq0\mid D_n=D_{n+1}\}$, which is bounded by $L(d,F)$, then the set of generating polynomials for $D_N=D$ is exactly what we want. The detailed procedure is presented as Algorithm \[alg:NTI\], in which $D_n=D_{n+1}$ is checked by the following result:

$D_n=D_{n+1}$ iff $f\in I(Z(T_\sigma))$, for all $\sigma\in\Sigma^n$ and all $f\in\prod_{\tau\in\Sigma^{n+1}}T_\tau$.

*Proof:* Since $D_n$ is always a superset of $D_{n+1}$, from equation (\[equ:Dn\]) we have $$D_n=D_{n+1}\Leftrightarrow \forall \sigma\in\Sigma^n:\ Z(T_\sigma)\subseteq \bigcup_{\tau\in\Sigma^{n+1}}Z(T_\tau).$$ Moreover, $\bigcup_{\tau\in\Sigma^{n+1}}Z(T_\tau)=Z(\prod_{\tau\in\Sigma^{n+1}}T_\tau)$. This completes the proof. $\Box$

**set of** polynomial sets $S_0\leftarrow \emptyset$ **set of** polynomial sets $S_1\leftarrow \{T_\epsilon\}$ **bool** $b\leftarrow {\rm False}$ **bool** $c\leftarrow {\rm True}$ **integer** $n\leftarrow -1$ $n$\

#### Complexity of Algorithm \[alg:NTI\]:

By Thorem \[thm:Dn\_D\], the **while** loop terminates after $N$ iterations, which is bounded by $L(d,F)$. In the $n$-th iteration, there are mainly two computation steps: the first one is to add the polynomial set $T_\tau$ into $S_1$ for each $\tau\in\Sigma^{n+1}$ and thus will be executed $O(|\Sigma^{n+1}|)=O(l^{n+1})$ times; and the second step is to check the condition $f\in I(Z(T_\sigma))$ for all $\sigma\in\Sigma^n$ and all $f\in\prod_{\tau\in\Sigma^{n+1}}T_\tau$, so the number of times of the membership checking is $O(l^n(n+2)^{l^{n+1}})$. Thus, the time complexity in total is $O(l^N(N+2)^{l^{N+1}})$ (which is expressed in the number of runs of membership checking for radical ideals).

In Algorithm \[alg:NTI\], the set of generating polynomials of $D_n$ is directly constructed as $\prod_{\sigma\in\Sigma^n}T_\sigma$ and is generally a huge set. To find a more efficient algorithm, we consider the generating polynomials defined as $B_0\triangleq\{G\}$ and $B_{n+1}\triangleq B_n\cup\prod_{a=1}^l(B_n\circ {\pmb{A}}_a)$ for $n=0,1,\cdots$. Then,

$D_n=Z(B_n)$ for all $n\geq 0$. Here $B_n\circ{\pmb{A}}_a\triangleq\{f\circ{\pmb{A}}_a\mid f\in B_n\}$.

*Proof:* It is easy to verify that $D_n=Z(B_n)\Rightarrow{\pmb{A}}_a^{-1}(D_n)=Z(B_n\circ {\pmb{A}}_a)$. Then employing Lemma \[lem:2\], the result can be proved immediately by induction on $n$. $\Box$

The advantage of constructing $B_n$ in this recursion way is that we can compute the reduced Gröbner basis of $B_n$ during the procedure so that the generating set of $D_n$ could be kept as small as possible. Using this method, a more efficient algorithm for computing the NTI is given in Algorithm \[alg:NTIgb\], whose correctness is guaranteed by the following result:

$\forall n\in \Bbb{N}. D_{\hat{N}}=D_{\hat{N}+n}$ for $\hat{N}\triangleq\min\, \{n\mid B_n=B_{n+1}\}$, and $\hat{N} \leq L(d,F)$, where $L(d,F)$ is same as in Theorem \[thm:Dn\_D\].

*Proof:* Note that $B_n\subseteq B_{n+1}$ for all $n$, so $\hat{N}$ is well-defined due to Theorem \[thm:asc-chain\], and bounded by Proposition \[prop:monomial\] and Theorem \[thm:bound\]. $\Box$

**set of** polynomials $B \leftarrow \{G\}$ **polynomial** $f \leftarrow 0$ **polynomial** $r \leftarrow 0$ **integer** $n \leftarrow -1$ **bool** $c \leftarrow {\rm True}$ $n$, $B$;\

#### Complexity of Algorithm \[alg:NTIgb\]:

There are $\hat{N}$ iterations of **while** loop in the execution. In the $n$-th iteration, there are at most $|B_{n+1}|$ polynomials to be added into $B$. Note that $|B_n|=O(2^{l^{n-1}})$. So, the time complexity is $O(2^{l^{\hat{N}}})$.

From the definitions, it is clear that the output $N$ of Algorithm \[alg:NTI\] is not greater than the output $\hat{N}$ of Algorithm \[alg:NTIgb\] for the same inputs. Moreover, we use the example below to show that $N$ may be different from $\hat{N}$. $$\textsc{while} \quad (x^2+y^2=0)\quad
  \left\{(x,y) \coloneqq (x,x+y);\right\}.$$ For this program as input, the output $N=0$ (for ${\mathbb{K}}=\mathbb{R}$) or $1$ (for ${\mathbb{K}}=\mathbb{C}$), while $\hat{N}=2$.

Polynomial guarded commands {#sec:pgc}
===========================

In this section, we consider to extend the above results to a more general model of polynomial programs, called *polynomial guarded commands* (PGCs). PGCs are specific guarded commands [@dijkstra75], thereof all expressions are polynomials, and guards are polynomial equalities. Formally,

\[def:pgc\] A PGC with equality guards has the form $$\label{equ:pgc}
    \begin{array}{lcl}
  \textsc{do} &  &  G_1({\pmb{x}})=0 \longrightarrow {\pmb{x}}\coloneqq {\pmb{A}}_{1}({\pmb{x}});\\
     &  \parallel & G_2({\pmb{x}})=0 \longrightarrow {\pmb{x}}\coloneqq {\pmb{A}}_{2}({\pmb{x}}); \\
 &   &  \quad \quad \vdots\\
  &  \parallel & G_{l-1}({\pmb{x}})=0 \longrightarrow {\pmb{x}}\coloneqq {\pmb{A}}_{l-1}({\pmb{x}}); \\
  &  \parallel & G_l({\pmb{x}})=0 \longrightarrow {\pmb{x}}\coloneqq {\pmb{A}}_{l}({\pmb{x}}); \\
  \textsc{od}, & &
   \end{array}$$ where

1.  ${\pmb{x}}\in {\mathbb{K}}^d$ denotes the vector of program variables;

2.  $ G_i\in {\mathbb{K}}[{\pmb{x}}]$ is a polynomial and $G_i({{\pmb{x}}})=0$ is a guard. As discussed before, a more general guard of the form $\bigvee_{i=1}^M\bigwedge_{j=1}^{N_i} G_{ij}({\pmb{x}})=0$ can be easily reduced to this simple case by letting $G({\pmb{x}})=\prod\limits_{i=1}^M\sum\limits_{j=1}^{N_i} G_{ij}^2({\pmb{x}})$, where $G_{ij}({\pmb{x}})$ are polynomials;

3.  $ {\pmb{A}}_{i}\in {\mathbb{K}}^d[{\pmb{x}}]$ ($ 1\leq i\leq l$) are vectors of polynomials, describing update of program variables in the guarded command.

#### Discussions

1.  Informally, the meaning of a PGC (\[equ:pgc\]) is that given an input ${\pmb{x}}$, whenever some guards $G_i$ are satisfied, one of them is nondeterministically chosen and the corresponding assignment is taken, then the procedure is repeated until none of the guards holds.

2.  Obviously, if all $G_i({\pmb{x}})$ are same, then the PGC is degenerated to an MPP; and if $G_i({\pmb{x}})=0\wedge G_j({\pmb{x}})=0$ has no real solution for any $i\neq j$, then the choice among these updates becomes deterministic.

3.  Notice that the deterministic choice derived from (\[equ:pgc\]) cannot be used to define the general deterministic choice $$\textsc{if}~ G({\pmb{x}})=0~ \textsc{then} ~{\pmb{x}}:= A_1({\pmb{x}})~ \textsc{else} ~ {\pmb{x}}:= A_2({\pmb{x}}),$$ as it is equivalent to $$\textsc{if}~ G({\pmb{x}})=0 \longrightarrow {\pmb{x}}:= A_1({\pmb{x}})~ \parallel ~  G({\pmb{x}})\neq 0 \longrightarrow {\pmb{x}}:= A_2({\pmb{x}}) ~~\textsc{fi},$$ which contains $G({\pmb{x}})\neq 0$. In [@Muller-Olm], the authors proved that PCP (Post Correspondence Problem) can be encoded into the extension of PGCs by allowing polynomial inequations in guards, so this means that the termination problem of such an extension is undecidable.

Given an input ${\pmb{x}}$, the set of paths starting from ${\pmb{x}}$ is defined by $$\begin{aligned}
      \textit{Path}({\pmb{x}}) & = &  \{\sigma \in \Sigma^*\cup \Sigma^{\omega} \mid \forall \tau\in \operatorname{Pre}(\sigma),i\in \Sigma.\, \\
      &  & \quad \quad  \tau\cdot i\in \operatorname{Pre}(\sigma) \Rightarrow G_i(A_{\tau}({\pmb{x}}))=0\}.
      \end{aligned}$$ For a path $\sigma \in \textit{Path}({\pmb{x}})$, the set of corresponding polynomials $T^-_{\sigma}$ is $\{G_i(A_{\tau}) \mid \tau\cdot i \in \operatorname{Pre}(\sigma)\}$. Similarly, we have $$\sigma \in \textit{Path}({\pmb{x}}) \Leftrightarrow {\pmb{x}}\in Z(T^-_{\sigma}).$$

We say a PGC is *non-terminating* for a given input ${\pmb{x}}$ if there exists $\sigma \in \textit{Path}({\pmb{x}})$ such that $|\sigma|=\infty$, otherwise *terminating*. We still denote the set of non-terminating inputs of the PGC by $D$.

Similar to MPP  (\[equ:mpp\]), we introduce the notion of *$n$-Termination* to PGC as follows:

\[def:Termi-pgc\]$\ $

1.  PGC (\[equ:pgc\]) is called $n$-terminating for an input ${\pmb{x}}\in {\mathbb{K}}^d$, if $|\sigma|\leq n$ for all $\sigma\in\operatorname{Path}({\pmb{x}})$.

2.  The set of $n$-non-terminating inputs ($n$-NTI) of PGC (\[equ:pgc\]) is defined as $$D_n=\{{\pmb{x}}\in{\mathbb{K}}^d\mid \exists \sigma\in\operatorname{Path}({\pmb{x}}):\ |\sigma|>n\}.$$

Regarding $n$-NTI $D_n$, we have the following properties:

\[thm:chain-pgc\]

1.  \[pgc-ite:algebraic\] For any $n\geq 0$, $D_n$ is an algebraic set.

2.  \[pgc-ite:chain\] $D_i$, $i\in \Bbb{N}$, form a descending chain of algebraic sets, i.e., $$\label{equ:chain-1}D_0\supseteq D_1\supseteq\cdots\supseteq D_n\supseteq\cdots$$ and there exists a least $M$ such that $$0\leq M \leq L(d,E) \wedge \forall n\in \Bbb{N}. D_M=D_{M+n},$$ where $E(i) {\hat{=}}cd^i$, in which $c=\max \{ \deg(G_1), \cdots, \deg(G_l)\}$ and $d=\max\{\deg(A_1), \cdots, \deg(A_l)\}$.

3.  \[pgc-ite:D=DN\] $D=D_M$ and $$\label{equ:chain-2}D_0\supset D_1\supset\cdots\supset D_M=D_{M+1} =\cdots$$

*Proof:* Similar to Theorem \[thm:Dn\_D\]. $\Box$

Based on Theorem \[thm:chain-pgc\], an algorithm similar to Algorithm \[alg:NTI\] for computing the NTI of a given PGC can be obtained without any substantial change.

Implementation and experimental results {#sec:case}
=======================================

We have implemented a procedure[^1] in *Maple* according to the presented algorithms for discovering non-terminating inputs for MPPs. The procedure takes an MPP as input, and gives the minimum integer $N$ subject to $D_N$ as a fixed point of the descending chain of algebraic sets. In particular, the essential computations of Gröbner basis and membership of ideals attributes to the `Groebner` package and the `PolynomialIdeals` package, respectively. In what follows we demonstrate our approach by some motivating examples, which have been evaluated on a 64-bit Windows computer with a 2.93GHz Intel Core-i7 processor and 4GB of RAM.

`liu2`$\quad$ $\ \;\textsc{while} \quad (x+y=0)\quad
  \left\{
   \begin{aligned}
   (x,y) &\coloneqq (x+1,y-1);  \\
   \parallel\, (x,y) &\coloneqq (x^2,y^2);  \\
    \end{aligned}
   \right\}$\
`loop`$\quad$ $\ \;\textsc{while} \quad ((x-2)^2+y^2=0)\quad
  \left\{
   \begin{aligned}
   (x,y) &\coloneqq (x+4,y);  \\
   \parallel\, (x,y) &\coloneqq (x+2,y+1);  \\
    \end{aligned}
   \right\}$\
`liu3`$\quad$ $\ \;\textsc{while} \quad ((x-1)(x-2)=0)\quad
  \left\{
   \begin{aligned}
   x &\coloneqq 1-x^2;  \\
   \parallel\, x &\coloneqq x+1;  \\
    \end{aligned}
   \right\}$\
`ineq`$\quad$ $\ \;\textsc{while} \quad (x-y^2=0) \quad
  \left\{
   \begin{aligned}
   (x,y) &\coloneqq (x-3,y-3);  \\
   \parallel\, (x,y) &\coloneqq (x-3y,y^2+x^2);  \\
   \parallel\,  (x,y) &\coloneqq (1,0);  \\
    \end{aligned}
   \right\}$\
`prod`$\quad$ $\begin{array}{ll}
\textsc{while} \quad ((x-1)^2+(y-1)^2+z^2=0) \\
  \left\{
   \begin{aligned}
   (x,y,z) &\coloneqq (2x,(y-1)/2,x+z);  \\
   \parallel\, (x,y,z) &\coloneqq (2x,y/2,z);  \\
    \end{aligned}
   \right\}
\end{array} $\
`liu4`$\quad$ $\begin{array}{ll}
\textsc{while} \quad (x-z^3=0 \vee y-z^2=0) \\
  \left\{
   \begin{aligned}
   (x,y,z) &\coloneqq (x,y+2z+1,z+1);  \\
   \parallel\, (x,y,z) &\coloneqq (x-3y+3z-1,y+2z-1,z-1);  \\
    \end{aligned}
   \right\}
\end{array} $\
`var4`$\quad$ $\begin{array}{ll}
\textsc{while} \quad (w+x+y+z=0) \\
   \left\{
   \begin{aligned}
   (w,x,y,z) &\coloneqq (w-2,x,y+2z+1,z+w);  \\
   \parallel\, (w,x,y,z) &\coloneqq (w^2,x-3y+3z-1,y+2z-1,z-1);  \\
    \end{aligned}
   \right\}
\end{array}$\

  ------------- --------------------- --- --- --- ------------------- ---------------------
                                                                      
  (lr)[6-7]{}                                       Algm. \[alg:NTI\]   Algm. \[alg:NTIgb\]
  `running`     \[$\,\star\,$\]        2   2   1                0.003                 0.003
  `liu1`        [@LXZZ14]              2   2   0                0.015                 0.001
  `liu2`        [@LXZZ14]              2   2   0                0.001                 0.001
  `loop`        [@CousotCousot77-1]    2   2   2             1088.669                 0.004
  `liu3`        [@LXZZ14]              1   2   2             1108.720                 0.002
  `ineq`        \[$\,\star\,$\]        2   3   2                   TO                 0.030
  `prod`        [@rodriguez:simple]    3   2   4                   TO                 0.928
  `liu4`        [@LXZZ14]              3   2   4                   TO                 0.544
  `var4`        \[$\,\star\,$\]        4   2   5                   TO                 4.591
  ------------- --------------------- --- --- --- ------------------- ---------------------

  : Evaluation results of some examples[]{data-label="tab1"}

\

Legends: the first two columns specify the name of the program, and the citation from where the program was adapted (the entry \[$\,\star\,$\] is for the examples developed by the authors). $d$ indicates the number of variables in the loop, $l$ represents the number of paralleled branches in the body of the loop, and the last two columns give the time (in seconds) taken by Algorithm \[alg:NTI\] and Algorithm \[alg:NTIgb\], respectively. Timeouts here are set to 1200 s (20 minutes) and are represented by TO. In addition, $\hat{N}=N$ for all the examples in this table.

Table \[tab1\] illustrates the experimental results on a bunch of examples presented so far, based on which one can draw the following conclusions:

1.  The implementation of Algorithm \[alg:NTIgb\] in *Maple* works quite efficient: it solves all the examples successfully over 6 s in total, and performs better than Algorithm \[alg:NTI\].

2.  In particular, Algorithm \[alg:NTIgb\] behaves more robust as no timeouts are obtained. While for Algorithm \[alg:NTI\], it tends to be strenuous when $l$ or the expected $N$ reaches 2, and gets timeouts with cases of $N \ge 3$.

3.  It can be observed that $N$ is roughly equal to $d$ in these examples, at least not getting too large w.r.t $d$, which well explains that despite with a worst-case complexity double-exponentially to $N$, Algorithm \[alg:NTIgb\] exhibits a promising performance in practice.

4.  Note in Example `ineq` that $x-y^2=0 \Rightarrow x \ge 0$, thus the generated NTI are also the non-terminating inputs of the program where we replace the condition $x-y^2=0$ by $x \ge 0$. This demonstrates that even for more general loops with inequality conditions, our approach provides an effective way to find the terminating counterexamples.

It is also worth highlighting that both Example `liu2` and `liu3` can not be handled in [@LXZZ14] by using the under/over-approximations of NTI, whereas they are successfully solved by the approach developed in this paper.

Conclusion {#sec:conc}
==========

In this paper, we proved that 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, is decidable. The complexity of the decision procedure is double exponential on the length of the descending chain of algebraic sets $D_n$ (i.e., the set of inputs that are non-terminating after $n$ iteration), which is bounded using Hilbert’s function and Macaulay’s theorem. To the best of our knowledge, the family of polynomial programs that we consider should be the largest one with a decidable termination problem so far. The experimental results indicate the efficiency although its theoretical complexity is quite high.

Our approach can be extended to invariant generation of polynomial programs, which is dual to the termination problem. By which, a complete approach for generating all invariants represented as polynomial equations is under consideration. Comparing with Rodríguez-Carbonell and Kapur’s result [@rodriguez:simple], the *solvability* assumption can be dropped. We will report these results in another paper.

Regarding future work, it is interesting to investigate if our approach works for nested polynomial loops.

[^1]: Both of the codes and the case studies in this section can be found at <http://lcs.ios.ac.cn/~chenms/tools/MPPs.tar.bz2>
