読者です 読者をやめる 読者になる 読者になる

qex 原理(その2)

p2t では abs,max2,min2 も

defrule(powertk2, abs(aa), (aa^2)^(1/2))$
defrule(powertk3, max2(aa,bb), (aa+bb+abs(aa-bb))/2)$
defrule(powertk4, min2(aa,bb), (aa+bb-abs(aa-bb))/2)$

により,冪乗関数に変換して処理しています.流れを例示します.

次の式は恒真です.

(%i1) f:max2(min2(a,b),c)=min2(max2(a,c),max2(b,c));
Evaluation took 0.0000 seconds (0.0000 elapsed) using 560 bytes.
(%o1) max2(min2(a,b),c) = min2(max2(a,c),max2(b,c))

実際

(%i2) qex(f);
Evaluation took 1.9800 seconds (2.7400 elapsed) using 265.126 MB.
(%o2) true

となります.前回同様,量化の具合を見ると

(%i3) p2em(f);
Evaluation took 0.2200 seconds (0.2200 elapsed) using 22.855 MB.
(%o3) qe([[E,rt1],[E,rt2],[E,rt3],[E,rt4],[E,rt5]],
         (rt1 >= 0) %and (rt1^2 = (b-a)^2) %and (rt2 >= 0)
                    %and ((rt2+((-rt1)+b+a)/2+c)/2
                     = ((-rt5)+(rt4+c+b)/2+(rt3+c+a)/2)/2)
                    %and (rt2^2 = (c-((-rt1)+b+a)/2)^2) %and (rt3 >= 0)
                    %and (rt3^2 = (c-a)^2) %and (rt4 >= 0)
                    %and (rt4^2 = (c-b)^2) %and (rt5 >= 0)
                    %and (rt5^2 = ((rt4+c+b)/2-(rt3+c+a)/2)^2))

のように5変数です.

これに至る過程は,まず,powertk4 で,f における min2 を abs で

(%i4) applyb1(f,powertk4);
Evaluation took 0.0000 seconds (0.0000 elapsed) using 88.875 KB.
(%o4) max2(((-abs(b-a))+b+a)/2,c) = ((-abs(max2(b,c)-max2(a,c)))+max2(b,c)+max2(a,c))/2

powertk3 で max2 も abs で

(%i5) applyb1(f,powertk4,powertk3);
Evaluation took 0.0000 seconds (0.0100 elapsed) using 809.602 KB.
(%o5) (abs(c-((-abs(b-a))+b+a)/2)+c+((-abs(b-a))+b+a)/2)/2
  = ((-abs((abs(c-b)+c+b)/2-(abs(c-a)+c+a)/2))
  +(abs(c-b)+c+b)/2+(abs(c-a)+c+a)/2)/2

さらに,powertk2 で abs を sqrt で表し,前回述べた方法で束縛変数に置き換えています.

(%i6) applyb1(f,powertk4,powertk3,powertk2);
Evaluation took 0.0200 seconds (0.0100 elapsed) using 1.960 MB.
(%o6) (sqrt((c-((-sqrt((b-a)^2))+b+a)/2)^2)+c+((-sqrt((b-a)^2))+b+a)/2)/2
  = ((-sqrt(((sqrt((c-b)^2)+c+b)/2-(sqrt((c-a)^2)+c+a)/2)^2))
  +(sqrt((c-b)^2)+c+b)/2+(sqrt((c-a)^2)+c+a)/2)/2

なお,%o6 を見ると,sqrt の出現は8箇所ですが,sqrt((c-a)^2),sqrt((b-a)^2),sqrt((c-b)^2) は2箇所ずつあるので,5変数に納まっています.これが8変数だと

(%i7) p2em(f),p2etype:0;
Evaluation took 0.2800 seconds (0.2900 elapsed) using 30.215 MB.
(%o7) qe([[E,rt1],[E,rt2],[E,rt3],[E,rt4],[E,rt5],[E,rt6],[E,rt7],[E,rt8]],
         (rt1 >= 0) %and (rt1^2 = (b-a)^2) %and (rt2 >= 0)
                    %and (rt2^2 = (b-a)^2) %and (rt3 >= 0)
                    %and ((rt3+((-rt1)+b+a)/2+c)/2
                     = ((-rt8)+(rt5+c+b)/2+(rt4+c+a)/2)/2)
                    %and (rt3^2 = (c-((-rt2)+b+a)/2)^2) %and (rt4 >= 0)
                    %and (rt4^2 = (c-a)^2) %and (rt5 >= 0)
                    %and (rt5^2 = (c-b)^2) %and (rt6 >= 0)
                    %and (rt6^2 = (c-a)^2) %and (rt7 >= 0)
                    %and (rt7^2 = (c-b)^2) %and (rt8 >= 0)
                    %and (rt8^2 = ((rt7+c+b)/2-(rt6+c+a)/2)^2))

となり,これを評価するのは,...