rewrite Expression.__nonzero__()

[rwst]

Symbolic expressions may be part of type-neutral 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 (x1-x2).is_trivial_zero() for symbolic x. The ticket should provide a different interface for cases requiring simplification/proof:

• bool(rel) equivalent to (not)(LHS-RHS).is_trivial_zero() for ==,!= ; and for <, >, <=, >= the result follows alpha order of lhs and rhs
• satisfiable(rel) attempting simplification/proof, returning (Yes,example)/False/Undefined
• solve(rel) in case of satisfiable=Yes returning the full solution set
• holds(rel), quick alias of satisfiable (later without giving an example)
• ex.is_zero(simplify=False) (default) calling the fast bool(ex==0)
• ex.is_zero(simplify=True) attempting simplification/proof by calling ex==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.

CC: @nexttime @behackl @kcrisman @eviatarbach

Component: symbolics

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

[videlec]

comment:1

Be careful that in a lot of Sage place there are

def my_generic_function(x):
    if not x:
        ...
    else:
        ...

or with not x replaced by x.is_zero().

So this change would also implies to change all of these in a uniform way.

[rwst]

comment:2

Replying to @videlec:

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 by x.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.

[rwst]

comment:3

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.

[videlec]

comment:4

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 sage-devel. 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.

[rwst]

comment:5

Replying to @videlec:

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?

sage: satisfiable(_)
True

This is a long-standing 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 sage-devel. 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.

[rwst]

comment:6

Replying to @rwst:

It would use #19000

Could. #19000 is not a necessity.

[rwst]

comment:7

Actually, proving equality would need quantifiers like:

sage: satisfiable(_, for_all(x))
True

[rwst]

Dependencies: #18980

[rwst]

Branch: u/rws/defuse_bool_x__0__performance_bomb

[rwst]

Commit: d94dec4

[rwst]

Author: Ralf Stephan

[rwst]

Changed dependencies from #18980 to none

[rwst]

New commits:

d94dec4

19040: draft, can't go further without 18980

[rwst]

Changed branch from u/rws/defuse_bool_x__0__performance_bomb to u/rws/19040

[sagetrac-git]

Changed commit from d94dec4 to 800ec56

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

f52dbd2	missing void declaration of Cython function causes unexpected crashes
f67f47f	19040 uncovers hidden calls of Expression.__nonzero__, fixed
38e983b	19040: handle numerics together with constants
800ec56	19040: draft3

[sagetrac-git]

Changed commit from 800ec56 to adab9a7

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

7a3a4d2	19040: infinity handled by Pynac
7c6a8aa	19040: contradicts() now uses satisfiable()
0d4e2a1	19040: prep satisfiable()
d8971ed	Merge branch 'develop' into t/19040/19040
adab9a7	19040: draft4

[rwst]

Dependencies: #17984

[rwst]

Changed dependencies from #17984 to #19256

[rwst]

comment:34

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.

[rwst]

Changed branch from u/rws/19040-2 to none

[rwst]

Changed commit from 595080c to none

[rwst]

Changed author from Ralf Stephan to none

[jdemeyer]

comment:35

Replying to @rwst:

This code cannot be separated from #19312

Please explain why.

[rwst]

comment:36

Replying to @jdemeyer:

Replying to @rwst:

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.

[jdemeyer]

comment:37

I would much prefer to separate #19040 from #19312, mainly to make the review easier (reviewing a package upgrade plus a huge number of Sage library changes is difficult).

[rwst]

comment:38

This will make it necessary to implement some (fast) functions from Pynac-0.5 in Python to achieve the same result. The two remaining fails are quite demanding.

[rwst]

comment:39

I succeeded to separate #19040 from #19312, so this branch needs rewrite after #19312 is merged.

[videlec]

comment:41

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

[videlec]

comment:42

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)

[rwst]

comment:43

Replying to @videlec:

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.

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.

[videlec]

comment:44

Replying to @rwst:

Replying to @videlec:

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.

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.

[rwst]

comment:45

Replying to @videlec:

Replying to @rwst:

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 SMT-solvers which could be copied.

[videlec]

comment:46

Replying to @rwst:

Replying to @videlec:

Replying to @rwst:

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.

[rwst]

comment:47

I will upload a fresh branch with this.

[cheuberg]

comment:50

Replying to @rwst:

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 sage-devel.

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.

[rwst]

comment:51

The easiest way for the user to see if behaviour has changed is to give the command git diff original-version /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't---however, 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

[cheuberg]

comment:52

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 @rwst:

The easiest way for the user to see if behaviour has changed is to give the command git diff original-version /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 well-written 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 one-year 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:

1. Not changing fundamental behaviour.
2. Changing fundamental behaviour at some really major release where we support old user code for much longer than usual (compare Python 2/Python 3)
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.

[rwst]

comment:53

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/19040-2.

[rwst]

comment:55

A good way to contribute to this is to review #16397. Mixed order comparison is part of the branch mentioned above.