陳世平劉　忠

（1.四川省商貿(mào)學(xué)校-中國民航飛行學(xué)院德陽校區(qū)，四川省　德陽市　618000；2.樂山職業(yè)技術(shù)學(xué)院，四川省　樂山市　614000）

三角函數(shù)多項式的實根分離

陳世平1劉忠2

（1.四川省商貿(mào)學(xué)校-中國民航飛行學(xué)院德陽校區(qū)，四川省德陽市618000；2.樂山職業(yè)技術(shù)學(xué)院，四川省樂山市614000）

本文探索非多項式型實函數(shù)的實根分離問題，實現(xiàn)了分離三角函數(shù)多項式實根的“完備算法”，即可以找出一個互不相交的區(qū)間列，每一個區(qū)間包含函數(shù)一個實根，整個列表包含函數(shù)的全部實根，且每個區(qū)間長度可以小于任意指定精度.

三角函數(shù)多項式；實根分離；區(qū)間列；終止性

0　引言

實根分離是實代數(shù)的基本算法之一，不僅有很強的理論意義，也有廣泛的應(yīng)用前景.其經(jīng)典工作都是圍繞一元整系數(shù)多項式以及零維多元多項式系統(tǒng)展開的，已有了豐富的成果和普遍的應(yīng)用，而對于非多項式型實函數(shù)，傳統(tǒng)的方法都不適用，因為只有多項式才有GCD算法、Sylvester結(jié)式、Sturm定理、Descartes符號法則等概念和方法［1-5］.當(dāng)然對非多項式型實函數(shù)的實根求解問題，也有學(xué)者在涉及，文獻［6］探索和解決了一類廣義多項式（指數(shù)多項式）的實根分離問題，文獻［7］利用符號計算中區(qū)間算術(shù)的思想和指數(shù)函數(shù)連分?jǐn)?shù)展開的技巧對算法進行了改進.有關(guān)其它非多項式型實函數(shù)方程的符號求解或精確求解此前未見報道.

本文的目標(biāo)是探討另一類廣義多項式（三角函數(shù)多項式）的實根求解問題，如已知漸開線方程θ=inv（α）=tan（α）-α的θ值，需要求解α的值.迭代法是此類問題通用而有效的數(shù)值求解方案（如Matlab），但迭代法需要輸入適合的初值，也不能求出所有的根或根的區(qū)間，不能判定根的總數(shù)，有很大的局限性，如何精確求出三角函數(shù)多項式的全部實根值得深入研究.文獻［9-10］為解決“類似sin（x）＜x＜tan（x）的超越不等式”的機器證明問題［11］，設(shè)計并實現(xiàn)了一個三角函數(shù)多項式不等式機器證明的完備算法：運用Taylor展開式建立一個逼近目標(biāo)函數(shù)的多項式區(qū)間套，從而將證明轉(zhuǎn)化為一系列的一元多項式不等式的驗證，然后借助代數(shù)不等式證明工具完成最后的工作，該算法回避了函數(shù)根的判定和求解問題.本文在該算法的基礎(chǔ)上，實現(xiàn)了一個基于不等式證明的三角函數(shù)多項式實根分離算法：可以找出一個互不相交的區(qū)間列，每一個區(qū)間包含一個實根，整個列表包含三角函數(shù)多項式在（0，/2］內(nèi)的全部實根，且每個區(qū)間長度可以小于任意指定精度.

1　三角函數(shù)多項式

定義1.1設(shè)f（x，x1，…，xn）是n+1元有理多項式，將變量x1，…，xn用sin（kx）、cos（kx）、tan（kx）（k為任意有理數(shù)）等三角函數(shù)替換后得到的函數(shù)稱為三角函數(shù)多項式.

給定二元有理系數(shù)多項式環(huán)Q［x，y］，定義該環(huán)上一個映射：hom：f（x，y）→F（x），將變量y用tan（x/2）代替.

正切函數(shù)多項式在求導(dǎo)運算下封閉，顯然

若無歧義，本文F（x）均表示正切函數(shù)多項式f（x，tan（x/2））.特別地，若fy′（x，y）恒等于0，f（x，y）是x的一元多項式，此時hom（f）=f；若fx′（x，y）恒等于0，此時f（x，y）是y的一元多項式.

定義1.3稱二元多項式f（x，y）是規(guī)范的，如果fy′（x，y）與fx′（x，y）均不恒等于0.

定義1.4x0是實函數(shù)r（x）的重根，如果r（x0）=r′（x0）=0.

引理1.3［12］若α≠0，則α與tan（α）二者之中至少有一為超越數(shù)；

證明由引理1.3知當(dāng)y0是代數(shù)數(shù)時，x0必為超越數(shù)，將f（x，y）按x降冪排列為qm（y）xm+qm-1（y）xm-1+…+q0（y），其中m＞0且qm（y）不恒等于0，因為f（x，y）不可約，所以qm（y0）、qm-1（y0）、…、q0（y0）是不能全為0的代數(shù)數(shù)，否則（y-y0）就是f（x，y）的因子，所以對任意超越數(shù)x，qm（y0）xm+qm-1（y0）xm-1+…+q0（y0）均不等于0，即F（x0）≠0.

同樣的道理，當(dāng)x0是代數(shù)數(shù)，則y0=tan（x0/2）為超越數(shù)，F(xiàn)（x0）=f（x0，y0）≠0.

引理1.5若f1（x）、f2（y）是一元有理多項式，f3（x，y）的每個因式都是二元有理規(guī)范多項式，則F1（x）=hom（f1（x））=f1（x）、F2（x）=hom（f2（y））=f2（tan（x/2））、F3（x）=hom（f3（x，y））=f3（x，tan（x/2））相互間無公根.

證明若x1是F1（x）的根，則x1是代數(shù)數(shù)，y1=tan（x1/2）必是超越數(shù)；

若x2是F2（x）=f2（tan（x/2））的根，則y2=tan（x2/2）是代數(shù)數(shù)，x2是超越數(shù)；

若x3是F3（x）的根，則必是f3（x，y）的某個不可約規(guī)范因式映射的正切函數(shù)多項式的根，由引理1.4，x3和y3=tan（x3/2）都是超越數(shù)；

所以F1（x）、F2（x）、F3（x）相互間均無公根.

由引理1.1和1.2以及1.5可以得出推論1.1.

推論1.1若（fx，y）為無重因子的二元有理多項式，則F（x）=hom（（fx，y））在（0，/2］內(nèi)無重根.

引理1.6［10］若（fx，y）為二元有理多項式，則F（x）=hom（（fx，y））在（0，/2］內(nèi)最多有有限個不同的根.

用f+和f-分別表示多項式f（x，y）展開式的正項和負項，顯然f=f++f-，且下面的引理成立：

引理1.7假設(shè)多項式T1（y）＞0，T2（y）＞0且T1（y）＜x＜T2（y），則

f+（T1（y），y）+f-（T2（y），y）＜f（x，y）＜f+（T2（y），y）+f-（T1（y），y）.

為方便，我們將實函數(shù)f（x）的在0點Taylor展開式中的前n項記為taylor（f（x），n）或taylor（f，n）（x），即當(dāng)n為奇數(shù)時taylor（arctan（x），n）=x-x3/3+…+x（2n-1）/（2n-1）（0＜x≦1），當(dāng)n為偶數(shù)時taylor（arctan（x），n）=x-x3/3+x5/5-…-x（2n-1）/（2n-1）（0＜x≦1）.

引理1.8當(dāng)0＜y≦1時，對任意自然數(shù)m，

（1）taylor（arctan（y），2m）＜arctan（y）＜taylor（arctan（y），2m-1）；

（2）taylor（arctan（y），2m）＜taylor（arctan（y），2m+2））；taylor（arctan（y），2m-1）＞taylor（arctan（y），2m+1）；

（3）當(dāng)n→∞時，taylor（arctan（y），2m）→arctan（y），taylor（arctan（y），2m-1）→arctan（y）；

定義1.5對任意自然數(shù)n，定義

f（x，y）的上限多項式為T_max（n，f）=f+（2*taylor（arctan（y），2n-1）），y）+f-（2*taylor（arctan（y），2n），y）；

f（x，y）的下限多項式為T_min（n，f）=f+（2*taylor（arctan（y），2n）），y）+f-（2*taylor（arctan（y），2n-1），y）.

T_max（n，f）和T_min（n，f）是關(guān)于y的單變量多項式.

給定二元有理系數(shù)多項式環(huán)Q［x，y］，定義該環(huán)上一個映射：HOM：f（x，y）→G（y），將變量x用2*arctan（y）代替，即HOM（f（x，y））=f（2*arctan（y），y））.

G（y）與f（x，y）、F（x）有如下關(guān)系：在tan（x/2）=y或x=2*arctan（y）的條件下，F(xiàn)（x）=f（x，y）=G（y）.

引理1.9任意n∈N，在（0，1］上，函數(shù)T_max（n，f）、T_min（n，f）、G滿足以下性質(zhì)：

（1）T_max（n，f）＞G＞T_min（n，f）；

（2）T_max（n，f）＞T_max（n+1，f），T_min（n，f）＜T_min（n+1，f）；

（3）T_max（n，-f）=-T_min（n，f），T_max（n，-f）=-T_min（n，f）；

（4）當(dāng)n→∞時，T_max（n，f）→G，T_min（n，f）→G.

即關(guān)于n，T_max（n，f）嚴(yán)格單調(diào)下降，T_min（n，f）嚴(yán)格單調(diào)上升，并且當(dāng)y∈（0，1］時，有如下關(guān)系：T_min（1，f）（y）＜T_min（2，f）（y）＜T_min（3，f）（y）＜…＜G（y）＜…＜T_max（3，f）（y）＜T_max（2，f）（y）＜T_max（1，f）（y），也就是說有一個多項式區(qū)間套來逼近G（y）：（T_min（1，f）（y），T_max（1，f）（y））?（T_min（2，f）（y），T_max（2，f）（y））?（T_min（3，f）（y），T_max（3，f）（y））?………?｛G（y）｝，

本文在設(shè)計狀態(tài)反饋控制器的基礎(chǔ)之上，增加了軌跡追蹤器環(huán)節(jié)，即討論了補償增益矩陣G的選取過程，使得系統(tǒng)狀態(tài)量和參考軌跡輸入量的誤差趨近于零。最終通過Simulink仿真結(jié)果表明，本文設(shè)計的狀態(tài)反饋控制器及軌跡追蹤器達到了理想的設(shè)計效果。

引理1.10［9］任意y0∈（0，1］，G（y0）＜0當(dāng)且僅當(dāng)存在n0，使得T_max（n0，f）（y0）≤0.

引理1.11任意y0∈（0，1］，G（y0）＞0當(dāng)且僅當(dāng)存在n0，使得T_min（n0，f）（y0）≥0.

證明G（y0）＞0等價于-G（y0）＜0，當(dāng)且僅當(dāng)存在n0，使得T_max（n0，-f）（y0）≤0，等價于T_min（n0，f）（y0）≥0.

引理1.12［9］不等式G（y）＞0在區(qū)間（0，1］成立，當(dāng)且僅當(dāng)存在n0使得不等式T_min（n0，f）（y）≥0在（0，1］成立.

引理1.13不等式G（y）＞0在區(qū)間（a，b］成立（其中（a，b］?（0，1］），當(dāng)且僅當(dāng)存在n0使得不等式T_min（n0，f）（y）≥0在（a，b］成立.

證明令y=（b-a）t+a，由引理1.12得證.

