Are there classes of functions f(x) (from R to R, or, more generally from R[sup]n[/sup] to R) for which it is possible to determine whether
f(x) = 0
has any real solutions without having to figure out what the solutions are?
e.g. if f(x) is a polynomial, can we figure out if it has any real roots without having to figure out the roots themselves?
For example, if f(x) is an odd-order polynomial, we know that f(x) = 0 always has at least one real root, without having to know anything about the value of the roots.
What about even-order polynomials? Is there a test we can perform on the coefficients of the polynomial to determine if f(x) = 0 has any real roots?
What about multinomials?
And, in the more general case, are there classes of functions for which we can “easily” check for the existence of real roots?
Descartes’ Rule of Signs can give you some information about the number of real roots. It can sometimes be used to show that there must be one, but not always. This Wikipedia page has a link to the article on Sturm’s Theorem, which is more complicated but more informative.
Of course, there’s always the Intermediate Value Theorem: If you can find a and b for which f(a) and f(b) have opposite signs, and f(x) is continuous on [a, b], f(x)=0 must have at least one real root between a and b.
It certainly is possible to determine for any polynomial with real coefficients whether it has any real roots, using Sturm’s theorem as mentioned above. You may be interested to know an amazing generalization of this result due to Alfred Tarski: one can algorithmically determine the truth value of any first-order statement about the ordered field of reals (that is, statements about real numbers built up using +, -, *, /, <, =, Boolean operations, and “for all” and “there exists” quantifiers), using a technique known as quantifier elimination. In general, this can be a pretty slow process, though: for every finite tower of exponentials 2^(2^(2^…(2^n)…)), Tarski’s particular algorithm takes at least that much time on some input of size n. And though Tarski’s totally impractical algorithm can be improved, it’s known that any quantifier elimination algorithm has worst-case behavior at least doubly exponential.
Of course, for the specific matter of satisfiability of a single polynomial equality, you don’t need all that generality/complexity. Still, it’s pretty amazing that such an algorithm exists. (A simpler proof leads to decision procedure for statements about the (unordered) field of complex numbers, as well. Tarski’s algorithm for the real case has an augmentation of Sturm’s theorem at its core, which can easily be swapped out for the fundamental theorem of algebra to deal with complex numbers instead).
That is precisely the sort of thing I was interested in.
It seems a bit more complex than I thought (finding all the Sturm functions by calculating a series of polynomial quotients), so I wonder how much less computationally complex it is than a straightforward root-finding algorithm.
That is, in a math SW package like Matlab or Mathematica, would it be computationally less complex to just find the roots of the polynomial and see if any are real, or use the Sturm functions to see how many real roots there are?
Maybe for a high-order polynomial, the Sturm function approach is computationally more efficient than using root-finding algorithms.
BTW, I have implemented the Sturm function approach in Matlab, and got it to work. Pretty cool tool. (Maybe I’ll time it versus the built-in root-finding algorithm to see which is faster)
The problem I am trying to solve, i.e. whether there exist real solutions to f(x) = 0, is precisely of the type mentioned above, i.e. an existential problem for a sentence with only existential quantifiers (if I understand the paper correctly)
The issue is, then, how complex is it to calculate the CAD. I’m not a mathematician, but from briefly going over the paper, it seems to me that calculating the CAD of a particular existential problem is not a trivial matter.