Quantifier elimination is the process of taking a formula that involves statements of the form "there exists a value for variable $x$ such that..." or "for all values of variable $x$, we have..." (represented with the quantifiers "there exists", or $\exists$, and "for all", or $\forall$, respectively), where the rest of the statement typically involves logical connectives such as "and" or "not" and polynomial formulas, and expressing this as an equivalent statement that does not include such quantifiers but depends only on the other variables that are not quantified over. These formulas are all interpreted over the real domain.

An example is probably in order. The following is known as the Davenport-Heintz problem:

$\exists c\: \left(\forall b\, a\: \left(\left(\left(a \= d \wedge b \= c\right) \vee \left(a\=c \wedge b\=1\right)\right) \Rightarrow a^2\=b\right)\right)$

This can be encoded as follows.

$\mathrm{input} ≔ \&E\left(\left[c\right]\right)\, \&A\left(\left[b\, a\right]\right)\, \left(\left(a\=d\right) \&\mathbf{and} \left(b \= c\right)\right) \&\mathbf{or} \left(\left(a \= c\right) \&\mathbf{and} \left(b \= 1\right)\right) \&\mathbf{implies} \left(a^2 \= b\right)$

The solution is very simple. The QuantifierElimination command is in the SemiAlgebraicSetTools subpackage of RegularChains.

$\mathrm{QuantifierElimination}\left(\mathrm{input}\right)$

It is easy to see by hand that these are indeed solutions to the given problem (with e.g. $c \= 1$ in both cases), but it is not obvious that there are no other solutions.

We can use this functionality to find all cases where the quadratic formula has roots. We get a more legible answer by using some optional arguments to the command:

$R ≔ \mathrm{PolynomialRing}\left(\left[x\, c\, b\, a\right]\right)\:$

$\mathrm{QuantifierElimination}\left(\&E\left(\left[x\right]\right)\, a x^2 \+ b x \+ c \= 0\, R\, \mathrm{output}\=\mathrm{rootof}\right)$

Cylindrical Algebraic Decomposition is a partition of the real, $n$-dimensional space into finitely many connected semi-algebraic subsets, called cells, such that any two cells are cylindrically arranged, that is, their projection onto a lower-dimensional space is either identical or disjoint. Here, a semi-algebraic set is a set given by polynomial equations, inequations, and inequalities.

The CylindricalAlgebraicDecompose command finds such a decomposition where the number of solutions for a given semi-algebraic system stays constant on each cell. A simple example is given as follows:

$R ≔ \mathrm{PolynomialRing}\left(\left[y\, x\right]\right)\:$

$\mathrm{cad} ≔ \mathrm{CylindricalAlgebraicDecompose}\left(\left[x^2 \+ y^2 \le 1\right]\, R\right)$

$\mathrm{Display}\left(\mathrm{cad}\, R\right)$

A more compact output is given with the option $\mathrm{output} \= \mathrm{rootof}$.

$\mathrm{CylindricalAlgebraicDecompose}\left(\left[x^2 \+ y^2 \le 1\right]\, R\, \mathrm{output}\=\mathrm{rootof}\right)$

The $\mathrm{CylindricalAlgebraicDecompose}$ command has been available for a long time. In Maple 2020, it has some new options. One of them is the optimization option. In the simplest form, it is simply a true/false option (with default value true). With this option, Maple tries to reduce the number of cells returned. This example uses the Info command, which returns a list with some information about each cell found; the number of elements of this list is the number of cells.

$F ≔ \left[x^2 \+ y^2 \= 1\, y^2 \= x\right]\:$

$\mathrm{cad\_nonopt} ≔ \mathrm{CylindricalAlgebraicDecompose}\left(F\, R\, \mathrm{optimization} \= \mathrm{false}\right)\:$

$\mathrm{numelems}\left(\mathrm{Info}\left(\mathrm{cad\_nonopt}\, R\right)\right)\;$

$\mathrm{cad\_opt} ≔ \mathrm{CylindricalAlgebraicDecompose}\left(F\, R\, \mathrm{optimization}\=\mathrm{true}\right)\:$

$\mathrm{numelems}\left(\mathrm{Info}\left(\mathrm{cad\_opt}\, R\right)\right)\;$

Another change is that the default algorithm used under the hood has changed. The previous algorithm can still be selected using the method option. The default value for the method option is incremental; the other possible value is recursive. For large systems, the incremental method is typically substantially faster. In this small example, the same difference in speed occurs.