推論1.2不等式G（y）＜0在區(qū)間（a，b］成立（其中（a，b］?（0，1］），當(dāng)且僅當(dāng)存在n0使得不等式-T_max（n0，f）（y）≥0在（a，b］成立.

由引理1.4可以得到：

引理1.14若f（x，y）是二元不可約規(guī)范有理多項式，則當(dāng)y0和x0=2*arctan（y0）二者有一個為代數(shù)數(shù)時，G（y0）=f（x0，y0）≠0.

推論1.3若f（x，y）是有理多項式，且每個因式都是規(guī)范的，則當(dāng)y0和x0=2*arctan（y0）二者有一個為代數(shù)數(shù)時，G（y0）=f（x0，y0）≠0.

證明若G（y0）=f（x0，y0）=0，則必然存在f（x，y）的某個不可約且規(guī)范的因式f0（x，y）滿足f0（x0，y0）=0，與引理1.14矛盾.

由引理1.6還可以得出引理1.15：

引理1.15若f（x，y）為二元有理多項式，G（y）=（f（2*arctan（y），y））在（0，1］內(nèi)最多有有限個不同的實根.

引理1.16若f（x，y）為無重因子二元有理多項式，G（y）=f（2*arctan（y），y）在（0，1］內(nèi)無重根.

證明若y0∈（0，1］是G（x）的重根，即G（y0）=G′（y0）=0，令x0=2*arctan（y0），顯然x0∈（0，/2］，則F（x0）=G（y0）=0，而F（′x0）=fx（′（x0，tan（x0/2））+（1+（tan（x0/2）2）*fy′（x，tan（x0/2））/2=fx′（x0，y0）+（1+y02）*fy′（x，y0）/2=G′（y0）*（1+y02）/2=0，即x0是F（x）的重根，與推論1.1矛盾.

引理1.17若f（x，y）為無重因子的二元有理多項式，G（y）=f（2*arctan（y），y），則在（0，1］內(nèi)不等式G（y）＞0與G（y）≧0等價，G（y）＜0與G（y）≦0等價.

證明假設(shè)G（y）＞0不成立但G（y）≧0成立，即存在y0∈（0，1］，G（y0）=0，由推論1.3，y0≠1，而由引理1.12，G（y）在（0，1］內(nèi)的根最多只有有限個，所以存在y0的某空心鄰域，G（y）在其內(nèi)不等于0，即G（y）＞0，由G（y）的可導(dǎo)性知G′（y0）=0，即y0是G（y）的重根，與引理1.16矛盾.

同理，G（y）＜0與G（y）≦0等價.

引理1.18若二元多項式f≠0，則G=HOM（f）≠0.

證明假設(shè)f≠0，而G=HOM（f）=0.

若fx′（x，y）≠0，將f（x，y）按x降冪排列為qm（y）xm+qm-1（y）xm-1+…+q0（y），m＞0且qm（y）不恒等于0.由tan（/4）=1和tan（2x）（1-tan（x）2）=2tan（x）知：tan（/2n）（n＞1）都是代數(shù)數(shù)，記tan（/2n）為tn，tn是代數(shù)數(shù)且arctan（tn）=/2n，而G（t）n=qm（t）n（/2n-）1m+qm-（1tn）（/2n-1）m-1+…+q（0tn），對任意n（＞1），每個q（itn）均為代數(shù)數(shù)，/2n-1為超越數(shù)，所以如果G（tn）=0，則qm（tn）=0，qm-1（tn）=0，…，q0（tn）=0.即方程qm（y）=0有無限多個不同的根，此時只有qm（y）恒等于0，與假設(shè)條件矛盾；

若fx′（x，y）=fy′（x，y）=0，即f為非0常數(shù)，此時G也等于該常數(shù)，即G≠0；若fx′（x，y）=0，fy′（x，y）≠0，此時f（x，y）是y的一次多項式，不妨記為p（y），此時G=HOM（p）=p，即G≠0，與假設(shè)條件矛盾.

引理成立.

由引理1.18知映射HOM是一一的，顯然也是Q［x，y］到G上的滿射，所以HOM存在逆映射HOM-1，并且f=HOM-1（HOM（f）），G=HOM（HOM-1（G））.

在以上討論的基礎(chǔ)上，我們設(shè)計了判斷實函數(shù)G（y）=f（2*arctan（y），y）在區(qū)間（a，b］上與0的大小關(guān)系的完備算法：

算法1.1 prove_arctan_interval

輸入：①反正切函數(shù)多項式G（y）；②區(qū)間（a，b］?（0，1］；

輸出：1表示G（y）在區(qū)間（a，b］內(nèi)恒大于0，-1表示恒小于0，0表示G與0在（a，b］內(nèi)無固定大小關(guān)系；

BEGIN

（1）n←1；

（2）f←HOM-1（G）；

計算f的上（下）限多項式T_max（n，f）、T_min（n，f）；

?。┤魡巫兞慷囗検讲坏仁絋_min（n，f）≥0在（a，b］內(nèi)成立，則不等式G＞0成立，return 1，算法結(jié)束；

ⅱ）若單變量多項式不等式-T_max（n，f）≥0在（a，b］內(nèi)成立，則不等式G＜0成立，return-1，算法結(jié)束；

ⅲ）若T_max（n，f）＞0和T_min（n，f）＜0在（a，b］內(nèi)均不成立，則G與0無固定大小關(guān)系return 0，算法結(jié)束；

（3）n←n+1，轉(zhuǎn)（2）.

END.

定理1.1G（y）=HOM（f（x，y）），若f（x，y）為無重因子的二元有理多項式，則算法

1.1必然終止.

證明若G（y）＞0或G（y）＜0在某區(qū)間（a，b］（其中（a，b］?（0，1］）成立，則由引理

1.13和推論1.2知算法終止；

