李 軼, 馮 勇

(中國科學院 重慶綠色智能技術(shù)研究院,重慶 401120)

嵌入式系統(tǒng)在人類生活中發(fā)揮著越來越大的作用,而作為嵌入式系統(tǒng)靈魂的嵌入式軟件在其中所占有的比重也越來越大.因此,嵌入式軟件的可靠性將變得更加重要.諸如航空、航天、軍事、交通、醫(yī)療等關(guān)鍵應用領(lǐng)域都對嵌入式系統(tǒng)的可靠性和安全性要求非常高,任何錯誤的發(fā)生都可能帶來災難性后果.嵌入式系統(tǒng)具有3 個重要屬性,即可達性、終止性、不變式.可達性是指一個系統(tǒng)能否從一個給定狀態(tài)到達另一個可接受狀態(tài).某些混成系統(tǒng)的可達性被證明是能用計算機代數(shù)工具來檢驗的.不變式是系統(tǒng)變量在循環(huán)迭代時永遠保持的特性.終止性是研究系統(tǒng)中是否會發(fā)生死循環(huán).不包括終止性分析的驗證被稱為程序的部分正確性證明.因此,程序的終止性分析是確保程序完全正確性的必要基礎(chǔ).

盡管程序的終止性問題早已被證明是不可判定的[1],但對其進行研究不僅具有理論意義,更具有實際意義.當前,國內(nèi)外主要通過計算秩函數(shù)來進行循環(huán)終止性分析.秩函數(shù)是驗證循環(huán)程序終止性的一條重要途徑.對給定的一個程序,若能找到其秩函數(shù),則表明該程序必然是終止的.例如在2001 年,Colon 等人[2,3]就利用多面體理論計算線性程序的線性秩函數(shù)(ranking functions).2004 年,針對線性循環(huán)程序,Poldelski 等人[4]提出一個完備的線性秩函數(shù)生成方法,并開發(fā)出工具RANKFINDER.他們的方法將線性程序的線性秩函數(shù)計算問題歸結(jié)為線性規(guī)劃(LP)問題.在2005 年,針對線性程序,Manna 等人[5,6]提出了字典秩函數(shù)的概念,并利用Farkas 引理呈現(xiàn)了線性字典秩函數(shù)的計算方法.最近,文獻[7,8]研究了現(xiàn)有幾種線性秩函數(shù)生成算法的時間復雜度.文獻[8]中進一步分析了程序變量在整數(shù)集合上取值時,這類線性程序的線性秩函數(shù)合成方法,并研究了這類問題的復雜度.但即便是線性程序,其秩函數(shù)也未必是線性的.因此,針對非線性程序,Cousot[9]通過半正定規(guī)劃方法SDP 研究了多項式秩函數(shù)的計算問題.該方法能夠找到高次數(shù)的秩函數(shù),但由于SDP 工具內(nèi)部采用的是數(shù)值計算,因此由計算誤差導致最終得到的函數(shù)未必是真正的秩函數(shù).同時,這個方法也不能回答一個程序是否具有預定義形式的秩函數(shù).

符號計算理論方法及其工具被逐漸應用于程序自動驗證.例如,我國科學家陳應華等人和楊路等人將秩函數(shù)和不變式的計算歸約為半代數(shù)系統(tǒng)的求解,并運用基于柱形代數(shù)分解的工具DISCOVERER,提出了多項式不等式型不變式和非線性秩函數(shù)生成方法[2,10].不同于文獻[9]中的方法,他們的方法能夠精確回答循環(huán)程序是否有給定模板的秩函數(shù)或不變式.

除了秩函數(shù)法以外,還出現(xiàn)了其他方法去進行循環(huán)程序的終止性研究.如,文獻[11,12]提出了試探性方法去探索給定循環(huán)程序的非終止性.眾所周知,一般的程序終止性問題是不可判定的,但對某些類特殊的程序而言,人們總希望能證明其終止性問題是可判定的.由此,鑒于終止性問題本身的不可判定性所帶來的實際困難,證明循環(huán)程序終止性的另一途徑就是避開秩函數(shù)的合成,而采用數(shù)學方法嚴格證明某類或某些類循環(huán)程序的終止性是可判定的,并建立相對完備的判定算法.這首先需要對程序進行分類.當限定程序中的賦值語句和條件語句均為線性多項式時,2004 年,Tiwari 在文獻[13]中首次證明了下列單重無分支線性循環(huán)程序在實域上的終止性是可判定的:

