指數函數多項式的實根分離算法

葛昕鈺，陳世平，劉忠

（1.中國科學院 成都計算機應用研究所，成都 610041； 2.中國科學院大學，北京 100049；3.四川省貿易學校 財經商貿系，四川 雅安 625107；4.樂山職業技術學院 電子信息工程系，四川 樂山 614000）（?通信作者電子郵箱geeexy@163.com）

指數函數多項式的實根分離算法

葛昕鈺1，2*，陳世平3，劉忠1，4

（1.中國科學院 成都計算機應用研究所，成都 610041； 2.中國科學院大學，北京 100049；3.四川省貿易學校 財經商貿系，四川 雅安 625107；4.樂山職業技術學院 電子信息工程系，四川 樂山 614000）（?通信作者電子郵箱geeexy@163.com）

針對超越函數多項式的實根分離問題，提出了一種指數函數多項式的區間分離算法exRoot，將非多項式型實函數的實根分離問題轉化為多項式正負性判定問題進而對其求解。首先，利用泰勒替換法構造目標函數的多項式區間套；然后，將指數函數的求根問題轉化為多項式在區間內正負性的判定問題；最后，給出綜合算法，并且試探性地應用于實特征值線性系統的可達性判定問題。所提算法在Maple中實現，輸出的結果可讀，且高效易行。區別于HSOLVER和數值計算方法fsolve，exRoot回避了直接討論根的存在性問題，理論上具有終止性和完備性，且可達到任意精度，應用于最優化問題時可避免數值解帶來的系統誤差。

指數函數多項式；實根分離；泰勒替換法；區間列；終止性

0 引言

實根分離算法作為實代數的基本算法之一，不僅具有很強的理論意義，還有著廣泛的應用前景。除了GCD（Greatest Common Divisor）算法、Sylvester結式、Descartes符號法則等經典工具外，對于多項式型函數實根分離的研究也有進展，例如Becker等［1］提出的Cisolate算法和Mehlhorn等［2］提出的漸進方法。而上述多項式型函數的實根分離算法對非多項式型實函數的實根求解問題并不適用，因此仍需進一步的研究［3-11］。目前求非多項式型實函數近似根的主要方法為迭代法，其過程中可能出現過分依賴初始近似值、迭代后局部收斂的問題，存在多個根時可能出現不收斂的情況。

在眾多非多項式型實函數中，指數函數在機器人逆運動學、分片代數簇、化學反應器穩定性分析等工程問題中有許多應用，例如在實特征值線性系統的可達性判定中，多項式等式型約束即可轉化為指數函數的實根分離。然而，用迭代法解決指數函數實根分離問題的過程同樣會存在上述問題，并且沒有消除超越因子，因此不能真正解決指數函數中的超越問題。由此，指數函數實根分離的自動證明和程序開發也成為人工智能和自動推理中重要且具有挑戰的任務。

近年來也有學者對其自動證明算法進行研究：文獻［11］中提出了針對exp-log-arctan型函數的實根分離方法，根據半傅里葉序列（semi-Fourier sequence）符號的變化數判定根的存在性，但算法的完備性依賴于尚未證明的Schanuel猜想；文獻［12］中利用羅爾中值定理對多項式的偽倒數進行判定從而分離其實根，其方法直接應用于超越函數exp（x）、ln（x）、arctan（x）以解決實數范圍的超越函數實根分離問題，部分決策過程已在計算機邏輯系統Redlog中實現；文獻［13］中采用連分數構造指數函數多項式的區間套，從而估計指數函數多項式在有理點上的值。

為了更好地解決指數函數的實根分離問題，可將其理解為指數多項式在特定區間上的正負性判定問題。文獻［3，14-17］中利用反正切函數泰勒展開式交錯級數的特性設計了混合三角多項式不等式的泰勒替換法，其核心思想是先確定根所在的區間，再構造其上、下界多項式找到包含非多項式型實函數的有理函數多項式列，從而判定該區間上三角函數多項式正負性，進而實根分離。文獻［3］中根據該算法已經完成了對三角函數多項式實根分離的自動求解程序，并在符號計算軟件Maple中實現。延續在三角函數上的思想，文獻［17］中提出了指數多項式不等式的判定方法。本文即在文獻［17］研究的基礎上，以指數多項式不等式的判定為主要工具，提出了針對形如f（x，）的指數函數的實根分離算法exRoot，并對指數函數的最優化問題進行了討論，得到了極值所在的確定區間。

