Opened 4 years ago

Last modified 3 years ago

#19040 needs_info enhancement

rewrite Expression.__nonzero__()

Reported by: rws Owned by:
Priority: major Milestone: sage-6.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 rws)

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.

Change History (56)

comment:1 follow-up: Changed 4 years ago by vdelecroix

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.

comment:2 in reply to: ↑ 1 Changed 4 years ago by rws

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

comment:3 Changed 4 years ago by rws

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 follow-up: Changed 4 years ago by vdelecroix

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.

comment:5 in reply to: ↑ 4 ; follow-ups: Changed 4 years ago by rws

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(_)
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.

comment:6 in reply to: ↑ 5 Changed 4 years ago by rws

Replying to rws:

It would use #19000

Could. #19000 is not a necessity.

comment:7 in reply to: ↑ 5 Changed 4 years ago by rws

Actually, proving equality would need quantifiers like:

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

comment:8 Changed 4 years ago by rws

  • Description modified (diff)

comment:9 Changed 4 years ago by rws

  • Description modified (diff)

comment:10 Changed 4 years ago by rws

  • Description modified (diff)

comment:11 Changed 4 years ago by rws

  • Description modified (diff)

comment:12 Changed 4 years ago by rws

  • Dependencies set to #18980

comment:13 Changed 4 years ago by rws

  • Branch set to u/rws/defuse_bool_x__0__performance_bomb

comment:14 Changed 4 years ago by rws

  • Authors set to Ralf Stephan
  • Commit set to d94dec443790faf1eb48230edb3ae1dc6c9c6eb6
  • Dependencies #18980 deleted

New commits:

d94dec419040: draft, can't go further without 18980

comment:15 Changed 4 years ago by rws

  • Branch changed from u/rws/defuse_bool_x__0__performance_bomb to u/rws/19040

comment:16 Changed 4 years ago by git

  • Commit changed from d94dec443790faf1eb48230edb3ae1dc6c9c6eb6 to 800ec56b0b930eb8a5b966c5871dc5e76724acb0

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

f52dbd2missing void declaration of Cython function causes unexpected crashes
f67f47f19040 uncovers hidden calls of Expression.__nonzero__, fixed
38e983b19040: handle numerics together with constants
800ec5619040: draft3

comment:17 Changed 4 years ago by rws

  • Description modified (diff)

comment:18 Changed 4 years ago by rws

  • Description modified (diff)

comment:19 Changed 4 years ago by git

  • Commit changed from 800ec56b0b930eb8a5b966c5871dc5e76724acb0 to adab9a7ea45475ab4c95b310280cda2d43848e48

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

7a3a4d219040: infinity handled by Pynac
7c6a8aa19040: contradicts() now uses satisfiable()
0d4e2a119040: prep satisfiable()
d8971edMerge branch 'develop' into t/19040/19040
adab9a719040: draft4

comment:20 Changed 4 years ago by rws

  • Dependencies set to #17984

comment:21 Changed 4 years ago by rws

  • Dependencies changed from #17984 to #19256
  • Summary changed from defuse bool(x!=0) performance bomb to rewrite Expression.__nonzero__()

comment:22 Changed 4 years ago by rws

  • Branch changed from u/rws/19040 to u/rws/19040-1

comment:23 Changed 4 years ago by rws

  • 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 lhs-rhs contains inexact ring elements. This way inclusion in those rings (i.e., pi in CC == True) is always guaranteed as before.


New commits:

5f4ffc019040: draft

comment:24 Changed 4 years ago by vdelecroix

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 4 years ago by rws

  • Branch changed from u/rws/19040-1 to u/rws/19040-2

comment:26 Changed 4 years ago by rws

  • Commit changed from 5f4ffc0b8929f971c649339ce451189ce6d8698d to fdd148a50b31610942b21f34d36facfff892246e
  • Status changed from new to needs_review

This should be it. Please review.


New commits:

fd2e72319040: core of rewrite Expression.__nonzero__()
5a0c829code changes in consequence of 19040
fdd148a19040: doctest changes

comment:27 Changed 4 years ago by rws

  • Description modified (diff)

comment:28 Changed 4 years ago by rws

  • Description modified (diff)

comment:29 Changed 4 years ago by rws

  • Description modified (diff)
  • Status changed from needs_review to needs_work

comment:30 Changed 4 years ago by git

  • Commit changed from fdd148a50b31610942b21f34d36facfff892246e to ba8824e7c84d81f87bb3969bb831003057c48fbd

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

f30fe23Merge branch 'develop' into t/19040/19040-2
ba8824e19040: add dedicated is_zero()

comment:31 Changed 4 years ago by rws

  • Description modified (diff)
  • Status changed from needs_work to needs_review

comment:32 Changed 4 years ago by git

  • Commit changed from ba8824e7c84d81f87bb3969bb831003057c48fbd to 595080cb5297e6d66471137c9d438b97a4f01c3e

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

857dc9c19040: add dedicated is_zero()
595080cMerge branch 'u/rws/19040-2' of trac.sagemath.org:sage into t/19040/19040-2

comment:33 Changed 4 years ago by rws

  • Status changed from needs_review to needs_work

Patchbot failures in hyperbolic space.

comment:34 follow-up: Changed 4 years ago by rws

  • Authors Ralf Stephan deleted
  • Branch u/rws/19040-2 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 ; follow-up: Changed 4 years ago by jdemeyer

Replying to rws:

This code cannot be separated from #19312

Please explain why.

comment:36 in reply to: ↑ 35 Changed 4 years ago by rws

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 4 years ago by jdemeyer

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).

comment:38 Changed 4 years ago by rws

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.

comment:39 Changed 4 years ago by rws

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

comment:40 Changed 4 years ago by leif

  • Cc leif added

comment:41 follow-up: Changed 3 years ago by vdelecroix

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 3 years ago by vdelecroix

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 ; follow-up: Changed 3 years ago by rws

Replying to vdelecroix:

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.

comment:44 in reply to: ↑ 43 ; follow-up: Changed 3 years ago by vdelecroix

Replying to rws:

Replying to vdelecroix:

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.

Last edited 3 years ago by vdelecroix (previous) (diff)

comment:45 in reply to: ↑ 44 ; follow-up: Changed 3 years ago by 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.

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.

comment:46 in reply to: ↑ 45 Changed 3 years ago by vdelecroix

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 3 years ago by rws

I will upload a fresh branch with this.

comment:48 Changed 3 years ago by behackl

  • Cc behackl added

comment:49 Changed 3 years ago by rws

  • Description modified (diff)

comment:50 in reply to: ↑ 5 Changed 3 years ago by cheuberg

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

comment:51 follow-up: Changed 3 years ago by rws

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

comment:52 in reply to: ↑ 51 ; follow-up: Changed 3 years ago by cheuberg

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

comment:53 in reply to: ↑ 52 Changed 3 years ago by rws

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.

comment:54 Changed 3 years ago by kcrisman

  • Cc kcrisman added

comment:55 Changed 3 years ago by rws

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

comment:56 Changed 3 years ago by eviatarbach

  • Cc eviatarbach added
Note: See TracTickets for help on using tickets.