這里,A,B均是實矩陣.相似的結(jié)論在2006 年被Braveman[14]推廣到整數(shù)環(huán)上.此外,為了避免Jordan 標準型的浮點計算,文獻[15]中提出了精確的符號計算方法對程序P進行終止性判定.既然一般形式的線性程序終止性是不可判定的[13],那么非線性多項式循環(huán)程序由于其更為復雜的動力行為使得其終止性分析將變得更加困難.一個程序被稱為非線性的,是指循環(huán)中的賦值映射或循環(huán)條件中的約束是非線性表達式.2005 年,利用有限差分樹理論,文獻[16]提出了試探性算法對一類含多分支語句的多項式程序的終止性問題進行判定.2010 年,針對一類賦值為線性且循環(huán)條件由非線性多項式不等式構(gòu)成的循環(huán)程序,文獻[17]分析了其終止性問題,證明了當這類程序滿足給定的NZM 條件時,其終止性是可判定的.2013 年,文獻[18]通過分析多項式映射fi的發(fā)散區(qū)間討論了一類多項式循環(huán)(迭代賦值型如xi:=fi(xi))的終止性問題.針對一類循環(huán)條件為多項式等式,賦值語句為多項式的多分支循環(huán)程序,詹乃軍等人在文獻[19]中給出了其可終止或不可終止的充分條件.最近,針對這類多分支程序.他們進一步證明了各條路徑形成的理想具有一致上界,從而證明了這類多分支程序的終止性是可判定的.記R為實數(shù)域,Q 為有理數(shù)域.R[x](Q[x])表示由關(guān)于x的實系數(shù)(有理系數(shù))多項式構(gòu)成的多項式環(huán).

本文主要研究具有以下形式的多分支線性循環(huán)程序在實數(shù)域上的終止性問題.

這里,B∈Qn×n為一可逆矩陣,b∈Qn,x∈Rn,Fi(x)=(fi1(x),…,fin(x))T為關(guān)于x的n維多項式映射,fij(x)∈Q[x],i=1,...,m,j=1,...,n.記Ω={x∈Rn:Bx≥b}.為方便,令P?P(Ω,F1,…,Fm).在上述多分支循環(huán)程序中,我們忽略了每個分支的條件判斷語句,這為多分支循環(huán)的終止性研究帶來了便利.這一處理方式并非新的,它早已存在于文獻[19]中.

對任意給定的v個n維多項式映射g1(x),…,gv(x),令個映射的復合.我們說多分支循環(huán)程序P在實域上是不可終止的,如果存在x0∈Rn和無窮下標列表,使得對任意的非負整數(shù)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在實數(shù)域上的終止性問題等價于下列程序在實數(shù)域上的終止性問題.

與程序P的不可終止定義類似,我們說程序U在實域上是不可終止的,如果存在y0∈Rn和無窮下標列表,使得對任意的非負整數(shù)n,有:

定理1.記號同上.程序P在實數(shù)域上不可終止等價于程序U在實數(shù)域上不可終止.

證明:若程序P在實數(shù)域上不可終止,則必存在x0∈Rn和無窮下標列表,使得對任意的n≥0,有:

這里,ij∈Λ,j=1,2,…,根據(jù)公式(3)、公式(4)中既然是從Ω到Ωy上的雙射,我們有:

反之,若程序U在實數(shù)域上不可終止,那么必存在一點y0和一個無窮下標列表,使得對任意的n≥0,我們有令x0=M(y0).根據(jù)公式(4)和M-1的可逆性,有:

根據(jù)定理1 可知,P的終止性問題總能等價歸結(jié)為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為關(guān)于x的n維多項式映射,tij(x)∈Q[x],i=1,…,m,j=1,…,n.記:

既然P等價于程序U的終止性,因此為判定P的終止性,我們可以先分析U的終止性.

下文中,我們將通過計算多項式秩函數(shù)的方法去判定公式(5)中的程序U的終止性.

1 預備知識