區別于文獻［11-12］的方法，本文將非多項式型實函數的實根分離問題轉化為多項式判定問題進而求解，回避了直接討論根的存在性問題，并應用于多項式優化問題中。算法exRoot已經在Maple中實現程序，可自動輸出含單根的區間列，且區間長度可以滿足任意精度，形成完備且可讀的證明過程。程序在Intel Core i5-6500 Windows x64 Maple2015環境下對隨機生成的實例運行時長均未超過15 s。

1 指數多項式

先給出一些有關代數數和超越數的基本知識。

定義1［15］給定一個數a，若存在系數不全為零的整系數多項式P（x）使得P（a）=0，則稱a是代數的或a是代數數，否則稱a是超越數。

引理1［15］每一個代數數系數多項式的根也是代數數。

定義2［15］給定二元有理系數多項式環Q［x，y］，將其中的變量y用eqx替換（），定義該環上的一個映射hom：f（x，y）→f（x，eqx）。二元有理多項式f（x，y）在該映射下的像F（x）=hom（f（x，y））=f（x，eqx）被稱為指數多項式。記映射后的環為Q［x，eqx］。

定義3［17］x0稱為實函數的重根，如果φ（x0）=φapos;（x0）=0。

引理2［17］若f（x，y）是二元有理多項式，那么指數多項式f（x，y）=f（x，ex）唯一可能的重根是0。

引理3若f（x，y）?0，則F（x）=hom（f（x，y））?0（此處f（x，y）?0表示f（x，y）不恒等于0，下同）。

下面討論mgt;0且cm（x）?0的情況。假設f（x，y）?0而F（x）=hom（f（x，y））≡0。由于（e2）n是超越的，而對有理多項式ci（2）是代數數。由定義2，F（e2）=cm（2）（e2）m+（++c0（2） =0說明cm（2）===c0（2）=0，代入則有f（x，y）?0，與假設矛盾。綜上所述，引理3成立。

定義在［0，+∞）的指數多項式具有環的代數結構，即hom是二元有理系數多項式環到指數多項式環的一個映射。由引理2可知映射hom是一對一的，顯然也是Q［x，y］到Q［x，eqx］滿射，那么存在其逆映射：F（x）=f（x，eqx）→f（x，y）。

引理4F（x）=f（x，ex）在求導運算下封閉。

引理5［17］對給定的二元有理多項式f（x，y），存在，使得指數多項式的任意正根。若變元序設定為，將f（x，y）按字典序降序排列，當xgt;MR時，若其首系為正，；若其首系為負，。

根據文獻［17］中對引理5的證明過程，有算法1計算根的上界。

算法1 upBound。

輸入 二元有理多項式f（x，y）；

輸出 有理多項式f（x，y）根的一個上界MR。

BEGIN

END

其中realroot（f（x），r）是Maple中關于有理多項式的實根分離命令：輸入有理多項式f（x）和精度r，返回一個互不相交的區間列。整個列表包含的實根，每個區間只包含一個實根，且各區間長度均不超過r。

引理6［16］對二元有理多項式f（x，y），F（x）=f（x，ex）在（0，+∞）內至多有有限個不同實根（重根只記一次）。

記G（x）在0點Taylor展開式的前n項之和為，例如，。可見，展開各項依次交錯，對此構造其多項式列，進而實現指數函數的多項式型放縮。

定義4記，，記，對hom：y=ex有。當時，記，否則。記Fd（x）=hom（fd（x，y））。

顯然f（x，y）=fd（x，y）·yn，那么對，有。

以下若未作特殊說明，均假設x∈（0，+∞）（對的討論可作變量替換）。

定義5若在區間（0，T］（）內滿足1）～3），則常數稱為T的臨界值，稱在區間上可規范展開。

1）F（x）gt;0；

引理7［17］假設多項式T1（x）gt;0，T2（x）gt;0且，則。

引理8［17］當時，對任意有：

3）當n→∞ 時，。

定義6對任意，記為Fd（x）的一個上界多項式，記為Fd（x）的一個下界多項式。

引理9［17］對任意，當時，有：

1）Tmax（x，n，Fd（x））gt;F（x）gt;Tmin（x，n，Fd（x））；

3）當n→∞時，Tmax（x，n，Fd（x））→Fd（x），Tmin（x，n，。

對關于x的單變量多項式，有以下性質：

定理1［17］任意x∈（0，T］，Fd（x）=f（x，e-x）gt;0成立當且僅當。

定理2［17］任意x∈（0，T］，Fd（x）=f（x，e-x）lt;0成立當且僅當Tmax（x，n，Fd（x））≤0。