若G（y）＞0和G（y）＜0均不成立，由引理1.13知G（y）≧0和G（y）≦0也均不成立，所以存在y1、y2∈（a，b］，使得G（y1）＜0，G（y2）＞0，由引理1.10和1.11知存在n1和n2，使得T_max（n1，f）（y1）≦0，T_min（n2，f）（y2）≧0，則算法在n0=max｛n1，n2｝步循環(huán)必然終止.此時G（y1）＜T_max（n0，f）（y1）≦T_max（n1，f）（y1）≦0，G（y2）＞T_min（n0，f）（y2）≧T_max（n1，f）（y1）≧0，即G（y）與0在（a，b］內(nèi)無固定大小關(guān)系.

下一章的討論還需要判定反正切函數(shù)多項式在某一有理點的正負性.

推論1.4若f（x，y）是有理多項式，則G（y）=f（2*arctan（y），y））在（0，1］內(nèi)的任意一有理點的正負性可判斷.

證明令f（x，y）=f1（x，y）*f2（x）*f3（y），其中f1（x，y）的每個因式都是規(guī)范的，設(shè)有理數(shù)y0∈（0，1］.

由推論1.3知G1（y0）=f1（x0，y0）≠0，由引理1.3，arctan（y0）必為超越數(shù)，從而G2（y0）=f2（x0）≠0.

若y0是一元有理多項式f3（y）的零點，則G（y0）=f3（y0）*G1（y0）*G2（y0）=0；若f3（y0）≠0，則G2（y0）≠0，由引理1.10和1.11，若G（y0）＞0則存在n0使得T_min（n0，f）（y0）≥0，若G（y0）＜0則存在n0使得T_max（n0，f）（y0）≤0，對每個自然數(shù)n，T_min（n，f）（y）和T_max（n，f）（y）都是一元有理多項式，在有理點y0的正負性可判斷.

由推論1.4知下面算法可終止.

算法1.2 sign_G##判定函數(shù)G（y）=f（2*arctan（y），y））在（0，1］內(nèi)的有理點的正負性

輸入 有理多項式f（x，y），有理數(shù)y0∈（0，1］；

輸出1（若G（y0）＞0），0（若G（y0）=0），-1（若G（y0）＜0）；

2　正切函數(shù)多項式的實根分離

本節(jié)討論函數(shù)F（x）=（fx，tan（x/2））在區(qū)間（0，/2］內(nèi)的實根分離問題，其中（fx，y）為二元有理多項式.基本步驟如下：首先分離實函數(shù)G（y）=f（2*arctan（y），y）在區(qū)間（0，1］上的實根，再將包含G（y）根的區(qū)間轉(zhuǎn)化為含F(xiàn)（x）根的區(qū)間，同時用二分法使區(qū)間滿足任意給定精度.而分離G（y）=f（2*arctan（y），y）在某區(qū)間（a，b］上的實根的基本思路是：G（y）在（a，b］上恒大于0或恒小于0，則在（a，b］上無實根；否則，若G（y）在（a，b］上單調(diào)，則有唯一實根，若G（y）在（a，b］上不單調(diào)，則用二分法分割區(qū)間，直到每個區(qū)間要么有唯一實根，要么無實根.

判定G（y）的單調(diào)性最有效的辦法就是判定其導(dǎo)數(shù)的正負，G（y）的導(dǎo)數(shù)G′（y）=2*fx′（2*arctan（y），y）/（1+y2）+fy′（2*arctan（y），y），為了去掉分母我們引入偽導(dǎo)數(shù)的概念：

定義2.1稱G′（y）*（1+y2）為反正切函數(shù)多項式G（y）的偽導(dǎo)數(shù)，記Ψ（G）.

反正切函數(shù)多項式的偽導(dǎo)數(shù)還是反正切函數(shù)多項式，并且若Ψ（G）在（0，1］內(nèi)某區(qū)間（a，b］恒大于0或小于0，則G（y）在該區(qū)間單調(diào).

由推論1.3知當(dāng)f（x，y）的每個因式都規(guī)范時，（0，1］內(nèi)的任意一有理點都不是G（y）的根，而下文算法2.1和2.2中所出現(xiàn)的區(qū)間均是以（0，1］為基礎(chǔ)使用二分法產(chǎn)生，即端點為有理數(shù)，都不是G（y）的根，所以在算法中沒有嚴(yán)格區(qū)分開區(qū)間和閉區(qū)間.

下面的算法2.1分離反正切多項式G（y）=f（2*arctan（y），y）在（a，b］上的實根.

算法2.1 myrealroot

輸入 反正切函數(shù)多項式G（y），區(qū)間（a，b］?（0，1］；##a、b為有理數(shù)

輸出 L=｛（an，bn］｝；##（an，bn］互不相交，G（y）在每個（an，bn］內(nèi)有唯一實根，L包含G（y）在（a，b］的全部實根

定理2.1若f（x，y）為無重因子的二元有理多項式，且每個因式每個因式都規(guī)范，則算法2.1必然終止.

證明由引理1.15和引理1.16知G（y）在（0，1］內(nèi)最多只有有限個根且無重根，不妨記G（y）在（0，1］內(nèi)的根為y1、y2、...、ym.令ε1為數(shù)軸上點y1、y2、...ym相互間距離的最小值的1/2，則y1、y2、...、ym的ε1鄰域互不相交；y1、y2、...ym不是G（y）的重根，所以G（y）在點y1、y2、...ym的導(dǎo)數(shù)均不等于0，當(dāng)然偽導(dǎo)數(shù)Ψ（G）也均不等于0，由Ψ（G）的連續(xù)性知存在ε2＞0，在y1、y2、...、ym的ε2鄰域內(nèi)Ψ（G）均不等于0.

