随着信息技术的迅猛发展,嵌入式系统在人类生活中发挥着越来越大的作用,嵌入式软件在其中所占有的比重也越来越大.因此,嵌入式软件的可靠性将变得更加重要.诸如航空、航天、军事、交通、医疗等关键应用领域都对嵌入式系统的可靠性和安全性要求非常高,任何错误的发生都可能带来灾难性后果.这些系统被称为攸关安全系统.

嵌入式系统具有3个重要属性,即可达性、终止性、不变式.可达性是指系统能否从给定状态到达另一个可接受状态,某些混成系统的可达性被证明是能用计算机代数工具来检验的;不变式则是用于描述在程序运行时保持函数不变性质的逻辑断言;而终止性是研究系统中是否会发生死循环,不包括终止性分析的验证被称为程序的部分正确性证明.因此,程序的终止性分析是确保程序完全正确性的必要基础.

尽管程序的终止性问题早已被证明是不可判定的^[12],但对其进行研究不仅具有理论意义,更具有实际意义.当前,国际上主要通过合成秩函数来进行循环终止性分析,并取得了一些突破.例如,Poldelski等人^[15]基于线性代数理论提出了完备的一类线性程序线性秩函数生成理论,并开发出工具RANKFINDER,该工具是他们与微软联合开发的程序终止性分析工具TERMINATOR的核心部分^[1].此外,利用Farkas引理及多面体理论,针对这类线性循环程序,文献^{[10, 11]}呈现了线性秩函数合成算法.最近,文献^[4]研究了现有几种秩函数生成算法的时间复杂 度.在2013年,文献^[5]进一步分析了程序变量在整数集合上取值时,这类线性程序的线性秩函数合成方法,并研究了这类问题的复杂度.

近年来,计算机代数和实代数理论已逐渐被应用于程序自动验证.例如,我国科学家杨路、夏壁灿、詹乃军和周巢尘等人将秩函数和不变式的计算归约为半代数系统的求解,并运用实代数工具DISCOVERER提出了多项式不等式型不变式和非线性秩函数生成方法^{[9, 20]}.不同于文献^[14]中的方法,他们的方法能够精确回答循环程序是否有给定模板的秩函数或不变式.合成秩函数是验证循环程序终止性的一条重要途径,但是秩函数的存在是循环可终止的充分而非必要条件^{[5, 7]}.人们容易构造一个循环程序,它是可终止的,但并没有秩函数.此外,文献^{[8, 13]}提出了试探性方法去探索给定循环程序的非终止性,对可终止的循环程序,他们的方法不再适用.尽管众所周知,一般的程序终止性问题是不可判定的,但对特定的一类程序而言,人们总希望能证明其终止性问题是可判定的.由此,证明循环程序终止性的另一途径就是避开秩函数的合成,而采用数学方法严格证明某类或某些类循环程序的终止性是可判定的,并建立相对完备的判定算法.目前,从可判定的角度进行终止性研究的结果甚少.在2004年,Tiwari在文献^[16]中首次证明了一类单重无分支线性循环程序在实域上的终止性是可判定的.相似的结论被Braveman^[7]推广到整数环上.此外,为避免Jordan标准型的浮点计算,文献^[17]中提出了精确的符号计算方法对这类线性程序进行终止性判定.既然一般形式的线性程序终止性是不可判定的^[16],那么非线性循环程序由于其更为复杂的动力行为使得其终止性分析将变得更加困难.一个程序被称为非线性的,是指循环中的赋值映射或循环条件中的约束是非线性表达式.在2005年,利用有限差分树理论,文献^[6]提出了试探性算法对一类含多分支语句的多项式程序的终止性问题进行判定.2010年,针对一类赋值为线性且循环条件由非线性多项式不等式构成的循环程序,文献^[18]分析了其终止性问题,证明了当这类程序满足给定的NZM条件时,其终止性是可判定的.2013年,文献^[3]通过分析多项式映射f_i的发散区间,讨论了一类多项式循环(迭代赋值型如x_i:=f_i(x_i))的终止性问题.

本文中,我们对赋值映射F为非线性、循环条件形成有界闭连通域S的一类非线性循环程序P(F,S)的终止性问题进行了分析.不同于文献^[6],本文呈现的方法并不依赖于有限差分树理论.同时,本文所研究的程序类型是文献^{[3, 7, 16, 17, 18]}中的程序类型的扩展.我们给出了适当的条件,证明了当循环程序满足这些条件时,这类循环程序在实域上可终止的充分必要条件为迭代映射F在有界闭连通域S上没有不动点.同时,对任给的连续迭代映射F,本文建立的引理1,便于我们分析当其有界闭连通域S取自哪个区域时,可使得F在该S上进行的迭代是可终止的.我们的算法依赖于计算机代数中的Groebner基理论和半代数系统求解,因此,计算机代数工具DISCOVERER^{[2, 19]},BOTTEMA^[2]以及Maple在算法中被运用.

1 主要结果

第1.1节,针对赋值映射F为连续的且S为有界闭连通域的循环程序,建立了相关终止性的一般性结论,将其终止性问题规约为:在满足一定条件下,迭代映射有无不动点的判定问题;但验证所需的前提条件是否被满足,则是需要讨论的问题.因此在第1.2节中,我们进一步限制F为多项式映射,然后给出方法去验证所需的前提条件是否成立.

