HOL Light - ATPとCASのこと

　SOS分解は，不等式のみではなく，一般の半代数系の全称命題の証明にも利用できます．今回は，その実装例であるHOL Light上のREAL_SOSのご紹介します．
　まず，必要なプログラムをダウンロードしましょう．分解にはcsdpが必要なので

sudo leafpad /etc/apt/sources.list

と開き

deb http://ftp.de.debian.org/debian squeeze main

を追加，保存

sudo apt-get update
sudo apt-get install coinor-csdp

とインストールします．後は本体をダウンロード

wget http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_220.tar.gz
tar xvfz ./hol_light_220.tar.gz
cd ./hol_light
wget http://www.cl.cam.ac.uk/~jrh13/hol-light/Linux/hol.sosa
chmod a+x ./hol.sosa

以上で準備完了

rlwrap ./hol.sosa

とすれば

HOL Light 2.20, built 22 December 2006 on OCaml 3.09.3
　　　　Preloaded with analysis and SOS
　
val it : unit = ()
#

のように起動します．

　このhol.sosaは「OCaml」のインタープリータにhol.mlをロードしたtheorem prover「HOL Light」にさらにsos.ml，analysis.mlをロードしたものを実行ファイルとして保存したもので，長大なmlファイルを毎回ロードせずに済みます．

　まず，HOL Lightでの論理記号は

　~　\/　/\　==>　<=>　!（全称）　?（特称）

そして，実数の扱いでは

　＆ｃ（定数ｃ）　x pow e

であることに注意します．

　導入される主な関数とその挙動は

SOS_CONV `f` ;;
外部SDPツールcsdpを用いて得た近似的な結果から正確なfの有理係数SOS分解を計算．

PURE_SOS `f >= g` ;;
SOS_CONVを直接用いてf≧gを証明．

REAL_SOS `P` ;;
Positivstellensatz（半代数系Pの全称閉包の否定が，SOS分解された多項式をふくむある種の等式の成立と等価であるという性質）によりPの全称閉包を証明．

INT_SOS `P` ;;
REAL_SOSのドメインを整数にしたもの．

SOS_RULE `P`
INT_SOSのドメインを非負整数にしたもの．ただし，
powではなくEXPを用い，定数に＆は不要，DIV，MODが使える．

　幾つか実行して見ましょう．まず，前回の例をSOS分解すると

SOS_CONV `x pow 4 + &2 * x pow 2 * y pow 2 + x pow 3 * z + z pow 4`;;
val it : thm =
|- x pow 4 + &2 * x pow 2 * y pow 2 + x pow 3 * z + z pow 4 =
&2 * (x * y) pow 2 +
&1 / &16 * (&4 * x pow 2 + &2 * x * z + -- &1 * z pow 2) pow 2 +
&1 / &16 * (&2 * x * z + z pow 2) pow 2 +
&7 / &8 * z pow 2 pow 2

のように係数がかなり簡単になります．もちろん

PURE_SOS `x pow 4 + &2 * x pow 2 * y pow 2 + x pow 3 * z + z pow 4 >= &0`;;
val it : thm =
|- x pow 4 + &2 * x pow 2 * y pow 2 + x pow 3 * z + z pow 4 >= &0

です．仮定を付けるなら

# time REAL_SOS `a >= &0 /\ b >= &0 /\ a * b = &1 ==> a pow 2 + b pow 2 >= a + b`;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
csdp warning: Reduced accuracy
Translating proof certificate to HOL
CPU time (user): 0.106659
val it : thm =
|- a >= &0 /\ b >= &0 /\ a * b = &1 ==> a pow 2 + b pow 2 >= a + b

となります．ここでポイントを一つ．Positivstellensatzでは，f＞0をf≠0 /\ f≧0として扱うことから

time REAL_SOS `a > &0 /\ b >= &0 /\ a * b = &1 ==> a pow 2 + b pow 2 >= a + b`;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
csdp warning: Reduced accuracy
Translating proof certificate to HOL
CPU time (user): 0.176655
val it : thm =
|- a > &0 /\ b >= &0 /\ a * b = &1 ==> a pow 2 + b pow 2 >= a + b
# time REAL_SOS `a > &0 /\ b > &0 /\ a * b = &1 ==> a pow 2 + b pow 2 >= a + b`;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
csdp warning: Reduced accuracy
Translating proof certificate to HOL
CPU time (user): 0.81328
val it : thm =
|- a > &0 /\ b > &0 /\ a * b = &1 ==> a pow 2 + b pow 2 >= a + b

のように，＞の利用は負荷になります．