品川プリンス
では最初に限定子除去(Quantifier Elimination)の手法を用いてハートの形に見える代数曲線の、xの範囲を求めました。その範囲を表す論理式を手で簡約化した、と書きました。その記事を書いた瞬間、心に引っかかるものがあったのですが、とりあえず記事を書き上げて投稿しました。
そのあと、ehitoさんのブログATPとCASのことを調べてみたらありました。この簡約化を実行してくれる関数が。
(%i1), (%i2)で定義されるnns(f), nnscan(f)は論理式fを簡約化した論理式を出力する関数です。 こちらの記事に載っている定義を使わせて頂きました。
(%i1) nns(f):=
block([cl,L,fk],cl(f,g):=length(f)<=length(g),
if atom(f) then return(f)
elseif op(f)="%and" then
(L:sort(rest(full_listify(powerset(setify(args(f))))),cl),
for k:1 thru length(L) do
(fk:substpart("%and",part(L,k),0),
if qe(,(fk)%implies(f))=true then return(fk)))
elseif op(f)="%or" then
(L:sort(rest(full_listify(powerset(setify(args(f))))),cl),
for k:1 thru length(L) do
(fk:substpart("%or",part(L,k),0),
if qe(,(f)%implies(fk))=true then return(fk)))
else f)$
(%i2) nnscan(f):=scanmap(nns,f)$
(%i3) H:x^6 + 3*x^4*y^2 + 6*x^4*y - 2*x^4 + 3*x^2*y^4 - 2*x^2*y^3 - 6*x^2*y^2 - 6*x^2*y + 3*x^2 + y^6 - 3*y^4 + 3*y^2 - 1 = 0;
$$ \tag{%o3} y^6+3\,x^2\,y^4-3\,y^4-2\,x^2\,y^3+3\,x^4\,y^2-6\,x^2\,y^2+3\,y^2+6\,x^4\,y-6\,x^2\,y+x^6-2\,x^4+3\,x^2-1=0 $$
(%i4) load(qepmax);
$$ \tag{%o4} \verb|/Users/yasube/Programming/qepmax/qepmax.mac| $$
(%i5) HX:qe([[E,y]],H);
$$ \tag{%o5} \left(64\,x^6-219\,x^4+192\,x^2-64\leq 0\right) \wedge \left(\left(64\,x^6-219\,x^4+192\,x^2-64=0\right) \lor \left(\left(x-1\leq 0\right) \wedge \left(x+1\geq 0\right)\right)\right) $$
(%i6) nns(HX);
$$ \tag{%o6} \left(64\,x^6-219\,x^4+192\,x^2-64=0\right) \lor \left(\left(x-1\leq 0\right) \wedge \left(x+1\geq 0\right)\right) $$
素晴らしすぎますね。
