国产日韩欧美一区二区三区三州_亚洲少妇熟女av_久久久久亚洲av国产精品_波多野结衣网站一区二区_亚洲欧美色片在线91_国产亚洲精品精品国产优播av_日本一区二区三区波多野结衣 _久久国产av不卡

?

基于SVM的多項(xiàng)式循環(huán)程序秩函數(shù)生成*

2019-08-13 05:06蔡天訓(xùn)樊建峰吳文淵
軟件學(xué)報(bào) 2019年7期
關(guān)鍵詞:分式代數(shù)線性

李 軼, 蔡天訓(xùn), 樊建峰,3, 吳文淵, 馮 勇

1(中國科學(xué)院 重慶綠色智能技術(shù)研究院 自動(dòng)推理與認(rèn)知重慶市重點(diǎn)實(shí)驗(yàn)室,重慶 400714)

2(薩基姆通訊(深圳)有限公司,廣東 深圳 518000)

3(中國科學(xué)院大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,北京 100093)

循環(huán)程序的終止性分析是程序驗(yàn)證的一個(gè)重要研究分支.在現(xiàn)代程序設(shè)計(jì)中,幾乎所有的程序都會(huì)含有循環(huán).然而,即使是簡單的循環(huán)程序,也很容易出錯(cuò).循環(huán)中的很多錯(cuò)誤往往需要執(zhí)行多次或在某些特定情況下才能被發(fā)現(xiàn).因此,確保循環(huán)程序是可終止的是保障軟件能夠可靠運(yùn)行的一個(gè)必要條件.盡管程序終止性問題早已被證明是一個(gè)不可判定問題[1,2].但是人們發(fā)現(xiàn),具有某些特征的循環(huán)程序的終止性是可判定的.如:Tiwari在2004年證明了一類線性循環(huán)程序在實(shí)數(shù)域上的終止性是可判定[3].這類程序的終止性在文獻(xiàn)[4-7]中被重新考慮.此外,Zhan等人在文獻(xiàn)[8]中考慮了循環(huán)條件為等式的多項(xiàng)式程序的終止性問題,并給出了該類程序可終止和不可終止的充分判準(zhǔn).在文獻(xiàn)[9]中,Zhang等人建立了針對(duì)程序終止性驗(yàn)證的高級(jí)自動(dòng)機(jī)算法.在循環(huán)非終止研究方面,Zhang給出了一種能夠檢測出簡單循環(huán)中出現(xiàn)死循環(huán)的充分條件[10].針對(duì)確定型線性賦值循環(huán)程序,Leike等人在文獻(xiàn)[11]中給出了GNTA條件去探測這類循環(huán)的不可終止性.

秩函數(shù)法是證明循環(huán)程序可終止性的主要方法.給定一個(gè)循環(huán)程序,倘若它的秩函數(shù)被找到,則表明該循環(huán)是終止的.為計(jì)算秩函數(shù)方便起見,人們往往計(jì)算多項(xiàng)式型的秩函數(shù).根據(jù)多項(xiàng)式秩函數(shù)的次數(shù)可以將多項(xiàng)式秩函數(shù)分為線性秩函數(shù)和非線性多項(xiàng)式秩函數(shù).

在線性秩函數(shù)研究方面,已有大量工作.譬如,2001年,Colón和Sipma通過凸多面體理論以及Farkas’ Lemma給出了一種計(jì)算線性秩函數(shù)的方法[12,13].2004年,Podelski和Rybalcheko提出了一種完備的方法來構(gòu)造線性約束的單分支循環(huán)程序的線性秩函數(shù)[14].2012年,Bagnara等人[15]研究了線性程序的線性秩函數(shù)的計(jì)算復(fù)雜度問題.在2013年,他們提出了最終的線性秩函數(shù)(eventual ranking function)這一概念[16],并通過合成最終的線性秩函數(shù)來證明單分支線性約束循環(huán)程序的終止性.該方法首先利用一個(gè)單調(diào)增函數(shù)對(duì)循環(huán)程序的狀態(tài)空間進(jìn)行劃分,然后利用Farkas’ Lemma來合成最終的秩函數(shù).文獻(xiàn)[17]將最終的線性秩函數(shù)進(jìn)行了推廣,提出了深度為L的最終線性秩函數(shù).2014年,Leike等人針對(duì)線性循環(huán)程序,給出了包括多階段秩函數(shù)在內(nèi)的多個(gè)秩函數(shù)定義[18].2017年,Ben-Amram等人[19]對(duì)多階段秩函數(shù)進(jìn)行了進(jìn)一步的研究,給出了一個(gè)能夠在多項(xiàng)式時(shí)間內(nèi)合成多階段秩函數(shù)的方法.同時(shí),他們還指出了多階段秩函數(shù)和線性字典序秩函數(shù)(lexicographic linear ranking function)、嵌套秩函數(shù)(nested ranking function)之間的相互聯(lián)系.相較于線性秩函數(shù)的研究,非線性多項(xiàng)式秩函數(shù)合成方面的工作較少,主要有以下幾篇文獻(xiàn)討論了非線性多項(xiàng)式秩函數(shù)的計(jì)算.Chen等人[20]利用柱形代數(shù)分解(CAD)算法給出了一種合成非線性多項(xiàng)式秩函數(shù)的方法.該方法首先設(shè)定循環(huán)程序的非線性秩函數(shù)模板,然后將秩函數(shù)合成問題轉(zhuǎn)化為半代數(shù)系統(tǒng)求解問題,從而可利用符號(hào)計(jì)算工具DISCOVERER和QEPCAD來求解半代數(shù)系統(tǒng),最終得出非線性秩函數(shù)模板中參數(shù)的解.此外,文獻(xiàn)[21,22]等人通過利用半正定規(guī)劃 SDP工具來計(jì)算非線性多項(xiàng)式秩函數(shù).

但程序的秩函數(shù)未必是多項(xiàng)式的.也即,可以構(gòu)造一個(gè)循環(huán)程序,它并沒有多項(xiàng)式秩函數(shù)但具有其他形式的秩函數(shù)[23].因此,當(dāng)給定程序沒有多項(xiàng)式秩函數(shù)時(shí),我們還不能說它是不可終止的,因?yàn)樗锌赡苡衅渌问降闹群瘮?shù).在本文中,我們主要研究下面給出的單重?zé)o條件分支的循環(huán)程序:

這里,p(x,z)=(p1(x,z),...,ps(x,z)),F(x,z)=(f1(x,z),...,fn(x,z)),且對(duì)任意的i∈[1,s],pi(x,z)∈Hn+1,di,對(duì)任意的j∈[1,n],fi(x,z)∈Hn+1,d.這里,對(duì)任意兩個(gè)整數(shù)a,b且a≤b,記[a,b]={a,a+ 1,…,b-1,b},由文獻(xiàn)[3,22]中的定理可知,程序與程序P在終止性上是等價(jià)的.

因此,不失一般性,本文主要分析下列齊次多項(xiàng)式循環(huán)程序終止性.

在下文中,我們將建立新的方法去探測程序Q的秩函數(shù).該方法的主要思路是:將秩函數(shù)計(jì)算問題歸結(jié)為二分類問題,然后利用機(jī)器學(xué)習(xí)中的支持向量機(jī)(SVM)算法[24,25]來合成所需秩函數(shù),最終驗(yàn)證合成的秩函數(shù)是否滿足秩函數(shù)定義.相較于當(dāng)前的基于 CAD或 SDP的多項(xiàng)式秩函數(shù)計(jì)算方法,本文的主要貢獻(xiàn)在于提出的基于SVM 的方法用于計(jì)算非多項(xiàng)式型秩函數(shù)——代數(shù)分式型秩函數(shù),從而將秩函數(shù)的研究從多項(xiàng)式型秩函數(shù)擴(kuò)展到代數(shù)分式型秩函數(shù),擴(kuò)大了可計(jì)算秩函數(shù)類型的范圍.

本文第1節(jié)介紹秩函數(shù)、支持向量機(jī)等相關(guān)概念.第2節(jié)建立基于SVM的秩函數(shù)探測算法,并通過實(shí)例詳細(xì)闡述該算法.第3節(jié)給出更多實(shí)驗(yàn).第4節(jié)總結(jié)全文.

1 預(yù)備知識(shí)

1.1 秩函數(shù)

