search

sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.34k stars 452 forks source link

rewrite Expression.__nonzero__() #19040

Open rwst opened 9 years ago

rwst commented 9 years ago

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:

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

rwst commented 8 years ago
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 commented 8 years ago
comment:39

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

videlec commented 8 years ago
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:

videlec commented 8 years ago
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 commented 8 years ago
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 commented 8 years ago
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 commented 8 years ago
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 commented 8 years ago
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 commented 8 years ago
comment:47

I will upload a fresh branch with this.

rwst commented 8 years ago

Description changed:

--- 
+++ 
@@ -1,8 +1,8 @@
 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)` returning `(Yes,example)/No/Undecidable/NotImplemented`
+* `satisfiable(rel)` attempting simplification/proof, returning `(Yes,example)/False/Undefined`
 * `solve(rel)` in case of `satisfiable=Yes` returning the full solution set
-* `holds(rel)` attempting simplification/proof, returning `True`/`False`, throwing `NotImplementedError` 
+* `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)
cheuberg commented 8 years ago
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 commented 8 years ago
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 commented 8 years ago
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 commented 8 years ago
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 commented 8 years ago
comment:55

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