徐 嘉

(西南民族大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，四川 成都 610041)

逐次差分代換算法起源于非常樸素的數(shù)學(xué)思想，即“非負(fù)實(shí)數(shù)相加或相乘仍然是非負(fù)的”.最初的差分代換方法是用于證明對(duì)稱(chēng)不等式的.眾所周知，這個(gè)方法有點(diǎn)類(lèi)似于數(shù)學(xué)分析中著名的阿貝爾(Abel)代換(用法有所不同)，國(guó)外也有人稱(chēng)之為buffalo way(水牛方法或暴力方法，簡(jiǎn)稱(chēng)BW).一些相當(dāng)困難的對(duì)稱(chēng)不等式可以輕易的被這個(gè)方法解決.而這些不等式(次數(shù)高變?cè)?是其它方法(或算法)很難處理的.有明確的資料顯示，這一方法曾經(jīng)被多人在正式的期刊中使用，如文獻(xiàn)[1].但是這些僅僅只是使用方法，而不是對(duì)方法本身的研究和探討.它的較為深刻的發(fā)展則是非常近的事.從差分代換到逐次差分代換是這一方法發(fā)展中的關(guān)鍵一步.這一步是在文獻(xiàn)[2]中完成的.Yang不但引入了一般的差分代換的概念和基本代換矩陣，還編寫(xiě)了Maple程序SDS，用于自動(dòng)探索性證明代數(shù)不等式.正是這個(gè)短程序SDS的有效性，激起了后續(xù)的進(jìn)一步研究.逐次差分代換的一個(gè)明顯的缺點(diǎn)是對(duì)不成立的不等式?jīng)]有任何作用.針對(duì)這一點(diǎn)，楊路和姚勇在文獻(xiàn)[3]中改進(jìn)了逐次差分代換算法，使用了非常簡(jiǎn)單的思想，即在做每一次代換的同時(shí)再驗(yàn)證一個(gè)點(diǎn)處的值(通常取點(diǎn) (1，…，1) 或者點(diǎn) (1，0，…，0)).改進(jìn)后的算法被稱(chēng)為T(mén)SDS，它被證明對(duì)不成立的不等式是完備判定的[3]，并且還能夠自動(dòng)輸出反例.這個(gè)改進(jìn)對(duì)探索不等式是非常有用的.因?yàn)樵诒蛔C明之前，我們并不知道所研究的不等式是否成立.TSDS驗(yàn)證了一系列不等式猜想是不正確的，其中包括Vasc猜想[4-5]和楊學(xué)枝猜想[6].

關(guān)于逐次差分代換算法的一個(gè)重要問(wèn)題是終止性問(wèn)題，也就是對(duì)什么樣的多項(xiàng)式TSDS算法會(huì)終止，輸出結(jié)論.這個(gè)問(wèn)題至今仍懸而未決.在雙變?cè)那闆r，文獻(xiàn)[7]中已經(jīng)解決.證明了雙變?cè)凝R次多項(xiàng)式如果無(wú)平方因子，則算法TSDS總是終止的.同樣重要的是對(duì)正定形式，逐次差分代換算法是否終止.很不幸，答案是負(fù)面的.在文獻(xiàn)[7]中，舉出了實(shí)例，說(shuō)明對(duì)正定形式，逐次差分代換算法仍可能不終止.姚勇因此考慮改變基本代換矩陣，引入了帶權(quán)重的基本代換矩陣[7].建立了新的差分代換算法NEWTSDS，新算法被證明對(duì)正定形式是終止的.姚勇和本文作者合作在文獻(xiàn)[8]中證明了新算法的適用范圍整體上優(yōu)于著名的Polya方法的適用范圍.

逐次差分代換算法被應(yīng)用于證明帶邏輯連詞“∧”(and)的不等式命題是不難的，在證明一類(lèi)根式不等式時(shí)會(huì)遇到，它已經(jīng)在文獻(xiàn)[9]中被大量使用.但是在實(shí)代數(shù)幾何中，常常也會(huì)遇到帶有邏輯連詞“∨”(or)的命題.下面就是一個(gè)簡(jiǎn)單的例子.

考慮二次多項(xiàng)式

假設(shè) a ＞ 0，c≥0，問(wèn)a，b，c滿足什么條件時(shí)，對(duì)任意x∈?+(x≥0)，下式都成立:

容易看到答案是:

這就是一個(gè)典型的帶邏輯連詞“∨”的不等式命題.如果a，b，c是常數(shù)，驗(yàn)證這樣的命題自然不會(huì)有什么困難，可是如果a，b，c帶有變量，那么這個(gè)問(wèn)題就不那么簡(jiǎn)單了.例如證明下面的二次型在上是非負(fù)的(這種二次型被稱(chēng)為copositive二次型[10]).

容易證明條件a＞0，c≥0是滿足的，按照上面的結(jié)論就還需要證明:

對(duì)任意點(diǎn) (x2，x3，x4，x5) ∈ ?4+有

或者判別式 -x2x4+x3x4-x3x5≤0.

可是-x2+x3+x4-x5和-x2x4+x3x4-x3x5在?4+上都是不定的.時(shí)而取正值，時(shí)而取負(fù)值.原來(lái)的逐次差分代換算法是不適用于證明這樣的命題的.

本文的目標(biāo)就是改進(jìn)原來(lái)的逐次差分代換算法，使得改進(jìn)后的算法可以用于證明含邏輯連詞“∧”和“∨”的不等式命題.本文剩余部分內(nèi)容的安排如下:第1節(jié)簡(jiǎn)單地描述了逐次差分代換算法的基本內(nèi)容；第2節(jié)是新的對(duì)偶算法的建立過(guò)程；第3節(jié)是對(duì)偶算法終止性的理論結(jié)果；最后一節(jié)是算法的初步應(yīng)用.

1 逐次差分代換算法的基本知識(shí)

在這一節(jié)，我們將對(duì)需要用到的基本知識(shí)作些簡(jiǎn)單介紹.本小節(jié)的主要內(nèi)容來(lái)自文獻(xiàn)[3，7，8]，也可見(jiàn)專(zhuān)著[11-13].

考慮如下n×n三角方陣

矩陣G被稱(chēng)為重心矩陣，如果G可以由Gn經(jīng)過(guò)行置換得到.

設(shè)Sn是集合 {1，2，…，n }上的置換對(duì)稱(chēng)群.Pσ是置換σ對(duì)應(yīng)的置換矩陣.重心矩陣也可以表示為:

多項(xiàng)式f的差分代換集被定義為DS(f):

一般地，多項(xiàng)式f的k階差分代換集被定義為DS(k)(f).

下面給出基于重心矩陣的逐次差分代換算法(GSDS).

算法1GSDS].輸出:“正半定形式”或“非正半定形式”1)k←0；DS(k)←{f}；Temp←{}.2)刪除DS(k)中系數(shù)非負(fù)的多項(xiàng)式后存入Temp.3)如果Temp是空集則輸出“正半定形式”.4)如果 ?g∈Temp，使得g(1，…，1) ＜ 0，則輸出“非正半定形式”.5)否則:DS(k+1)← ∪輸入:整系數(shù)齊次多項(xiàng)式f∈? x1，…，xn[g(GσxT)6)k←k+1.7)程序結(jié)束.g∈Temp ∪σ∈Sn

這里的逐次差分代換算法GSDS是基于重心矩陣的.最初的差分代換是基于矩陣

只需將算法1中的矩陣Gn換為矩陣An就可得到原來(lái)的逐次差分代換算法.

算法1的正確性證明可以參看文獻(xiàn)[7-8].由楊路和姚勇編寫(xiě)的程序TSDS5是算法1的Maple平臺(tái)實(shí)現(xiàn)，可到相關(guān)網(wǎng)站下載該程序.

這一節(jié)只舉一個(gè)應(yīng)用的例子.

例1.1(arqady)已知a，b，c＞0且滿足a+b+c＝1.證明:

這是一個(gè)有名的形式簡(jiǎn)單，證明困難的不等式.通過(guò)去分母，齊次化，上式轉(zhuǎn)變?yōu)樽C明:運(yùn)行程序 TSDS5中的命令“TSDS”或“NEWTSDS”，都在5步代換之后終止，運(yùn)行時(shí)間分別為0.063s，0.047s.輸出結(jié)果為:

‘The form is positive semi-definite’也就是不等式成立.

2 對(duì)偶算法

?n表示n維實(shí)向量空間.其中的點(diǎn)用列向量表示.標(biāo)準(zhǔn)單純形Δn由下式定義

本節(jié)中關(guān)心的是Δn上的單純形.設(shè)B1，…，Bn是Δn上n個(gè)仿射無(wú)關(guān)的點(diǎn)，它們張成(n-1)維單純形 [B1，…，Bn]Δ，即

記號(hào)“[]Δ”帶下標(biāo)是為了與矩陣記號(hào)“[]”相區(qū)別.而 [B1，…，Bn]是表示以B1，…，Bn作為列的矩陣 .記x＝(x1，…，xn)T，則單純形可以表示為更簡(jiǎn)潔的形式

這就是單純形的頂點(diǎn)表示法.

可以通過(guò)重心矩陣來(lái)表達(dá)標(biāo)準(zhǔn)單形的重心剖分，也就是

這里記號(hào) [ Gσ]Δ表示矩陣Gσ的列所張成的單純形，下同.

下面的引理來(lái)自文獻(xiàn)[7-8].

引理2.1 多項(xiàng)式f∈?[x1，…，xn]，則有如下等價(jià)關(guān)系成立

這個(gè)引理是逐次差分代換算法的基礎(chǔ).重心矩陣的集合

一般地，定義GS(k)

仿照算法1有算法2.

?

?

接下來(lái)比較算法1和算法2的不同點(diǎn).

算法1中的局部變量Temp存儲(chǔ)的是多項(xiàng)式，而算法2中的局部變量Temp存儲(chǔ)的是單純形 (或代換).換句話說(shuō)，在算法1中，代換始終保持不變，多項(xiàng)式在不停的變化.在算法2中，給定的多項(xiàng)式始終不變，代換卻在不停的變化.可以明顯的看到，算法1能完成的任務(wù)，算法2仍然可以.

下面考慮一組帶有邏輯連詞“∧”(and)和“∨”(or)的多項(xiàng)式集合.

對(duì)形如

的公式，明顯算法1和算法2都是適用的.下面主要考慮形如

的公式.為了使算法2能夠適用于判斷公式Φ是否成立，還需對(duì)算法2做一點(diǎn)小的修改.

?

?

說(shuō)明:

①算法3中的矩陣Gσ也可換為An以獲得同最初的逐次差分代換類(lèi)似的改進(jìn)算法.它也是有應(yīng)用價(jià)值的，見(jiàn)例4.1.

②算法3的基本思想仍然是明顯的.根據(jù)重心剖分的基本性質(zhì)，每循環(huán)一次，單純形的直徑將減小1/3.因此算法3記錄的單純形，隨著循環(huán)次數(shù)的增加，將變得非常小，漸漸趨近于一些點(diǎn).粗略的看這就相當(dāng)于將點(diǎn)代入多項(xiàng)式，來(lái)觀察多項(xiàng)式系數(shù)的變化規(guī)律.

③算法3的正確性是明顯的.它的終止性同算法1一樣可能不終止.它的適用范圍明顯比算法1大了很多.下一節(jié)將證明算法3關(guān)于終止性的理論結(jié)果.

3 主要理論結(jié)果

在這一節(jié)將要證明兩個(gè)關(guān)于算法3的終止性的定理.

定理3.1 f1，…，fs∈ ? [x1，…，xn] 是齊次多項(xiàng)式，給定公式:

如果存在點(diǎn)P∈Δn，使得公式Φ不成立，則算法3是終止的，并且輸出“false”.

證明:假設(shè)點(diǎn)P∈Δn使得公式Φ不成立，也就是P滿足

由多項(xiàng)式函數(shù)的連續(xù)性，我們知道存在點(diǎn)P的一個(gè)鄰域O(P，ε)，這個(gè)鄰域中的點(diǎn)都滿足

根據(jù)重心剖分的基本性質(zhì)，算法3每循環(huán)一次，單純形的直徑將減小1/3.隨著循環(huán)次數(shù)的增加，單純形將變得非常小，漸漸趨近于一些點(diǎn).因此對(duì)充分大的k，存在單純形

此時(shí)有:

也就是算法3最多經(jīng)k次循環(huán)將輸出 “false”.

定理3.2f1，…，fs∈? [x1，…，xn] 是齊次多項(xiàng)式，給定公式

如果對(duì)任意點(diǎn)P∈Δn，都有

則算法3是終止的，并且輸出“true”.

證明:這里的證明依賴于Δn的緊致性和文獻(xiàn)[8]中的主引理.

不失一般性，可以假設(shè)給定點(diǎn)P對(duì)某個(gè)固定的i成立

(注意，這里對(duì)不同的P，多項(xiàng)式fi可能是不同的)由多項(xiàng)式函數(shù)的連續(xù)性，我們知道存在P的一個(gè)鄰域O(P，ε)，這個(gè)鄰域中的點(diǎn)都滿足

也就是說(shuō)，在鄰域O(P，ε)內(nèi)下面公式是真命題

由于點(diǎn)P的任意性，對(duì)Δn的每一點(diǎn)選擇一個(gè)鄰域，可以得到Δn的一個(gè)開(kāi)覆蓋，根據(jù)有限覆蓋定理，可以選出有限個(gè)鄰域蓋住Δn.因此當(dāng)對(duì)Δn進(jìn)行充分多階的重心剖分后，每一個(gè)細(xì)小單形將被某個(gè)鄰域蓋住，不妨設(shè)單形:

如果fi(G1…Gkx)的系數(shù)都是非負(fù)的，則結(jié)論已經(jīng)成立.如果fi(G1…Gkx)的系數(shù)中還含有負(fù)數(shù)，按假設(shè)fi在小單形為[G1…Gk]Δ上的值是嚴(yán)格正的，則根據(jù)文獻(xiàn)[7]中的主引理，單形為[G1…Gk]Δ可以進(jìn)一步細(xì)分，使得[G1…Gk]Δ的有限次重心剖分的每一個(gè)小單形[Λ]Δ?[G1…Gk]Δ都有fi(Λx)的系數(shù)是非負(fù)的.也就是，算法3最終將輸出“true”.

下面的定理是定理3.1和定理3.2的明顯推論.

推論3.3f1，…，fs∈? [x1，…，xn] 是齊次多項(xiàng)式，給定公式

如果算法3不終止，則所給定的公式Φ是真命題.

推論3.3表明對(duì):

這類(lèi)命題算法3是半可判定的.

4 應(yīng)用

現(xiàn)在來(lái)應(yīng)用算法3.

例4.1證明?(a，b，c，d) ∈ Δ4如下公式成立

證明:考慮矩陣

對(duì)稱(chēng)群S4有24個(gè)元素.所以，初始的GS(0)中有24個(gè)矩陣.

記f1＝b+c-a-d，f2＝ac+bd-bc.首先計(jì)算

f2所有的系數(shù)全是正的.所以，將A4從GS(0)中刪除.同樣計(jì)算全部24個(gè)矩陣發(fā)現(xiàn):

f1(PσA4(a，b，c，d)T) ， f2(PσA4(a，b，c，d)T) ，中至少有一個(gè)是系數(shù)全是正的，所以Temp是空集.程序輸出“true”后停止.

例4.1比較簡(jiǎn)單，程序運(yùn)行了一次循環(huán)就停止了，證明了公式是成立的.下面將考慮困難得多的問(wèn)題:

在文獻(xiàn)[5]中提出了如下公開(kāi)問(wèn)題:

例 4.2a，b，c是正實(shí)數(shù). 證明

為了解決這個(gè)問(wèn)題，需要如下引理，它來(lái)自文獻(xiàn)[14].

引理4.3u，v，w，t是正實(shí)數(shù)，則下面等價(jià)關(guān)系成立

其中

例4.2的證明:令

代入R1，R2，R3.通過(guò)去分母，轉(zhuǎn)化為三個(gè)齊次多項(xiàng)式，分別有次數(shù) 9，18，36. 其中具有424項(xiàng)，最大系數(shù)為235583387168.

