多项式循环程序的秩函数探测∗

李 轶, 冯 勇

(中国科学院 重庆绿色智能技术研究院,重庆 401120)

嵌入式系统在人类生活中发挥着越来越大的作用,而作为嵌入式系统灵魂的嵌入式软件在其中所占有的比重也越来越大.因此,嵌入式软件的可靠性将变得更加重要.诸如航空、航天、军事、交通、医疗等关键应用领域都对嵌入式系统的可靠性和安全性要求非常高,任何错误的发生都可能带来灾难性后果.嵌入式系统具有3 个重要属性,即可达性、终止性、不变式.可达性是指一个系统能否从一个给定状态到达另一个可接受状态.某些混成系统的可达性被证明是能用计算机代数工具来检验的.不变式是系统变量在循环迭代时永远保持的特性.终止性是研究系统中是否会发生死循环.不包括终止性分析的验证被称为程序的部分正确性证明.因此,程序的终止性分析是确保程序完全正确性的必要基础.

尽管程序的终止性问题早已被证明是不可判定的[1],但对其进行研究不仅具有理论意义,更具有实际意义.当前,国内外主要通过计算秩函数来进行循环终止性分析.秩函数是验证循环程序终止性的一条重要途径.对给定的一个程序,若能找到其秩函数,则表明该程序必然是终止的.例如在2001 年,Colon 等人[2,3]就利用多面体理论计算线性程序的线性秩函数(ranking functions).2004 年,针对线性循环程序,Poldelski 等人[4]提出一个完备的线性秩函数生成方法,并开发出工具RANKFINDER.他们的方法将线性程序的线性秩函数计算问题归结为线性规划(LP)问题.在2005 年,针对线性程序,Manna 等人[5,6]提出了字典秩函数的概念,并利用Farkas 引理呈现了线性字典秩函数的计算方法.最近,文献[7,8]研究了现有几种线性秩函数生成算法的时间复杂度.文献[8]中进一步分析了程序变量在整数集合上取值时,这类线性程序的线性秩函数合成方法,并研究了这类问题的复杂度.但即便是线性程序,其秩函数也未必是线性的.因此,针对非线性程序,Cousot[9]通过半正定规划方法SDP 研究了多项式秩函数的计算问题.该方法能够找到高次数的秩函数,但由于SDP 工具内部采用的是数值计算,因此由计算误差导致最终得到的函数未必是真正的秩函数.同时,这个方法也不能回答一个程序是否具有预定义形式的秩函数.

符号计算理论方法及其工具被逐渐应用于程序自动验证.例如,我国科学家陈应华等人和杨路等人将秩函数和不变式的计算归约为半代数系统的求解,并运用基于柱形代数分解的工具DISCOVERER,提出了多项式不等式型不变式和非线性秩函数生成方法[2,10].不同于文献[9]中的方法,他们的方法能够精确回答循环程序是否有给定模板的秩函数或不变式.

除了秩函数法以外,还出现了其他方法去进行循环程序的终止性研究.如,文献[11,12]提出了试探性方法去探索给定循环程序的非终止性.众所周知,一般的程序终止性问题是不可判定的,但对某些类特殊的程序而言,人们总希望能证明其终止性问题是可判定的.由此,鉴于终止性问题本身的不可判定性所带来的实际困难,证明循环程序终止性的另一途径就是避开秩函数的合成,而采用数学方法严格证明某类或某些类循环程序的终止性是可判定的,并建立相对完备的判定算法.这首先需要对程序进行分类.当限定程序中的赋值语句和条件语句均为线性多项式时,2004 年,Tiwari 在文献[13]中首次证明了下列单重无分支线性循环程序在实域上的终止性是可判定的:

这里,A,B均是实矩阵.相似的结论在2006 年被Braveman[14]推广到整数环上.此外,为了避免Jordan 标准型的浮点计算,文献[15]中提出了精确的符号计算方法对程序P进行终止性判定.既然一般形式的线性程序终止性是不可判定的[13],那么非线性多项式循环程序由于其更为复杂的动力行为使得其终止性分析将变得更加困难.一个程序被称为非线性的,是指循环中的赋值映射或循环条件中的约束是非线性表达式.2005 年,利用有限差分树理论,文献[16]提出了试探性算法对一类含多分支语句的多项式程序的终止性问题进行判定.2010 年,针对一类赋值为线性且循环条件由非线性多项式不等式构成的循环程序,文献[17]分析了其终止性问题,证明了当这类程序满足给定的NZM 条件时,其终止性是可判定的.2013 年,文献[18]通过分析多项式映射fi的发散区间讨论了一类多项式循环(迭代赋值型如xi:=fi(xi))的终止性问题.针对一类循环条件为多项式等式,赋值语句为多项式的多分支循环程序,詹乃军等人在文献[19]中给出了其可终止或不可终止的充分条件.最近,针对这类多分支程序.他们进一步证明了各条路径形成的理想具有一致上界,从而证明了这类多分支程序的终止性是可判定的.记R为实数域,Q 为有理数域.R[x](Q[x])表示由关于x的实系数(有理系数)多项式构成的多项式环.

本文主要研究具有以下形式的多分支线性循环程序在实数域上的终止性问题.

这里,B∈Qn×n为一可逆矩阵,b∈Qn,x∈Rn,Fi(x)=(fi1(x),…,fin(x))T为关于x的n维多项式映射,fij(x)∈Q[x],i=1,...,m,j=1,...,n.记Ω={x∈Rn:Bx≥b}.为方便,令P≜P(Ω,F1,…,Fm).在上述多分支循环程序中,我们忽略了每个分支的条件判断语句,这为多分支循环的终止性研究带来了便利.这一处理方式并非新的,它早已存在于文献[19]中.

对任意给定的v个n维多项式映射g1(x),…,gv(x),令个映射的复合.我们说多分支循环程序P在实域上是不可终止的,如果存在x0∈Rn和无穷下标列表,使得对任意的非负整数n,有:

考虑程序P.令y=M-1(x)=Bx-b,Ωy={y:y≥0}.既然程序P中的矩阵B是可逆的,则M-1为可逆映射,记M-1的逆映射为M(y)=B-1(y+b).因此,M,M-1互为Rn→Rn的可逆映射.显然有,M-1是Ω到Ωy上的双射.同样地,M是Ωy到Ω上的双射.故下面的定理表明P在实数域上的终止性问题等价于下列程序在实数域上的终止性问题.

与程序P的不可终止定义类似,我们说程序U在实域上是不可终止的,如果存在y0∈Rn和无穷下标列表,使得对任意的非负整数n,有:

定理1.记号同上.程序P在实数域上不可终止等价于程序U在实数域上不可终止.

证明:若程序P在实数域上不可终止,则必存在x0∈Rn和无穷下标列表,使得对任意的n≥0,有:

这里,ij∈Λ,j=1,2,…,根据公式(3)、公式(4)中既然是从Ω到Ωy上的双射,我们有:

反之,若程序U在实数域上不可终止,那么必存在一点y0和一个无穷下标列表,使得对任意的n≥0,我们有令x0=M(y0).根据公式(4)和M-1的可逆性,有:

根据定理1 可知,P的终止性问题总能等价归结为U的终止性问题.为方便分析,不失一般性,将原来U中的程序变元y替换为x,M-1◦Fi◦M(y)替换为Ti(x),则程序U可被重写为以下形式.

这里,x=(x1,x2,…,xn)T∈Rn,Ti(x)=(ti1(x),…,tin(x))T为关于x的n维多项式映射,tij(x)∈Q[x],i=1,…,m,j=1,…,n.记:

既然P等价于程序U的终止性,因此为判定P的终止性,我们可以先分析U的终止性.

下文中,我们将通过计算多项式秩函数的方法去判定公式(5)中的程序U的终止性.

1 预备知识

本节将介绍有关秩函数、Polya 定理的相关基本知识.

定义1.给定如公式(5)定义的循环程序U.函数ρ(x)∈R[x]被称为程序U的秩函数,如果存在一个正数c＞0,使得ρ(x)满足:

•(有界):∀x,(x∈Ωx⇒ρ(x)≥0);

注:根据定义1 及下面的定义3,计算程序U的秩函数等价于在Ωx上探测m+1 个半正定多项式:

众所周知,如果一个循环程序具有秩函数,那么这个程序必定是终止的.对程序U,文献[3,5,6,20]中的方法均不能计算其秩函数.这是因为U中的表达式可以是非线性多项式表达式,而上述文中基于Farkas 引理的方法仅能计算线性循环程序的线性秩函数.针对程序U,目前有两种方法可以计算它的非线性多项式秩函数.

•一种是由杨路等人提出的基于符号计算的多项式秩函数计算方法,他们的方法是纯符号的方法,并不涉及近似计算.这一方法的特点是能够完备判定给定的程序是否具有预设模板形式的秩函数,但该方法是基于复杂度较高的柱形代数分解算法的,故可用以计算含变元较少、次数较低的秩函数合成问题.

•另一种是由Cousot 提出的基于SDP 的秩函数计算方法.利用SDP 的求解是多项式时间复杂度,该方法能够探测到含有较高次数、较多变元的秩函数.但不足之处在于,由于SDP 采用浮点计算,从而导致最终得到的秩函数可能是不精确的,故还需要进一步验证.

在下一节中,我们将给出一种新的多项式秩函数计算方法.我们的方法是基于下面的Polya 定理.首先给出一些多项式相关的定义.

定义2.给定多元齐次多项式f(x)∈R[x].我们说f是关于x的齐次多项式,如果其中的所有非零系数项的次数都相同.

这里,aα=c(α)⋅bα,其中,c(α)为α的函数.例如,考虑2 元齐2 次多项式:

其中,c((2,0))=1,b(2,0)=2,c((1,1))=2,b(1,1)=-3.

定义3.给定n元齐次(或非齐次)多项式f(x1,…,xn)∈R[x]和S⊆Rn.f在S上是正定的,如果对任意的x∈S{0},都有f(x)＞0;同时,f在S上是半正定的,如果对任意的x∈S,有f(x)≥0.

显然,若f在S上是正定的,那么f在S上必然是半正定的.记单形

定理2(Polya 定理).给定n元齐次多项式f(x)∈R[x],如果f在Δn上是正定的,那么当N充分大时,表达式(x1+…+xn)Nf(x1,…,xn)展开后的所有系数均为正.

注:Polya 定理表明,如果给定的齐次多项式f在单形上是正定的,那么必然存在N,使得展开后各项系数为正;反之,若存在N,使得展开后各项系数为正,则f在单形是半正定的(正定多项式一定是半正定的).因此,Polya 定理给出了f在单形上是正定的必要条件,同时也给出了f是单形上的半正定多项式的充分条件.但Polya 定理并没告诉我们N的界.在文献[21]中,Powers 等人构造了Polya 定理中N的界,并证明了那样的界仅仅依赖于多项式f的次数、系数和f在单形上的最小值.

定理3[21].给定在单形Δn上正定的n元齐d次多项式f(x).如果

那么,(x1+…+xn)Nf(x1,…,xn)的所有系数为正.其中,L=L(f)=max{|bα|:|α|=d},λ=λ(f)=min{f(x):x∈Δn}.

注:关于定理3 有几点说明.

(A)若存在正整数N,使得(x1+…+xn)Nf(x1,…,xn)的所有系数为正,那么对任意的非负整数j,有(x1+…+xn)N+jf(x1,…,xn)的所有系数为正.这是因为(x1+…+xn)中各项前的系数均为正数,故(x1+…+xn)j中各项前的系数必为正数.所以当(x1+…+xn)Nf(x1,…,xn)的所有系数为正时,(x1+…+xn)N+jf(x1,…,xn)=(x1+…+xn)j(x1+…+xn)Nf(x1,…,xn)的所有系数仍然为正.

(B)N的下界公式,即公式(7)中,N的下界值与L的值成正比而与最小值成反比.在下一节中,我们将通过对公式(7)中L或λ的值进行放缩来调整N的下界公式,并在新的下界公式下建立相应算法.

(C)若存在N,使得(x1+…+xn)Nf(x1,…,xn)的所有系数为正,那么f(x1,…,xn)至少是单形上的半正定多项式.这是因为所有变量取值于单形,故均为非负变量;同时,每项系数都为正.

2 程序U 的秩函数计算

