wrong symbolic results in case the answer is not known

[sagetrac-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

Dependencies: pynac-0.3.9.3/-0.4.3

CC: @eviatarbach @sagetrac-tmonteil @slel @videlec

Component: symbolics

Stopgaps: todo

Issue created by migration from https://trac.sagemath.org/ticket/17700

[eviatarbach]

comment:2

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.

[rwst]

comment:3

I'll gladly do a review of this ticket.

[rwst]

Description changed:

--- 
+++ 
@@ -18,6 +18,5 @@
 ( 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
 
-

[sagetrac-jakobkroeker]

Description changed:

--- 
+++ 
@@ -8,6 +8,13 @@
 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
@@ -20,3 +27,6 @@
 
 See also https://groups.google.com/forum/?hl=en#!topic/sage-devel/4DUsgt670MA
 
+
+
+

[nexttime]

comment:6

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.

[rwst]

comment:7

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

[rwst]

comment:8

In pynac/pynac#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.

[rwst]

Dependencies: pynac-0.3.9.3/-0.4.3