2011-11-17

9 HOL’s number systems

　今回は，HOL Lightにおける数の体系のお話です．
　これまでも多くの例で扱ってきたhol_typeが:numであり，これは自然数（非負整数）全体の集合でした．同様に，hol.mlのロードだけで利用できる:int，:realは整数，実数全体の集合であり

#use "./Complex/make.ml";;

により導入される:complexは複素数全体の集合です．

■　:numはデフォルトの数のhol_typeで，初期状態では

# type_of`a+b`;;
val it : hol_type = `:num`

であり，所謂，自然数の割り算における

　商　DIV
　余り　MOD

も扱えます．
　:numの元の証明は

# ARITH_RULE `1 + 2 EXP 3 - 4 * 5 DIV 6 = 9`;;
val it : thm = |- 1 + 2 EXP 3 - 4 * 5 DIV 6 = 9

計算は

# NUM_REDUCE_CONV `1 + 2 EXP 3 - 4 * 5 DIV 6`;;
val it : thm = |- 1 + 2 EXP 3 - 4 * 5 DIV 6 = 9

とできますが，cutoff，つまり

# ARITH_RULE `a <= b ==> a - b = 0`;;
val it : thm = |- a <= b ==> a - b = 0
# ARITH_RULE `a-b+b=a`;;
Exception: Failure "linear_ineqs: no contradiction".
# ARITH_RULE `a>=b ==> (a-b)+b=a`;;
val it : thm = |- a >= b ==> a - b + b = a
# NUM_REDUCE_CONV `1-2+2`;;
val it : thm = |- 1 - 2 + 2 = 2

という性質で，-を含んだ:numの元の計算は慎重に進めねばなりません．

■　略した際の数のhol.typeの設定を変えるには

# prioritize_real();;
val it : unit = ()
# type_of`a+b`;;
val it : hol_type = `:real`
# prioritize_int();;
val it : unit = ()
# type_of`a+b`;;
val it : hol_type = `:int`
# prioritize_num();;
val it : unit = ()
# type_of`a+b`;;
val it : hol_type = `:num`

のようにします．勿論，使用時に明示すれば

# prioritize_num();;
val it : unit = ()
# type_of`a+(b:int)`;;
val it : hol_type = `:int`
# type_of`(a:real)+b`;;
val it : hol_type = `:real`

となります．

■　:int，;realでは

# prioritize_int();;
val it : unit = ()
# INT_REDUCE_CONV `&1- &2+ &2`;;
val it : thm = |- &1 - &2 + &2 = &1
# INT_ARITH `&1- &2+ &2= &1`;;
val it : thm = |- &1 - &2 + &2 = &1
# prioritize_real();;
val it : unit = ()
# REAL_RAT_REDUCE_CONV `&0- &2/ &2`;;
val it : thm = |- &0 - &2 / &2 = -- &1
# REAL_ARITH `&0- &2/ &2= -- &1`;;
val it : thm = |- &0 - &2 / &2 = -- &1

のように普通の計算ができるわけですが，各数は，:numからの包含写像&の像なので，左の+-*/=などと結合しないよう，&の前にスペースが必要です．また

　`a`の反数は`-- a`
　指数関数はpow

と記し，絶対値関数absや2変数関数max，minも使えます．

2011-11-17

9.1 Arithmetical decision procedures

■　prover ARITH_RULE(: term -> thm = )の:int版，:real版としてINT_ARITH，REAL_ARITHがあるわけですが，それらの特徴は
・代数的な並び替えなら非線形でも扱える

