Opened 6 years ago
Last modified 5 years ago
#19040 needs_info enhancement
rewrite Expression.__nonzero__()
Reported by:  rws  Owned by:  

Priority:  major  Milestone:  sage6.9 
Component:  symbolics  Keywords:  
Cc:  leif, behackl, kcrisman, eviatarbach  Merged in:  
Authors:  Reviewers:  
Report Upstream:  N/A  Work issues:  
Branch:  Commit:  
Dependencies:  Stopgaps: 
Description (last modified by )
Symbolic expressions may be part of typeneutral computations, e.g. matrices, polynomials. Developers do not expect proof machinery to crank up when writing if x!=0
, but this is just what happens. So bool(x1!=x2)
should be changed to mean not (x1x2).is_trivial_zero()
for symbolic x
. The ticket should provide a different interface for cases requiring simplification/proof:
bool(rel)
equivalent to(not)(LHSRHS).is_trivial_zero()
for ==,!= ; and for <, >, <=, >= the result follows alpha order of lhs and rhssatisfiable(rel)
attempting simplification/proof, returning(Yes,example)/False/Undefined
solve(rel)
in case ofsatisfiable=Yes
returning the full solution setholds(rel)
, quick alias ofsatisfiable
(later without giving an example)ex.is_zero(simplify=False)
(default) calling the fastbool(ex==0)
ex.is_zero(simplify=True)
attempting simplification/proof by callingex==0
.holds()prove(rel)
showing more or less steps of simplification (which is out of reach for the moment)
This ticket will implement the new behaviour of bool(rel)
and put all other functionality of ex.__nonzero__()
into holds()
and ex.is_zero(simplify=True)
.
See also #19162.
Change History (56)
comment:1 followup: ↓ 2 Changed 6 years ago by
comment:2 in reply to: ↑ 1 Changed 6 years ago by
Replying to vdelecroix:
if not x:
bool(not x)
calls PyObject_IsTrue
which calls Expression.__nonzero__
which atm tries to prove that x
is nonzero
or with
not x
replaced byx.is_zero()
.
This calls PyObject_IsTrue
as well.
So this change would also implies to change all of these in a uniform way.
Right, Expression.__nonzero__
will then call x.is_trivial_zero()
and everyone who wants a proof needs a dfferent method.
comment:3 Changed 6 years ago by
It's not too bad. Catching !=
and ==
in __nonzero__
and comparing trivially yields only a few dozen doctest fails in symbolic
and calculus
, mainly from bool(...)
. No fail in src/doc
.
comment:4 followup: ↓ 5 Changed 6 years ago by
I agree that the change would be actually good (for the reason why you created this ticket).
Thoug, for symbolic expression we want to create equations and check their validity
sage: cos(x)**2 + sin(x)**2 == 1 cos(x) == sin(x) sage: bool(_) True
The above will not be enough anymore. What would be the new way of checking? This needs to be emphasized a lot in the documentation as it is backward incompatible. And I guess it is worth a thread on sagedevel. Not necessarily right now, it is always good to have concrete propositions.
You should also have a look to sage/tests/*
where I am sure some of the things are broken.
comment:5 in reply to: ↑ 4 ; followups: ↓ 6 ↓ 7 ↓ 50 Changed 6 years ago by
Replying to vdelecroix:
Thoug, for symbolic expression we want to create equations and check their validity
sage: cos(x)**2 + sin(x)**2 == 1 cos(x) == sin(x) sage: bool(_) TrueThe above will not be enough anymore. What would be the new way of checking?
sage: satisfiable(_) True
This is a longstanding omission, and it would resolve conceptual problems of #17700. It would use #19000 and, if that finds no solution, Maxima as before. SMT solvers can also give a satisfying x
in case of satisfiability, but no full solution which is the task of solve
.
This needs to be emphasized a lot in the documentation as it is backward incompatible. And I guess it is worth a thread on sagedevel. Not necessarily right now, it is always good to have concrete propositions.
You should also have a look to
sage/tests/*
where I am sure some of the things are broken.
Three fails.
comment:6 in reply to: ↑ 5 Changed 6 years ago by
comment:7 in reply to: ↑ 5 Changed 6 years ago by
Actually, proving equality would need quantifiers like:
sage: satisfiable(_, for_all(x)) True
comment:8 Changed 6 years ago by
 Description modified (diff)
comment:9 Changed 6 years ago by
 Description modified (diff)
comment:10 Changed 6 years ago by
 Description modified (diff)
comment:11 Changed 6 years ago by
 Description modified (diff)
comment:12 Changed 6 years ago by
 Dependencies set to #18980
comment:13 Changed 6 years ago by
 Branch set to u/rws/defuse_bool_x__0__performance_bomb
comment:14 Changed 6 years ago by
 Commit set to d94dec443790faf1eb48230edb3ae1dc6c9c6eb6
 Dependencies #18980 deleted
New commits:
d94dec4  19040: draft, can't go further without 18980

comment:15 Changed 6 years ago by
 Branch changed from u/rws/defuse_bool_x__0__performance_bomb to u/rws/19040
comment:16 Changed 6 years ago by
 Commit changed from d94dec443790faf1eb48230edb3ae1dc6c9c6eb6 to 800ec56b0b930eb8a5b966c5871dc5e76724acb0
comment:17 Changed 6 years ago by
 Description modified (diff)
comment:18 Changed 6 years ago by
 Description modified (diff)
comment:19 Changed 6 years ago by
 Commit changed from 800ec56b0b930eb8a5b966c5871dc5e76724acb0 to adab9a7ea45475ab4c95b310280cda2d43848e48
comment:20 Changed 6 years ago by
 Dependencies set to #17984
comment:21 Changed 6 years ago by
 Dependencies changed from #17984 to #19256
 Summary changed from defuse bool(x!=0) performance bomb to rewrite Expression.__nonzero__()
comment:22 Changed 6 years ago by
 Branch changed from u/rws/19040 to u/rws/190401
comment:23 Changed 6 years ago by
 Commit changed from adab9a7ea45475ab4c95b310280cda2d43848e48 to 5f4ffc0b8929f971c649339ce451189ce6d8698d
 Dependencies #19256 deleted
It may not be possible to get the desired behaviour in the structure/parent.pyx
doctests, so we oblige Parent.__contains__
by throwing an exception if lhsrhs
contains inexact ring elements. This way inclusion in those rings (i.e., pi in CC == True
) is always guaranteed as before.
New commits:
5f4ffc0  19040: draft

comment:24 Changed 6 years ago by
A small remark: From the documentation of the method holds
If Sage knows exactly that the relation is undecidable it will throw an ``AttributeError``.
For one relation there always is an algorithm which is either return True
or return False
. What is not possible is to design an algorithm whose input is an equation and answers the validity of the input. Your sentence makes no sense. A right formulation would be
If Sage does not know if the equation is valid it will throw a ``NotImplementedError``. Note that the validity of equations is an undecidable problem. Hence there will always be instances for which such error is raised.
(AttributeError
makes no sense here).
comment:25 Changed 6 years ago by
 Branch changed from u/rws/190401 to u/rws/190402
comment:26 Changed 6 years ago by
 Commit changed from 5f4ffc0b8929f971c649339ce451189ce6d8698d to fdd148a50b31610942b21f34d36facfff892246e
 Status changed from new to needs_review
comment:27 Changed 6 years ago by
 Description modified (diff)
comment:28 Changed 6 years ago by
 Description modified (diff)
comment:29 Changed 6 years ago by
 Description modified (diff)
 Status changed from needs_review to needs_work
comment:30 Changed 6 years ago by
 Commit changed from fdd148a50b31610942b21f34d36facfff892246e to ba8824e7c84d81f87bb3969bb831003057c48fbd
comment:31 Changed 6 years ago by
 Description modified (diff)
 Status changed from needs_work to needs_review
comment:32 Changed 6 years ago by
 Commit changed from ba8824e7c84d81f87bb3969bb831003057c48fbd to 595080cb5297e6d66471137c9d438b97a4f01c3e
comment:33 Changed 6 years ago by
 Status changed from needs_review to needs_work
Patchbot failures in hyperbolic space.
comment:34 followup: ↓ 35 Changed 6 years ago by
 Branch u/rws/190402 deleted
 Commit 595080cb5297e6d66471137c9d438b97a4f01c3e deleted
 Status changed from needs_work to needs_info
This code cannot be separated from #19312 so I included it there. I'll let this ticket stay here for the description unless someone objects.
comment:35 in reply to: ↑ 34 ; followup: ↓ 36 Changed 6 years ago by
comment:36 in reply to: ↑ 35 Changed 6 years ago by
Replying to jdemeyer:
Replying to rws:
This code cannot be separated from #19312
Please explain why.
Correction: an advanced version of this code cannot be separated from #19312. So, this is already obsolete. If, however, #19312 merge is not in the forseeable future I'll consider presenting this branch for review again.
comment:37 Changed 6 years ago by
comment:38 Changed 6 years ago by
This will make it necessary to implement some (fast) functions from Pynac0.5 in Python to achieve the same result. The two remaining fails are quite demanding.
comment:39 Changed 6 years ago by
comment:40 Changed 6 years ago by
 Cc leif added
comment:41 followup: ↓ 43 Changed 6 years ago by
What would be the difference between the output NotImplemented
and Undecidable
!?
As I already mentioned in comment 24, it makes few sense that satisfiable(expr)
returns Undecidable
. Each formula is either True
or False
. I am here only assuming that mathematics are consistent. Of course satisfiable
can not work for all input and when it can not it should return NotImplemented
. That being said, some formula expr
have no proof of their truthness (from Godel), but then I doubt any computer would actually be able to prove it.
In an ideal world, the function satisfiable(expr)
would return one of:
(True, example)
(False, proof)
NotImplemented
comment:42 Changed 6 years ago by
other remark: If I understand correctly satisfiable
would corresponds to a exists quantifier for all the variables in the formula. While the holds
would correspond to for all. What about something more elaborate such as
for all x, exists y, for all z expr(x,y,z)
comment:43 in reply to: ↑ 41 ; followup: ↓ 44 Changed 6 years ago by
Replying to vdelecroix:
What would be the difference between the output
NotImplemented
andUndecidable
!?As I already mentioned in comment 24, it makes few sense that
satisfiable(expr)
returnsUndecidable
. Each formula is eitherTrue
orFalse
. I am here only assuming that mathematics are consistent. Of coursesatisfiable
can not work for all input and when it can not it should returnNotImplemented
. That being said, some formulaexpr
have no proof of their truthness (from Godel), but then I doubt any computer would actually be able to prove it.
Agreed if we look at equalities. Inequalities can be undecidable if we know one side has no order relation. I don't know if there could be other reasons. I haven't decided yet if __nonzero__
should throw an exception for this.
for all x, exists y, for all z expr(x,y,z)
Such will not be in the first versions.
comment:44 in reply to: ↑ 43 ; followup: ↓ 45 Changed 6 years ago by
Replying to rws:
Replying to vdelecroix:
What would be the difference between the output
NotImplemented
andUndecidable
!?As I already mentioned in comment 24, it makes few sense that
satisfiable(expr)
returnsUndecidable
. Each formula is eitherTrue
orFalse
. I am here only assuming that mathematics are consistent. Of coursesatisfiable
can not work for all input and when it can not it should returnNotImplemented
. That being said, some formulaexpr
have no proof of their truthness (from Godel), but then I doubt any computer would actually be able to prove it.Agreed if we look at equalities. Inequalities can be undecidable if we know one side has no order relation. I don't know if there could be other reasons. I haven't decided yet if
__nonzero__
should throw an exception for this.
What do you mean? Do you have an example of such inequality?
for all x, exists y, for all z expr(x,y,z)
Such will not be in the first versions.
But do you have a syntax in mind for it. It would be cool to not multiply ad libitum the satisfiable
, holds
, etc which are exactly the same thing with a choice of quantifiers.
comment:45 in reply to: ↑ 44 ; followup: ↓ 46 Changed 6 years ago by
Replying to vdelecroix:
Replying to rws:
Agreed if we look at equalities. Inequalities can be undecidable if we know one side has no order relation. I don't know if there could be other reasons. I haven't decided yet if
__nonzero__
should throw an exception for this.What do you mean? Do you have an example of such inequality?
Comparison of real/infinity with complex.
for all x, exists y, for all z expr(x,y,z)
Such will not be in the first versions.
But do you have a syntax in mind for it. It would be cool to not multiply ad libitum the
satisfiable
,holds
, etc which are exactly the same thing with a choice of quantifiers.
No syntax in my mind. There could be precedents in SMTsolvers which could be copied.
comment:46 in reply to: ↑ 45 Changed 6 years ago by
Replying to rws:
Replying to vdelecroix:
Replying to rws:
Agreed if we look at equalities. Inequalities can be undecidable if we know one side has no order relation. I don't know if there could be other reasons. I haven't decided yet if
__nonzero__
should throw an exception for this.What do you mean? Do you have an example of such inequality?
Comparison of real/infinity with complex.
Then I would qualify this as undefined and not undecidable. The latter introduces confusion with the standard notion related to proofs and computability.
comment:47 Changed 5 years ago by
I will upload a fresh branch with this.
comment:48 Changed 5 years ago by
 Cc behackl added
comment:49 Changed 5 years ago by
 Description modified (diff)
comment:50 in reply to: ↑ 5 Changed 5 years ago by
Replying to rws:
You should also have a look to
sage/tests/*
where I am sure some of the things are broken.Three fails.
Which probably means lots of user code being broken, see my experience on sagedevel.
In my opinion, for any change in this area, be it fixing a perceived bug or not, we definitely need a deprecation. We do not need on what user's code relies and sage/tests/*
is in no ways a representative sample (but even some code fails there).
The existing deprecation framework may not be enough: for some time, old and new code should be compared and a warning should be raised if the outcome is different. Users should be able to silence this warning once they have converted their code to the new behaviour; and the sage library should also silence the warning for its own use only. No idea how to implement this nicely, but I see no other option.
comment:51 followup: ↓ 52 Changed 5 years ago by
The easiest way for the user to see if behaviour has changed is to give the command git diff originalversion /path/to/file
and check if doctests were changed. Since the system is huge and users have different needs you either need to do this yourself or Sage automates this by providing some sort of subscription service. Since Sage cannot know which of your changes should be monitored for different behaviour (because there is no distinction between a user adding code and a developer adding code), you would need to initiate this subscription yourself. Anyway, a deprecation message every time bool(relation)
is called is out of the question, much more so for all possible changes to Sage. Also, performance would suffer because of all the checks.
You seem to be of the opinion that there exists a representative sample of tests that covers all eventualities. Needless to say there isn'thowever, Sage development tries to come close with the code coverage tools. I think a good dose of realism can be gathered from, for example https://www.youtube.com/watch?v=VfRVz1iqgKU
comment:52 in reply to: ↑ 51 ; followup: ↓ 53 Changed 5 years ago by
The discussion is perhaps theoretical at this moment because there is no branch attached, so I do not know what will actually change.
Replying to rws:
The easiest way for the user to see if behaviour has changed is to give the command
git diff originalversion /path/to/file
and check if doctests were changed. Since the system is huge and users have different needs you either need to do this yourself or Sage automates this by providing some sort of subscription service.
We are speaking about users, not developers.
The most we could perhaps expect from users is to read wellwritten release notes giving a hint what changed. We do not currently have those.
Since Sage cannot know which of your changes should be monitored for different behaviour (because there is no distinction between a user adding code and a developer adding code), you would need to initiate this subscription yourself. Anyway, a deprecation message every time
bool(relation)
is called is out of the question, much more so for all possible changes to Sage. Also, performance would suffer because of all the checks.
Library code could call a new method or something like that. But it is certainly ugly.
We do have a deprecation policy for much less serious cases: if a method is renamed, we have a oneyear deprecation period; the only harm done is that a user gets a message that a method does no longer exist.
Changing the behaviour of bool(...)
silently leads to different results which might be wrong.
I see the following options:
 Not changing fundamental behaviour.
 Changing fundamental behaviour at some really major release where we support old user code for much longer than usual (compare Python 2/Python 3)
 Some kind of deprecation system
Simply making a fundamental change in a random version (say 7.2) and letting users alone with their old code is not an option for me.
You seem to be of the opinion that there exists a representative sample of tests that covers all eventualities.
Certainly not, I think the contrary.
I was surprised that at some point on this ticket, changed behaviour was caught by tests in src/sage/tests
, given that those tests there seem to be quite random.
comment:53 in reply to: ↑ 52 Changed 5 years ago by
Replying to cheuberg:
The discussion is perhaps theoretical at this moment because there is no branch attached, so I do not know what will actually change.
The branch is not listed in the ticket field but the recent commits are visible in the comments. The branch can be checked out via git trac checkout 19040 branch=u/rws/190402
.
comment:54 Changed 5 years ago by
 Cc kcrisman added
comment:55 Changed 5 years ago by
A good way to contribute to this is to review #16397. Mixed order comparison is part of the branch mentioned above.
comment:56 Changed 5 years ago by
 Cc eviatarbach added
Be careful that in a lot of Sage place there are
or with
not x
replaced byx.is_zero()
.So this change would also implies to change all of these in a uniform way.