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`;;
...
...
...