1.1 有界闭连通域上的循环终止性分析

本节中,我们对循环条件围成的区域S为有界闭连通域、赋值映射F为非线性连续映射的循环程序终止性问题进行分析.这里,我们设置S为有界闭的,是因为物理世界中的诸多变量,如速度、加速度等都是有界的量;而闭性的限制则是为了保证收敛序列的极限点能落到S中.这类循环程序被称为是不可终止的,如果存在一点X^*$\in $R,使得对任意的非负整数k,有F^k(X^*)$\in $S.如果这样的点不存在,则称这类循环在实数域上是可终止的.这里,

${{F}^{k}}=\underbrace{F\circ F\circ ...\circ F}_{k}$

首先,我们给出引理1:

引理1. 设S是n维空间中的有界闭的连通域,给定n维连续映射F:X|→F(X).如果循环程序:

$\begin{matrix} while\ \ X\in \ S\ \ do \\ \{X=F(X)\} \\ endwhile \\ \end{matrix}$

(1)

在S上不可终止,则对任意正整数k,集合{X$\in $Rⁿ:|F^k(X)=|X|}与S均相交(这里,|o|表示向量o的欧式范数).

证明:若上述循环程序在S上不可终止,则必存在一个点X$\in $S,生成无穷点列:

Δ={X0,F(X0),F2(X0),…}⊆S.

记${r_ \bot } = sup\{ |{F⊥n}({X_0})|\} _{n = 0}⊥\infty ,{r_ \top } = inf\{ |{F⊥n}({X_0})|\} _{n = 0}⊥\infty $.令$|\Delta | = \{ |{F⊥n}({X_0})|\} _{n = 0}⊥\infty = \{ {r_n}\} _{n = 0}⊥\infty $.下面证明k=1时定理成立,k=2,3,…时的证明完全类似.

我们首先证明,分别存在两点${X_ \bot } \in \{ X \in {R⊥n}:|X| = {r_ \bot }\} \cap S,{X_ \top } \in \{ X \in {R⊥n}:|X| = {r_ \top }\} \cap S$,使得:

$|F({{X}_{\bot }})|\le |{{X}_{\bot }}|,|F({{X}_{\top }})|\ge |{{X}_{\top }}|$

我们仅证明|F(X_⊥)|≤|X_⊥|,$|F({X_ \top })| \ge |{X_ \top }|$的证明类似.

首先,若r_⊥$\in $|Δ|,不妨记为r_⊥=|F^t(X₀)|=|X_t|,则显然有|F(X_t)|≤|X_t|=r_⊥,令X_⊥=X_t;倘若r_⊥$\notin $|Δ|,既然Δ为有界数列,则由确界性质,必存在|Δ|的子列$\{ {r_{{n_k}}}\} $收敛于r_⊥,即${\lim _{k \to \infty }}{r_{{n_k}}} = {r_ \bot }$.既然${F^{{n_k}}}({X_0}) = {X_{{n_k}}} = {r_{{n_k}}}{(\eta _{{n_k}}^{(1)},\eta _{{n_k}}^{(2)},...,\eta _{{n_k}}^{(n)})^T}$,令:

${{\eta }_{{{n}_{k}}}}={{(\eta _{{{n}_{k}}}^{(1)},\eta _{{{n}_{k}}}^{(2)},...,\eta _{{{n}_{k}}}^{(n)})}^{T}},|{{\eta }_{{{n}_{k}}}}|=1$

显然,数列$\{ {\eta _{{n_k}}}\} _{k = 0}^\infty $是有界的.根据Bolzano-Weierstrass定理可知,Rⁿ上的有界数列必有收敛子列.因此,存在$\{ {\eta _{{n_k}}}\} $的子列$\{ {\eta _{{n_{{k_v}}}}}\} $,有:

$\underset{v\to \infty }{\mathop{\lim }}\,{{\eta }_{{{n}_{{{k}_{v}}}}}}={{\eta }^{*}}$

又因为${\lim _{k \to \infty }}{r_{{n_k}}} = {r_ \bot }$,故其任意收敛子列也收敛于r_⊥,因此有:

$\underset{v\to \infty }{\mathop{\lim }}\,{{r}_{{{n}_{{{k}_{v}}}}}}{{\eta }_{{{n}_{{{k}_{v}}}}}}={{r}_{\bot }}{{\eta }^{*}}$

因此,在Δ中存在子列$\{ {F^{{n_{{k_v}}}}}({X_0})\} _{v = 0}^\infty $,使得${\lim _{v \to \infty }}{F^{{n_{{k_v}}}}}({X_0}) = {r_ \bot }{\eta ^ * }$.令X_⊥=r_⊥$\eta $.

既然Δ⊆S,则X_⊥$\in ${X$\in $Rⁿ:|X|=r_⊥}$\cap $S.

又因为r_⊥$\notin $|Δ|且为|Δ|上确界,则$|F({{F}^{{{n}_{{{k}_{v}}}}}}({{X}_{0}}))|<|{{X}_{\bot }}|={{r}_{\bot }}$.两边取极限,由F的连续性,

$\underset{v\to \infty }{\mathop{\lim }}\,|F({{F}^{{{n}_{{{k}_{v}}}}}}({{X}_{0}}))|=|F(\underset{v\to \infty }{\mathop{\lim }}\,{{F}^{{{n}_{{{k}_{v}}}}}}({{X}_{0}}))|=|F({{X}_{\bot }})|\le |{{X}_{\bot }}|={{r}_{\bot }}$

