能動的な簡約

QEPCAD B,従って,qepmax では

(%i1) qe([[A,x]],(x=1)%eq(x^2+a*x+b=0));
                        2
(%o1)                 (a  - 4 b = 0) %and (b + a + 1 = 0)
(%i2) qe([[A,x]],(x^2+x=1)%implies(x^2+a*x=b^2));
                                4      2      2    2
(%o2)        (a - 1 = 0) %and (b  + a b  - 3 b  - a  + a + 1 = 0)

のように簡約が充分でない(と人間には見える)出力になる場合があります.

ですが,我々は maxima 上なので,solve を用いれば

(%i3) solve(args(%o1));
(%o3)                         [[b = 1, a = - 2]]
(%i4) solve(args(%o2));
(%o4)                 [[b = - 1, a = 1], [b = 1, a = 1]]

とできます.

では,不等式との連言をとってみましょう.

(%i5) qe([[A,x]],(x^2+x=1)%implies(x^2+a*x=b^2))%and(b<0);
                                       4      2      2    2
(%o5)  (a - 1 = 0) %and (b < 0) %and (b  + a b  - 3 b  - a  + a + 1 = 0)
(%i6) solve(args(%));

solve: more equations than unknowns.
Unknowns given :  
[b, a]
Equations given:  
                    4      2      2    2
[a - 1 = 0, b < 0, b  + a b  - 3 b  - a  + a + 1 = 0]
 -- an error. To debug this try: debugmode(true);

もちろんダメです.

ということで,quantifier-free の半代数系に含まれる方程式の次数を下げる(or見易く整理する)関数 nnsolve を作りました.

(%i7) nnsolve(%o1);
(%o7)                    (a + 2 = 0) %and (b - 1 = 0)
(%i8) nnsolve(%o2);
(%o8)           (a - 1 = 0) %and ((b - 1 = 0) %or (b + 1 = 0))
(%i9) nnsolve(%o5);
(%o9)                    (a - 1 = 0) %and (b + 1 = 0)
(%i10) qe([],((x^2-1)*(x^2-4)>0)%and(y^3=y)%and(x<y));
(%o10) (x - 1 < 0) %and (x + 1 # 0) %and (x + 2 # 0)
 %and (((x < 0) %and (x + 1 > 0) %and (y = 0))
 %or ((x + 1 > 0) %and (y - 1 = 0)) %or ((x + 2 < 0) %and (y - 1 = 0))
 %or ((x + 2 < 0) %and (y = 0)) %or ((x + 2 < 0) %and (y + 1 = 0)))
 %and (y - 1 <= 0) %and (y + 1 >= 0)
(%i11) nnsolvexx(%);
(%o11) ((x - 1 < 0) %and (x + 1 > 0) %and (y - 1 = 0))
 %or ((x < 0) %and (x + 1 > 0) %and (y = 0)) %or ((x + 2 < 0) %and (y - 1 = 0))
 %or ((x + 2 < 0) %and (y = 0)) %or ((x + 2 < 0) %and (y + 1 = 0))
(%i12) qe([[A,x],[A,y]],(%o10)%eq(%o11));
(%o12)                                true

コードは少し長いので段階的に公開したいと思います.