Lazard's method（その１）

1994年（Unpublished manuscript は 1990年）に Daniel Lazard が発表した（https://link.springer.com/chapter/10.1007/978-1-4612-2628-4_29）CAD の構成方法は，一般化された根の重複度を保つ分割によるもので，その projection set（主係数，定数項，判別式，終結式のみ）は，当時知られていた Collins，McCallum，Hong タイプの何れよりも小型でしたが，正当性の証明に不備がありました．

そのため，2001年に発表された，より小型の McCallum-Brown projection がこれまでの標準でしたが，その正しさが保証されているは well-oriented という条件を満たす場合であるため，他の場合には Hong タイプと使い分ける，或いは，別途多項式を追加するといった制約がありました．

しかし，ここ数年，Scott McCallum らによる検証（https://www.researchgate.net/project/Validity-proof-of-Lazards-method-for-CAD-construction）が進み，遂に 2016年7月，Lazard's method の正当性の証明が発表されたのです（https://arxiv.org/abs/1607.00264）．これは非常に大きな進展であり，本年 6 月の MEGA 2017（https://mega2017.inria.fr/files/2017/06/Parusinski.pdf）に続き，9 月の JARCS 2017（http://www.maths.usyd.edu.au/u/laurent/RCSW/）は今回の研究メンバーが主催者に含まれていることもあり，注目しています．

なお，Lazard' method の lifting では，多項式の係数への sample point の代入を拡張し，sample point を根にもつ 1 次式で割り切れる限り割った商に代入したもの，つまり，sample の変数についての multi-index（Lazard valuation）が辞書式順序で最小である 0 でない偏微分係数の 0 でない定数倍（Lazard evaluation）を用います（実装においては，この処理は多項式が消失する場合のみで十分です）．

実行例：d = 0, c = 0 のとき，256*a^2*d^3-128*a*b^2*d^2+(144*a*b*c^2+16*b^4)*d-27*a*c^4-4*b^3*c^2 は消失しますが，上記の処理により，Lazard evaluation -4*b^3（実行例の 72*a*b*d-81*a*c^2-2*b^3 に対応）が得られます．

(%i1) (qvpeds ([all],[d,c,a,b,x],0,l,r11,0 ),
       g1:qe( bfpcad(ext( '(  a*x^4+b*x^2+c*x+d>=0 ) )))  );
Evaluation took 3.6700 seconds (3.6800 elapsed) using 506.869 MB.
(%o1) [[d = root(d,1),c = root(c,1),root(a,1) <= a,
        root(72*a*b*d-81*a*c^2-2*b^3,1) <= b,true],
       [root(d,1) < d,c < root(c,1),root(a,1) <= a,
        root(256*a^2*d^3-128*a*b^2*d^2+(144*a*b*c^2+16*b^4)*d-27*a*c^4
                        -4*b^3*c^2,2)
          <= b,true],
       [root(d,1) < d,c = root(c,1),root(4096*a*d^3+27*c^4,1) <= a,
        root(256*a^2*d^3-128*a*b^2*d^2+(144*a*b*c^2+16*b^4)*d-27*a*c^4
                        -4*b^3*c^2,1)
          <= b,true],
       [root(d,1) < d,root(c,1) < c,root(a,1) <= a,
        root(256*a^2*d^3-128*a*b^2*d^2+(144*a*b*c^2+16*b^4)*d-27*a*c^4
                        -4*b^3*c^2,2)
          <= b,true]]

(%i2) %pp;
Evaluation took 0.0000 seconds (0.0000 elapsed) using 0 bytes.
(%o2) [[d],[c],[a,256*a*d^3-27*c^4,4096*a*d^3+27*c^4],
       [256*a^2*d^3-128*a*b^2*d^2+(144*a*b*c^2+16*b^4)*d-27*a*c^4-4*b^3*c^2],
       [a*x^4+b*x^2+c*x+d]]

(%i3) laz_eval([[],[d=0,c=0,a=-1/2]],%pp[4]);
Evaluation took 0.0000 seconds (0.0100 elapsed) using 368.906 KB.
(%o3) [[b],[4*(72*a*b*d-81*a*c^2-2*b^3)]]

(%i4) qex([],F2G(g1) %eq qex([[A,x]], a*x^4+b*x^2+c*x+d>=0 )  );
Evaluation took 30.2000 seconds (35.1300 elapsed) using 4898.136 MB.
(%o4) true