定義1.記號(hào)同上.給定齊次多項(xiàng)式循環(huán)程序Q.令ρ(x)為一個(gè)n元函數(shù).ρ(x)被稱為程序Q的秩函數(shù),如果下列條件被滿足:

則ρ(x)為程序Q的秩函數(shù).

1.2 支持向量機(jī)

在樣本空間中,劃分超平面可用線性方程aTx+k=0來描述,其中,a=(a1,…,ad)是超平面的法向量,k是截距項(xiàng).支持向量機(jī)可用于找到最“居中”的那一個(gè)超平面.如圖1所示,支持向量機(jī)可以找到劃分超平面aTx+k=0,該超平面將圖中的兩類樣本點(diǎn)劃分開,其中,落在aTx+k=1和aTx+k=-1上的點(diǎn)叫作支持向量.支持向量機(jī)的求解通常使用SMO算法[24]來實(shí)現(xiàn).LIBSVM[25]是一個(gè)關(guān)于SVM的集成軟件包,由臺(tái)灣大學(xué)的Chih-Wei Hsu、Chih-Chung Chang以及Chih-Jen Lin編寫完成.軟件的主要部分采用C語言編寫完成,可在MATLAB上調(diào)用.本文的主要計(jì)算部分即采用該軟件包完成.

2 主要結(jié)果

本節(jié)闡述如何將型如程序Q的秩函數(shù)計(jì)算問題歸結(jié)為二分類問題,以便可以利用支持向量機(jī)(SVM)工具來計(jì)算得到一個(gè)候選秩函數(shù),最后再對(duì)該候選秩函數(shù)進(jìn)行驗(yàn)證,以檢驗(yàn)其是否滿足秩函數(shù)的兩個(gè)條件(a)和(c).

一般地,計(jì)算程序Q的秩函數(shù),需要首先預(yù)設(shè)一個(gè)秩函數(shù)模板.秩函數(shù)模板形式可以是多種多樣的.但為了方便計(jì)算,人們常將秩函數(shù)模板設(shè)定為多項(xiàng)式模板.但是,由于程序Q是齊次多項(xiàng)式程序,即其中的所有表達(dá)式都是齊次多項(xiàng)式的,因此下面的定理告訴我們,程序Q沒有多項(xiàng)式秩函數(shù).

定理2.記號(hào)同上.程序Q沒有多項(xiàng)式秩函數(shù).

這顯然與式(3)矛盾.故程序Q沒有多項(xiàng)式秩函數(shù).

2.1 程序Q的秩函數(shù)計(jì)算歸結(jié)為二分類問題

下面的命題表明,若T(x)在Ω上有定義,那么,函數(shù)T(x)為有界函數(shù).也即,存在正數(shù)δ,使得對(duì)任意的x∈Ω有|T(x)|≤δ.

命題3.記號(hào)同上.若T(x)在Ω上有定義,那么,T(x)在Ω上有界.

證明:既然T(x)在Ω上有定義,則對(duì)Ω中任意一點(diǎn)x,T(x)中各個(gè)分量的分母均不會(huì)為0.考慮T(x)中第v段,即

這里,

顯然有,

既然T(x),U(x)可被看作是?n→?k映射,若它們?cè)讦干嫌卸x,則記

根據(jù)命題 3,若T(x)在Ω上有定義,那么T(Ω)是?k空間中的有界域.倘若存在某a∈?k,使得連續(xù)函數(shù)L(u)=aT?u在U(Ω)上有下界 1,即

那么,根據(jù)U(Ω)的定義有,

根據(jù)上述向量a,構(gòu)造T(Ω)上的連續(xù)函數(shù)L′(t) =aT?t.既然T(Ω)有界,故L′(t)在T(Ω)上必有下確界,即存在c,使得?t∈T(Ω) ?L′(t)=aT?t≥c.根據(jù)T(Ω)的定義,上式等價(jià)于

令ρ(x)=aT?T(x)-c.不難看出,上述式(6)對(duì)應(yīng)于秩函數(shù)定義中的條件(c),式(7)對(duì)應(yīng)于條件(a).因此,根據(jù)式(6)和式(7)以及秩函數(shù)定義,易知ρ(x)=aT?T(x)-c恰好是程序Q的秩函數(shù),且是代數(shù)分式型的秩函數(shù).從上述分析可以看出,若使得式(5)或者式(6)成立的向量a被找到,那么式(7)自然成立,從而可以構(gòu)造得到程序Q的秩函數(shù)ρ(x)=aT?T(x)-c.因此,計(jì)算程序Q的秩函數(shù),我們可以通過計(jì)算可滿足式(5)或式(6)的向量a來得到.由此可得下列命題.

