5
$\begingroup$

Does quantifier elimination (by cylindrical decomposition) work for systems of polynomial equations and inequalities where some or all of the variables are complex numbers of unit modulus, rather than being real numbers? If it works in principle - has it been implemented?

Addendum: of course it works in principle, but can it be made to work in practice, i.e., without doubling the number of variables? (Cylindrical decomposition has doubly exponential complexity on the number of variables.)

$\endgroup$
3
  • 3
    $\begingroup$ What is the language in which the quantifier elimination “in $S^1$“ would occur? $\endgroup$
    – user44143
    Commented Jan 19, 2022 at 2:01
  • 1
    $\begingroup$ Good question - I take you are asking about inequalities. Let's say that all inequalities involve norms (which are real). $\endgroup$ Commented Jan 19, 2022 at 10:24
  • 1
    $\begingroup$ So you are looking for quantifier elimination in the structure $(\mathbb{C},+,-,\times,\|,0,1)$, restricted to sentences where each variable is restricted to being either real or of unit norm. The norm allows equivalents for $a\in\mathbb{R}$ (by $a^2=|a|^2$) and $a<b$ (by $b-a=|b-a|$), so it could work. $\endgroup$
    – user44143
    Commented Jan 19, 2022 at 20:54

2 Answers 2

6
$\begingroup$

Um, for each variable $z_k = x_k + iy_k$ we throw in the equation $x_k^2 + y_k^2 = 1$ and rewrite everything in terms of $x_k$ and $y_k$. I am missing something, I think.

$\endgroup$
6
  • 1
    $\begingroup$ Ooops. OTOH, this will be completely unpractical, since it doubles the number of variables. $\endgroup$ Commented Jan 18, 2022 at 21:02
  • 1
    $\begingroup$ ... and cylindrical decomposition has doubly exponential complexity on the number of variables. $\endgroup$ Commented Jan 18, 2022 at 21:03
  • $\begingroup$ Well, yes. But perhaps you might get very very very lucky and thus not have to do any work this way. (Worst case analyses do not necessarily apply to particular cases.) $\endgroup$
    – Sam Nead
    Commented Jan 18, 2022 at 21:04
  • 1
    $\begingroup$ in practice, quantifier elimination is very slow already for 3 or 4 real variables. $\endgroup$ Commented Jan 19, 2022 at 17:40
  • 1
    $\begingroup$ @DimaPasechnik Yes, that's the point. I was dealing with a problem with two variables in $S^1$. I can actually solve it by hand, but I'll come across similar problems, and I was wondering whether they could be solved by barrel-organ. $\endgroup$ Commented Jan 20, 2022 at 11:43
5
$\begingroup$

If your main complexity objective is to keep the number of variables down, you can use a rational parametrization of the circle: for each variable $z_k\in S^1$, introduce a real variable $t_k$ and rewrite everything using the substitution $$z_k=\frac{i-t_k}{i+t_k}=\frac{1-t_k^2}{1+t_k^2}+i\frac{2t_k}{1+t_k^2}.$$ (You will have to deal with $z_k=-1$ somehow.)

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .