#352 asksign asks redundant question

open
nobody
5
2006-07-07
2003-07-11
Stavros Macrakis
No

assume(a*b>0)
assume(a+b>0)

asksign(a*b) => pos (ok)
asksign(a+b) => pos (ok)

asksign(a*b*(a+b))

Is a b positive,negative, or zero?

But it just answered that correctly!

I *am* surprised, I must say, that it doesn't even get is
(equal(a,0)) => false since a*b>0 immediately gives you
a#0 and b#0. For that matter, assume(not equal
(c*d,0)) *does* get is(equal(c,0)) => false.

By the way, with those facts, you can deduce that a>0
and b>0, but that would be a feature request, not a bug
report.

Transcript below.

(C1) assume(a*b>0,a+b>0);
(D1) [a b > 0, b + a > 0]
(C2) asksign(a*b);
(D2) POS
(C3) asksign(a+b);
(D3) POS
(C4) asksign(a*b*(a+b));
Is a b positive, negative, or zero?
pos;
(D4) POS
(C5) is(equal(a,0));
MACSYMA was unable to evaluate the predicate:
EQUAL(a, 0)
-- an error. Quitting. To debug this try DEBUGMODE
(TRUE);)
(C6) assume(not equal(c*d,0));
(D6) [NOT EQUAL(C d, 0)]
(C7) is(equal(c,0));
(D7) FALSE
(C8) facts();
(D8) [a b > 0, b + a > 0, NOT EQUAL(C, 0), NOT
EQUAL(d, 0)]
<< note how it recorded not equal(c*d,0) >>

Maxima 5.9.0 gcl 2.5.0

Discussion

  • Logged In: YES
    user_id=588346

    Hmm. Further experimentation shows that with assume(a*b):

    asksign(a*b*c) asks the sign of a*b*c, not just c
    asksign(a^2*b) asks the sign of a^2*b

    and most surprisingly

    asksign atan(a*b) asks the sign of atan(a*b), not just a*b.
    This one is actually easy to fix: in sign-oddinc, use sign1
    rather than sign.

    The first two cases can be explained by assuming that it
    doesn't check the sign of the a*b subexpression, since it
    doesn't "notice" it as a subexpression. It's not clear how
    you'd fix that: do you really want sign-mtimes to check all
    2^n-n-2 subproducts of a length-n product to see if they're
    in the database? This will rarely be useful and is expensive.
    Perhaps the database needs to keep a list of "terms included
    in products"....

    There are similar issues with sums. Consider assume
    (m>n,n>0); sign(m-n)=>pos, but sign(m-n+1)=>pnz.

    The original problem can probably be solved by re-checking
    the sign of the product of the odds before returning from
    sign1, but you have to be careful to avoid an infinite
    recursion here.

     
  • Robert Dodier
    Robert Dodier
    2006-07-07

    • labels: --> Lisp Core - Assume