帶約束條件多項式的差分代換及其應用

劉保乾

（西藏自治區組織編制信息中心，西藏拉薩850000）

帶約束條件多項式的差分代換及其應用

劉保乾

（西藏自治區組織編制信息中心，西藏拉薩850000）

對三角形幾何不等式判定算法agl進行了改進和補充，并根據這種算法設計了agl程序的升級版agl2009，討論了帶約束條件差分代換在證明根式型不等式中的應用；給出了用agl程序發現的若干優美的三角形幾何不等式.

差分代換；三角形幾何不等式；agl算法；機器證明

0 引言

筆者在文獻中介紹了2004年12月提出的用增量代換證明銳角三角形不等式的思想[1]，從而產生了帶約束條件多項式的差分代換問題.此后又對這種思想做了進一步闡述[2]和改進[3-4]，得到了一種判定三角形幾何不等式的算法agl.編寫的同名程序對判定三角形幾何不等式，尤其是含有角平分線或半角三角函數的不等式十分有效，且在一些方面性能優于Bottema軟件[5].本文擬對agl的算法進行改進和補充，并討論了帶約束條件差分代換在證明根式型不等式中的應用.

以下約定：△ABC三邊為a、b、c，面積為Δ，角平分線、中線、高、傍切圓半徑分別為wa、wb、wc，ma、mb、mc，ha、hb、hc和ra、rb、rc，內切圓和外接圓半徑分別為r和R，用∑表示循環和.另外，本文不等式驗證環境均在Intel（R）Pentium（R）4 CPU 2.40 GHz，2.41 GHz，1.00 GB內存環境下完成.

1 agl算法的改進和補充

正如文獻［3］所述，agl不是一個完備的算法，對一些三角形幾何不等式可能失效.在解決這些失效不等式問題的過程中，筆者發現如果對帶約束條件的多項式和條件同步進行差分代換，可以部分地解決這個問題.為了保證多項式和條件的同步性，通常將多項式f和條件u≥0寫在一起構成一個列表t=[f，u]，稱這個列表為一個條件組.顯然條件組是由兩部分構成，第一部分是多項式部分，用tf標識；第二部分是約束條件部分，用tu標識.為證明不等式f≥0成立，需要用條件u對f按照agl算法進行測試，稱這個過程為對條件組t進行正性測試.為了說明agl算法的改進思路，先介紹一下agl算法.

算法agl由文獻［3-4］可知，三角形幾何不等式的證明，最后可化為條件組w=的正性判定，由于agl算法要進行多項式的相除運算，故需要約定一個主變元，我們約定z是主變元.算法agl的思路就是用w的tu部分去除tf部分差分代換集中的各個多項式，如果得到的商和余式均平凡非負，則可證得不等式f（m，n，z）≥0成立，如果商和余式中仍含有負系數項，則可繼續去除，直至得到的多項式中沒有負系數項，或者z的次數小于2為止.顯然算法agl總是可以終止的.但是要注意，當temp2不為空時，輸出的多項式如果是半正定的，則f（m，n，z）≥0一定成立；輸出的多項式的正性若不可判定，則f（m，n，z）≥0可能成立也可能不成立，此時agl的算法失效.下面以條件組t=[f，u]為例，說明agl算法的改進思路.

1）對條件組t作差分代換.

2）條件組t的差分代換是一些新的條件組構成的集合S.為了便于敘述和用程序控制，按代換結果的特征和約束條件，可將S中的條件組分成如下幾類.

i.如果條件組中tu部分的諸項系數全部為負數，則意味著出現了矛盾的結果（條件u≥0不能滿足），稱此條件組為矛盾條件組.矛盾條件組應當放棄.出現這種情況的原因是，我們是按照差分代換全集的公式計算S的.以3元為例，多項式f（m，n，z）的差分代換（全集的）計算公式為[6]：在約束條件下，顯然z≤m，z≤n不會出現（否則會導出n≥m），這樣式（1）中的代換式f（m+z，m+n+z，z），f（m+n+z，m+z，z）就是多余的.

ii.如果條件組中tu部分的諸項系數全部為正數，而tf部分的諸項系數全部為負數，則意味著f≥0不成立，稱這樣的條件組為反例條件組.顯然這里定義的反例條件組是一種極端反例，沒有包括tf部分含有正系數項的反例，是最遲出現的反例，這也是本改進算法發現反例效率不高的主要原因之一.

