本日のC.A.D.
複素平面上の 2 つの集合 S，T に対して，集合 { s*t ; s∈S，t∈T }（S，T の積）を求めるのが今回の話題です．この集合に z が属する条件の複素変数での定式化
∃s∃t(z=s*t ∧ s∈S ∧ t∈T) ……… （１）
は，S，T に対して対称ですが，例えば，T が ￢(0∈T) を満たす場合には，原点を中心とする共役反転と相似拡大の合成による T の像と S との共有点の存在条件
∃t(z/t∈S ∧ t∈T) ……… （２）
となり，とくに，S，T がそれぞれ中心 c1，c2，半径 r1(>0)，r2(>0) の円周であり，|c2|≠r2 である場合，（２）は
∃t(|z/t-c1|=r1 ∧ |t-c2|=r2) ≡ ∃t(|z-c1*t|=r1*|t| ∧ |t-c2|=r2)
のように「円周，或いは，直線」と T との共有点の存在条件（或いは，それらの根軸と T との共有点の存在条件）と等価となるので，例えば，i=√{-1}，S={ z ; |z-(3+4*i)|=1 }，T={ z ; |z-(5-6*i)|^2=2 } の場合，実変数 x，y，a，b を z=x+y*i，t=a+b*i として QE したのが次の結果です．
? tst12([ex,ex],[x,y,a,b],and,"(x-(3*a-4*b))^2+(y-(4*a+3*b))^2==a^2+b^2,(a-5)^2+(b+6)^2==2"); *** using Lazard's method (MPP17). [b,2] [a,3] [y,7] [x,12] time = 158 ms. 65 1481(36,42) 15871(386,1068) 972(7966,2008) *** combined adjacent 948 cells. time = 2,841 ms. ? tst12([all,all],[x,y,a,b],(f1,f2,f3)->imp(f1*f2,f3),"(x-(3*a-4*b))^2+(y-(4*a+3*b))^2==a^2+b^2,(a-5)^2+(b+6)^2==2,2005056 - 220896*x + 8908*x^2 - 156*x^3 + x^4 - 11328*y + 624*x*y - 8*x^2*y + 2840*y^2 - 156*x*y^2 + 2*x^2*y^2 - 8*y^3 + y^4 <= 0");Ans(); *** using Lazard's method (MPP17). [b,2] [a,3] [y,7] [x,12] time = 275 ms. 65 1481(36,42) 15871(386,1068) 77633(11846,3624) *** combined adjacent 77632 cells. 1[true,true,true,true] time = 8,134 ms. ? tst12([ex,ex],[x,y,a,b],(f1,f2,f3)->imp(f3,f1*f2),"(x-(3*a-4*b))^2+(y-(4*a+3*b))^2==a^2+b^2,(a-5)^2+(b+6)^2==2,2005056 - 220896*x + 8908*x^2 - 156*x^3 + x^4 - 11328*y + 624*x*y - 8*x^2*y + 2840*y^2 - 156*x*y^2 + 2*x^2*y^2 - 8*y^3 + y^4 <= 0");Ans(); *** using Lazard's method (MPP17). [b,2] [a,3] [y,7] [x,12] time = 134 ms. 65 1481(36,42) 12065(386,1068) 1481(3896,2008) *** combined adjacent 1480 cells. 1[true,true,true,true] time = 2,624 ms.
なお，tst12 には荷が勝ちすぎますが，Mathematica では（１），（２）それぞれの実変数化の等価性が直ちに確認できます．
In[1]:= f1 = Exists[{x1,y1,x2,y2}, x == x1 x2 - y1 y2 && y == x1 y2 + x2 y1 && (x1 - 3)^2 + (y1 - 4)^2 == 1 &&
(x2 - 5)^2 + (y2 + 6)^2 == 2 ];
In[2]:= f2 = Exists[{a,b}, (x - (3 a - 4 b))^2 + (y - (4 a + 3 b))^2 == a^2 + b^2 && (a - 5)^2 + (b + 6)^2 == 2];
In[3]:= g1 = Resolve[f1, Reals];
In[4]:= g2 = Resolve[f2, Reals];
In[5]:= CylindricalDecomposition[Equivalent[g1,g2],{x,y}]//Timing
Out[5]= {7.246666, True}C. W. Brown "Simple CAD Construction and its Applications"
https://www.usna.edu/Users/cs/wcbrown/qepcad/B/examples/EdgeSquareProd/ESP.html
https://github.com/chriswestbrown/tarski/raw/master/interpreter/ex/EdgeSquareProduct.txt
https://github.com/chriswestbrown/tarski/raw/master/interpreter/ex/RectSquareProduct.txt
https://github.com/chriswestbrown/tarski/raw/master/interpreter/ex/CircleCircleProd.txt