本節(jié)將介紹有關(guān)秩函數(shù)、Polya 定理的相關(guān)基本知識.

定義1.給定如公式(5)定義的循環(huán)程序U.函數(shù)ρ(x)∈R[x]被稱為程序U的秩函數(shù),如果存在一個正數(shù)c＞0,使得ρ(x)滿足:

?(有界):?x,(x∈Ωx?ρ(x)≥0);

注:根據(jù)定義1 及下面的定義3,計算程序U的秩函數(shù)等價于在Ωx上探測m+1 個半正定多項式:

眾所周知,如果一個循環(huán)程序具有秩函數(shù),那么這個程序必定是終止的.對程序U,文獻[3,5,6,20]中的方法均不能計算其秩函數(shù).這是因為U中的表達式可以是非線性多項式表達式,而上述文中基于Farkas 引理的方法僅能計算線性循環(huán)程序的線性秩函數(shù).針對程序U,目前有兩種方法可以計算它的非線性多項式秩函數(shù).

?一種是由楊路等人提出的基于符號計算的多項式秩函數(shù)計算方法,他們的方法是純符號的方法,并不涉及近似計算.這一方法的特點是能夠完備判定給定的程序是否具有預設(shè)模板形式的秩函數(shù),但該方法是基于復雜度較高的柱形代數(shù)分解算法的,故可用以計算含變元較少、次數(shù)較低的秩函數(shù)合成問題.

?另一種是由Cousot 提出的基于SDP 的秩函數(shù)計算方法.利用SDP 的求解是多項式時間復雜度,該方法能夠探測到含有較高次數(shù)、較多變元的秩函數(shù).但不足之處在于,由于SDP 采用浮點計算,從而導致最終得到的秩函數(shù)可能是不精確的,故還需要進一步驗證.

在下一節(jié)中,我們將給出一種新的多項式秩函數(shù)計算方法.我們的方法是基于下面的Polya 定理.首先給出一些多項式相關(guān)的定義.

定義2.給定多元齊次多項式f(x)∈R[x].我們說f是關(guān)于x的齊次多項式,如果其中的所有非零系數(shù)項的次數(shù)都相同.

這里,aα=c(α)?bα,其中,c(α)為α的函數(shù).例如,考慮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)展開后的所有系數(shù)均為正.

注:Polya 定理表明,如果給定的齊次多項式f在單形上是正定的,那么必然存在N,使得展開后各項系數(shù)為正;反之,若存在N,使得展開后各項系數(shù)為正,則f在單形是半正定的(正定多項式一定是半正定的).因此,Polya 定理給出了f在單形上是正定的必要條件,同時也給出了f是單形上的半正定多項式的充分條件.但Polya 定理并沒告訴我們N的界.在文獻[21]中,Powers 等人構(gòu)造了Polya 定理中N的界,并證明了那樣的界僅僅依賴于多項式f的次數(shù)、系數(shù)和f在單形上的最小值.

定理3[21].給定在單形Δn上正定的n元齊d次多項式f(x).如果

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

注:關(guān)于定理3 有幾點說明.

(A)若存在正整數(shù)N,使得(x1+…+xn)Nf(x1,…,xn)的所有系數(shù)為正,那么對任意的非負整數(shù)j,有(x1+…+xn)N+jf(x1,…,xn)的所有系數(shù)為正.這是因為(x1+…+xn)中各項前的系數(shù)均為正數(shù),故(x1+…+xn)j中各項前的系數(shù)必為正數(shù).所以當(x1+…+xn)Nf(x1,…,xn)的所有系數(shù)為正時,(x1+…+xn)N+jf(x1,…,xn)=(x1+…+xn)j(x1+…+xn)Nf(x1,…,xn)的所有系數(shù)仍然為正.

(B)N的下界公式,即公式(7)中,N的下界值與L的值成正比而與最小值成反比.在下一節(jié)中,我們將通過對公式(7)中L或λ的值進行放縮來調(diào)整N的下界公式,并在新的下界公式下建立相應算法.

(C)若存在N,使得(x1+…+xn)Nf(x1,…,xn)的所有系數(shù)為正,那么f(x1,…,xn)至少是單形上的半正定多項式.這是因為所有變量取值于單形,故均為非負變量;同時,每項系數(shù)都為正.