$\mathrm{CodeTools}:-\mathrm{Usage}\left(\mathrm{CylindricalAlgebraicDecompose}\left(F\, R\, \mathrm{method}\=\mathrm{recursive}\right)\right)\:$

$\mathrm{CodeTools}:-\mathrm{Usage}\left(\mathrm{CylindricalAlgebraicDecompose}\left(F\, R\, \mathrm{method}\=\mathrm{incremental}\right)\right)\:$

The new command IntersectionMultiplicity returns the intersection multiplicity of a space curve at every point of that curve defined by a regular chain. This is shown in the following example.

$R ≔ \mathrm{PolynomialRing}\left(\left[x\, y\, z\right]\right)\:$

$F ≔ \left[x^2\+y\+z-1\, y^2\+x\+z-1\, z^2\+x\+y-1\right]\:$

We consider the points of intersection of all three surfaces. First, we compute these as regular chains.

$\mathrm{dec} ≔ \mathrm{Triangularize}\left(F\, R\right)\:$

$\mathrm{Display}\left(\mathrm{dec}\, R\right)\;$

By inspection, these solutions correspond to the points $\left[x\, y\, z\right] \= \left[-1\, -1\, -1\right]\pm \left[\sqrt{2}\,\sqrt{2}\,\sqrt{2}\right]$ (two points), $\left[0\, 0\, 1\right]$, $\left[0\, 1\, 0\right]$, and $\left[1\, 0\, 0\right]$, respectively.

The three surfaces look as follows. We show a larger plot that includes all intersection points of all three surfaces, and two close ups: one of the point $\left[-1\+\sqrt{2}\,-1\+\sqrt{2}\,-1\+\sqrt{2}\right]$ and one of the point $\left[0\, 0\, 1\right]$.

We see that in the second close up, the pairwise intersection curves appear to be locally tangent, which is not the case in the first close up. This is confirmed by the $\mathrm{IntersectionMultiplicity}$ command.

$\mathrm{map}\left(\mathrm{IntersectionMultiplicity}\, \mathrm{dec}\, F\, R\right)$

This confirms that the intersection multiplicity of all points in the first regular chain is 1, whereas it is 2 for the others.

The new command TangentCone computes a tangent cone to a given space curve at a given set of points. Consider the following example.

$R ≔ \mathrm{PolynomialRing}\left(\left[x\, y\, z\right]\right)\:$

$\mathrm{rc} ≔ \mathrm{Chain}\left(\left[z-1\, y\, x\right]\, \mathrm{Empty}\left(R\right)\, R\right)\:$

$\mathrm{rc}$, defined above, represents the point $\left[x\, y\, z\right] \= \left[0\, 0\, 1\right]$.

$F ≔ \left[x^2\+y^2\+z^2-1\, x^2-y^2-z \cdot \left(z-1\right)\right]\:$

We will find the tangent cone to the intersection of the surfaces defined in $F$ at the point defined in $\mathrm{rc}$. First let us examine these surfaces visually.

$\mathrm{solutions} ≔ \mathrm{map}\left(\mathrm{solve}\, F\, z\right)$

We are interested in the first and third solution. We create a plot of these two surfaces, call it $p$, and display it.

We now compute the tangent cone.

