qex 原理(その1)

qex は入力を関数 p2t を通して,qe に渡すだけの関数なので,以下は,p2t のお話です.

p2t (rational power to Tarski) とは,有理数乗を含む入力を特称量化することで多項式による系に変換する関数で,その原理は,原始式 A と x の既約分数 a/b 乗とに対して

 A(x^(a/b)) ⇔ ∃y(y=x^(a/b) ∧ A(y)) ⇔ ∃y( (if b is even then y>=0 ∧) y^b=x^a ∧ A(y) )

となる性質であり,この変換後の式を qe に処理させています.

実際の量化を内部コマンド p2em (power to ex, scanmap ver.) で確認してみましょう.

(%i1) p2em(x<sqrt(2));
Evaluation took 0.0600 seconds (0.0600 elapsed) using 1.698 MB.
(%o1) qe([[E,rt1]],(rt1 >= 0) %and (rt1^2 = 2) %and (x < rt1))

次の例では,sqrt(2) の出現は2箇所ですが,束縛変数は rt1 にまとめられています.出現が少ない場合は,出現毎に新たな変数を設ける方が処理が簡潔ですが,式が大きくなると後述のように変数の個数の節減は必須となるので,このようにしました.

(%i2) p2em(x<sqrt(2)/(3^(2/3)-sqrt(2)));
Evaluation took 0.1000 seconds (0.1300 elapsed) using 7.201 MB.
(%o2) qe([[E,rt1],[E,rt2]],
          (rt1 >= 0) %and (rt1^2 = 2) %and (rt2^3 = 9)
                     %and (x < rt1/(rt2-rt1)))

一方,次の例では,変数の個数を減らすには量化を選言全体に施した方が良さそうです.

(%i3) p2em(x<-sqrt(3) %or sqrt(3)<x);
Evaluation took 0.0700 seconds (0.0800 elapsed) using 2.432 MB.
(%o3) (qe([[E,rt1]],(rt1 >= 0) %and (rt1 < x) %and (rt1^2 = 3)))
  %or (qe([[E,rt1]],(rt1 >= 0) %and (rt1^2 = 3) %and (x < -rt1)))
(%i4) qe([],ev(%,eval));
Evaluation took 0.5200 seconds (1.1200 elapsed) using 28.026 MB.
(%o4) x^2-3 > 0

実際,この場合には

(%i5) qe([[E,rt1]],(rt1 >= 0) %and (rt1^2 = 3) %and ((x < -rt1) %or (rt1 < x)));
Evaluation took 0.2900 seconds (0.4700 elapsed) using 19.952 MB.
(%o5) x^2-3 > 0

が得られます.しかし,...

(%i6) p2em(1+sqrt(3)<x %implies 4+2*sqrt(3)<x^2);
Evaluation took 0.0400 seconds (0.0400 elapsed) using 1.239 MB.
(%o6) qe([[E,rt1]],(rt1 >= 0) %and (rt1+1 < x) %and (rt1^2 = 3))
  %implies qe([[E,rt1]],(rt1 >= 0) %and (2*rt1+4 < x^2) %and (rt1^2 = 3))
(%i7) qe([],ev(%,eval));
Evaluation took 0.6100 seconds (1.1800 elapsed) using 28.977 MB.
(%o7) true

に対しては

(%i8) qe([[E,rt1]],(rt1 >= 0) %and (rt1^2 = 2) %and ((rt1+1 < x) %implies (2*rt1+4 < x^2)));
Evaluation took 0.1700 seconds (0.3700 elapsed) using 3.884 MB.
(%o8) (x-1 < 0) %or (x^2-2*x-1 <= 0) %or (x^4-8*x^2+8 > 0)

となり,これは

(%i9) fullall(%);
Evaluation took 0.7300 seconds (1.1000 elapsed) using 31.596 MB.
(%o9) false

のように恒真にはなりません.その理由は,特称量化が否定を潜ると全称量化となることであり,それが生じるか形か否かを判定させるより,各原始式に量化を map する(安易な?)設計になっています.