# INT_ARITH
`!a b a' b' D:int.
(a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
(a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2`;;
val it : thm =
|- !a b a' b' D.
(a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
(a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2

・線形多項式不等式は扱える

# REAL_ARITH `!a b x:real. a >= &2 * x + b <=> x <= ( a - b ) / &2`;;
val it : thm = |- !a b x. a >= &2 * x + b <=> x <= (a - b) / &2
# REAL_ARITH `!x y:real. abs(abs(x) - abs(y)) <= abs(x - y)`;;
val it : thm = |- !x y. abs (abs x - abs y) <= abs (x - y)

・線形多項式方程式は勿論扱える（次の例はPrologIIIのデモで有名になったものですが，HOL Lightは素朴に場合分けるだけなので，あなたよりも低速かも知れません．）

# REAL_ARITH
`!x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
x3 = abs(x2) - x1 /\
x4 = abs(x3) - x2 /\
x5 = abs(x4) - x3 /\
x6 = abs(x5) - x4 /\
x7 = abs(x6) - x5 /\
x8 = abs(x7) - x6 /\
x9 = abs(x8) - x7 /\
x10 = abs(x9) - x8 /\
x11 = abs(x10) - x9
==> x1 = x10 /\ x2 = x11`;;
val it : thm =
|- !x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11.
x3 = abs x2 - x1 /\
x4 = abs x3 - x2 /\
x5 = abs x4 - x3 /\
x6 = abs x5 - x4 /\
x7 = abs x6 - x5 /\
x8 = abs x7 - x6 /\
x9 = abs x8 - x7 /\
x10 = abs x9 - x8 /\
x11 = abs x10 - x9
==> x1 = x10 /\ x2 = x11

といったところです．

■　conversion NUM_REDUCE_CONV，INT_REDUCE_CONV，REAL_RAT_REDUCE_CONVは，theorem |- (引数のterm)=(それを簡約したもの) を返します．

# NUM_REDUCE_CONV `1-1=0`;;
val it : thm = |- 1 - 1 = 0 <=> T
# NUM_REDUCE_CONV `1-1`;;
val it : thm = |- 1 - 1 = 0
# NUM_REDUCE_CONV `1-1=0`;;
val it : thm = |- 1 - 1 = 0 <=> T
# NUM_REDUCE_CONV `a-a`;;
val it : thm = |- a - a = a - a
# NUM_REDUCE_CONV `a-a=0`;;
val it : thm = |- a - a = 0 <=> a - a = 0
# REAL_RAT_REDUCE_CONV `(&2 / &3) pow 100` ;;
val it : thm =
|- (&2 / &3) pow 100 =
&1267650600228229401496703205376 /
&515377520732011331036461129765621272702107522001

■　変数を含む場合には，conversion INT_POLY_CONV，REAL_POLY_CONV を用います．

# INT_POLY_CONV `(&1 + x:int) pow 5` ;;
val it : thm =
  |- (&1 + x) pow 5 =
     x pow 5 + &5 * x pow 4 + &10 * x pow 3 + &10 * x pow 2 + &5 * x + &1

# INT_POLY_CONV `(&1 + x) pow 5` ;;
val it : thm = |- (&1 + x) pow 5 = (&1 + x) pow 5

# REAL_POLY_CONV `(&1 + x) pow 5` ;;
val it : thm =
  |- (&1 + x) pow 5 =
     x pow 5 + &5 * x pow 4 + &10 * x pow 3 + &10 * x pow 2 + &5 * x + &1

# REAL_POLY_CONV `&8 * (a + b + c / &2) pow 3 - &6 * (a + b) * (&2 * b + c) * (c
 + &2 * a)` ;;
val it : thm =
  |- &8 * (a + b + c / &2) pow 3 - &6 * (a + b) * (&2 * b + c) * (c + &2 * a) =
     &8 * a pow 3 + &8 * b pow 3 + c pow 3

2011-11-17

9.2 Nonlinear reasoning

　では，非線形系の自動処理はどの程度実装されているのでしょう？
　まず，変数どうしの積を含む方程式系の評価，つまり，環における prover として，NUM_RING，REAL_RINGがあります（INT_RINGはありませんが，環の構造を提供する関数RINGを用いれば実装可能で，上記の2つはその例です)．

# ARITH_RULE`!a b. a*b=0 <=> a=0 \/ b=0`;;
Exception: Failure "linear_ineqs: no contradiction"
# NUM_RING `!a b c d. a*b*c*d=0 <=> a=0 \/ b=0 \/ c=0 \/ d=0`;;
...
val it : thm =
|- !a b c d. a * b * c * d = 0 <=> a = 0 \/ b = 0 \/ c = 0 \/ d = 0
# REAL_RING `x pow 9 - &3 *x pow 6 + &10 *x pow 4 + &4 * x pow 8- &40 *x pow 5-
&11*x pow 3+ &55*x pow 2+x- &7 = &0 ==> x pow 4+ &4*x pow 3-x pow 2+x- &7 = &0 \
/ x pow 5+x pow 3- &8*x pow 2+ &1 = &0`;;
...
val it : thm =
|- x pow 9 - &3 * x pow 6 +
&10 * x pow 4 +
&4 * x pow 8 - &40 * x pow 5 - &11 * x pow 3 +
&55 * x pow 2 +
x - &7 =
&0
==> x pow 4 + &4 * x pow 3 - x pow 2 + x - &7 = &0 \/
x pow 5 + x pow 3 - &8 * x pow 2 + &1 = &0

　 $\pm\sqrt{2}$ の実装

# REAL_RING `a pow 2 = &2 /\ x pow 2 + a * x + &1 = &0 ==> x pow 4 + &1 = &0`;;
3 basis elements and 0 critical pairs
val it : thm =
|- a pow 2 = &2 /\ x pow 2 + a * x + &1 = &0 ==> x pow 4 + &1 = &0

　一般化された根と係数との関係

# REAL_RING
`(a * x pow 2 + b * x + c = &0) /\
(a * y pow 2 + b * y + c = &0) /\
~(x = y)
==> (a * x * y = c) /\ (a * (x + y) + b = &0)`;;
...
val it : thm =
|- a * x pow 2 + b * x + c = &0 /\ a * y pow 2 + b * y + c = &0 /\ ~(x = y)
==> a * x * y = c /\ a * (x + y) + b = &0

　3次方程式の2次方程式への簡約（Vieta’s substitution）

# REAL_RING
`p = (&3 * a1 - a2 pow 2) / &3 /\
q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\
x = z + a2 / &3 /\
x * w = w pow 2 - p / &3
==> (z pow 3 + a2 * z pow 2 + a1 * z + a0 = &0 <=>
if p = &0 then x pow 3 = q
else (w pow 3) pow 2 - q * (w pow 3) - p pow 3 / &27 = &0)`;;
...
val it : thm =
|- p = (&3 * a1 - a2 pow 2) / &3 /\
q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\
x = z + a2 / &3 /\
x * w = w pow 2 - p / &3
==> (z pow 3 + a2 * z pow 2 + a1 * z + a0 = &0 <=>
(if p = &0
then x pow 3 = q
else w pow 3 pow 2 - q * w pow 3 - p pow 3 / &27 = &0))

　分数式を含む等式の評価には，体に対応した prover REAL_FIELD があります．

# REAL_FIELD `~(&0 = x) /\ ~(-- &1 = x) ==> &1 / x - &1 / (&1 + x) = &1 / (x * (
&1 + x))`;;
...val it : thm =
|- ~(&0 = x) /\ ~(-- &1 = x)
==> &1 / x - &1 / (&1 + x) = &1 / (x * (&1 + x))
# REAL_FIELD `&6=a*b*c /\ &6=a+b+c /\ &7= &3*( a/(b*c) + b/(c*a) + c/(a*b) ) ==>
&1=a \/ &1=b \/ &1=c`;;
...
val it : thm =
|- &6 = a * b * c /\
&6 = a + b + c /\
&7 = &3 * (a / (b * c) + b / (c * a) + c / (a * b))
==> &1 = a \/ &1 = b \/ &1 = c

　高々2次方程式の根の公式

# REAL_FIELD
`s pow 2 = b pow 2 - &4 * a * c
==> (a * x pow 2 + b * x + c = &0 <=>
if a = &0 then
if b = &0 then
if c = &0 then T else F
else x = --c / b
else x = (--b + s) / (&2 * a) \/ x = (--b + --s) / (&2 * a))`;;
...
val it : thm =
|- s pow 2 = b pow 2 - &4 * a * c
==> (a * x pow 2 + b * x + c = &0 <=>
(if a = &0
then if b = &0 then if c = &0 then T else F else x = --c / b
else x = (--b + s) / (&2 * a) \/ x = (--b + --s) / (&2 * a)))

■　とは言うものの，これらのproverは非線形不等式に対しては，甚だ無力です．

# REAL_FIELD `&0 &0

　しかし，semidefinite programming による近似的な結果から rational SOS decomposition を得るパッケージを

#use "Examples/sos.ml";;

とロードすれば，ARITH_RULE，INT_ARITH，REAL_ARITHとそれぞれ同じ係数のクラスに対応した強力なprover SOS_RULE，INT_SOS，REAL_SOSが使えます．

# REAL_SOS `&0<x /\ &0<y ==> &0<x*y`;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
val it : thm = |- &0 < x /\ &0 < y ==> &0 < x * y

　Hardy's inequalityの簡単な場合

# REAL_SOS
`!a1 a2 a3 a4:real.
&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4
==> a1 pow 2 +
((a1 + a2) / &2) pow 2 +
((a1 + a2 + a3) / &3) pow 2 +
((a1 + a2 + a3 + a4) / &4) pow 2
<= &4 * (a1 pow 2 + a2 pow 2 + a3 pow 2 + a4 pow 2)`;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
val it : thm =
|- !a1 a2 a3 a4.
&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4
==> a1 pow 2 +
((a1 + a2) / &2) pow 2 +
((a1 + a2 + a3) / &3) pow 2 +
((a1 + a2 + a3 + a4) / &4) pow 2 <=
&4 * (a1 pow 2 + a2 pow 2 + a3 pow 2 + a4 pow 2)

　Nesbitt's inequalityに少し手を加えたもの

# REAL_SOS
`!a b c:real.
a >= &0 /\ b >= &0 /\ c >= &0
==> &3 / &2 * (b + c) * (a + c) * (a + b) <=
a * (a + c) * (a + b) +
b * (b + c) * (a + b) +
c * (b + c) * (a + c)`;;
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
val it : thm =
|- !a b c.
a >= &0 /\ b >= &0 /\ c >= &0
==> &3 / &2 * (b + c) * (a + c) * (a + b) <=
a * (a + c) * (a + b) +
b * (b + c) * (a + b) +
c * (b + c) * (a + c)

　更に，REAL_FIELDのSOS版である REAL_SOSFIELD は，REAL_FIELDでは扱えなかった不等式を含む系も扱えます．

# REAL_FIELD `&0 &0< &1/x` ;;
2 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
2 basis elements and 1 critical pairs
3 basis elements and 1 critical pairs
3 basis elements and 0 critical pairs
Exception: Failure "linear_ineqs: no contradiction".
# REAL_SOSFIELD `&0 &0< &1/x` ;;
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
val it : thm = |- &0 < x ==> &0 < &1 / x
# REAL_SOSFIELD `&0 a/b + b/a >= &2`;;
2 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
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
Translating proof certificate to HOL
val it : thm = |- &0 < a * b ==> a / b + b / a >= &2

　なお，これらが利用しているSOS分解そのものは

# SOS_CONV `&2 * x pow 4 + &2 * x pow 3 * y - x pow 2 * y pow 2 + &5 * y pow 4`;
;
val it : thm =
|- &2 * x pow 4 + &2 * x pow 3 * y - x pow 2 * y pow 2 + &5 * y pow 4 =
&1 / &2 * (&2 * x pow 2 + x * y + -- &1 * y pow 2) pow 2 +
&1 / &2 * (x * y + y pow 2) pow 2 +
&4 * y pow 2 pow 2

のようなconversionとして実装されており，Positivstellensatz による imples の処理を経ずに，これを不等式の証明に直接用いるproverが PURE_SOS であり，その引数は f>=0，f>0 といった不等式そのものです．

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

　ただし，このSOS分解に基づくproversは，その作動原理から適用が，全称量化された系に限られます．

REAL_SOS `?x. &1=x*x`;;
...
...
...