東ロボくんのこと（５）Tarski-Seidenbergの定理

　東ロボくんが答案でその名を挙げていた表題のもの，最も初期のQEの結果ということで，関連した論文の歴史紹介では必ず触れられますが，現在主流のCAD(Cylindrical Algebraic Decomposition)やVS(Virtual Substitution)より複雑で，正直，Tarski(1948), A decision method for elementary algebra and geometry の証明は．．．です．

という訳で，今回はその改良版である Seidenberg(1954), A new decision method for elementary algebra に従う方法をスケッチしてみます．これは一言で言うと

　半代数系版のスツルムの定理の応用

であり，具体的には

・最も内側にある量化子とその束縛変数が消去できれば後は繰り返しなので，その部分の∀は¬∃¬に置き換え，ドモルガン則を適用し，不等号を整理
・分数式は分母の符号で場合を分けて分母を払う
・自由変数を含む主係数も符号で場合を分け
・f≧0はf＝0∨f＞0に，f≠0は-f＞0∨f＞0に置き換え
・選言標準形に直した後，∃を分配する

という処理により，扱う式は

　∃x( f1(p,x)＝0 ∧ … ∧ fm(p,x)＝0 ∧ g1(p,x)＞0 ∧ … ∧ gn(p,x)＞0 )

（pは自由変数の列）としてよく，更にこれは

　∃x( (f1(p,x))^2+…+(fm(p,x))^2＝0 ∧ g1(p,x)＞0 ∧ … ∧ gn(p,x)＞0 )

と等価なので（！），最初から

　∃x( f(p,x)＝0 ∧ g1(p,x)＞0 ∧ … ∧ gn(p,x)＞0 )

を扱えばよい．なお，等式が現れない

　∃x( g1(p,x)＞0 ∧ … ∧ gn(p,x)＞0 )

は
　各不等式の左辺の主係数が正
または
　偶数次の各不等式の左辺の主係数が正，かつ，奇数次の各不等式の左辺の主係数が負
または，各不等式の左辺の積をg(p,x)とおくと，ロールの定理により

　∃x( g_{x}(p,x)＝0 ∧ g1(p,x)＞0 ∧ … ∧ gn(p,x)＞0 )

（g_{x}はgのxについての偏導関数）と等価となる．

という前処理の後，半代数系版のスツルムの定理（f_{x}の代わりにf_{x}とΠ_{k=1}^{n}(gk)^(ek)との積（ek=0,1により2^n通りある）を用いた互除法で，係数が分数式になるところは分母の符号で場合を分けて分母を払うもの）により，実根の個数が0でない符号の全ての組み合わせに対応する場合分けの式を得て，選言を求めればよい．

というものです．

　なお，方程式を含む半代数系を扱うツールはMapleが充実しています．http://d.hatena.ne.jp/ehito/20110619/1308471129