命題4.記號(hào)同上.若存在aT使得?u∈U(Ω)?L(u)=aT?u≥1,那么程序Q有代數(shù)分式秩函數(shù).要尋找使得式(5)成立的向量aT,我們可先對(duì)Ω的像集U(Ω)進(jìn)行分析.

限制條件(C1)成立等價(jià)于O?U(Ω ).

命題5.記號(hào)同上.假設(shè)U(x)在Ω上有定義.倘若?k空間中的原點(diǎn)O?U(Ω),那么,計(jì)算使得式(5)成立的向量aT的問題就等價(jià)于:在空間?k中尋找可將原點(diǎn)O∈?k與像集U( Ω )∈?k嚴(yán)格分離的超平面.

(i) ?u∈U(Ω)?π(u)=aT?u+k>0且π(O)<0;

(ii) ?u∈U(Ω)?π(u)=aT?u+k<0且π(O)>0.

命題5將程序Q的秩函數(shù)計(jì)算問題與兩個(gè)點(diǎn)集(單點(diǎn)集{O}與像集U(Ω)的隔離問題建立了等價(jià)關(guān)系.下面的情形(II)表明,即便原點(diǎn)O?U(Ω),能嚴(yán)格分離單點(diǎn)集{O}與像集U(Ω)的超平面也未必存在.

命題6.記號(hào)同上.U(Ω*)是?k中有界閉集.

既然U(Ω*)=U(Ω*∩Θ),故有U(Ω*)是有界閉的.

如果O?U(Ω*),根據(jù)命題6,既然U(Ω*)是有界閉集,那么在O與像集U(Ω*)之間存在間隙,因而有可能在二者之間存在嚴(yán)格分離超平面.既然U(Ω)?U(Ω*),當(dāng)O?U(Ω*)時(shí),如果存在超平面π(u)能夠嚴(yán)格分離原點(diǎn)O與像集U(Ω*),那么π(u)也能嚴(yán)格分離原點(diǎn)O與U(Ω).類似于命題5的證明,我們有下列結(jié)論.

定理7.記號(hào)同上.假設(shè)U(x)在Ω*上有定義且原點(diǎn)O?U(Ω*)??k.如果存在超平面π(u)可將原點(diǎn)O與像集U(Ω*)嚴(yán)格分離,那么一定存在向量aT使得式(5)成立.

S1:從B集中取出有限個(gè)點(diǎn)記為B0?B.轉(zhuǎn)S2;

S2:調(diào)用SVM算法計(jì)算單點(diǎn)集A與有限點(diǎn)集B0的分離超平面,記為π(u)=aT·u+k.轉(zhuǎn)S3;

2.2 有限點(diǎn)集B0的構(gòu)造

在上述的 S1中,需要從B=U(Ω*)中取出有限個(gè)點(diǎn)構(gòu)成B0.由命題 8的證明可知,U(Ω*)=U(Ω*∩Θ).這里,Ω*∩Θ是一個(gè)有界閉集,Θ為單位球.因此,要構(gòu)造B0,我們可以先從有界閉集Ω*∩Θ中取出有限點(diǎn)集C,然后通過U(x)映射得到點(diǎn)集U(C),從而得到B0=U(C).顯然,直接在球面Θ上通過打格點(diǎn)的方式取點(diǎn)并不方便.但單位球Θ總是可以被包含在某個(gè)超立方體Δ中.故,為了構(gòu)造Ω*∩Θ上的點(diǎn)集C,我們采取如下思路:先在區(qū)域Ω*∩Δ上構(gòu)造點(diǎn)集S.這里,Δ=[-m,m]n為一超立方體.然后對(duì)點(diǎn)集S中的點(diǎn)進(jìn)行歸一化,得到歸一化后的點(diǎn)集S0.顯然,S0?Ω*∩Θ.最后令C:=So.而在超立方體Δ上打格子是相對(duì)容易的.因此,在區(qū)域Ω*∩Δ上構(gòu)造點(diǎn)集S時(shí)我們可以通過對(duì)超立方體Δ打格子,然后將落入Ω*的格點(diǎn)收集起來構(gòu)成點(diǎn)集S.圖2所示為一個(gè)算法化的取點(diǎn)過程.

在上述算法中,需要設(shè)置m的值.在我們的實(shí)驗(yàn)中,m被取為100.此外,取點(diǎn)的間距h需要根據(jù)計(jì)算機(jī)的計(jì)算能力進(jìn)行適當(dāng)?shù)恼{(diào)整,在計(jì)算機(jī)的實(shí)際計(jì)算能力范圍內(nèi),間距越小,取得的樣本點(diǎn)越多,最終計(jì)算出的代數(shù)分式函數(shù)經(jīng)過驗(yàn)證成為真正秩函數(shù)的可信度就越高.

2.3 例 子

本節(jié)將通過一個(gè)例子來闡述上文提出的方法.

例1:考慮下列循環(huán):

該循環(huán)若使用 RegularChains[26]或者redlog[27]來求解線性或者非線性秩函數(shù),均會(huì)因復(fù)雜度太高,而無法在有效的時(shí)間內(nèi)得出結(jié)論.接下來將演示如何通過上文提出的基于SVM的方法來探測循環(huán)程序P1的代數(shù)分式秩函數(shù).

(a) 首先將循環(huán)程序Q1進(jìn)行齊次化處理,變成終止性等價(jià)的循環(huán)程序Q1′,如下所示:

若式(8)無解,則表明O?U(Ω*).由于代數(shù)分式以及根式的出現(xiàn)使得我們直接計(jì)算上述系統(tǒng)是否有解較為困難,因此,我們采取了一些化簡措施.比如,將上述系統(tǒng)中的代數(shù)分式化為多項(xiàng)式,利用平方手段消除根號(hào)等.由此我們得到下列多項(xiàng)式系統(tǒng):

顯然,式(8)的任何一個(gè)解也必是式(9)的解.調(diào)用 Maple中的命令 solve計(jì)算可得式(9)僅有零解(0,0,0).顯然,(0,0,0)?Ω*.因?yàn)榱憬獠豢赡苁鞘?8)的解,故式(8)無解.這表明原點(diǎn)O?U(Ω*).