2 程序U 的秩函數(shù)計算

本節(jié)中,我們將程序U的秩函數(shù)計算問題歸結(jié)為單形上的正定多項式的探測問題,并基于Polya 和Powers等人的結(jié)果,將單形上正定多項式探測的問題歸結(jié)為線性規(guī)劃問題.

定義1 中的秩函數(shù)定義是傳統(tǒng)秩函數(shù)定義,呈現(xiàn)在許多文獻中.在定義1 中,秩函數(shù)定義的有界和下降兩個條件是由有限個蘊涵式刻畫,且蘊涵式后件為非嚴格不等式.但為了便于利用正定多項式的性質(zhì),我們將定義1中程序U的秩函數(shù)定義做了稍微修改,即將定義1 中蘊涵式后件中的非嚴格不等式全部替換為嚴格不等式.

定義4.給定如公式(5)定義的循環(huán)程序U,函數(shù)ρ(x)是程序U的秩函數(shù),若存在一個正數(shù)c＞0,使得ρ(x)滿足:

?(有界):?x,(x∈Ωx?ρ(x)＞0);

注:修改后的秩函數(shù)定義與傳統(tǒng)秩函數(shù)定義是等價的.這可被簡單證明如下.

首先,若ρ(x)是滿足定義1 中兩個條件的秩函數(shù),即有?x,(x∈Ωx?ρ(x)≥0)且,進而有?x,(x∈Ωx?ρ(x)≥0＞-1)且.那么令,則有:存在一個正數(shù)c′＞0,使得ρ′(x)滿足定義4 中的有界和下降兩個條件.反之,若ρ(x)是滿足定義4 中兩個條件的秩函數(shù),那么ρ(x)顯然也滿足定義1 中的兩個條件.因此,根據(jù)定義4,計算U的秩函數(shù)等價于在Ωx上探測m+1 個正定多項式.既然定義1 與定義4 等價,故計算U的秩函數(shù)?在Ωx上探測m+1 個半正定多項式?在Ωx上探測m+1 個正定多項式.根據(jù)定義4,要計算程序U的秩函數(shù),僅需探尋函數(shù)ρ(x),使其滿足定義4 中的有界和下降條件.

?(有界):

?(下降):

這里,Hi(x)=ρ(x)-ρ(Ti(x)),c＞0.一般地,公式(8)和公式9)中蘊含式后件的多項式表達式未必是關(guān)于x的齊次多項式,但我們總可以引入新的變元進行齊次化,并能保證齊次化后的蘊含式與原蘊含式是等價的.令=(,z),x記,記為Rn+1中的原點.顯然,.

命題1.給定非齊次多項式G(x)∈R[x],記G的次數(shù)為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,故

假設(shè)公式(8)和公式(9)中的多項式ρ(x),Hi(x)-c的次數(shù)分別為,然后引入新變元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.給出秩函數(shù)模板——帶參數(shù)的多項式表達式.不失一般性,可假設(shè)為ρ(x)=aT?Γ,其中,a為參系數(shù)向量,Γ是所有單項式構(gòu)成的向量.如ρ(x)=a1x2y+a2x+a3y+a4,則a=(a1,…,a4)T,Γ=(x2y,x,y,1)T.

S2.將ρ(x)代入到定義4 中給出的秩函數(shù)條件中,從而構(gòu)造公式(8)和公式(9).其中,可記公式(9)中的Hi(x)=.這里,ba為一向量,其每個分量均是關(guān)于a的齊次線性表達式;?！錇閱雾検綐?gòu)成的向量.如,給定循環(huán)程序的第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.根據(jù)上述分析,因為公式(13)?公式(12),所以要使得公式(12)成立,只需保證公式(13)成立即可.再根據(jù)命題2 可知,公式(13)成立等價于公式(14)成立.進而將問題歸結(jié)為保證公式(14)成立.

S5.探測是否存在參系數(shù)(a,ba,c)的一組取值,使得滿足公式(14).若那樣的一組取值存在,則表明程序U是終止的.

從上面5 個步驟可以看出,計算程序U秩函數(shù)的問題被歸約為探測單形上的正定多項式的問題.也即若單形上的正定多項式被探測到,則表明程序U具有秩函數(shù),從而證明程序U是終止的.

