能動的な簡約
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
コードは少し長いので段階的に公開したいと思います.