iii.如果條件組中tf部分的諸項系數全部為正數，則稱這樣的條件組為平凡條件組.

iv.如果條件組中tf和tu兩部分的系數均有正有負，則稱這樣的條件組為待測組.集合中的絕大多數屬于待測組.

v.如果條件組中tu部分的系數全部為正，而tf部分的諸項系數有正有負，則意味著這個條件組中tf部分正半定的條件可以擴大為任意正數，從而把條件不等式化為關于正數的不等式，稱這樣的條件組為正數組.很顯然，正數組的條件可以去掉成為普通的多項式不等式，但是否成立仍需要進一步判定.

vi.在算法agl中，由于考慮的是單個條件組的正性判定，tu部分的條件保持不變，故不需要對條件多項式進行檢測.但對條件組做逐次差分代換[7]過程中，tu部分要發生變化.如果tu部分主變元最高次的系數出現字母，則多項式相除運算會產生分式，此時可能會產生一些不可預料的結果，這種條件組對agl算法來講是有瑕疵的.稱tu部分主變元最高次的系數出現字母的條件組為瑕疵組.如果出現瑕疵組，則輸出相關信息并轉入人工處理.

3）對S中符合2）的諸類型條件組進行過濾，以排除極端情形，尋找反例，并轉入不同的處理流程.

4）按照agl算法，用待測組中的tu部分對tf部分進行正性測試，如果測試成功，則將該待測組拋棄.

5）對正數組的正性進行機器或人工測試.

6）如果某個待測組的正性不易判定，則可嘗試給這個待測組作逐次差分代換，對代換結果再進行測試，以確定正性或進一步尋找反例條件組.

根據上述思路，下面以3元多項式為例，給出agl的改進算法ag.以下用?（f）表示多項式f的次數.

算法ag算法ag過程如下.

A1）設有3元齊次多項式不等式f（x，y，z）≥0，滿足約束條件g（x，y，z）≥0，且?（g）≤?（f）.

A2）建立初始條件組[f（x，y，z），g（x，y，z）]，并置入集合變量o中，得條件組集o={[f（x，y，z），g（x，y，z）]}；為保存o變量的狀態，同時將o置入temp1中.

A3）對temp1作差分代換，并將代換結果置入temp1之中.

A4）對temp1中的矛盾條件組、平凡條件組進行過濾，剩余部分仍置于temp1中.

A5）檢測temp1中的反例條件組，如果有，輸出反例并停機.

A6）檢測temp1中的瑕疵條件組.

A6.1）如果有瑕疵條件組，則連續做若干次（本文程序中設置為5次）逐次差分代換，并對每次代換尋找反例.若有反例，則輸出反例并停機；無反例，則輸出人工處理提示信息，停機.

A6.2）如果沒有瑕疵條件組，則對temp1中的條件組按agl算法進行正性測試，將測試成功的條件組拋棄，剩余的部分仍置于temp1之中.

A7）檢測temp1是否為空集，如果是，則輸出不等式成立的信息并停機；如果不是，則轉向A3.

可以看出，ag算法的終止性是不能保證的，這是因為：一是ag算法的終止是有缺陷的，這一點可以由A6.1看出，因為對于f（x，y，z）≥0成立但ag無法判定的情形，不可能輸出反例，這樣程序會進入死循環，為了避免這種情況，程序中設置了測試次數;二是當f（x，y，z）≥0成立但逐次差分代換過程中又沒有出現瑕疵條件組時（相當于A6.2時段），程序無法自動終止，此時要強制停機，轉入人工處理，這也是ag算法的最大缺點.后面的例11演示了人工處理的例子.

2 三角形幾何不等式判定程序agl2009

根據ag算法，筆者編寫了三角形不等式判定程序agl2009（源程序見http://www.irgoc.org/viewtopic.php?f=27&t=121&sid=ddaa5759422763f544551e5962898c69或http://www.mathlinks.ro/Forum/viewtopic.php?p=1705932#1705932）.它可以看作是文獻［3－4］中agl程序的升級版本，因為它不僅兼顧了agl的功能，而且還增加了許多新功能.

2.1 agl2009程序的功能及命令格式