同理可证:存在${{X}_{\top }}\in \{X\in {{R}^{n}}:|X|={{r}_{\top }}\}\cap S$,有$|F({{X}_{\top }})|\ge |{{X}_{\top }}|$.记G=|F(X)|-|X|.既然存在两点${{X}_{\bot }},{{X}_{\top }}\in S$,使得$G({{X}_{\bot }})\le 0,G({{X}_{\top }})\ge 0$,若上述两式其中一个等号成立,则令${{X}^{*}}={{X}_{\bot }}({{X}_{\top }})$,有G(X^*)=0.因此不失一般性,假设两式中的等号都不成立,则根据多元连续函数在有界闭集上的性质可知:必存在一点${{X}^{*}}\in L({{X}_{\bot }},{{X}_{\top }})$,使得G(X^*)=0.这里,$L({{X}_{\bot }},{{X}_{\top }})\in S$为S中连接${{X}_{\bot }},{{X}_{\top }}$两点的一条折线.因此,集合{X$\in $Rⁿ:|F(X)=|X|}与S必相交.

同样地,将上述证明中F改为F^k,k=2,3,…,采用类似的方法可证明:存在两点X_⊥$\in ${X$\in $Rⁿ:|X|=r_⊥}$\cap $S,${{X}_{\top }}\in \{X\in {{R}^{n}}:|X|={{r}_{\top }}\}\cap S$,使得$|{{F}^{k}}({{X}_{\bot }})|\le |{{X}_{\bot }}|,|{{F}^{k}}({{X}_{\top }})|\ge |{{X}_{\top }}|$,k=2,3,…,进而可证{X$\in $Rⁿ:|F^k(X)=|X|}与S必相交.

注:根据上述定理,倘若存在正整数k使得|F^k(X)|=|X|与S不相交,则该循环程序在S上可终止.实际上,既然|F^k(X)|=|X|等价于|F^k(X)|²=|X|²,故若存在正整数k使得|F^k(X)|²=|X|²与S不相交,则该循环程序在S上可终止.这样,在实际的计算中可避免根号的处理.

根据引理1,给定迭代映射F,我们可以确定:当S取自哪些区域时,形如公式(1)的循环程序是可终止的.为方便起见,这样的区域称为安全区域.

例1:考虑使得下列循环可终止的安全区域.

$\begin{matrix} \mathbf{while}\ \ x\in S\ \ \mathbf{do} \\ x:=xy+2{{x}^{2}}+y+1 \\ y:=x-{{y}^{2}}+y-5 \\ \mathbf{endwhile} \\ \end{matrix}$

(2)

令F=(f₁,f₂)^T=(xy+2x²+y+1,x-y²+y-5)^T.作T_k(x,y)=|F^k(X)|²-|X|².令$\Theta $_k=Rⁿ-{(x,y)$\in $R²:T_k(x,y)=0}.因此,对固定的k,则$\Theta $_k中的任意有界闭域都是该循环的安全区域.如在此例中,倘若令k=1,S={x²-y≥1,y≥2,x≤7},因为S$\cap $T_k(x,y)=∅,则F在S上的迭代可终止.即,这样设置的S是循环(2)的一个安全区域.

引理1为循环(1)的可终止性提供了充分判准.首先给出下面一类特殊的循环,根据引理1可知,其终止性与不动点有着紧密的联系.

令$R_{+}^{n}=\{({{x}_{1}},...,{{x}_{n}})\in {{R}^{n}}:{{x}_{i}}>0,i=1,...,n\},{{S}_{+}}\subset R_{+}^{n}$为有界闭连通域.令$\hat{F}(X)$为多项式映射,即:

$\hat{F}(X)={{({{f}_{1}},{{f}_{2}},...,{{f}_{n}})}^{T}},{{f}_{i}}\in R[X]且{{f}_{i}}={{c}_{i}}{{x}_{i}}+\sum\nolimits_{\alpha }{}\,{{c}_{\alpha }}{{X}^{\alpha }}({{X}^{\alpha }}=x_{1}^{{{\alpha }_{1}}}x_{2}^{{{\alpha }_{2}}}...x_{n}^{{{\alpha }_{n}}}),$

其中,c_i≥1,c_{$\alpha $}>0.通常称x_i为多项式f_i的导元.因此,$\hat{F}$中每个f_i均含有其导元的线性项,且该项的系数大于等于1,而其余项系数均为正数,譬如$\hat{F}={{({{x}_{1}}+{{x}_{1}}{{x}_{2}}+4x_{2}^{2},3{{x}_{2}}+7{{x}_{1}}+2)}^{T}}$.给定型如下列类型的循环程序(3):

$\begin{matrix} \mathbf{while}\ \ X\in \ {{S}_{+}}\ \ \mathbf{do} \\ \{X=\hat{F}(X)\} \\ \mathbf{endwhile} \\ \end{matrix}$

(3)

则根据引理1,可建立下列结果.

定理2. 记号同上.循环程序(3)不可终止的充分必要条件是$\hat{F}$在S₊上有不动点.

