2
$\begingroup$

Given two expressions A and B involving integers, $\pi$, powers to rational exponents, and cosine, is there a software that determines if A = B? (Previous question asked A > B, but the bottleneck is equality.)

I am aware of the long-standing sum-of-square-roots problem in complexity theory. I am asking if there is a software implementation of a sound algorithm, which may take a long time or even not always terminate. As far as I know, standard math software, even if symbolic, resorts to decimal expansion to determine if A > B; but without mathematical guarantee.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ I'm not sure what you mean by the "(slow) known algorithm". If you know that $A \ne B$, then just use interval arithmetic. The difficulty is getting a bound on how much precision you might need (and whether a reasonable amount suffices), but that's not an obstacle in practice. Just increase the precision if it doesn't suffice, and in practice you'll get an answer with quite reasonable precision. On the other hand, dealing with exact equality is much more algorithmically subtle, and there's no known algorithm that's even guaranteed to terminate at all without assuming Schanuel's conjecture. $\endgroup$
    – Henry Cohn
    Commented Jun 17, 2012 at 14:11
  • $\begingroup$ I do need to decide exact equality. I didn't know about the conjecture you mention, and I am editing my question to clarify. Still, is there a sound algorithm which may work on specific instances? $\endgroup$
    – Manu
    Commented Jun 17, 2012 at 14:32
  • $\begingroup$ You may want to try Wolfram|Alpha. I know that, for at least basic expressions, you can simply ask $f(x)=g(x)?$ and Wolfram|Alpha will output "True" or "False". $\endgroup$
    – Samuel Reid
    Commented Jun 17, 2012 at 18:41
  • 3
    $\begingroup$ Input: cos(0) = cos(0.0000000000000000001) Answer: TRUE ;-) $\endgroup$
    – Manu
    Commented Jun 17, 2012 at 18:46

2 Answers 2

Reset to default
5
$\begingroup$

I believe that what you are looking for is MetiTarski. It is written (in part) by Larry Paulson, principal author of the theorem prover Isabelle.

Note also that Maple has an interval arithmetic package (evalr), which can also be used to show that certain inequalities are true. Maple does not use 'raw' floating point arithmetic to decide exact problems - that would be horribly unsound.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you for the pointers! Could you please elaborate on how to solve such problems in Maple? Maple would be much more convenient for me, as I don't need variables or boolean logic which may make MetiTarski a bit too complicated. $\endgroup$
    – Manu
    Commented Jun 17, 2012 at 14:21
  • 2
    $\begingroup$ For deciding $A>B$, try evalr(Signum(B-A)). This will evaluate the sign of B-A using interval arithmetic. It can return 1, -1 or FAIL. Or you can replace one of the constants in your expression by INTERVAL(c-eps..c+eps) and use evalr directly (but probably still on B-A). You might need to use a high Digits setting for tricky (but solveable) cases. Email me an example if this is not clear enough. $\endgroup$
    – Jacques Carette
    Commented Jun 17, 2012 at 15:30
  • $\begingroup$ I just tried evalr(signum(cos(1/2)^2 + sin(1/2)^2 - 1) and I got FAIL -- even with Digits := 2000; Is there a way to solve exactly this? Do you know if this would work with MetiTarski? My problems are quadratic polynomials in cos/sin in Pi (a/b) for integers a, b. $\endgroup$
    – Manu
    Commented Jun 17, 2012 at 18:17
  • $\begingroup$ I meant Signum, not signum. $\endgroup$
    – Manu
    Commented Jun 17, 2012 at 19:54
  • $\begingroup$ For deciding identities, you need to use entirely different techniques. You cannot verify identities numerically (although you could show they are false that way). $\endgroup$
    – Jacques Carette
    Commented Jun 18, 2012 at 12:15
2
$\begingroup$

In Maple, you might try the probabilistic equivalence-tester testeq. For example:

testeq(407-768*cos(1/5*Pi)-716*cos(1/7*Pi)-364*cos(11/35*Pi)-170*cos(1/35*Pi)+170*cos(6/35*Pi)+364*cos(4/35*Pi)-594*cos(9/35*Pi)+594*cos(16/35*Pi)+692*cos(2/5*Pi)+670*cos(2/35*Pi)+670*cos(12/35*Pi)-440*cos(3/35*Pi)-440*cos(17/35*Pi)+246*cos(8/35*Pi)-246*cos(13/35*Pi)-292*cos(3/7*Pi)+486*cos(2/7*Pi)=0);

true

EDIT: For trigonometric polynomials in rational multiples of $\pi$ with rational coefficients, equality can be checked algebraically. Let $x = \sum_{n=1}^n a_j \cos(b_j \pi/m)$ where $m$, $a_j$ and $b_j$ are integers, $0 \le b_j < 2m$. Then if $\omega=e^{i\pi/m}$ we have $x=\sum_{j=1}^n a_j(\omega^{b_j}+\omega^{−b_j})/2$. So $x=0$ iff the minimal polynomial of $\omega$, which is the cyclotomic polynomial $\Phi_m(z)$, divides $\sum_{j=1}^n a_j (z^{2m+b_j} + z^{2m-b_j})$.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thanks, this looks useful. Is there an implementation of testeq that is always correct but may take a long time? $\endgroup$
    – Manu
    Commented Jun 18, 2012 at 13:41
  • $\begingroup$ testeq is by design probabilistic. If it returns false, it is always correct, if it returns true, there is a very small chance it is wrong. User beware. For certainty, see my comments on my answer. $\endgroup$
    – Jacques Carette
    Commented Jun 18, 2012 at 15:40
  • $\begingroup$ Thanks, but my question still stands. One can obtain a zero-error "testeq" by trying all random choices. Is this available somewhere? Also, I think this all boils down to bounding the distance from 0 of non-zero expressions -- are there bounds available for expressions involving cos/sin and powers? I am aware of Baker's work on logarithmic forms. $\endgroup$
    – Manu
    Commented Jun 19, 2012 at 14:22
  • 1
    $\begingroup$ For trigonometric polynomials in rational multiples of $\pi$ with rational coefficients, equality can be checked algebraically. Let $x = \sum_{j=1}^n a_j \cos(b_j \pi/m)$ where $m$, $a_j$ and $b_j$ are integers, $0 \le b_j < 2 m$. Then if $\omega = e^{i\pi/m}$ we have $x = \sum_{j=1}^n a_j (\omega^{b_j} + \omega^{-b_j})/2$. So $x = 0$ iff the minimal polynomial of $\omega$, which is the cyclotomic polynomial $\Phi_m(z)$, divides $\sum_{j=1}^n a_j (z^{2m+b_j}+z^{2m-b_j})$. $\endgroup$
    – Robert Israel
    Commented Jun 19, 2012 at 15:27
  • $\begingroup$ Thanks! This seems to solve basically what I asked, except I guess you can only handle integer exponents this way? It is also not hard to implement. If you make it an answer I'll accept it. $\endgroup$
    – Manu
    Commented Jun 20, 2012 at 19:03

You must log in to answer this question.

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