根據(jù)下面的命題可知,在上述S5 中,存在參系數(shù)(a,ba,c)的一組取值,使得滿足公式(14),等價于存在參系數(shù)(a,ba,c)在中的一組取值使得滿足式(14).這里,?=|(a,ba,c)|為向量(a,ba,c)中分量的個數(shù).表明,向量(a,ba,c)中每個分量都在區(qū)間[-1,1]中取值.

命題3.記號同上.存在,使得滿足公式(14),等價于存在,使得滿足公式(14).

根據(jù)定義4、命題1～命題3,我們可以建立下面的結(jié)論.

定理4.給定程序U,若存在的一組取值,使得滿足公式(14),那么程序U必然終止.

這里,L=L(f)=max{|bα|:|α|=d},λ=λ(f)=min{f(x):x∈Δn}.根據(jù)下面的結(jié)論,我們可以將公式(15)中的L替換為1.

命題4.記號同上.給定齊d次n元多項式,這里,非負整數(shù)向量α=(α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.

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

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

注:給定齊d次n元多項式,在公式(15)中,

定理5.給定齊d次n元多項式,且其所有系數(shù)aα均在區(qū)間[-1,1]中.如果f在Δn上是正定的,則當:

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

根據(jù)定理4 得知,可以在系數(shù)空間[-1,]1?中探測滿足公式(14)的齊次多項式.這里,.同時,滿足公式(14)的恰好是單形Δn+1上的正定多項式.因此,既然在單形Δn+1上正定且其所有系數(shù)均在中取值,那么根據(jù)定理5,必然存在一個N(其值僅僅依賴于最小值λ),使得的所有系數(shù)為正.因此,為了得到(a,ba,c)的一組取值,我們可以從中抽取出所有系數(shù)(它們均是關(guān)于(a,ba,c)的齊次線性表達式),并令所有系數(shù)大于0,且加上約束,從而構(gòu)造出關(guān)于(a,ba,c)的不等式組Sys.若Sys有實解,則它的任一組解就正好給出了單形Δn+1上的(半)正定多項式(這是因為根據(jù)定理2 或定理3 的注解可知,若存在N,使得展開后各項系數(shù)為正,則f在單形是半正定的).下面的定理表明,若系統(tǒng)Sys有實解,則程序U可終止.

定理6.記號同上.給定程序U,若系統(tǒng)Sys有實解,則程序U是終止的.

根據(jù)命題2 及其注解,上式等價于

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

根據(jù)定義1 可知,滿足上式的ρ*(x)是程序U的秩函數(shù).故程序U可終止.□

注:根據(jù)定理6,若系統(tǒng)Sys有解,則能夠得到一個最小值為預設(shè)定值λ*的具有預定形式的秩函數(shù);反之,若系統(tǒng)Sys無解,則表明在單形上沒有最小值為預設(shè)定值λ*且具有預定形式的正定多項式.

算法1.

輸入:一個程序U,探測深度depth,變元個數(shù)n,次數(shù)d.

輸出:一個具有預定形式的n元d次多項式秩函數(shù).

Step 1:設(shè)定多項式秩函數(shù)模板ρ(x)=aT?Γ

Step 3:Fori=1 todepth

Step 3.3:用線性規(guī)劃工具Simplex 計算Sys:若Sys有解,則輸出多項式秩函數(shù)ρ*(x);否則,轉(zhuǎn)Step 3.4

下面通過一個例子來闡述本文的方法.

例1:考慮循環(huán)程序:

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

(a)設(shè)定秩函數(shù)模板ρ(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)的取值,根據(jù)定理 5,需首先計算出N的值.根據(jù)公式(17),N依賴于各自次數(shù)以及各自在Δ3上的最小值λ.但這里,和M1(x,y,z),M2(x,y,z)均是參系數(shù)齊次多項式,故其在單形上的最小值是隨著參數(shù)取值的變動而變動的.因此,在N的實際計算中,我們需要事先固定λ的值,比如可令然后,既然該例中和M1(x,y,z),M2(x,y,z)的次數(shù)分別為3,9,5,那么根據(jù)公式(17),分別計算對應的N的取值范圍為

同時,根據(jù)秩函數(shù)的定義4 可知,c＞0.最后,求解不等式組.若Sys有解,則表明該程序具有預定形式的3 次秩函數(shù).根據(jù)定理4 可知,該程序是終止的.但是因為Maple 自帶的線性規(guī)劃工具Simplex 僅能夠求解非嚴格的不等式組——不等式組中的所有不等式都是非嚴格的,所以為了使用工具Simplex,在實際計算中,我們讓合并同類項后,各自抽取出關(guān)于x,y,z項的所有系數(shù),然后再令所有系數(shù)≥某個正數(shù)δ.這相當于對,中的所有不等式做了一個小小的擾動,即將＞0 替換為≥δ(δ＞0).記擾動后的系數(shù)集為.同時,將c＞0 擾動為c≥δ.顯然,擾動后的系統(tǒng)為非嚴格不等式組,如果它有解,則原系統(tǒng)Sys也必有解.為方便,我們讓Sys,不僅表示不等式系統(tǒng),而且還表示不等式系統(tǒng)所對應的解集.在本例中,我們?nèi)?利用Maple 中的線性規(guī)劃工具包Simplex,求解不等式組,得到:

注:對于該程序,文獻[3,5,6,20]中的方法已不能計算其預定形式的3 次秩函數(shù).因為這些方法僅能計算線性循環(huán)程序的線性秩函數(shù),而本例中的循環(huán)是非線性的,且所要計算的秩函數(shù)也是3 次的.此外,對該程序,我們也嘗試利用一些基于量詞消去技術(shù)[22]的工具,如Redlog、RegularChains,去計算該程序的預定形式的3 次秩函數(shù)(其中,RegularChains 集成了當前功能強大的實解分類工具DISCOVERER[23],作者此前的諸多工作也是在該工具的支持下予以開展).這等價于利用這些量詞消去工具從秩函數(shù)定義4 中的兩個蘊含公式(8)和公式(9)中消去變元x,y即可.但由于量詞消去算法的雙指數(shù)復雜度以及所處理的系統(tǒng)都是非線性的,從而使得這兩個工具均無法計算得到該程序的3 次秩函數(shù).同時,我們也嘗試用Cousot 在文獻[9]中的方法——半正定規(guī)劃(SDP),并借助半正定規(guī)劃求解器YALMIP[24]計算得到一個函數(shù):

但經(jīng)過檢驗發(fā)現(xiàn),該函數(shù)并不滿足秩函數(shù)定義中的有界條件,因此它不是程序的秩函數(shù).

例2:考慮循環(huán)程序:

通過本文方法,我們得到該循環(huán)的一個3 次秩函數(shù):

例3:考慮循環(huán)程序:

基于Polya 定理,算法1 提供了一個試探性方法去探測程序U的多項式秩函數(shù).下面我們將證明,給定齊d次n元多項式若

(A)所有系數(shù)均為整數(shù),即aα∈Z,

(B)其系數(shù)的絕對值被界定,即存在正數(shù)η,使得|aα|≤η,則Polya 定理中關(guān)于N的下界公式可以被改寫為

顯然,上述N的下界公式僅依賴于多項式f(x)的次數(shù)、變元個數(shù)以及系數(shù)的絕對值上界.根據(jù)公式(21),我們將建立不同于算法1 的新算法.在證明上述結(jié)論之前,我們首先引入文獻[25]中建立的關(guān)于整系數(shù)正定多項式在單形上的最小值下界的一個重要結(jié)果.

定理7[25].給定d次n元齊次整系數(shù)多項式,其系數(shù)均被正數(shù)η界定,即|aα|≤η.記為單形.如果f(x)在單形Δn上是正定的,那么有:

注:因本文僅考慮單形上的正定多項式,故定理7 只引述了文獻[25]中引理3.3 中的前部分結(jié)論,其后部分所涉及到單形上的負定多項式的內(nèi)容在此被舍去.

根據(jù)定理2、定理3 及其定理7,我們建立下列定理8.

定理8.給定d次n元齊次整系數(shù)多項式,且其系數(shù)均被正數(shù)η界定,即|aα|≤η.如果f在Δn上是正定的,那么當

時,有(x1+…+xn)Nf(x1,…,xn)的所有系數(shù)為正.這里,