证明:倘若$\hat{F}$在S₊上有不动点,则循环程序(3)显然不可终止.因此,下面仅证明当$\hat{F}$在S₊上没有不动点时,循环程序(3)是可终止的.既然$|\hat{F}(X){{|}^{2}}-|X{{|}^{2}}=\sum\nolimits_{i=1}^{n}{}\,f_{i}^{2}-\sum\nolimits_{i=1}^{n}{}\,x_{i}^{2}$,

$\begin{align} & \sum\limits_{i=1}^{n}{}\,f_{i}^{2}-\sum\limits_{i=1}^{n}{}\,x_{i}^{2} & =\sum\limits_{i=1}^{n}{}\,{{({{f}_{i}}-{{x}_{i}})}^{2}}+2\sum\limits_{i=1}^{n}{}\,{{x}_{i}}{{f}_{i}}- \\ & 2\sum\limits_{i=1}^{n}{}\,x_{i}^{2}=\sum\limits_{i=1}^{n}{}\,{{({{f}_{i}}-{{x}_{i}})}^{2}}+2\sum\limits_{i=1}^{n}{}\,({{x}_{i}}({{f}_{i}}-{{x}_{i}})) \end{align}$

根据已知,$\hat{F}$在S₊上没有不动点,因此对任意的X$\in $S₊,有$\sum\nolimits_{i=1}^{n}{}\,{{({{f}_{i}}(X)-{{x}_{i}})}^{2}}>0$.同时,根据$\hat{F}$的构造可知(即,每个f_i均含有其导元的线性项,且该项的系数大于等于1),x_i(f_i-x_i)在S₊上非负,因此,$\sum\nolimits_{i=1}^{n}{}\,f_{i}^{2}-(\sum\nolimits_{i=1}^{n}{}\,x_{i}^{2})$在S₊上恒为正.故对任意的X$\in $S₊,$|\hat{F}(X){{|}^{2}}\ne |X{{|}^{2}}$.也即:对任意的X$\in $S₊,$|\hat{F}(X)|\ne |X|$.

根据引理1,循环程序(3)是可终止的.

针对如式(3)的一类特殊循环程序,根据定理2,我们将这类程序的终止性问题归约为有无不动点的判定,从而使得该类特殊程序的终止性变得便于分析.通过定理4可知:利用不动点来分析循环终止性的方法不仅适用于循环(3),在一定条件下,这种方法对更加一般类型的循环(1)仍然适用.我们首先给出下列引理,其中的S,F的定义同引理1.

给定正整数N,令${{\Gamma }_{N}}(X)=\sum\limits_{k=1}^{N}{}\,||{{F}^{k}}(X){{|}^{2}}-|X{{|}^{2}}|$,令

$\begin{align} & {{V}_{R}}({{\Gamma }_{N}}(X))=\{X\in {{R}^{n}}:\ {{\Gamma }_{N}}(X)=0\}=\{X\in {{R}^{n}}:\ |F(X){{|}^{2}}- \\ & |X{{|}^{2}}=0,...,|{{F}^{N}}(X){{|}^{2}}-|X{{|}^{2}}=0\}, \\ & {{V}_{R}}(F-X)=\{X\in {{R}^{n}}:\ F(X)=X\}, \\ \end{align}$

令V_C($\Gamma $_N(X))={X$\in $Cⁿ:|F(X)|²-|X|²=0,…,|F^N(X)|²-|X|²=0},V_C(F-X)={X$\in $Cⁿ:F(X)=X}.

这里,R,C分别表示实数域和复数域.在给出本文的主要定理前,我们需要下面的引理.

引理3. 记号同上.假设存在正整数N,使得V_R($\Gamma $_N(X))=V_R(F-X).那么如果F在S上没有不动点,则必存在常数n>0,使得对任意的X$\in $S,有:

$\sum\limits_{k=1}^{N}{}\,||{{F}^{k}}(X){{|}^{2}}-|X{{|}^{2}}|\ge \nu \cdot |F(X)-X|$

证明:根据题设F在S上没有不动点,即:对任意的X$\in $S,|F(X)-X|≠0.又因为V_R($\Gamma $_N(X))=V_R(F-X),故对任意的X$\in $S,$\Gamma $_N(X)≠0.也即:对任意的X$\in $S,X$\notin $V_R($\Gamma $_N(X)).

因此,对任意的X^*$\in $S,必然存在正数v(X^*),使得$\Gamma $_N(X^*)≥v(X^*)×|F(X^*)-X^*|.

又因为函数$\Gamma $_N(X),|F(X)-X|均是连续的(因为F是连续的),故根据连续性,必存在X^*的开邻域O(X^*,$\varepsilon $),使得对任意的X$\in $O(X^*,$\varepsilon $),有$\Gamma $_N(X^*)≥v(X^*)×|F(X^*)-X^*|.由X^*的任意性以及S有界闭性,存在无穷个开邻域覆盖有界闭连通域S.由有限开覆盖定理,存在有限个开邻域$O(X_{1}^{*},{{\varepsilon }_{1}}),O(X_{2}^{*},{{\varepsilon }_{2}}),O(X_{3}^{*},{{\varepsilon }_{3}}),...,O(X_{t}^{*},{{\varepsilon }_{t}})$覆盖S,即:

$S\subseteq \bigcup\nolimits_{i=1}^{t}{}\,O(X_{i}^{*},{{\varepsilon }_{i}})$

令$\nu =\min \{\nu (X_{1}^{*}),\nu (X_{2}^{*}),...,\nu (X_{t}^{*})\}$,则根据上述分析有:

$\sum\limits_{k=1}^{N}{}\,||{{F}^{k}}(X){{|}^{2}}-|X{{|}^{2}}|\ge \nu \cdot |F(X)-X|.$

根据引理1和引理3,我们可以建立如下结果.首先,令$\overline{[1,N]}=\{1,2,3,...,N\}$.

定理4. 设S是n维空间中的有界闭的连通域.给定n维连续映射F:X|→F(X).如果满足:

(i)  存在正整数N,使得V_R($\Gamma $_N(X))=V_R(F-X);

(ii)  存在$j\in \overline{[1,N]}$和正数h,使得对任意的$k\in \overline{[1,N]},k\ne j$,有:

||Fj(X)|2-|X|2|≥h×||Fk(X)|2-|X|2|(X$\in $S),

则循环程序(1)在S上是不可终止的充分必要条件为:迭代映射F在S中有不动点.

证明:倘若F在S中有不动点,则循环程序(1)显然是不可终止的.因此,仅需证明:若F在S中没有不动点,则循环(1)可终止.既然假设V_R($\Gamma $_N(X))=V_R(F(X)-X)成立,根据引理3,若F在S上没有不动点,则存在正数n,使得对任意的X$\in $S,$\sum\nolimits_{k=1}^{N}{}\,||{{F}^{k}}(X){{|}^{2}}-|X{{|}^{2}}|\ge \nu \cdot |F(X)-X|$.根据假设(ii)得知:对任意的X$\in $S,

$\left( 1+(N-1)\frac{1}{\hbar } \right)||{{F}^{j}}(X){{|}^{2}}-|X{{|}^{2}}|\ge \sum\nolimits_{k=1}^{N}{}\,||{{F}^{k}}(X){{|}^{2}}-|X{{|}^{2}}|\ge \nu \cdot |F(X)-X|$

又因为F在S中没有不动点,则|F(X)-X|≠0.故||F^j(X)|²-|X|²|≠0(∀X$\in $S).根据引理1可知,循环(1)必然终止.

定理4说明:在满足给定的假设(i)、假设(ii)时,循环程序(1)的终止性可归为在S中有无不动点的判定.因此,关键问题是验证假设(i)、假设(ii)是否成立.一般地,因为F的任意性,假设(i)的验证是困难的,但是当映射F=(f₁,f₂,…,f_n)^T中的每个分量f_i都是多项式时,即F为多项式映射,我们可将数域从实数域拓展到复数域,从而使得我们可利用多项式代数中的相关理论和工具去判定假设(i)是否成立.即:判定是否存在N,使得V_C($\Gamma $_N(X))= V_C(F(X)-X)成立.这是因为,若V_C($\Gamma $_N(X))=V_C(F(X)-X),则V_R($\Gamma $_N(X))=V_R(F(X)-X).而验证假设(ii)是否成立可转换为不等式证明问题,后者可使用杨路等人开发的不等式证明器BOTTEMA^[2]进行验证.因此在下一节中,我们将着重讨论当F为多项式映射的循环终止性问题,这类循环被称为多项式循环程序.

1.2 迭代映射为多项式映射

根据定理4,当迭代映射F为连续的循环程序满足两个假设条件(i)、假设(ii)时,其终止性判定问题可转为有无不动点的判定.本节中,我们限定循环(1)中的迭代映射F为多项式的,因此F必是连续的.既然定理4中的假设条件(ii)可用工具BOTTEMA予以验证,因此在本节,针对这类多项式循环程序,我们着重分析如何对定理4中的假设条件(i)进行验证的问题,并给出了可计算的验证方法.由于需要用到多项式代数的相关理论,如理想、Groebner基等,因此首先给出一些基本概念.

定义5^[22]. 令R[X]为多项式环.子集I$\subset $R[X]被称为一个多项式理想,如果I满足以下条件:

(1)  0$\in $I;

(2)  若a,b$\in $I,则a+b$\in $I;

(3)  若a$\in $I,b$\in $R[X],则b×a$\in $I.

任给N(N≤+∞)个多项式p₁,p₂,…,p_N$\in $R[X],可构建一个多项式理想I=〈p₁,p₂,…,p_N〉.多项式p₁,p₂,…,p_N称为理想I的一组生成元.称多项式a$\in $I,如果存在多项式q₁,…,q_s$\in $R[X]和多项式f₁,…,f_s$\in $I,使得$a=\sum\nolimits_{i=1}^{s}{}\,{{q}_{i}}{{f}_{i}}$.我们称理想I₁⊆I₂,如果对任意的元素a$\in $I₁,都有a$\in $I₂.任意多项式理想I,在给定项序下,都有一组具有良好性质的生成元——约化Groebner基,记为G.显然,〈G〉=I.给定一个理想,根据约化Groebner基的性质,可以判定任意多项式a是否属于这个理想.令V_C(I)={X$\in $Cⁿ:p_i(X)=0,∀i=1,2,…,N}为理想I的零点集.若I₁=I₂,则V_C(I₁)=V_C(I₂);若I₁⊆I₂,则V_C(I₁)⊇V_C(I₂);若I₁=〈f₁,…,f_s〉,I₂=〈g₁,…,g_t〉,则I₁$\cup $I₂=〈f₁,…,f_s,g₁,…,g_t〉.有关多项式理想及Groebner基的详细介绍见文献^[22].譬如,令理想I=〈p₁,p₂〉=〈xz-y²,x³-z²〉$\in $R[X].给定多项式f=-4x²y²z²+y⁶+3z³,判定在分级字典序下是否有f$\in $I?使用计算机代数系统Maple,可找到理想I的约化Groebner基.