綜上所述,該循環(huán)程序滿足定理7的前提條件.因此,根據(jù)定理7,秩函數(shù)計(jì)算問題可歸結(jié)為O與U(Ω*)之間嚴(yán)格分離超平面的計(jì)算問題.

(b) 取樣本點(diǎn).

采用第 2.2節(jié)介紹的取點(diǎn)算法,并將該算法中的參數(shù)m=100.在本例中我們令取點(diǎn)間距h=1.由于在約束條件中有x3≥0的條件,故x3不必從-100開始取點(diǎn).通過取點(diǎn)算法,我們得到U(Ω*)中的有限點(diǎn)集B0=U(C).將B0中的點(diǎn)的標(biāo)簽置為 1,而令單點(diǎn)集A=(O)的標(biāo)簽為-1.接下來調(diào)用 SVM 算法計(jì)算A與B0的嚴(yán)格分離超平面π0(u)=aT·u+k.

(c) 使用LIBSVM軟件包計(jì)算出像空間中的劃分超平面.

本文采用MATLAB調(diào)用LIBSVM軟件包的方式來計(jì)算一個(gè)“硬分隔”的超平面.令=A∪B0.在求得劃分超平面之后,需要對(duì)中的點(diǎn)進(jìn)行一次完整的測試,測試結(jié)果必須是 100%完全精確才能進(jìn)行下一步操作.對(duì)該例通過計(jì)算得到劃分超平面中aT和k的值,

a=(2.798739925884132,-6.058645127373750,6.167554957795089),k=-1.000000000061875.

由上述計(jì)算得到的aT和k的值可確定一個(gè)嚴(yán)格分離超平面π0(u)=aT·u+k,它將A={O}與B0(?U(Ω*))嚴(yán)格分離.即:

(i) ?u∈B?π0(u)=aT?u+k>0且π0(O)<0;

(ii) ?u∈B?π0(u)=aT?u+k<0且π0(O)>0.

