SOS分解 - ATPとCASのこと

　先に述べたQEの
【２】過程が普通の証明の参考にならない
という性質に関連して，今回は一目瞭然の不等式の証明を提供する「SOS分解」をお話します．
　SOS（sum of squares）分解とは，与えられた多項式を多項式の平方和に分解する「平方完成の親玉」であり，これを実現する手段としては，ある種の固有値問題を解くのが一般的なことから，高次方程式を解かねばならず，答えが近似的になるのですが，近似的な結果から有理係数の結果を得るプログラムも幾つか存在します．
　今回はそのうち，CSDPなどの外部のSDP（半正定値計画法）ツールを必要としない，Macaulay2上のSOS.m2パッケージをご紹介します．
　まずは，コードファイルをダウンロード．
http://control.ee.ethz.ch/~hpeyrl/Projects/SOS/M2_Code/SOS.zip
http://control.ee.ethz.ch/~hpeyrl/Projects/SOS/M2_Code/simpleSDP.m2
http://control.ee.ethz.ch/~hpeyrl/Projects/SOS/M2_Code/LDL.m2
http://control.ee.ethz.ch/~hpeyrl/Projects/SOS/M2_Code/BlkDiag.m2
適当な場所に保存，SOS.zipを展開したら，

M2

としてMacaulay2を起動

Macaulay 2, version 0.9.95
with packages: Classic, Core, Elimination, IntegralClosure, LLLBases,
Parsing, PrimaryDecomposition, SchurRings, TangentCone
i1 :

と表示されたら

installPackage"BlkDiag";
installPackage"LDL";
installPackage"simpleSDP";
installPackage"SOS";
loadPackage"SOS";

と入力すれば準備完了です．
　実装されている主な関数は
getSOS，gindSOS，sumSOS
の３つで，例えば，x^4+2*x^2*y^2+x^3*z+z^4を分解するには

QQ[x,y,z]
f=getSOS(x^4+2*x^2*y^2+x^3*z+z^4)

と入力すると

と出力されます．これは

({p1,...,pm},{c1,...,cm})

の書式で，

c1＊(p1)^2＋…＋cm＊(pm)^2

という分解を表しています．この結果をテキストにするには

toString(f)
({ x ＊ y, x^2+1/2 ＊ x ＊ z-2/5 ＊ z^2, 5/21 ＊ x ＊ z+z^2, x ＊ z},{2/1, 1/1, 21/25, 211/420})

とすればよく，分解の正しさを確認するには

sumSOS(f)

とすれば，平方和を展開したものが出力されます．
　一方

findSOS

は分解に用いるグラム行列などを出力するもので，getSOSはこれを呼び出しています．
　また，getSOSの引数の個数を２にして

QQ[x,a]
(f,g,h)=getSOS(x^4-x^3+a*x+a,{a})

とすると，x^4-x^3+a*x+aがSOS分解できるようなaを用いた分解とそのaの値が，引数の個数を３にして

QQ[x,a]
(f,g,h)=getSOS(x^4-x^3+a*x+a,{a},a)

とすると，同様のaのうち，第３引数の１次関数を最小にするもの用いた分解とそのaの値が出力され，第４引数を

rndTol=>正の整数

のように指定すると，近似値を参照する際の精度を調整出来ます．
　なお，非負値多項式のうち，必ずSOS分解できるのは
・１変数
・２次
・２変数かつ４次
のみで，その他の場合には分解できない例が存在します．例えば

QQ[a,b,c];(f,g)=getSOS(a^2*b^4+a^4*b^2+c^6-3*a^2*b^2*c^2)
...
Gram Matrix is not positive semidefinite
...

となります．しかし

QQ[a,b,c];
(f,g)=getSOS( (a^2+b^2)^2 ＊ (a^2＊b^4+a^4＊b^2+c^6-3＊a^2*b^2＊c^2) )
toString(f,g)

とすれば

({-457/1024*a^4*b-567/1024*a^2*b^3+a^2*b*c^2,
-567/1024*a^3*b^2-457/1024*a*b^4+a*b^2*c^2,
a^2*b^2*c-1/2*a^2*c^3-1/2*b^2*c^3, -a^4*b+a^2*b^3, a^3*b^2-a*b^4,
-1/2*a^3*b*c-1/2*a*b^3*c+a*b*c^3, a^2*c^3-b^2*c^3,
-a^3*b*c+a*b^3*c},{4/1, 4/1, 169/64, 53295/262144, 53295/262144,
87/64, 87/256, 59/256})

factor(sumSOS(f,g))

のように，Hilbertの第１７問題の具体例を確認できます．