G=(p1,p2,p3,p4,p5)=(xz-y2,x3-z2,x2y2-z3,xy4-z4,y6-z5).

根据G,可通过理想成员测试算法得到:

f=(-4xy2z-4y4)×p1+0×p2+0×p3+0×p4+(-3)×p5.

因此,f$\in $〈G〉=I.另外,给定两个多项式理想I₁,I₂,我们也可以通过计算其各自的约化Groebner基G₁,G₂来判定是否I₁=I₂,这是因为G₁=G₂当且仅当I₁=I₂.

定理6^[22]. 假设I₁$\subset $I₂$\subset $I₃$\subset $…⊆R[X]是一组理想升链,则存在正整数N,使得对任意n≥N都有I_n=I_n+1=I_n+2=….

根据定理6,一组理想升链必在某个N处达到稳定.等价地,这组理想升链的零点集也在N处达到稳定.也即:

${{V}_{C}}({{I}_{1}})\supset {{V}_{C}}({{I}_{2}})\supset ...\supset {{V}_{C}}({{I}_{{{N}^{*}}}})={{V}_{C}}({{I}_{{{N}^{*}}+1}})=...$

在本文的具体问题中,令I_i=〈|F(X)|²-|X|²,|F²(X)|²-|X|²,…,|Fⁱ(X)|²-|X|²〉为多项式理想,显然有I_i⊆I_i+1.通过定理6可知:必存在正整数N^*,使得${{I}_{{{N}^{*}}}}={{I}_{{{N}^{*}}+1}}$.

命题7. 给定多项式映射F,令I_i=〈|F(X)|²-|X|²,|F²(X)|²-|X|²,…,|Fⁱ(X)|²-|X|²〉为多项式理想,则必存在正整数N^*,使得${{I}_{{{N}^{*}}}}={{I}_{{{N}^{*}}+1}}$.

证明:这是显然的.根据I_i的构造可知,I_i⊆I_i+1(这是因为理想I_i+1的生成元比理想I_i多出一个生成元|Fⁱ⁺¹(X)|²-|X|²).假设使得${{I}_{{{N}^{*}}}}={{I}_{{{N}^{*}}+1}}$成立的N^*不存在,则这些理想将形成一条严格升链I₁I₂I₃…,那么根据定理6,必存在N^*,使得${{I}_{{{N}^{*}}}}={{I}_{{{N}^{*}}+1}}$.故假设不成立.

根据命题7,使得${{I}_{{{N}^{*}}}}={{I}_{{{N}^{*}}+1}}$的正整数N^*必定存在.而下面的算法1可计算出N^*.

算法1.

输入:给定n维多项式映射F:X|→F(X);

输出:N^*.

S1. 构建理想I_i=〈|F(X)|²-|X|²,|F²(X)|²-|X|²,…,|Fⁱ(X)|²-|X|²〉;

S2. 如果I_i≠I_i$\cup $〈|Fⁱ⁺¹(X)|²-|X|²〉,则转S3;否则,转S4;

S3. I_i←I_i$\cup $〈|Fⁱ⁺¹(X)|²-|X|²〉,转S2;

S4. 返回N=i.

由命题7可知,算法1显然有限终止.在算法1中,两个理想是否相等等价于它们的约化Groebner基是否相等.因此,可调用Maple中的命令函数计算各自的约化Groebner基.既然根据算法1可以得到N^*,可构建${{I}_{{{N}^{*}}}}=\langle |F(X){{|}^{2}}-|X{{|}^{2}},|{{F}^{2}}(X){{|}^{2}}-|X{{|}^{2}},...,|{{F}^{{{N}^{*}}}}(X){{|}^{2}}-|X{{|}^{2}}\rangle $.另外,根据${{\Gamma }_{{{N}^{*}}}}(X)$的定义,显然有:

${{V}_{C}}({{I}_{{{N}^{*}}}})={{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))$