通過(guò)引理4.3，還需要證明如下公式成立

在Maple平臺(tái)編程，算法3在運(yùn)行了7次循環(huán)之后終止，輸出了結(jié)果“true”.用時(shí)74s.

討論:例4.2的方法可以被應(yīng)用于更加廣泛的型如

不等式的機(jī)器證明.

現(xiàn)在考慮帶有量詞"?"的命題.注意到公式

等價(jià)于

因此算法3可以被應(yīng)用到尋找滿足一組不等式的特解問(wèn)題.恰好配平方和就可以歸結(jié)到這樣的問(wèn)題.下面僅舉一個(gè)簡(jiǎn)單的例子.

例4.3請(qǐng)給出多項(xiàng)式

的平方和表示.

根據(jù)Gram矩陣方法，問(wèn)題可以歸結(jié)到尋找實(shí)數(shù)a使得如下的矩陣C(f)是半正定的矩陣.

計(jì)算它的特征多項(xiàng)式

矩陣C(f)是半正定的等價(jià)于T(z)的根都是非負(fù)實(shí)數(shù).也就是a需要滿足不等式組

把條件放寬一點(diǎn)，a，b＞0滿足如下嚴(yán)格不等式是足夠的.

這樣就轉(zhuǎn)化為了

a分兩部分a≥0，a＜0.分別求解上面的公式.使用算法3，僅僅循環(huán)了一次就獲得了一個(gè)解

回到不等式(4.1)，a＝-1是一個(gè)解.因此得到一個(gè)半正定矩陣

分解為C(f)＝BBT，

最后獲得平方和表示為

[1]AN ZHENGPING.Some Techniques for Proving Inequalities[J].High-School Mathematics，1995，5:7-10.

[2]YANG LU.Solving Harder Problems with Lesser Mathematics.Proceedings of the 10thAsian Technology Conference in Mathematics[C].ATCM Inc，2005:37-46.

[3]YANG LU，YAO YONG.Difference Substitution Matrices and Decision on Nonnegativity of Polynomials[J].Journal of Systems Science and Mathematical Science，2009，29(9):1169-1177.(in Chinese).

[4]VASILECIRTOAJE.Algebra Inequalities:old and new methods[M].Zalau:GIL Publishing House，2006，46.

[5]VASILECIRTOAJE，VO QUOC BA CAN，TRAN QUOC ANH.Inequalities with Beautiful Solutions[M].Zalau:GIL Publishing House，2006.

[6]YANG XUE ZHI.Research on Mathematical Olympiad inequalities[M].Harbin，Harbin Institute of Technology Press，2009.(in Chinese).

[7]YAO YONG.Infinite product convergence of column stochastic mean matrix and machine decision for positive semi-definite forms[J]，Science China Mathematics ，2010，40(3):251-264.

[8]XU JIA，YAO YONG.Polya’s Method and the Successive difference substitution Method[J].Scientia Sinica Mathematica，2012，42(3):203-213.(in Chinese).

[9]XU JIA，YAO YONG.Rationalizing Algorithm and Automated Proving for a Class of Inequalities Involving Radicals[J].Chinese Journal of Computers，2008，31(1):24-31.(in Chinese).

[10]徐嘉，李高平.copositive二次型與copositive矩陣[J].西南民族大學(xué)學(xué)報(bào)(自然科學(xué)版)，2011，37(4):504-508.

[11]YANG LU，XIA BI CAN.Automated Proving and Discovering on Inequalities[M].Beijing:Science Press，2008.(in Chinese).

[12]XIA BI CAN，YANG LU.Automated Inequality Proving and Discovering[M].Singapore:World Scientific Publishing Co.Pte.Ltd.，2016.

[13]WANG WAN LAN.Approaches to Prove Inequalities.Harbin，Harbin Institute of Technology Press，2011.(in Chinese).

[14]徐嘉.三類(lèi)根式不等式的有理化與機(jī)器證明[J].西南民族大學(xué)學(xué)報(bào)(自然科學(xué)版)，2016，42(2):200-206.