agl2009是在Maple平臺上開發的應用程序，專門對三角形幾何不等式進行判定.首先將agl2009拷貝到Maple的安裝目錄下，在進入Maple環境后就可以運行這個程序.具體運行指令是read`agl2009.txt`，執行了這個指令，就可以使用agl2009了.

auto命令

功能：對一個三角形幾何不等式f（△ABC）≥0，作角代換A→π-2A，B→π－2B，C→π-2C，并將代換式化為用三角形邊長表示的形式，輸出這個代換式的分子w1和分母w2，而且w1和w2已經取掉了平凡非負因式.

指令格式：auto（ineq），其中ineq表示一個待判定正性的三角形幾何量表達式.

例1判定wa-ha的正性.判定步驟如下：

＞read`agl2009.txt`；#讀入agl2009程序.

＞wa-ha；#鍵入欲判定不等式表達式.

＞auto（%）；#%表示前次輸入的式子wa-ha，即對wa-ha施行auto命令.

執行上述命令后，顯示出用雙線隔開的兩組多項式，前組多項式表示對wa-ha施行角代換后，得到式子的分子和分母；后組表示取掉平凡非負因式后的分子和分母.之所以顯示前一組，是為了觀察到更多的信息（如不等式的取等號條件等）.

特別值得一提的是，如果w1=0，則預示著發現了一個三角形恒等式.此時程序自動出現“The Inequality may be an identity!”提示.

需要指出的是，auto命令對一些三角形幾何量表達式（如含有中線奇次方，根式型幾何量和有理式混合等情形）不能自動完成有理化，此時要想辦法進行人工有理化.

agl命令

功能：對一個用三角形邊長表示的多項式正性進行判定.對不成立者能夠自動輸出反例條件組；對不能判定者，可以輸出一些提示信息.

指令格式：agl（ineq），或者agl（ineq，[ineqs]），其中ineq表示一個用三角形邊長表示的多項式；ineqs表示一個條件，目前只能接受aa參數，表示三角形為銳角三角形.

需要指出的是，在agl模塊中設置了全局變量o.當程序判定不成功時，變量o能夠帶出初始條件組的差分代換集，以便于人工進行分析.

qht命令

功能：尋找一些特殊退化條件下取等號的不等式的最佳系數，這個方法是試探性的.這個模塊應用了文獻[8]提供的恒等式.它本質上是利用了退化三角形＜1，1，2＞，＜1，1，0＞，或者銳角三角形退化為等腰直角三角形.

指令格式：subs（qht，ineq），其中ineq表示一個對應于三角形幾何不等式的表達式.

例2確定三角形幾何量表達式f1-kf2中可能有的最佳系數，需輸入下面的指令:

＞w:=subs（qht，f1-k*f2）；#將所給表達式代換后賦給變量w，以便于調用.

＞solve（subs（x=0，w），k）；#嘗試退化條件＜1，1，0＞時可能有的最佳值.

＞solve（subs（x=1，w），k）；#嘗試退化條件＜1，1，2＞時可能有的最佳值.

>so lv e（su b s（x=sq rt（2）/2，w），k）；#嘗試銳角三角形退化為等腰直角三角形時的情形.

所有這些最佳值得到后，均要用a g l2 0 0 9或其他軟件進行驗證確認.

e q命令

功能：尋找三角形幾何不等式一些特殊的取等號條件.

指令格式：e q（in e q）.注意在用e q找取等號條件時，應通過平方運算盡量將根式化掉.

te stf命令

功能：用三角形邊長的經驗數據驗證不等式.

指令格式：te stf（in e q，[a，b，c]），其中in e q表示不等式對應的表達式，a，b，c表示三角形邊長的驗證數據.

te stf命令雖然不能判定不等式是否成立，但它作為一個驗證命令還是十分有用的.

a g g命令

功能：對單個的條件組按照a g l算法進行測試.如果條件組的正性得到判定，返回-1，否則返回1.

指令格式：a g g（lst），其中lst表示一個條件組.

sd sd命令

功能：對條件組構成的集合進行差分代換，并進行正性測試.

指令格式：sd sd（in e q），其中in e q表示一個條件組集.

a b c to x命令

功能：將一個三角形幾何量表達式化為關于正數x，y，z的形式.

指令格式：sd sd（in e q），其中in e q表示一個三角形幾何量表達式.

命令a g g、sd sd和a b c to x均是為了方便人工處理而設計的.

2.2 a g l2 0 0 9程序應用舉例

例3（文獻[9]中的l5 8）在△A B C中，證明

證明用a g l2 0 0 9程序證明如下：

>g:=w b*w c/（2*ra+w a）-2*（b+c）*a*r/（（a+b）*（a+c））；#輸入不等式表達式.

>a u to（%）；#由顯示的w 1知，不等式（2）有取等號條件b=c.

由于程序對w 1和w 2取平凡非負因式后，均已經是正數，故不等式（2）成立.

由w1的表達式知，不等式（2）有取等號條件b=c，現用e q命令再找一些不等式（2）的取等號條件.輸入命令e q（g），則顯示：

根據此提示信息可找到不等式（2）的部分取等號條件為{a+c=b}，{b=c}，{a+b=c}.

例4在△A B C中，確定不等式ma≥ha的取等號條件.

解運行e q（m a-h a）命令后，得到部分取等號條件為：

可以看出，第1個取等號條件特別有趣.

例5在銳角△ABC中，證明

解輸入以下命令序列：

>（sgm(wa*b））^2-（sqrt（3）/2*sgm（a*b））^2；#為便于有理化，對不等式兩邊要同時平方.>auto（%）；

>agl（w1，[aa]）；#由于是銳角三角形，故要帶aa參數.

經過數秒運算后，打印出“The inequality holds”，故不等式（3）成立.

解鍵入以下命令序列：

>sgm（（hb-hc）^2）-k*sgm（（wb-wc）^2）；

>subs（qht，%）；#qht的本質是根據文獻［8］建立的公式集.

>factor（subs（x=sqrt（2）/2，solve（%，k）））；則顯示：

用agl具體驗證知，當k=0.6時成立，但k=0.61時不成立（用Bottema軟件否定）.雖然這里未能嚴格證明這個常數就是最佳值，但這個結果仍然讓人鼓舞，因為用其他軟件是難以得到這種結果的.

例7證明恒等式

證明運行auto命令后發現w1=0，故式（4）是一個恒等式.

例8設k∈R，證明含參不等式

證明不等式（5）化為關于k的一元二次不等式

用agl易證二次項系數非負，判別式為-4g，其中g=（-bwa+awa-cwb+bwb+cwc-awc）·（-cwa+awa-awb+bwb+cwc-bwc），用agl易證g≥0成立，由此證得不等式（5）.

例9試對不等式

進行判定.

解運行agl（w1）命令后，數秒給出反例多項式.而運行帶銳角參數的命令agl（w1，[aa]），很快判定式（6）在銳角三角形中成立.

注如果用Bottema軟件尋找不等式（6）的反例，程序運行2 697 s后仍然沒有結束跡象.由此可見，agl2009在發現和探討三角形不等式方面，有一些不可替代的作用.例10在△ABC中，證明不等式

證明不等式（7）兩邊同時平方，并運行agl（w1）命令后，發現w1中有因式（a-b）2·（b-c）2（c-a）2，故知不等式（7）在等腰三角形時取等號（這類不等式一般非常強），其余證明略.

例11在△ABC中，證明不等式

證明鍵入agl（w1）命令后，判定沒有成功，轉入人工處理.經檢查知，全局變量o中有一個條件組，且是一個正數組，故證明不等式（8）轉化為證明o中正數組的tf部分關于正數m，n，z成立，而這可以用文獻中的第二類差分代換程序完成[10].

3 帶約束條件差分代換的其他應用

應用帶約束條件多項式的差分代換方法，可以將一些根式形式且不易有理化的三角形幾何不等式問題轉化為條件不等式加以解決.

例12在△ABC中，證明

證明不等式（9）等價于如下條件不等式：

對此條件不等式進行代數化，得到一個條件組[f1，f2]（表達式略）.對條件組[f1，f2]進行一次差分代換，得到由3個條件組構成的差分代換集.用agg命令對這3個條件組一一進行檢測，結果發現其中有2個是半正定的，另外1個正性不能判定.對這個正性不能判定的條件組繼續作差分代換，用agg對得到的條件組進行測試，結果發現全部是正半定的，故不等式（9）成立.

例13在△ABC中,證明

證明不等式（10）可化為條件不等式

這個條件不等式代數化后可化為一個條件組，對這個條件組作一次差分代換，得到條件組集合（為節約篇幅，這里僅寫出了部分表達式）：

其中，

顯然w中有2個正數組，其中g3≥0容易用逐次差分代換程序sds[7]判定成立，g1≥0不容易直接判定，但經過倒數代換加速[10]后容易判定.經驗證知，剩余的條件組[g2，gu]的正性不能用agl算法判定，故這里我們未完成對不等式（10）的證明.

由例13可以看出，一般條件不等式的證明是十分復雜的.如何對由式（11）決定的條件組[g2，gu]的正性進行判定仍是一個待解決的問題.

4 用agl2009程序發現的優美不等式

截至目前，用agl2009程序已經發現了500多個優美的三角形幾何不等式，這些不等式加強或隔離了一些著名的結果，而且其中的許多結果是用其他軟件難以判定的.下面摘錄若干個形式比較優美的結果（更多結果見http://www.mathlinks.ro/Forum/viewtopic.php?t=315511），同時注明用agl2009程序驗證所花費的時間（這些不等式如果用Bottema軟件驗證，大多數時間超長或不能驗證）.

5 結語

本文給出的算法ag，較好地改進了agl算法的不足，據此編寫的程序agl2009適用于一大類三角形幾何不等式的判定.從使用情況看，由于agl2009程序運行速度提高，形成了人的思維和判定結果同步和互動的局面，這使得一些難度甚大且形式新穎的優美不等式被發現（事實證明，如果不等式證明器的運行時間過長，將會使預熱了的思維冷卻和遲滯，瞬間產生的靈感火花由于等待而減弱或熄滅，從而使研究效率和質量大打折扣）.雖然如此，agl2009程序尚存在以下不足或問題：一是agl2009給出的反例是條件組，是一種間接反例；二是對于有些不等式，agl2009輸出反例的時間過長，而從算法分析來看，反例條件組作為最遲出現的反例，是有改進余地的；三是agl2009的終止性是有缺陷的.另外，由本文可以看出，對于agl算法失效的情形，逐次差分代換不是總能奏效的.如何建立一般條件不等式的判定算法和程序，并向多元進行推廣，這些都是十分有價值的研究課題.

最后再提幾個有趣的不等式問題：

[1] 劉保乾.三角形幾何不等式新探[J].不等式研究通訊，2009，16（4）：440-451.

[2] 劉保乾.不等式研究的幾個新結論和新問題[J].嘉應學院學報，2008，26（6）：19-26.

[3]劉保乾.銳角三角形幾何不等式的差分代換證法及應用程序[J].佛山科學技術學院學報，2009，27（5）：33-38.

[4] 劉保乾.條件Si類多項式的構造及其他[J].廣東教育學院學報，2009，29（5）：8-13.

[5] 楊路，夏壁燦.不等式機器證明與自動發現[M].北京：科學技術出版社，2008：117-142.

[6] 劉保乾.用差分代換研究實數域中多項式的半正定性[J].佛山科學技術學院學報，2008，26（2）：8-11.

[7] 楊路.差分代換與不等式機器證明[J].廣州大學學報，2006，5（2）：1-7.

[8] 闕浩濤.否定三角形不等式猜想的一種方法[M]//劉保乾.Bottema，我們看見了什么——三角形幾何不等式研究的新理論、新方法和新結果.拉薩：西藏人民出版社，2003：552-556.

[9] 劉保乾.100個優美的三角形不等式新問題[M]//中國初等數學研究（第1輯）.哈爾濱：哈爾濱工業大學出版社，2009：92-95.

[10] 劉保乾.再談第二類差分代換[J].佛山科學技術學院學報，2009，27（2）：1-6.

Constrained Polynomial Differential Substitution and Applications

LIU Bao-qian
(Information Center，Department of Personnel，Tibet Autonomous Region，Lasa 850000，Tibet，China)

Geometric inequality algorithm is improved and an upgraded version agl2009 isdesigned.Constrainedpolynomial differential substitution isstudied for square root inequalityand several geometric inequalities are found by the agl algorithm.

differential substitution；geometric inequality algorithm；agl algorithm；machine proofing

O 122.3

A

1001-4217（2010）02-0001-10

2009-11-24

劉保乾（1962-），男，陜西鳳翔人，計算機本科.研究方向：多項式不等式與機器證明.E-mail：wshr987@163.com