證明:首先,根據(jù)定理3 可知,如果n元齊d次多項式f(x)在單形上正定,那么存在正整數(shù)N,當其滿足:

時,有(x1+…+xn)Nf(x1,…,xn)的所有系數(shù)為正.其中,L=L(f)=max{|bα|:|α|=d},λ=λ(f)=min{f(x):x∈Δn}.再根據(jù)命題4及其注解可知,倘若f的所有系數(shù)aα均在區(qū)間[-η,η]中,那么,

同時,根據(jù)已知題設(shè),既然f在單形上正定且其所有系數(shù)均為整數(shù)并均被正數(shù)η界定,那么由定理7 可得,f在單形Δn上的最小值:

根據(jù)公式(25)和公式(26)將公式(24)進行放縮,即得到公式(23).□

注:定理8 中,公式(23)中N的下界公式僅僅依賴多項式的次數(shù)、變元個數(shù)以及系數(shù)絕對值上界.

(i)根據(jù)公式(23)計算N的值,記為NG;

這里,gα(v)為齊次整系數(shù)線性函數(shù)這一限定具有一般性.這是因為,若多項式G的系數(shù)均是有理數(shù),那么總可以通過乘上所有有理數(shù)的分母將其系數(shù)變?yōu)檎麛?shù).根據(jù)公式(5),程序U中的所有系數(shù)均為有理數(shù),故參數(shù)模板多項式的所有系數(shù)均為有理數(shù).因此,可以將所有有理數(shù)系數(shù)的分母(若有負號,則將負號放到分子上)都乘在一起,記為β.則在公式(14)中的不等式兩端同時乘上β并不會改變不等式的符號,故有的系數(shù)均為整數(shù).也即β?gα(ba,c)是關(guān)于參數(shù)ba,c的齊次整系數(shù)線性函數(shù).因此,若含有有理系數(shù),則可以乘上一個正數(shù)β,使得其所有系數(shù)為整數(shù).根據(jù)公式(23),分別計算并抽取的所有系數(shù)分別構(gòu)造不等式組.令S.既然所有參數(shù)均被設(shè)定為整數(shù),故需要在整數(shù)環(huán)上求解系統(tǒng)類似定理6,下面的定理9表明,若Sys?有整數(shù)解,則程序U是終止的.

定理9.記號同上.給定程序U.若系統(tǒng)SysZ有整數(shù)解,那么程序U有預定形式的且系數(shù)絕對值上界為η的秩函數(shù).

證明:該證明完全類似于定理6 的證明.在此省略.□

注:定理9 表明,若系統(tǒng)SysZ有整數(shù)解,則程序U有一個整系數(shù)多項式秩函數(shù);反之,如果系統(tǒng)SysZ沒有整數(shù)解,則表明在單形上沒有預定形式的且系數(shù)在[-η,η]的正定多項式.此時需要增大上界η的值繼續(xù)構(gòu)造新的系統(tǒng)并求解.因此,整個過程仍是試探性的.

算法2.

輸入:一個程序U,變元個數(shù)n,次數(shù)d,系數(shù)絕對值上界η.

輸出:一個具有預定形式的n元d次整系數(shù)多項式秩函數(shù);不確定(unknown).

Step 1:設(shè)定多項式秩函數(shù)模板ρ(x)=aT?Γ

3 總結(jié)

針對一類多項式循環(huán)程序,本文給出了一種新的方法去計算這類程序的多項式秩函數(shù).該方法將這類程序的秩函數(shù)計算歸結(jié)為單形上的正定多項式的探測問題;然后,利用Polya 定理,將單形上的正定多項式探測問題歸結(jié)為線性不等式約束系統(tǒng)的可行問題.從這一角度看,我們的方法是一個“線性化”的方法.而線性不等式系統(tǒng)的可行問題則可以利用(整數(shù))線性規(guī)劃工具進行求解.相對于現(xiàn)有諸如Redlog、RegularChains 等基于柱形代數(shù)分解的量詞消去工具,本文的算法1 可以在可接受時間內(nèi)進行復雜秩函數(shù)的計算.同時,也不同于基于SDP 的方法,通過本文方法計算得到的函數(shù)是精確的秩函數(shù),因此不必再次驗證計算所得的函數(shù)是否為秩函數(shù).