記ε=min｛ε1，ε2｝，則在y1、y2、...ym的ε鄰域內(nèi)G（y）有唯一根且其偽導(dǎo)數(shù)恒大于或恒小于0.

取n0=［log2（1/ε）］+1（此處［x］表示不大于x的最大整數(shù)，以下同），則當(dāng)n≧n0時，1/2n＜ε，而對每一個根yi，必然存在自然數(shù)si（0＜si≦2n），使得yi∈（（si-1）/2n，si/2n］，由推論1.3知道yi∈（（si-1）/2n，si/2n），此時（（si-1）/2n，si/2n）?o（yi，ε），即在區(qū)間（（si-1）/2n，si/2n）內(nèi)G（y）有唯一根且其偽導(dǎo)數(shù)恒大于或小于0.

所以算法2.1在不超過n0層遞歸必然終止.

算法2.1能夠輸出一個互不相交的區(qū)間列，在其每個區(qū)間G（y）單調(diào)并有唯一根，且區(qū)間列包含G（y）在（0，1］內(nèi)的全部根，下面還有兩個問題需要解決：①轉(zhuǎn)化為F（x）的根；②精度問題.

引理2.1若f（x，y）為無重因子的二元有理多項式，G（y）=f（2*arctan（y），y）在（0，1］上根的個數(shù)與F（x）=（fx，tan（x/2））在（0，/2］上根的個數(shù)相等.

設(shè)｛（an，bn］｝是算法2.1輸出G（y）在（0，1］上的區(qū)間列，yn為G（y）在（an，bn］上的唯一根，則xn=2*arctan（yn）是F（x）的根，且xn∈（2*arctan（an），2*arctan（bn）］?（2*taylor（arctan（y），2m）（an），2*taylo（rarctan（y），2m-1）（bn）］，令un=2*taylo（rarctan（y），2m）（an），vn=2*taylo（rarctan（y），2m-1）（bn），則F（x）在區(qū)間（un，vn］內(nèi)有根xn，若｛（un，vn］｝還互不相交，由引理2.1知F（x）在區(qū)間（un，vn］內(nèi)有唯一根；因為｛（an，bn］｝互不相交，所以只要每一個（an，bn］對應(yīng)的區(qū)間（un，vn］滿足un≧2*arctan（an），vn≦2*arctan（bn）（或tan（un/2）≦an，tan（vn/2）≦bn），則｛（un，vn］｝也互不相交，由引理2.1知此時｛（un，vn］｝應(yīng)包含F(xiàn)（x）=（fx，tan（x/2））在（0，/2］上的全部根.提高精度的方案還是選擇二分法.

算法2.2 accuracy

輸入：①反正切函數(shù)多項式G（y）；②區(qū)間（a，b］?（0，1］；③精度r；

##G（y）在（a，b］內(nèi)單調(diào)且有唯一根，a、b為有理數(shù)；r＞0

輸出：區(qū)間（c，d］；##①F（x）在（c，d］內(nèi)有唯一根；②tan（c/2）≧a，tan（d/2）≦b；③d-c≦r

定理2.2若f（x，y）為無重因子的二元有理多項式，且每個因式每個因式都規(guī)范，r是任意固定精度，G（y）在（a，b］內(nèi)單調(diào)且有唯一根，a、b為有理數(shù)，則算法2.2必然終止.

證明記算法2.2第n次循環(huán)后變量s、t、u、v、max_a、min_b的值分別為s（n）、t（n）、u（n）、v（n）、max_a（n）、min_b（n）；

令L=b-a，則在n次循環(huán)后區(qū)間（s（n），t（n）］的長度（t（n）-s（n））為L/2n，取n1=［log2（L/tan（r/4））］+1，則當(dāng)n＞n1時，（t（n）-s（n））＜tan（r/4）；

設(shè)y0是G（y）在（a，b］內(nèi)的根，令M=min｛y0-a，b-y0｝，由推論1.3知b≠y0，從而M≠0，再令n2=［log2（L/M）］+1，則當(dāng)n＞n2時，（t（n）-s（n））＜M，此時t（n）-y0＜t（n）-s（n）＜b-y0，所以t（n）＜b，y0-s（n）＜t（n）-s（n）＜y0-a，所以s（n）＞a；

取n3=max｛n1，n2｝+1，則循環(huán)在第n3步時得到的區(qū)間（s（n3），t（n3）］滿足：（1）G（y）在（s（n3），t（n3）］內(nèi)單調(diào)且有唯一根；（2）a＜s（n3）＜t（n3）＜b；（3）（t（n3）-s（n3））＜tan（r/4）；

又因為當(dāng)n→∞時，taylor（arctan，2n）（s（n3））→arctan（s（n3）），所以存在n4，使得當(dāng)n＞n4時，arctan（s（n3））-taylor（arctan，2n）（s（n3））＜min｛r/8，（arctan（s（n3））-arctan（a））/2｝，從而arctan（s（n3））-taylor（arctan，2n）（s（n3））＜r/8（記為①式）以及2*taylor（arctan，2n）（s（n3））＞arctan（s（n3））+arctan（a））（記為②式）；

當(dāng)n→∞時，taylor（arctan，2n-1）（t（n3））→arctan（t（n3）），所以存在n5，使得當(dāng)n＞n5時，taylor（arctan，2n-1）（t（n3））-arctan（t（n3））＜min｛r/8，（arctan（b）-arctan（t（n3）））/2｝，從而taylor（arctan，2n-1）（t（n3））-arctan（t（n3））＜r/8（記為③式）以及2*taylor（arctan，2n-1）（t（n3））＜arctan（b）+arctan（t（n3））（記為④式）；

又因為當(dāng)n→∞時，taylor（arctan，2n-1）（a）→arctan（a），所以存在n6，使得當(dāng)n＞n6時，taylor（arctan，2n-1）（a）-arctan（a）＜（arctan（s（n3））-arctan（a））/2，從而2*taylor（arctan，2n-1）（a）＜arctan（s（n3））+arctan（a）；（記為⑤式）；

