maxima

how do maxima facts work? why is a neg minus a pos not a neg, too?


I am a newbie to maxima. I am confused about basic facts in maxima.

% maxima
Maxima 5.46.0 https://maxima.sourceforge.io
using Lisp SBCL 2.3.3
...
(%i1) assume( S >= 0, IS < S );
(%o1)                          [S >= 0, S > IS]
(%i2) asksign( IS - S );
(%o2)                                 neg
(%i3) asksign( IS - S - 1 );
Is S - IS + 1 positive, negative or zero?

if I subtract 1 from a negative number, is the result not supposed to be negative, too?

could someone please explain to me how maxima thinks and how I can convince it to believe the right thing? (this matters in some integrations that I want to perform, where the integration asks me the same silly question.)


Solution

  • Maxima's system for deducing inferences from declared inequalities is not too strong. From what I can tell, the collection of declarations (collectively called "the assume database" in discussions about this stuff) is structured as a tree, and determining the sign of the expression under consideration has something to do with traversing the tree, and perhaps applying some heuristics.

    I say "from what I can tell" because the assume database is widely regarded as one of the more obscure parts of the code base -- no small feat. It works well enough for simple cases, and it is pretty fast, but it is easy to bump into cases which are not handled well.

    The reported behavior might or might not be a bug in the sense that the behavior of the assume stuff is not well specified, but at any rate it is a definite deficiency; I'll post a bug report about it.

    As to how to work around it for now, maybe it's workable to say assume(c < 0) and then substitute c for IS - S throughout. One way to do that is to say subst(IS = c + S, <expr>) -- that has the desired effect on expressions other than literal IS - S.