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

等価性

nns,nnss と同じく,qex,solvex の入力と出力とは等価,つまり,変数に任意の実数を代入したとき,それらの true,false は一致します.

例えば,sqrt を含む場合,定義:y=sqrt(x)⇔(y^2=x∧y>=0) により,x<0 のとき,y=sqrt(x) は false ですから,前回の最後の例の入力:[ [x^2=a,x>-1] ],出力:[ [a < 1,x = -sqrt(a)],[x = sqrt(a)] ] の等価性は,a<0 のとき入出力とも false,1<=a のとき出力は [ [false],[x = sqrt(a)] ],つまり,[ [x = sqrt(a)] ] といった具合に確かめられますし,xa 座標平面における入力,出力が表す図形が一致することからも判るでしょう.

システム自身に等価性をチェックさせるには,solvex の実行直後に

(%i36) thischeck();
Evaluation took 1.9700 seconds (3.1300 elapsed) using 117.474 MB.
(%o36) true

とすればよく,入出力は

(%i37) thisin;
Evaluation took 0.0000 seconds (0.0000 elapsed) using 48 bytes.
(%o37) (x > -1) %and (x^2 = a)
(%i38) thisout;
Evaluation took 0.0000 seconds (0.0000 elapsed) using 48 bytes.
(%o38) [[a < 1,x = -sqrt(a)],[x = sqrt(a)]]

のように参照出来ます.