本节中,我们将程序U的秩函数计算问题归结为单形上的正定多项式的探测问题,并基于Polya 和Powers等人的结果,将单形上正定多项式探测的问题归结为线性规划问题.

定义1 中的秩函数定义是传统秩函数定义,呈现在许多文献中.在定义1 中,秩函数定义的有界和下降两个条件是由有限个蕴涵式刻画,且蕴涵式后件为非严格不等式.但为了便于利用正定多项式的性质,我们将定义1中程序U的秩函数定义做了稍微修改,即将定义1 中蕴涵式后件中的非严格不等式全部替换为严格不等式.

定义4.给定如公式(5)定义的循环程序U,函数ρ(x)是程序U的秩函数,若存在一个正数c＞0,使得ρ(x)满足:

•(有界):∀x,(x∈Ωx⇒ρ(x)＞0);

注:修改后的秩函数定义与传统秩函数定义是等价的.这可被简单证明如下.

首先,若ρ(x)是满足定义1 中两个条件的秩函数,即有∀x,(x∈Ωx⇒ρ(x)≥0)且,进而有∀x,(x∈Ωx⇒ρ(x)≥0＞-1)且.那么令,则有:存在一个正数c′＞0,使得ρ′(x)满足定义4 中的有界和下降两个条件.反之,若ρ(x)是满足定义4 中两个条件的秩函数,那么ρ(x)显然也满足定义1 中的两个条件.因此,根据定义4,计算U的秩函数等价于在Ωx上探测m+1 个正定多项式.既然定义1 与定义4 等价,故计算U的秩函数⇔在Ωx上探测m+1 个半正定多项式⇔在Ωx上探测m+1 个正定多项式.根据定义4,要计算程序U的秩函数,仅需探寻函数ρ(x),使其满足定义4 中的有界和下降条件.

•(有界):

•(下降):

这里,Hi(x)=ρ(x)-ρ(Ti(x)),c＞0.一般地,公式(8)和公式9)中蕴含式后件的多项式表达式未必是关于x的齐次多项式,但我们总可以引入新的变元进行齐次化,并能保证齐次化后的蕴含式与原蕴含式是等价的.令=(,z),x记,记为Rn+1中的原点.显然,.

命题1.给定非齐次多项式G(x)∈R[x],记G的次数为d,引进新变元z,对G进行齐次化得到GH(x,z).记w1=∀x,(x∈Ωx⇒G(x)＞0)和,则有w1⇔w2.

证明:w2⇒w1是显然成立的.这是因为当蕴涵式w2成立时,令w2中的z=1 即可得到w1也成立.下证w1⇒w2.

若蕴涵式w1成立,即∀x,(x∈Ωx⇒G(x)＞0).又.若z＞0,则(x1,…,xn)∈Ωx等价于t1≥0,…,tn≥0.既然已知w1成立,因此有t1≥0∧…∧tn≥0⇒G(t1,…,tn)＞0.又因为z＞0,故

假设公式(8)和公式(9)中的多项式ρ(x),Hi(x)-c的次数分别为,然后引入新变元z,对ρ(x),Hi(x)-c,i=1,…,m进行齐次化.记齐次化所得的表达式分别为

令Δn+1={(x1,…,xn,z)∈Rn+1:x1≥0,…,xn≥0,z≥0,x1+…+xn+z=1}.

命题2.记号同上.公式(13)⇔公式(14).

注:若将公式(13)和公式(14)中的所有不等式均改为非严格不等式,则命题2 仍然成立.

S1.给出秩函数模板——带参数的多项式表达式.不失一般性,可假设为ρ(x)=aT⋅Γ,其中,a为参系数向量,Γ是所有单项式构成的向量.如ρ(x)=a1x2y+a2x+a3y+a4,则a=(a1,…,a4)T,Γ=(x2y,x,y,1)T.

S2.将ρ(x)代入到定义4 中给出的秩函数条件中,从而构造公式(8)和公式(9).其中,可记公式(9)中的Hi(x)=.这里,ba为一向量,其每个分量均是关于a的齐次线性表达式;Γ′为单项式构成的向量.如,给定循环程序的第i个赋值语句Ti(x)≜(x:=3x-4y2,y:=y)T,则Hi(x)=ρ(x)-ρ(Ti(x))=-8a1x2y-2a2x+24a1y3x+4a2y2-16a1y5.故,a=(-8a1,-2a2,24a1,4a2,-16a1)T,Γ′=(x2y,x,y3x,y2,y5)T.

S3.对公式(8)和公式(9)中的ρ(x),Hi(x)-c进行齐次化,得到:

S4.根据上述分析,因为公式(13)⇒公式(12),所以要使得公式(12)成立,只需保证公式(13)成立即可.再根据命题2 可知,公式(13)成立等价于公式(14)成立.进而将问题归结为保证公式(14)成立.

S5.探测是否存在参系数(a,ba,c)的一组取值,使得满足公式(14).若那样的一组取值存在,则表明程序U是终止的.

从上面5 个步骤可以看出,计算程序U秩函数的问题被归约为探测单形上的正定多项式的问题.也即若单形上的正定多项式被探测到,则表明程序U具有秩函数,从而证明程序U是终止的.

根据下面的命题可知,在上述S5 中,存在参系数(a,ba,c)的一组取值,使得满足公式(14),等价于存在参系数(a,ba,c)在中的一组取值使得满足式(14).这里,ℓ=|(a,ba,c)|为向量(a,ba,c)中分量的个数.表明,向量(a,ba,c)中每个分量都在区间[-1,1]中取值.

命题3.记号同上.存在,使得满足公式(14),等价于存在,使得满足公式(14).

根据定义4、命题1～命题3,我们可以建立下面的结论.

定理4.给定程序U,若存在的一组取值,使得满足公式(14),那么程序U必然终止.

这里,L=L(f)=max{|bα|:|α|=d},λ=λ(f)=min{f(x):x∈Δn}.根据下面的结论,我们可以将公式(15)中的L替换为1.

命题4.记号同上.给定齐d次n元多项式,这里,非负整数向量α=(α1,…,αn)∈Nn,则(α1+…+αn)!≥α1!…αn!.

证明:考虑n=2.

显然,(α1-0+α2)≥α1,(α1-1+α2)≥α1-1,(α1-2+α2)≥α1-2,…,(α1-(α1-1)+α2)≥1.故

考虑n=3.

根据公式(16),有(α1+α2+α3)!=(α3+(α1+α2))!≥(α3)!(α1+α2)!≥α3!α1!α2!.

以此类推,可得(α1+…+αn)!≥α1!…αn!.□

注:给定齐d次n元多项式,在公式(15)中,

定理5.给定齐d次n元多项式,且其所有系数aα均在区间[-1,1]中.如果f在Δn上是正定的,则当:

有(x1+…+xn)Nf(x1,…,xn)的所有系数为正.其中,λ=λ(f)=min{f(x):x∈Δn.

根据定理4 得知,可以在系数空间[-1,]1ℓ中探测满足公式(14)的齐次多项式.这里,.同时,满足公式(14)的恰好是单形Δn+1上的正定多项式.因此,既然在单形Δn+1上正定且其所有系数均在中取值,那么根据定理5,必然存在一个N(其值仅仅依赖于最小值λ),使得的所有系数为正.因此,为了得到(a,ba,c)的一组取值,我们可以从中抽取出所有系数(它们均是关于(a,ba,c)的齐次线性表达式),并令所有系数大于0,且加上约束,从而构造出关于(a,ba,c)的不等式组Sys.若Sys有实解,则它的任一组解就正好给出了单形Δn+1上的(半)正定多项式(这是因为根据定理2 或定理3 的注解可知,若存在N,使得展开后各项系数为正,则f在单形是半正定的).下面的定理表明,若系统Sys有实解,则程序U可终止.

定理6.记号同上.给定程序U,若系统Sys有实解,则程序U是终止的.

根据命题2 及其注解,上式等价于

在上式中令z=1,得到:

根据定义1 可知,满足上式的ρ*(x)是程序U的秩函数.故程序U可终止.□

注:根据定理6,若系统Sys有解,则能够得到一个最小值为预设定值λ*的具有预定形式的秩函数;反之,若系统Sys无解,则表明在单形上没有最小值为预设定值λ*且具有预定形式的正定多项式.

算法1.

输入:一个程序U,探测深度depth,变元个数n,次数d.

输出:一个具有预定形式的n元d次多项式秩函数.

Step 1:设定多项式秩函数模板ρ(x)=aT⋅Γ

Step 3:Fori=1 todepth

Step 3.3:用线性规划工具Simplex 计算Sys:若Sys有解,则输出多项式秩函数ρ*(x);否则,转Step 3.4

下面通过一个例子来阐述本文的方法.

例1:考虑循环程序:

记T1=(1-3x-4y-x3,-x-y),T2=(-y-1,-7x2+y).

(a)设定秩函数模板ρ(x)=a1x3+a2x2y+a3xy2+a4x2+a5xy+a6y2+a7x+a8y+a9,令

(b)对Hi(x)-c进行齐次化,得到,其中,

(c)判定是否存在(a1,...,a9)的一组取值,使得和M1(x,y,z),M2(x,y,z)在单形Δ2+1上都同时正定.要计算得到那样的一组(a1,...,a9)的取值,根据定理 5,需首先计算出N的值.根据公式(17),N依赖于各自次数以及各自在Δ3上的最小值λ.但这里,和M1(x,y,z),M2(x,y,z)均是参系数齐次多项式,故其在单形上的最小值是随着参数取值的变动而变动的.因此,在N的实际计算中,我们需要事先固定λ的值,比如可令然后,既然该例中和M1(x,y,z),M2(x,y,z)的次数分别为3,9,5,那么根据公式(17),分别计算对应的N的取值范围为

同时,根据秩函数的定义4 可知,c＞0.最后,求解不等式组.若Sys有解,则表明该程序具有预定形式的3 次秩函数.根据定理4 可知,该程序是终止的.但是因为Maple 自带的线性规划工具Simplex 仅能够求解非严格的不等式组——不等式组中的所有不等式都是非严格的,所以为了使用工具Simplex,在实际计算中,我们让合并同类项后,各自抽取出关于x,y,z项的所有系数,然后再令所有系数≥某个正数δ.这相当于对,中的所有不等式做了一个小小的扰动,即将＞0 替换为≥δ(δ＞0).记扰动后的系数集为.同时,将c＞0 扰动为c≥δ.显然,扰动后的系统为非严格不等式组,如果它有解,则原系统Sys也必有解.为方便,我们让Sys,不仅表示不等式系统,而且还表示不等式系统所对应的解集.在本例中,我们取.利用Maple 中的线性规划工具包Simplex,求解不等式组,得到:

注:对于该程序,文献[3,5,6,20]中的方法已不能计算其预定形式的3 次秩函数.因为这些方法仅能计算线性循环程序的线性秩函数,而本例中的循环是非线性的,且所要计算的秩函数也是3 次的.此外,对该程序,我们也尝试利用一些基于量词消去技术[22]的工具,如Redlog、RegularChains,去计算该程序的预定形式的3 次秩函数(其中,RegularChains 集成了当前功能强大的实解分类工具DISCOVERER[23],作者此前的诸多工作也是在该工具的支持下予以开展).这等价于利用这些量词消去工具从秩函数定义4 中的两个蕴含公式(8)和公式(9)中消去变元x,y即可.但由于量词消去算法的双指数复杂度以及所处理的系统都是非线性的,从而使得这两个工具均无法计算得到该程序的3 次秩函数.同时,我们也尝试用Cousot 在文献[9]中的方法——半正定规划(SDP),并借助半正定规划求解器YALMIP[24]计算得到一个函数:

但经过检验发现,该函数并不满足秩函数定义中的有界条件,因此它不是程序的秩函数.

例2:考虑循环程序:

通过本文方法,我们得到该循环的一个3 次秩函数:

例3:考虑循环程序:

基于Polya 定理,算法1 提供了一个试探性方法去探测程序U的多项式秩函数.下面我们将证明,给定齐d次n元多项式若

(A)所有系数均为整数,即aα∈Z,

(B)其系数的绝对值被界定,即存在正数η,使得|aα|≤η,则Polya 定理中关于N的下界公式可以被改写为

显然,上述N的下界公式仅依赖于多项式f(x)的次数、变元个数以及系数的绝对值上界.根据公式(21),我们将建立不同于算法1 的新算法.在证明上述结论之前,我们首先引入文献[25]中建立的关于整系数正定多项式在单形上的最小值下界的一个重要结果.

定理7[25].给定d次n元齐次整系数多项式,其系数均被正数η界定,即|aα|≤η.记为单形.如果f(x)在单形Δn上是正定的,那么有:

注:因本文仅考虑单形上的正定多项式,故定理7 只引述了文献[25]中引理3.3 中的前部分结论,其后部分所涉及到单形上的负定多项式的内容在此被舍去.

根据定理2、定理3 及其定理7,我们建立下列定理8.

定理8.给定d次n元齐次整系数多项式,且其系数均被正数η界定,即|aα|≤η.如果f在Δn上是正定的,那么当

时,有(x1+…+xn)Nf(x1,…,xn)的所有系数为正.这里,

证明:首先,根据定理3 可知,如果n元齐d次多项式f(x)在单形上正定,那么存在正整数N,当其满足:

时,有(x1+…+xn)Nf(x1,…,xn)的所有系数为正.其中,L=L(f)=max{|bα|:|α|=d},λ=λ(f)=min{f(x):x∈Δn}.再根据命题4及其注解可知,倘若f的所有系数aα均在区间[-η,η]中,那么,

同时,根据已知题设,既然f在单形上正定且其所有系数均为整数并均被正数η界定,那么由定理7 可得,f在单形Δn上的最小值:

根据公式(25)和公式(26)将公式(24)进行放缩,即得到公式(23).□

注:定理8 中,公式(23)中N的下界公式仅仅依赖多项式的次数、变元个数以及系数绝对值上界.

(i)根据公式(23)计算N的值,记为NG;

这里,gα(v)为齐次整系数线性函数这一限定具有一般性.这是因为,若多项式G的系数均是有理数,那么总可以通过乘上所有有理数的分母将其系数变为整数.根据公式(5),程序U中的所有系数均为有理数,故参数模板多项式的所有系数均为有理数.因此,可以将所有有理数系数的分母(若有负号,则将负号放到分子上)都乘在一起,记为β.则在公式(14)中的不等式两端同时乘上β并不会改变不等式的符号,故有的系数均为整数.也即β⋅gα(ba,c)是关于参数ba,c的齐次整系数线性函数.因此,若含有有理系数,则可以乘上一个正数β,使得其所有系数为整数.根据公式(23),分别计算并抽取的所有系数分别构造不等式组.令S.既然所有参数均被设定为整数,故需要在整数环上求解系统类似定理6,下面的定理9表明,若Sysℤ有整数解,则程序U是终止的.

定理9.记号同上.给定程序U.若系统SysZ有整数解,那么程序U有预定形式的且系数绝对值上界为η的秩函数.

证明:该证明完全类似于定理6 的证明.在此省略.□

注:定理9 表明,若系统SysZ有整数解,则程序U有一个整系数多项式秩函数;反之,如果系统SysZ没有整数解,则表明在单形上没有预定形式的且系数在[-η,η]的正定多项式.此时需要增大上界η的值继续构造新的系统并求解.因此,整个过程仍是试探性的.

算法2.

输入:一个程序U,变元个数n,次数d,系数绝对值上界η.

输出:一个具有预定形式的n元d次整系数多项式秩函数;不确定(unknown).

Step 1:设定多项式秩函数模板ρ(x)=aT⋅Γ

3 总结

针对一类多项式循环程序,本文给出了一种新的方法去计算这类程序的多项式秩函数.该方法将这类程序的秩函数计算归结为单形上的正定多项式的探测问题;然后,利用Polya 定理,将单形上的正定多项式探测问题归结为线性不等式约束系统的可行问题.从这一角度看,我们的方法是一个“线性化”的方法.而线性不等式系统的可行问题则可以利用(整数)线性规划工具进行求解.相对于现有诸如Redlog、RegularChains 等基于柱形代数分解的量词消去工具,本文的算法1 可以在可接受时间内进行复杂秩函数的计算.同时,也不同于基于SDP 的方法,通过本文方法计算得到的函数是精确的秩函数,因此不必再次验证计算所得的函数是否为秩函数.