因此,要判定${{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{C}}(F(X)-X)$是否成立,等价于判定${{V}_{C}}({{I}_{{{N}^{*}}}})={{V}_{C}}(F(X)-X)$.由此,根据算法2,我们可以判定${{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{C}}(F(X)-X)$是否成立.

算法2.

输入:${{I}_{{{N}^{*}}}},F(X)-X={{({{f}_{1}}-{{x}_{1}},...,{{f}_{n}}-{{x}_{n}})}^{T}}$;

输出:T(相等),F(不相等).

S1. 计算理想${{I}_{{{N}^{*}}}}$的约化Groebner基${{G}_{{{N}^{*}}}}$;

S2. 如果对任意的i=1,2,…,n,均有${{f}_{i}}-{{x}_{i}}\in {{G}_{{{N}^{*}}}}$,则返回T;否则,返回F.

命题8. 若算法2返回T,则必有${{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{C}}(F(X)-X).$

证明:根据题设,若算法2返回T,则表明对任意的i,有${{f}_{i}}-{{x}_{i}}\in {{G}_{{{N}^{*}}}}$,也即${{f}_{i}}-{{x}_{i}}\in {{I}_{{{N}^{*}}}}$,这是因为$\langle {{G}_{{{N}^{*}}}}\rangle ={{I}_{{{N}^{*}}}}.$因此,理想$\langle F(X)-X\rangle =\langle {{f}_{1}}-{{x}_{1}},...,{{f}_{n}}-{{x}_{n}}\rangle \subseteq {{I}_{{{N}^{*}}}}.$故${{V}_{C}}(F(X)-X)\supseteq {{V}_{C}}({{I}_{{{N}^{*}}}})$.又因为${{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{C}}({{I}_{{{N}^{*}}}}),$有:

${{V}_{C}}(F(X)-X)\supseteq {{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X)).$

同时,又因为${{V}_{C}}(F(X)-X)\subseteq {{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))$,故${{V}_{C}}(F(X)-X)={{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X)).$

根据命题8,若算法2返回T,则${{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{C}}(F-X)$,故${{V}_{R}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{R}}(F(X)-X),$满足定理4的题设.此时,循环程序(1)是否可终止的问题等价于F在S中有无不动点的问题.因此,我们有下列的结论.

定理9. 设S是n维空间中的有界闭的连通域.给定n维多项式映射F:X|→F(X),令:

Ii=〈|F(X)|2-|X|2,|F2(X)|2-|X|2,…,|Fi(X)|2-|X|2〉.

如果同时满足:

(i)  存在正整数N^*,使得${{I}_{{{N}^{*}}}}={{I}_{{{N}^{*}}+1}}$且${{V}_{C}}({{I}_{{{N}^{*}}}})={{V}_{C}}(F(X)-X);$

(ii)  存在$j\in \overline{[1,{{N}^{*}}]}$和正数h,使得∀X$\in $S,$||{{F}^{j}}(X){{|}^{2}}-|X{{|}^{2}}|\ge \hbar \cdot ||{{F}^{k}}(X){{|}^{2}}-|X{{|}^{2}}|(\forall k\in \overline{[1,{{N}^{*}}]},k\ne j).$ 则循环程序(1)在S上是不可终止的当且仅当F在S中有不动点.

证明:因为${{V}_{C}}({{I}_{{{N}^{*}}}})={{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X)),{{V}_{C}}({{I}_{{{N}^{*}}}})={{V}_{C}}(F(X)-X)$,从而有${{V}_{C}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{C}}(F(X)-X)$,故有:

${{V}_{R}}({{\Gamma }_{{{N}^{*}}}}(X))={{V}_{R}}(F(X)-X).$

因此,定理4中的假设均成立.由定理4,结论显然成立.

注:当F为多项式映射时,算法1和算法2给出了可计算的方法去验证定理9中的假设(i)是否成立.而假设(ii)中,判定是否存在正数h,使得∀X$\in $S,||F^j(X)|²-|X|²|≥h×||F^k(X)|²-|X|²|可以等价转化为存在正数h,使得下列半代数系统:

S$\cap ${X$\in $Rn:||Fj(X)|2-|X|2|<h×||Fk(X)|2-|X|2|}

无实解.后者可用Collins早期提出的基于柱形代数分解^[21]的实量词消去技术进行判定,因而也是可计算的.已有多种实量词消去的工具,如QEPCAD,Redlog,DISCOVERER,BOTTEMA,RegularChains等.本文中,我们主要利用工具BOTTEMA,DISCOVERER来进行计算.进而,当定理9中的两个假设条件都被满足时,则这类多项式循环程序的终止性问题可归结为有无不动点的判定问题.而后者的判定是简单的,这是因为判定F是否在S中有不动点,等价于计算下列半代数系统:{X$\in $Rⁿ:F(X)-X=0}$\cap $S是否非空:若非空,则表明F在S中有不动点;否则,在S上没有不动点.而一个半代数系统是否为空的判定问题等价于实量词消去问题,因而适合运用计算机代数工具DISCOVERER予以求解.

根据定理9,我们给出本文的主要算法,描述如下.

算法3.

输入:形如(1)的循环程序P;

输出:True(终止),False(不终止),ND(不确定).

S1. 从循环程序P中抽取迭代映射F,循环条件形成的区域S,转S2;

S2. 调用算法1计算出正整数N^*,转S3;

S3. 调用算法2判定${{V}_{C}}({{I}_{{{N}^{*}}}})={{V}_{C}}(F(X)-X)$是否成立:若成立,则转S4;否则,输出ND;

S4. 利用工具BOTTEMA判定定理9中的条件(ii)是否成立:若成立,则转S5;否则,输出ND;

S5. 利用工具DISCOVERER判定半代数系统{X$\in $Rⁿ:F(X)-X=0}$\cap $S是否有解:若有解,则输出false;否则,输出true.

在算法3中,S3和S4分别判定定理9中的两个前提条件(i)、条件(ii)是否都满足:倘若其中某个条件不满足,那么输出ND;否则,若这两个条件都满足,那么我们可通过判定S中是否有不动点来判定程序P是否终止.

2 实 例

例2:考虑下列循环的终止性.

$\begin{align} & \mathbf{while}\ \ {{x}^{2}}+{{y}^{2}}\le 1\text{ }\And \And \text{ }x\ge 0\text{ }\And \And \text{ }y\ge 0\ \ \mathbf{do} \\ & \ \ \ \ \ \ \ \ \ \ x:=2{{x}^{2}}-3xy+1 \\ & \ \ \ \ \ \ \ \ \ \ y:=xy+7x+5 \\ & \mathbf{endwhile} \\ \end{align}$

(4)

令F=(f₁,f₂)=(2x²-3xy+1,xy+7x+5)^T,S={X$\in $R²:x²+y²≤1,x≥0,y≥0}为有界闭连通的.调用算法1,得到N^*=3,则I₃=〈|F(X)|²-|X|²,|F²(X)|²-|X|²,|F³(X)|²-|X|²〉.根据算法2,首先计算I₃的Groebner基G₃=(3y²-2+24x-17y,xy+5+7x-y,2x²+16+20x-3y),然后根据理想成员判定算法得知:

•  f₁-x=0×(3y²-2+24x-17y)+(-3)×(xy+5+7x-y)+1×(2x²+16+20x-3y);

•  f₂-y=0×(3y²-2+24x-17y)+1×(xy+5+7x-y)+0×(2x²+16+20x-3y).

故f₁-x$\in $G₃,f₂-y$\in $G₃.根据命题8可知V_C(I₃)=V_C(G₃(X))=V_C(F(X)-X),满足定理9的条件(i).为验证条件(ii)是否成立,我们调用BOTTEMA得知:当h=10^-20时,有||F(X)|²-|X|²|≥h||F²(X)|²-|X|²|且||F(X)|²-|X|²|≥h||F³(X)|²-|X|²|,从而满足定理9的条件(ii).因此根据定理9,由于迭代映射F的不动点都不在S中,因此该循环是可终止的.

例3:考虑下列循环的终止性:

$\begin{align} & \mathbf{while}\ \ x\le 1\ \And \And \ x\ge -4\ \And \And \ y\le 2\ \And \And \ y\ge -1\ \ \mathbf{do} \\ & \ \ \ \ \ \ \ \ \ x:=-7-y-4{{x}^{2}}-{{y}^{2}} \\ & \ \ \ \ \ \ \ \ \ y:=-62x+4y+5 \\ & \mathbf{endwhile} \\ \end{align}$

(5)

令F=(-7-y-4x²-y²,-62x+4y+5)^T,S={X$\in $R²:x≤1,x≥-4,y≤2,y≥-1}为有界闭连通的.调用算法1,得到N^*=3,则I₃=〈|F(X)|²-|X|²,|F²(X)|²-|X|²,|F³(X)|²-|X|²〉.调用算法2,可判定出V_C(I₃)=V_C(F(X)-X).同时,调用BOTTEA可知,当h=10^-4时,有:

||F3(X)|2-|X|2|≥h||F(X)|2-|X|2|且||F3(X)|2-|X|2|≥h||F2(X)|2-|X|2|.

故满足定理9的两个条件.由于迭代映射F的不动点都不在S中,根据定理9,该循环是可终止的.

在表1中,我们列举了更多实例来阐明本文方法的适用性.

表中的ND表示本文方法对其终止性无法确定.

从算法3中可以看出:主要的计算都集中在S2~S5,且涉及的计算主要包括Grobner基计算和柱形代数分解. Groebner基是Buchberger在他的博士论文中首先引进的,该方法能从任意多项式理想的一组给定生成元有效地计算出另一组性质良好的生成元,即Groebner基.Collins在1975年首次提出了较为实用的基于柱形代数分解的量词消去算法,用于实闭域上的量词消去问题.S2中主要计算多项式理想的约化Groebner基,在文献^[23]中,其计算复杂度在糟糕情形下被证明是${{2}^{{{2}^{O(n)}}}}$,其中,n为多项式变元个数,该复杂度是双指数的.S3中涉及理想成员的判定计算,即,判定给定多项式f是否属于理想I,这等价于在给定相同的项序下判定理想I$\cup ${f}与理想I是否相等.而后者的判定等价于计算两个理想的约化Groebner基是否相等(理想的约化Groebner基总是唯一的).既然在S2中计算理想的约化Groebner基的复杂度糟糕情况下是双指数的,因此,S3的计算复杂度在糟糕情形下也是双指数的.在S4和S5中,我们采用Collins提出的基于柱形代数分解(CAD)的量词消去技术来判定半代数系统是否有实解.而CAD的计算复杂度在最糟糕情形下被证明是(n是变元个数)也是双指数的^{[24, 25]}.因此,算法3的复杂度在糟糕情形下不可避免是双指数的.

借助计算机代数中的Groebner基理论,本文研究了一类单重无分支非线性循环程序的终止性问题.尽管程序终止性问题被证明是不可判定的,但对本文所研究的这类循环程序,我们证明了在给定条件下,此类循环的终止性判定问题可归约为不动点的判定问题,而不动点的计算可被规约为半代数系统的求解.本文采用的柱形代数分解(CAD)和Groebner基计算都是精确的符号计算,从而导致本文呈现的算法是指数时间复杂度的.尽管高复杂度,但当问题规模不大时,可以在合理时间内得到判定结果.随着近年来符号-数值混合CAD技术以及并行Groebner基计算的发展,本文算法的效率有望得到提升.我们今后的工作将继续沿此思路探索更加一般的循环程序的终止性,并将其终 止性的判定问题归结为不动点的判定问题.

致谢  感谢上海高可信计算重点实验室对作者的支持.