$\mathrm{tc} ≔ \mathrm{TangentCone}\left(\mathrm{rc}\, F\, R\, \mathrm{output}\=\'\mathrm{equations}\'\, \left[X\, Y\, Z\right]\right)$

We see that it corresponds to the lines given by $z \= 1$ and $y \= \pm \sqrt{3}\cdot x$. We show this in the same plot.

$\mathrm{lines} ≔ \mathrm{seq}\left(\mathrm{plottools}:-\mathrm{line}\left(\left[-\frac{1}{2 \cdot \sqrt{3}}\, -\frac{s}{2}\,1\right]\, \left[\frac{1}{2 \cdot \sqrt{3}}\,\frac{s}{2}\,1\right]\, \mathrm{color}\=\mathrm{green}\, \mathrm{thickness}\=3\right)\, s \in \left\{-1\, 1\right\}\right)\:$

Another new feature of the $\mathrm{RegularChains}$ library is its ability to determine the geometry of curves specified as the solution set of some equations. In particular, the library can find where the leading coefficients of these equations vanish, and whether the curve is locally real at those points or not. An example follows.

Consider the equations $-y^3\+y^2\+z^5 \=0$ and $x z^4 \+ y^3 - y^2\=0$. The surfaces defined by them look as follows; this is purely for illustration and the method of drawing it won't be explained here. The first equation's surface is rendered in red, the second in blue, and the curve that is their intersection in green. You can also see a transparent black plane at $z\=0$, and the two intersection points of the curve with this plane in black; these are explained below.

If we view the variables as having the order $x\>y\>z$, then the leading coefficients of these equations are 1 and $z^4$, respectively. The first coefficient doesn't vanish; the second vanishes at $z\=0$. The LimitPoints command can find the intersections of the curve, that is, the intersection of the red and blue surfaces. By default, this computation is done over the complex numbers.

$\mathrm{p1} ≔ -y^3 \+ y^2 \+z^5\:$ 

$\mathrm{p2} ≔ x z^4 \+ y^3 - y^2\:$ 

$R ≔ \mathrm{PolynomialRing}\left(\left[x\,y\,z\right]\right)\:$

$\mathrm{rc} ≔ \mathrm{Chain}\left(\left[\mathrm{p1}\, \mathrm{p2}\right]\, \mathrm{Empty}\left(R\right)\, R\right)\:$

$\mathrm{Display}\left(\mathrm{LimitPoints}\left(\mathrm{rc}\, R\right)\, R\right)$

We see that there are two such limit points. Indeed, if we evaluate the polynomials defining the equations at these points, they vanish. These are the two points shown in the graph above.

$\genfrac{}{}{0ex}{}{\left[\mathrm{p1}\, \mathrm{p2}\right]}{\phantom{y}}|\genfrac{}{}{0ex}{}{\phantom{x}}{\left\{x\=0\, y\=0\, z\=0\right\}}$

$\genfrac{}{}{0ex}{}{\left[\mathrm{p1}\, \mathrm{p2}\right]}{\phantom{y}}|\genfrac{}{}{0ex}{}{\phantom{x}}{\left\{x\=0\, y\=1\, z\=0\right\}}$

It looks like there is a cusp at the origin: the curve is not smooth there. We can confirm that this is indeed the case:

$\mathrm{Display}\left(\mathrm{LimitPoints}\left(\mathrm{rc}\, R\, \mathrm{coefficient}\=\mathrm{real}\right)\, R\right)$

By using the $\mathrm{coefficient}\=\mathrm{real}$option, we include only points where the curve is locally smooth in real space: where it locally has a Puiseux series with real coefficients. This computation uses the underlying command RegularChainBranches, which returns a truncated Puiseux series at each of these points for all branches.

$\mathrm{rbs} ≔ \mathrm{RegularChainBranches}\left(\mathrm{rc}\, R\, \left[z\right]\right)\:$

$\mathrm{map}\left(\mathrm{print}\, \mathrm{rbs}\right)\:$

The first two results each contain a $\mathrm{RootOf}$ function which represents $I$ (or $-I$). We see that they have nonreal coefficients.

The last result is a truncated Puiseux series with only real coefficients. One might wonder if there are later terms of this series that have nonreal coefficients; but the algorithm used guarantees that this is not the case. The $\mathrm{RegularChainBranches}$ command can be instructed to return only truncated Puiseux series for real branches, as follows:

$\mathrm{real\_branch} ≔ \mathrm{RegularChainBranches}\left(\mathrm{rc}\, R\, \left[z\right]\, \mathrm{coefficient}\=\mathrm{real}\right)$

When we examine it in the plot, we can see that this is locally a good approximation to the intersection curve for real values of the parameter, but the other two branches are not. Indeed, the $z$-component of the curve is nonnegative, whereas the curve is present only for $z \le 0$. When we re-parametrize these nonreal branches by the change of variables $\mathrm{\_T} \= I T$, we get the following. (The call to $\mathrm{convert}\/\mathrm{radical}$ converts the $\mathrm{RootOf}$ function into $I$.)

$\mathrm{complex\_branches} ≔ \mathrm{convert}\left(\mathrm{eval}\left(\mathrm{rbs}\left[1..2\right]\, \mathrm{\_T} \= I T\right)\, \mathrm{radical}\right)\:$

$\mathrm{map}\left(\mathrm{print}\, \mathrm{complex\_branches}\right)\:$

Now the leading coefficient for each of the coordinates is real. Of course the (truncated) series itself can still not be embedded in real space, but we will be able to examine its real part, which should approximate the series well for small values of $T$. Below, this real part of the truncated Puiseux series is shown in purple and the real truncated Puiseux series in pink.