定理1和定理2說明函數在區間（0，T］上任意一有理點的正負性是可判定的。在此基礎上本文設計了算法2，用來判定函數F（x）=f（x，ex）在區間（a，b）∈（0，T）上的值域與0的大小關系。具體思路如下：1）判定上界多項式是否在該范圍內恒小于0，如果是，那么該段上函數值均為負，判定結果記為；2）判定下界多項式是否在該范圍內恒大于0，如果是，那么該段上函數值均為正，判定結果記為1；3）判定在該范圍內下界多項式小于0、上界多項式大于0，如果是，那么函數在該段正負性不確定，判定結果記為0；4）如果上述情況均不符合，則遞歸進行其項展開繼續判定，直至得出判定結果。

由于區間端點均為有理數，因此端點值不會是非多項式型實函數的根，故在如下討論中不考慮端點，均使用開區間。

算法2 determination。

輸入 1）Fd（x）=f（x，），2）a（），3）b（）；

輸出sgn。 #返回值sgn表示在區間（a，b）上的值域與0的關系：表示函數在該區間內值域下界大于0，表示函數在該區間內值域上界小于0；表示在該區間內值域包含0。

BEGIN

#該段函數值為正，算法結束

#該段正負性不定，算法結束

END

其中，prove（ineq，（a，b））表示對不等式ineq在區間（a，b）上的判定，ineq在（a，b）上成立則返回true，否則返回false。可通過Maple的不等式證明程序包Bottema中的判定工具xprove（ineq，［xgt;a，xlt;b］）實現。

定理3［17］對不可約二元有理多項式，算法2必然終止。

根據算法1和算法2有對應程序upBound（expr）、determination（expr，a，b）。

2 指數多項式的實根分離

2.1 指數多項式的實根分離算法

而判定fd（x，y）在區間（0，MR）內根的存在性的基本思路是：對不可約多項式fd（x，y），fd（x，y）在（a，b）上恒大于0或恒小于0，則在（a，b）上無實根；否則對fapos;d（x，y）進行判定，若在（a，b）上單調，則有唯一實根；若fd（x，y）在（a，b）上既不恒大于0，也不恒小于0，在（a，b）上也不單調，那么采用二分法分離區間，再遞歸進行判定。根據以上說明，本文構造了算法3用于實根分離。

算法3 isolation。

BEGIN

END

定理4若f（x，y）為不可約二元有理多項式，算法3必然終止。

證明f（x，y）在區間（0，T）上任意一有理點的正負性總是可判定的，并由引理6可知，f（x，y）最多有有限個根，那么判定過程必然是有限步的。過程采用二分法，保證各區間不相交。那么，算法3必然終止。

對已有但不滿足精度要求的區間列，可用二分法分割區間直至滿足精度要求（算法4）。

算法4 accuracy。

輸入 1）Fd（x），2）Fd（x）的單根區間（a，b），3）給定精度r（rgt;0）；

輸出 （c，d）。#F（x）在（c，d）內有唯一根且

BEGIN

END

綜上所述，本文提出綜合算法5對多項式進行轉化和判定：輸入（此時）求出MR后，同除y的最高次冪將多項式變形為，運行算法3對其實根分離，得到區間列后采用算法4提升精度，輸出滿足設置精度的、互不相交的區間列，每個區間內有且只有一個根。

輸入 1）二元有理多項式f（x，y），2）；

BEGIN

END

根據算法3、算法4和算法5有對應程序isolation（expr，a，b）、accuracy（expr，a，b，r）和exRoot（expr，r）。

例1，。

利用算法5求解該例過程如下：

c）輸出區間列｛（0，1）｝。

4）運行accuracy（Fd（x），0，1，2，1/10），二分法求精度，結果為（11/16，3/4）。

2.2 實根分離算法應用實例

例2［13］指數函數多項式，考慮φ（x）的根。

對不可約多項式φ（x）有。

例4［18］對線性非齊次系統：

運行程序exRoot（f（x，y），1/4），得到結果為｛（3/4，1）｝。也就是說，該系統在內可達。

上述實例已在Intel Core i5-6500，Windows 7 x64， Maple2015環境下進行驗證，運行時間如表1所示。其中，fsolve為Maple中實根隔離的數值工具，每次只能隔離出一個實根。同時，相較HSOLVER，exRoot對例4的計算時間明顯較短，且例2的計算結果與fsolve一致。

表1 實例運行時間Tab. 1 Running times of examples

3 最優化問題

3.1 最優化算法