由類似于命題5的證明可知,無論哪種情形發(fā)生,都將有

接下來將驗(yàn)證超平面π0(u)是否能將A={O}與B=U(Ω*)嚴(yán)格分離.為此,就需要驗(yàn)證下列兩種情形之一是否成立.

(i) ?u∈U(Ω*)?π0(u)=aT?u+k>0且π0(O)<0;

(ii) ?u∈U(Ω*)?π0(u)=aT?u+k<0且π0(O)>0.

既然像點(diǎn)u∈U(Ω*)且由U(Ω*)的定義可知U(Ω*)={u∈?k:u=U(x),x∈Ω*},那么驗(yàn)證上述(i),(ii)兩式就等價(jià)于驗(yàn)證:

(i*) ?x∈Ω*?β(x)=aT[T(x)-T(M(x))]+k>0且k<0;

(ii*) ?x∈Ω*?β(x)=aT[T(x)-T(M(x))]+k<0且k>0.

這是因?yàn)?顯然地,若(i)(或(ii))成立,那么(i*)(或(ii*))也必成立.反之亦然.

(e) 使用BOTTEMA軟件包進(jìn)行驗(yàn)證.

既然k=-1.000000000061875<0,那么我們需要驗(yàn)證:

是否成立.由于最終需要驗(yàn)證式(5)或式(6)是否成立,所以,在本例中,我們直接驗(yàn)證:

是否成立.BOTTEMA是一款強(qiáng)有力的不等式證明軟件.它可以驗(yàn)證帶復(fù)雜根式的代數(shù)表達(dá)式的不等式是否成立.我們可以在Maple上調(diào)用BOTTEMA中的各類函數(shù).通過驗(yàn)證發(fā)現(xiàn),

的確成立.故,

是該程序的代數(shù)分式型秩函數(shù).因此循環(huán)程序是可終止的.

3 實(shí) 驗(yàn)

下面給出基于SVM的多項(xiàng)式循環(huán)程序秩函數(shù)探測的具體算法.

實(shí)驗(yàn)是在一臺(tái)裝有7.86GB的可用內(nèi)存、處理器頻率為2.59GHz、操作系統(tǒng)64位的Windows操作系統(tǒng)的計(jì)算機(jī)上進(jìn)行的.下面我們選取了4個(gè)循環(huán)程序用于對(duì)比.每個(gè)循環(huán)程序具體的計(jì)算方法可以參照前文中的例1.

針對(duì)表1中的6個(gè)循環(huán)程序,我們先后用量詞消去工具Redlog和Maple中的RegularChains軟件包來計(jì)算各自的線性秩函數(shù),從表2可以看出,除了循環(huán)程序P4和P5外,其他5個(gè)循環(huán)程序都不能通過量詞消去方法來證明其是終止的.原因在于,量詞消去算法的復(fù)雜度太高,當(dāng)循環(huán)程序的賦值語句或循環(huán)條件中含有非線性項(xiàng)時(shí),無法在有效的時(shí)間內(nèi)給出計(jì)算結(jié)果.在表2中,unknown表示計(jì)算時(shí)間超過10個(gè)小時(shí)仍未得出結(jié)果.Terminating表示相應(yīng)的線性秩函數(shù)或代數(shù)分式秩函數(shù)被成功找到,故表明循環(huán)是終止的.特別地,在Terminating后面的括號(hào)中給出了計(jì)算秩函數(shù)所花費(fèi)的時(shí)間.顯然,當(dāng)循環(huán)中的表達(dá)式是線性時(shí),基于量詞消去的工具即能有效地計(jì)算它們的線性秩函數(shù).但,當(dāng)表達(dá)式中含有非線性項(xiàng)時(shí),實(shí)驗(yàn)結(jié)果表明,量詞消去工具較難在可接受的時(shí)間內(nèi)計(jì)算線性秩函數(shù).此外,本文提出的基于SVM的方法所涉及的時(shí)間開銷包括:樣本點(diǎn)集的構(gòu)造所需時(shí)間、SVM計(jì)算時(shí)間以及用 BOTTEMA驗(yàn)證代數(shù)分式是否為秩函數(shù)所需時(shí)間.在實(shí)驗(yàn)中我們發(fā)現(xiàn),本文方法最主要的時(shí)間開銷在于樣本點(diǎn)集的構(gòu)造.譬如,循環(huán)P3,樣本點(diǎn)集的構(gòu)造花費(fèi)了76分鐘.當(dāng)然,我們也可以嘗試使用量詞消去的方法來合成非線性秩函數(shù),但是,非線性項(xiàng)的引入同樣會(huì)帶來高復(fù)雜度的問題.從表 2中可以看出,本文提出的基于SVM的秩函數(shù)探測方法能夠探測出上述6個(gè)循環(huán)程序的確具有代數(shù)分式型秩函數(shù),從而證明了這6個(gè)程序均是可終止的.上述6個(gè)循環(huán)程序在使用SVM的方法時(shí),各自的取點(diǎn)間距h以及所產(chǎn)生的劃分超平面aT·u+k中的參數(shù)aT和參數(shù)k的計(jì)算值見表3.

