wrong symbolic results in case the answer is not known

[jakobkroeker]

A failing example is taken from

​http://ask.sagemath.org/question/10388/testing-inequalities-in-sage/

var('a','b')
bool( abs(a+b) <= abs(a) + abs(b) ) # False, expected True or 'Unknown'
assert (not False == bool( abs(a+b) <= abs(a) + abs(b) ) ) #fails

The documentation of bool() says "Returns True when the argument x is true, False otherwise."

Formally this includes returning False in case the answer is unknown and it seems that bool() was specified to behave like it does. But I find that is very unfortunate and even improving the documentation (explicitly mention the 'answer is unknown' case) is not sufficient.

see also discussion at ​https://groups.google.com/d/msg/sage-devel/vNxnHSeRBW4/0OpeL0yv9YUJ

In that thread the exception variant is preferred in case of 'don't know'

Please also take into consideration Tristate variants ( A sandbox for a Tristate class: ​https://github.com/jakobkroeker/Tristate.py )

See also ​https://groups.google.com/forum/?hl=en#!topic/sage-devel/4DUsgt670MA

[eviatarbach]

Thanks for opening this ticket! I think this is a huge problem in Sage symbolics.

I can't remember what I did to change the behaviour so that when a comparison is made and the result can't be determined it raises an exception instead of returning False; I'll try to look into it this weekend.

I like the idea of having a three-valued logic (​https://en.wikipedia.org/wiki/Three-valued_logic); unfortunately Python makes this very difficult, as the Tristate class shows. There does not seem to be an elegant solution, so I wonder if it's not just best to stick with exceptions.

[rws]

I'll gladly do a review of this ticket.

[leif]

Btw., also the coercion framework occasionally leads to "surprising" results (because silently False is returned upon comparison when no coercion can be established, such that for example a == b and a == c doesn't imply b == c). This and similar has been discussed on sage-devel a couple of times.

[rws]

The ticket is about symbolics so let's get concrete. It happens that at the moment I'm implementing more logic affecting comparisons/relations/zero tests of expressions in Pynac. The decision process for the logic in Sage is:

Expression.__nonzero__() is called on input of bool. __nonzero__ is the one that should throw an exception for unknown results. In __nonzero__,

1. first the relations of constants are decided
2. Pynac's relational_to_bool is called (relational::safe_bool()), it does:
   1. relations with one or two infinities; any result gets returned by __nonzero__ right away
   2. if l.h.s - r.h.s is a Python object (other than Expression) compare it to zero, i.e., delegate to the resp. class
   3. else if relation is >= or <= use positive flag of (l.h.s - r.h.s) or its negative to decide (Pynac-0.3.9.3/0.4.3)
3. the previous result may now get changed in case of not-equal; already here Maxima may be called (I think this is wrong, Maxima should always be the last resort)
4. if no assumptions are needed now is time for test_relation which has some detailed logic and uses interval fields to disprove relations ("interval fields never return false positives"); it already has tristate logic by returning NotImplemented if unsure
5. if the previous neither returns True/False return what symbolic/relation.py:test_relation_maxima() returns
   1. the relation is tested and any True is returned immediately
   2. simplification is attempted before returning the final True/False

EDIT: __nonzero__ is not called by Pynac EDIT: add info about upcoming Pynac snippet

[rws]

In ​https://github.com/pynac/pynac/issues/80 we implement multistate for item 2 above. The Sage part raises a TypeError with text Undecidable relation: ... if Pynac returns undecidable and continues on with item 3/4 in case of not implemented.

[rws]

The second issue this ticket depends on concerns the Maxima interface in item 5. There is e.g.:

sage: from sage.symbolic.relation import test_relation_maxima
sage: test_relation_maxima(I>0)
False

because in Maxima

(%i8) is(%i>0);
(%o8)                               false

so the 'false' result should raise a NotImplementedError in __nonzero__ because Maxima does not distinguish between false, known undecidable, and unknown. This produces hundreds of doctest fails in symbolics alone.

Moreover, trying to snatch this decision functionality from Maxima presupposes an independent assumption framework.

EDIT: I is %i in Maxima

[eviatarbach]

I started doing some work on this. Since Sage already has an Unknown object for representing indeterminate truth values, I thought we could adapt it for use here. Ticket #20920 makes some changes to Unknown to raise an error when attempting to evaluate its truth value with __nonzero__, as well as adding an Undecidable object.

[rws]

Great. See also #19040.