當(dāng)n→∞時，taylor（arctan，2n）（b）→arctan（b），存在n7，使得當(dāng)n＞n7時，arctan（b）-taylor（arctan，2n）（b）＜（arctan（b）-arctan（t（n3）））/2，從而2*taylor（arctan，2n）（b）＞arctan（b）+arctan（t（n3））（記為⑥式）；

取n8=max｛n3，n4，n5，n6，n7｝+1，顯然s（n3）≦s（n8），t（n8）≦t（n3），

（v（n8）-u（n8））/2

=taylor（arctan，2n8-1）（t（n8））-taylor（arctan，2n8）（s（n8））

≦taylor（arctan，2n8-1）（t（n3））-taylor（arctan，2n8）（s（n3））

=（taylor（arctan，2n8-1）（t（n3））-arctan（t（n3）））+（arctan（s（n3））-taylor（arctan，2n8）（s（n3）））+（arctan（t（n3））-arctan（s（n3）））

＜r/4+（arctan（t（n3））-arctan（s（n3）））（由①和③得到）

又tan（arctan（t（n3））-arctan（s（n3）））=（t（n3）-s（n3））/（1+t（n3）*s（n3））＜（t（n3）-s（n3））＜tan（r/4），

即arctan（t（n3））-arctan（s（n3））＜r/4，所以（v（n8）-u（n8））/2＜r/2，從而v（n8）-u（n8）＜r.

又由②和⑤可以得到：

u（n8）=2*taylor（arctan，2n8）（s（n8））≧2*taylor（arctan，2n8）（s（n3））＞arctan（s（n3））+arctan（a））＞2*taylor（arctan，2n8-1）（a）=2*max_a（n8）；

由④和⑥可以得到：

v（n8）=2*taylor（arctan，2n8-1）（t（n8））≦2*taylor（arctan，2n8-1）（t（n3））＜arctan（s（n3））+arctan（b）＜2*taylor（arctan，2n8）（b）=2*min_b（n8）.

所以當(dāng)算法2.1中的循環(huán)在第n8步時，變量u和v滿足：（1）v（n8）-u（n8）＜r；（2）u（n8）＞2*max_a（n8），v（n8）＜2*min_b（n8），必然終止.

本節(jié)以上的討論中假定了多項式的每個因式每個因式f（x，y）都規(guī)范，即fy′（x，y）≠0和fx′（x，y）≠0，現(xiàn)對這兩種特殊情況加以分析：若fy′（x，y）=0，hom（f）是x的一元多項式，其求根問題可直接使用成熟的軟件（如MAPLE、DISCOVER等）解決；若fx′（x，y）=0，hom（f）是y的一元多項式，針對此種情況我們設(shè)計了算法2.3來求解.

算法2.3realroot_y

輸入一元有理多項式f（y），精度r；

輸出L=｛（um，vm）｝；##（um，vm）互不相交，f（tan（x/2））在每個（um，vm）內(nèi)有唯一實根，L包含（ftan（x/2））在（0，/2）的全部實根，每個區(qū)間長度小于r

定理2.3算法2.3可終止，且輸出的區(qū)間互不相交.

證明算法2.3可終止等價于步驟（3）對L0中的每個區(qū)間（am，bm）循環(huán)可終止.

對區(qū)間（am，bm），記第n次循環(huán)后變量u、v、max_a、min_b的值分別為u（n）、v（n）、max_a（n）、min_b（n）；

因為當(dāng)n→∞時，taylor（arctan，2n）（am）→arctan（am），所以存在n1當(dāng)n＞n1時，arctan（am）-taylor（arctan，2n）（am）＜min｛r/8，（arctan（am）-arctan（s1））/2｝，從而2*taylor（arctan，2n）（am）＞arctan（am）+arctan（s1）（記為①式）；

因為當(dāng)n→∞時，taylor（arctan，2n-1）（bm）→arctan（bm），所以存在n2當(dāng)n＞n2時，taylor（arctan，2n-1）（bm）-arctan（bm）＜min｛r/8，（arctan（s2）-arctan（bm））/2｝，從而2*taylor（arctan，2n-1）（bm）＜arctan（s2）+arctan（bm）（記為②式）；

因為當(dāng)n→∞時，taylor（arctan，2n-1）（s1）→arctan（s1），所以存在n3當(dāng)n＞n3時，taylor（arctan，2n-1）（s1）-arctan（s1）＜（arctan（am）-arctan（s1））/2，從而2*taylor（arctan，2n-1）（s1）＜arctan（am）+arctan（s1）（記為③式）；

因為當(dāng)n→∞時，taylor（arctan，2n）（s2）→arctan（s2），所以存在n4當(dāng)n＞n4時，arctan（s2）-taylor（arctan，2n）（s2）＜（arctan（s2）-arctan（bm））/2，從而2*taylor（arctan，2n）（s2）＞arctan（s2）+arctan（bm）（記為④式）；

令n5=max｛n1，n2，n3，n4｝+1；

而tan（arctan（bm）-arctan（am））=（bm-am）（/1+bm*am）＜（bm-am）＜r/4，所以arctan（bm）-arctan（am）＜arctan（r/4）＜r/4；

從而（v（n5）-u（n5））/2＜r/2，v（n5）-u（n5）＜r；

由①和③，u（n5）=2*taylor（arctan，2n5）（am）＞arctan（am）+arctan（s1）＞2*taylor（arctan，2n5-1）（s1）=2*max_a（n5）；

由②和④ v（n5）=2*taylor（arctan，2n5-1）（bm）＜arctan（s2）+arctan（bm）＜2*taylor（arctan，2n5）（s2）=2*min_b（n5）.

所以循環(huán)到第n5步必然終止.

