品川プリンス

 

 では最初に限定子除去(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;
$$ ag{%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);
$$ ag{%o4} verb|/Users/yasube/Programming/qepmax/qepmax.mac| $$
(%i5) HX:qe([[E,y]],H);
$$ ag{%o5} left(64,x^6-219,x^4+192,x^2-64leq 0 ight) wedge left(left(64,x^6-219,x^4+192,x^2-64=0 ight) lor left(left(x-1leq 0 ight) wedge left(x+1geq 0 ight) ight) ight) $$
(%i6) nns(HX);
$$ ag{%o6} left(64,x^6-219,x^4+192,x^2-64=0 ight) lor left(left(x-1leq 0 ight) wedge left(x+1geq 0 ight) ight) $$

素晴らしすぎますね。