Table 1 More examples表1 更多實(shí)例

從表3可以看出,循環(huán)程序P3和P4所采用的取點(diǎn)間距為0.5,而循環(huán)程序P2采用的取點(diǎn)間距為0.2.從理論上來說,取點(diǎn)間距越小,所選取的樣本點(diǎn)越多,最終計(jì)算出的代數(shù)分式函數(shù)被成功驗(yàn)證為秩函數(shù)的可能性就越大.但是考慮到計(jì)算機(jī)的實(shí)際計(jì)算能力,針對(duì)不同的循環(huán)程序,取點(diǎn)間距要作適當(dāng)?shù)恼{(diào)整.

Table 3 The parameters generated using the SVM method表3 使用SVM的方法所產(chǎn)生的參數(shù)

4 總 結(jié)

本文提出了一種基于支持向量機(jī)(SVM)理論的求解單重?zé)o條件分支多項(xiàng)式循環(huán)程序秩函數(shù)的方法.該方法將秩函數(shù)計(jì)算問題歸結(jié)為二分類問題,然后利用SVM工具計(jì)算出一個(gè)候選的代數(shù)分式型函數(shù),最后借助不等式自動(dòng)驗(yàn)證工具BOTTEMA對(duì)其進(jìn)行驗(yàn)證,以確定該代數(shù)分式型函數(shù)是否為循環(huán)程序的秩函數(shù).由于SVM方法內(nèi)部采用數(shù)值計(jì)算,因此相較于現(xiàn)有的基于量詞消去的秩函數(shù)計(jì)算方法,本文方法能在可接受時(shí)間內(nèi)探測形式較為復(fù)雜的秩函數(shù).實(shí)驗(yàn)結(jié)果表明,針對(duì)某些循環(huán)程序,傳統(tǒng)的量詞消去方法不能在合理時(shí)間內(nèi)判斷出它們是否有線性秩函數(shù),但通過本文提出的方法卻可以找到其代數(shù)分式型秩函數(shù).

猜你喜歡
分式代數(shù)線性
二階整線性遞歸數(shù)列的性質(zhì)及應(yīng)用
3-李-Rinehart代數(shù)的導(dǎo)子與交叉模
線性回歸方程的求解與應(yīng)用
半結(jié)合3-代數(shù)的雙模結(jié)構(gòu)
3-李-Rinehart代數(shù)的結(jié)構(gòu)
例談一類分式不等式問題的解法
非齊次線性微分方程的常數(shù)變易法
線性回歸方程知識(shí)點(diǎn)剖析
一個(gè)新發(fā)現(xiàn)的優(yōu)美代數(shù)不等式及其若干推論
學(xué)習(xí)分式的五個(gè)禁忌
保定市| 萝北县| 海阳市| 新干县| 大石桥市| 嘉义县| 镇康县| 东明县| 武邑县| 金昌市| 建昌县| 惠水县| 浠水县| 拜城县| 宁津县| 于田县| 阳新县| 重庆市| 会宁县| 长治县| 永嘉县| 多伦县| 莫力| 娱乐| 沧源| 陵川县| 嘉义市| 荃湾区| 资源县| 泰州市| 库尔勒市| 丹寨县| 调兵山市| 禄丰县| 桓台县| 儋州市| 南投市| 宜兰县| 海兴县| 丰台区| 广南县|