同時，實根分離算法還可用于最優化問題。

定理5 對有理多項式F（x）有。

根據定理5可以由各極值比較得出最值點所在的區間。算法6（算法7）是比較兩個極值區間中較大（小）的極值點所在的區間，這樣可以通過算法8得到最值點所在的區間。

算法6 comparisonMax。

輸入 1）F（x），2）極大值點（a1，b1），3）極大值點（a2，b2），4）n0；

BEGIN

END

算法7 comparisonMin。

輸入 1）F（x），2）極小值點，3）極小值點，4）n0；

BEGIN

END

得到最值點區間后進而求出最值區間，同樣利用定理5進行進一步放縮。

對最大值點所在區間（amax，bmax），有。

將F（x）的上、下界多項式代入，進一步得到。

對值域不滿足精度要求的結果，可進一步通過算法4操作使其達到精度限制。

算法8 optimization。

輸入 1）F（x），2）F（x）的駐點區間列，3）n0；

BEGIN

END

3.2 最優化算法應用實例

求解過程如下：

運行產生的分子分母大整數的分數會降低結果的可讀性，可采取如下簡化策略：將分數的分子分母從個位開始同時去掉若干位數（分母保留的位數不得低于，否則無法達到指定精度r），再將區間左端點的分母加1，右端點的分子加1，這樣得到的區間是端點的分子分母的位數可以小于給定數且包含原區間的最小區間［3］。通過如上放縮后區間簡化為，即F（x）最小值所在區間為。最優化過程在Intel Core i5-6500，Windows 7 x64操作系統，Maple2015環境下運行時間0.87 s。

4 結語

本文在指數函數多項式判定算法的基礎上，將指數函數的實根分離問題轉化為多項式判定問題進而求解，實現了指數函數實根分離的完全算法exRoot。該算法回避了根的存在性問題，找出了包含全部實根且區間互不相交的區間列（每個區間有且僅有一個實根），區間長度可達到任意精度。然后將其應用于多項式優化問題中，通過對指數多項式導數的實根分離得到駐點存在的區間，最終得到極值的確定范圍。本文解決了一類超越函數解的問題，簡單易行，十分高效。

[1] BECKER R， SAGRALOFF M， SHARMA V， et al. A near-optimal subdivision algorithm for complex root isolation based on the Pellet test and Newton iteration ［J］. Journal of Symbolic Computation， 2018， 86： 51-96.

[2] MEHLHORN K， SAGRALOFF M， WANG P M. From approximate factorization to root isolation with application to cylindrical algebraic decomposition ［J］. Journal of Symbolic Computation， 2015， 66：34-69.

[3] 陳世平，劉忠.三角函數多項式的實根分離［J］.汕頭大學學報（自然科學版），2016，31（3）：25-39.（CHEN S P， LIU Z. Real root isolation of trigonometric function polynomial ［J］. Journal of Shantou University （Natural Science Edition）， 2016， 31（3）：25-39.）

[4] 楊路，夏壁燦.不等式機器證明與自動發現［M］.北京：科學出版社，2008：126-130.（YANG L， XIA B C. Inequality Machanical Proving and Automatic Discovery ［M］. Beijing： Science Press， 2008： 126-130.）

[5] ACHATZ M， McCALLUM S， WEISPFENNING V. Deciding polynomial-exponential problems ［C］// Proceedings of the 2008 21st International Symposium on Symbolic and Algebraic Computation. New York： ACM， 2008： 215-222.

[6] WU W T. Basic principles of mechanical theorem proving in elementary geometries ［J］. Journal of Automated Reasoning， 1986， 2（3）： 221-252.

[7] BUCHBERGER B， COLLINSS G E， KUTZLER B. Algebraic methods for geometric reasoning ［J］. Annual Review of Computer Science， 1988， 3： 85-119.

[8] YANG L， ZHANG J. A practical program of automated proving for a class of geometric inequalities ［C］// Proceedings of the 2000 International Workshop on Automated Deduction in Geometry， LNCS 2061. Berlin： Springer， 2000： 41-57.

[9] 陸征一，何碧，羅勇.多項式系統的實根分離算法及其應用［M］.北京：科學出版社，2004：34-44. （LU Z Y， HE B， LUO Y， Real Root Isolation Algorithm of Polynomial System and Its Applications ［M］. Beijing： Science Press， 2004： 34-44.）

[10] DAI L Y， FAN Z， XIA B C， et al. Logcf： an efficient tool for real root isolation ［J］. Journal of Systems Science and Complexity，2019， 32（6）： 1767-1782.

[11] STRZEBO?SKI A. Real root isolation for exp-log-arctan functions ［J］. Journal of Symbolic Computation， 2012， 47（3）： 282-314.

[12] MCCALLUM S， WEISPFENNING V. Deciding polynomial-transcendental problems ［J］. Journal of Symbolic Computation， 2012， 47（1）： 16-31.

[13] 徐鳴.程序驗證與系統分析中的若干符號問題［D］.上海：華東師范大學，2010：11-20.（XU M. Some symbolic computation issues in program verification and system analysis ［D］. Shanghai： East China Normal University， 2010： 11-20.）

[14] CHEN S P， LIU Z. Automated proof of mixed trigonometric-polynomial inequalities ［J］. Journal of Symbolic Computation， 2020， 101： 318-329.

[15] 陳世平，劉忠.一類超越函數多項式不等式的自動證明［J］.系統科學與數學，2019，39（5）：804-822.（CHEN S P， LIU Z. Automated proving for a class of transcendental-polynomial inequalities ［J］. Journal of Systems Science and Mathematical Sciences， 2019， 39（5）： 804-822.）

[16] 陳世平，劉忠.三角函數多項式不等式的自動證明［J］.汕頭大學學報（自然科學版），2015，30（3）：43-55.（CHEN S P， LIU Z. Automated proving of trigonometric function polynomial inequalities ［J］. Journal of Shantou University （Natural Science Edition）， 2015， 30（3）： 43-55.）

[17] 陳世平，劉忠.指數多項式不等式的自動證明［J］.系統科學與數學，2017，37（7）：1692-1703.（CHEN S P， LIU Z. Automated proving of exponent polynomial inequalities ［J］. Journal of Systems Science and Mathematical Sciences， 2017， 37（7）： 1692-1703.）

[18] XU M， CHEN L Y， ZENG Z B， et al. Reachability analysis of rational eigenvalue linear systems ［J］. International Journal of Systems Science，2010， 41（12）： 1411-1419.

Real root isolation algorithm for exponential function polynomials

GE Xinyu1，2*， CHEN Shiping3， LIU Zhong1，4

（1.Chengdu Institute of Computer Application，Chinese Academy of Sciences，Chengdu Sichuan610041，China；2.University of Chinese Academy of Sciences，Beijing100049，China；3.Department of Finance and Commerce，Sichuan Trade School，Ya’an Sichuan625107，China；4.Department of Electronic Information Engineer ing，Leshan Vocational and Technical College，Leshan Sichuan614000，China）

For addressing real root isolation problem of transcendental function polynomials， an interval isolation algorithm for exponential function polynomials named exRoot was proposed. In the algorithm， the real root isolation problem of non-polynomial real functions was transformed into sign determination problem of polynomial， then was solved. Firstly， the Taylor substitution method was used to construct the polynomial nested interval of the objective function. Then， the problem of finding the root of the exponential function was transformed into the problem of determining the positivity and negativity of the polynomial in the intervals. Finally， a comprehensive algorithm was given and applied to determine the reachability of rational eigenvalue linear system tentatively. The proposed algorithm was implemented in Maple efficiently and easily with readable output results. Different from HSOLVERand numerical calculation method fsolve，exRoot avoids discussing the existence of roots directly， and theoretically has termination and completeness. It can reach any precision and can avoid the systematic error brought by numerical solution when being applied into the optimization problem.

exponential function polynomial; real root isolation; Taylor substitution method; sequence of intervals; termination

TP181

A

1001-9081（2022）05-1524-07

10.11772/j.issn.1001-9081.2021030440

2021?03?22；

2021?07?14；

2021?07?14。

四川省科學技術廳科技計劃項目（2016GFW0048）。

葛昕鈺（1995—），女，河南安陽人，博士研究生，CCF會員，主要研究方向：自動推理、機器證明； 陳世平（1970—），男，四川遂寧人，高級講師，博士，主要研究方向：機器證明、符號計算； 劉忠（1968—），男，四川樂山人，教授，博士，主要研究方向：自動推理、機器證明。

This work is partially supported by Scientific and Technological Program of Science and Technology Department of Sichuan Province （2016GFW0048）.

GE Xinyu， born in 1995， Ph. D. candidate. Her research interests include automated reasoning， mechanical proving.

CHEN Shiping， born in 1970， Ph. D.， senior lecturer. His research interests include mechanical proving，symbolic computation.

LIU Zhong， born in 1968， Ph. D.， professor. His research interests include automated reasoning，mechanical proving.