所以算法終止.

又對于輸出的區(qū)間列｛（um，vm）｝，um＞2*max_a=taylor（arctan，2n-1）（sep_lst［m］）＞arctan（sep_lst［m］），而vm-1＜2*min_b=taylor（arctan，2n）（sep_lst［m］）＜arctan（sep_lst［m］），即um＞vm-1，（um-1，vm-1）與（um，vm）不相交，也就是說L中的區(qū)間按升序排列且互不相交.

定理2.3成立.

3　三角函數(shù)多項式實根分離與其應(yīng)用實例

f（x，sin（x），cos（x），tan（x））（其中f（t，x，y，z）是有理四元多項式）是常見的三角函數(shù)多項式模型，本節(jié)具體實現(xiàn)其實根的分離.

文獻［13］中的算法可將目標(biāo)函數(shù)轉(zhuǎn)化為f（x，tan（x/2））型正切函數(shù)多項式，對應(yīng)的二元多項式f（x，y）可能是可約的，可先分解因式，去掉重因子，不妨還是記為f（x，y）.剩下的因子可以分為三部分：①只含x的因子，其乘積記為f1（x）；②只含y的因子，其乘積記為f2（y）；③規(guī)范的二元因子，其乘積記為f3（x，y）.即f（x，y）=f1（x）*f2（y）*f3（x，y）.由引理1.5知F1（x）=hom（f1（x））=f1（x）、F2（x）=hom（f2（y））=f2（tan（x/2））、F3（x）=hom（f3（x，y））=f3（x，tan（x/2））相互間無公根.

針對f1（x），可直接使用MAPLE（或其它軟件，如DISCOVER）的realroot（f1（x），r）得到根的區(qū)間列L1；針對f2（y），可使用本文的算法2.3得到區(qū)間列L2；針對f3（x，y），可首先使用本文算法2.1，再調(diào)用算法2.2得到F3（x）的根的區(qū)間列L3.

在以上討論基礎(chǔ)上，我們用MAPLE實現(xiàn)了分離三角函數(shù)多項式實根的“完備”算法tria_realroot.

算法3.1 tria_realroot

輸入 三角函數(shù)多項式F（x）=f（x，sin（x），cos（x），tan（x）），精度r0；##f是有理四元多項式

輸出 互不相交的區(qū)間列L，每一個區(qū)間包含F(xiàn)（x）一個實根，整個列表包含F(xiàn)（x）在（0，/2］的全部實根，且區(qū)間長度可以小于r0；

定理3.1算法3.1必然終止.

證明F1（x）、F2（x）、F3（x）相互間無公根，由引理1.6，F(xiàn)1（x）*F2（x）*F3（x）最多有有限個根，設(shè)ε為其根相互間距離的最小值的1/2，則當(dāng)精度小于ε時，L的區(qū)間必然互不相交.即算法3.1必然終止.

下面舉例描述算法運行過程和效果：

求解過程如下：

（2）運行算法2.1，

算法1.2可以證明函數(shù)G（y）=16 arctan（y）y-2-2y2在（0，1］內(nèi)既不恒大于0也不恒小于0；

G（y）的偽導(dǎo)數(shù)為12y+16 arctan（y）y2+16 arctan（y）-4y3，算法1.2可以證明該函數(shù)在（0，1］內(nèi)恒大于0，所以G（y）在（0，1］內(nèi)有唯一解，即算法2.1輸出區(qū)間列［（0，1，1］］（前兩個數(shù)值表示區(qū)間的左右端點，最后一個數(shù)為1表示函數(shù)在該區(qū)間內(nèi)單調(diào)上升）；

（3）運行算法2.2，結(jié)果如下：

當(dāng)m=1，［s，t］=［0，1/2］，［u，v］=［0，1］，［max_a，min_b］=［0，2/3］；

當(dāng)m=2，［s，t］=［1/4，1/2］，［u，v］=［421441/860160，223/240］，［max_a，min_b］=［0，76/105］；

當(dāng)m=3，［s，t］=［3/8，1/2］，［u，v］=［1186498729839/1653562408960，74783/80640］，［max_a，min_b］=［0，2578/3465］；

當(dāng)m=4，［s，t］=［3/8，7/16］，［u，v］=［63178718862833823/88048891152302080，11951935082 346919849/14490331801064570880］，［max_a，min_b］=［0，33976/45045］；

當(dāng)m=5，［s，t］=［3/8，13/32］［u，v］=［83585951172346396810929/116489387385624870256 640，879340483391699978597928424757/1139388406470395704577076756480］［max_a，min_b］=［0，11064338/14549535］.

若將左右端點的化簡函數(shù)分別記為truncate_left（x，n）和truncate_right（x，n），其中n是整數(shù)的最大長度，則算法2.2中的兩條運算u←2*taylor（arctan，2m）（s）和v←2*taylor（arctan，2m-1）（t）可以優(yōu)化為u←truncate_left（2*taylor（arctan，2m）（s），n）和v←truncate_ right（2*taylor（arctan，2m-1）（t），n），這樣可以保證輸出的結(jié)果同樣滿足①v-u≦r和②tan（u/2）≧a，tan（v/2）≦b的要求.相應(yīng)地，算法2.3也作類似的優(yōu)化.

為描述算法3.1的運行過程和效果，我們隨機產(chǎn)生例3：

（2）若r=1/100，整數(shù)長度為5，則輸出結(jié)果為：

例4求反漸開線函數(shù)的值［17］：漸開線函數(shù)θ=inv（α）=tan（α）-α是機械工程中重要的函數(shù)，其中inv為漸開線involute的縮寫，α是漸開線壓力角，θ是漸開線展角，且α∈［0，/2］，θ∈［0，+∞），漸開線函數(shù)的逆運算稱為反漸開線函數(shù)，即已知θ值，求α的值，記為α=arcinv（θ），求arcinv（θ）有許多成熟的算法，但這些算法一般都是基于迭代法，只能給出其近似值。算法3.1可以輕松計算有理數(shù)的反漸開線函數(shù)值的任意精度區(qū)間，比如當(dāng)精度r=1/10000時，arcinv（1/2）

5　總結(jié)

本文在三角函數(shù)多項式不等式的自動證明算法基礎(chǔ)上，實現(xiàn)了三角函數(shù)多項式實根分離完全算法：可以找出一個互不相交的區(qū)間列，每一個區(qū)間包含一個實根，整個列表包含全部實根，且區(qū)間長度可以達到任意精度.算法簡單易行，十分高效，算法還可以推廣到任意有理倍數(shù)三角函數(shù)f（x，tan（k1x），sin（k2x），cos（k3x））（其中k1、k2、k3為任意有理數(shù)）.特別地，算法可以輕松求解反漸開線函數(shù)，即已知漸開線方程θ=inv（α）=tan（α）-α的θ值，可以求解α的值.

在本文的討論中，我們將F（x）=f（x，tan（x/2））的定義域限定在（0，/2］是因為arctan（y）的taylor展開式在|y|≤1時收斂.針對更一般的任意有理倍數(shù)有理三角函數(shù)多項式（fx，tan（k1x），sin（k2x），cos（k3x））（k1、k2、k3為任意有理數(shù)），根據(jù)文獻［15］知函數(shù)f可以“歸一”到（fx，tan（k0x））模型（其中k0為有理數(shù)），當(dāng)f的定義域滿足k0x（0，/4］時，算法3.1同樣適用。但是，目前算法還只能求出（fx，tan（x/2））在區(qū)間（0，π/2］內(nèi)的根，因為若作類似x=t+k的變量替換后多項式可能會出現(xiàn)超越數(shù)系數(shù)，從而關(guān)于有理三角函數(shù)多項式的性質(zhì)不再成立，算法也就可能不再適用.怎么求出函數(shù)在整個實數(shù)域的全部實根或求解任意系數(shù)三角函數(shù)多項式還是值得進一步研究的課題.

［1］BUCHBERGER B，COLLINSGE.Algebraic method for geometric reasoning［J］.Annual Reviewof Computer Science，1988，3：85.

［2］WU W T.Basic principles of mechanical theorem proving in elementary geometries［J］.Journal of Systems Science and Mathematical Science，1984，4（3）：207.

［3］YANG L，ZHANG J.A practical program of automated proving for a class of geometric inequalities.proceedings ofthe automated deduction in geometry［M］.Berlin：Springer Verlag，2001：41.

［4］楊路，夏壁燦.不等式機器證明與自動發(fā)現(xiàn)［M］.北京：科學(xué)出版社，2008.

［5］陸征一，何碧，羅勇.多項式系統(tǒng)的實根分離算法及其應(yīng)用［M］.北京：科學(xué)出版社，2004.

［6］ACHATZM，MCCALLUMS，WESPFENNINGV.Decidingpolynomial-exponential problems［M］.NewYork：ACMPress，215-222.

［7］徐鳴.程序驗證與系統(tǒng)分析的若干符號計算問題［D］.上海：華東師范大學(xué)，2010.

［8］陳世平.三角函數(shù)不等式的自動證明［J］.四川大學(xué)學(xué)報（自然科學(xué)版），2013，50（3）：537-540.

［9］陳世平，劉忠.Taylor展開式與三角函數(shù)不等式的自動證明［J］.系統(tǒng)科學(xué)與數(shù)學(xué)，已錄用

［10］陳世平，劉忠.三角函數(shù)多項式不等式的自動證明［J］.汕頭大學(xué)學(xué)報（自然科學(xué)版），2015（03）：43-55.

［11］楊路，郁文生.常用基本不等式的機器證明［J］.智能系統(tǒng)學(xué)報，2011，6（5）：377-390.

［12］PARSHIN A N，SHAFAREVIVH I R.Number theory IV：transcendental numbers［M］.北京：科學(xué)出版社，2009.

［13］陳世平，張景中.初等不等式的可讀證明的自動生成［J］.四川大學(xué)學(xué)報（工程科學(xué)版），2003，35（4）：86-93.

［14］陳世平，張景中.三角不等式的自動證明［J］.四川大學(xué)學(xué)報（自然科學(xué)版），2003，40（4）：686-690.

［15］陳世平，劉忠.一類三角形幾何不等式的自動證明［J］.計算機應(yīng)用研究，2012，29（5）：1732-1736.

［16］楊路，姚勇.差分代換矩陣與多項式的非負性判定［J］.系統(tǒng)科學(xué)與數(shù)學(xué)，2009，29（9）：1169-1177.

［17］徐克根.基于級數(shù)方法的反漸開線函數(shù)研究［J］.機械工程師，2010（6）：30-32.

Real Root Isolation of Trigonometric Function Polynomial

CHEN Shiping1，LIU Zhong2
（1.Sichuan Trade School and DeyangBranch of Civil Aviation Flight Universityof China，Deyang618000，Sichuan，China；2.Leshan Vocational TechnologyCollege，Leshan 614000，Sichuan，China）

The real root isolation for non-polynomial functions is discussed.Acomplete algorithm to isolate the real zeros of trigonometric function polynomial is presented，which can output a list of mutually disjoint intervals.Each interval contains only one zero of the generalized polynomial and the list contains all the roots of the polynomial.Furthermore，the length of each interval can be less than any given positive real number.

trigonometric function polynomial；real root isolation；interval list；termination

TP181

A

1001-4217（2016）03-0025-15

2015-09-01

陳世平（1970—），男（漢族），四川省遂寧市人，博士，研究方向：計算機代數(shù)、機器證明.E-mail：chinshiping@sina.com