I don't know if any of SymPy has been formally proved. That's not very easy to do without a very strict type system that isn't easy to do in Python, and IMHO limits what you can do.
There are algorithms implemented which have been proven correct in the papers that describe them (for example, all the algorithms in the risch algorithm are proven correct), but those are under the assumptions that the input sanitizer is correct, and, probably just as important, that there are no bugs or typos in the implementation of the algorithm. The best thing to do for this is to just have a lot of tests. I think what you're talking about is a little different. You are alluding to a very core limitation of computer algebra, which is that very core algorithms may be undecidable (or more practically, even if they are decidable, a decision procedure is not known or at least not implemented). A very simple and common example of this is zero equivalence. Richardson's theorem states that, for a certain class of functions (which is not that complicated, the functions that SymPy can represent are a superset of these), it is undecidable if a given mathematical expression is identically zero. This is a *huge* issue. Basically, anywhere that some algorithm divides by something, it implicitly assumes that it is not zero. Any result that it obtains may be incorrect if it is (you can Google for "proof that 1 = 0" for many clever examples of this). Sometimes there are no ways around this. We have to just assume that an expression that doesn't look like zero isn't. Other times, we can get around it by changing what our output looks like. For example, integrate(x**y, x) returns Piecewise((log(x), Eq(y, -1)), (x**(y + 1)/(y + 1), True)). This result is always correct, even if y is replaced with an expression that is identically equal to -1, like integrate(x**(-sin(y)**2 - cos(y)**2), x), because in that case, the Piecewise is mathematically the same as Piecewise((log(x), True)) == log(x). So to answer your questions: - Correctness is important. It's better to have no algorithm than an algorithm that is sometimes wrong. - Sometimes you can get around the issue by changing the format of your answer to something that is always right. Piecewise is a good example of this. And to take your limit example, we can just return a Limit() object (I'm not sure why this isn't done; this is how other things like integrate() and summation() handle input it can't deal with). - Another option is to limit yourself to a subset of expressions that you know you can deal with. For example, with the zero equivalence problem, for rational functions in any number of variables you can determine exactly when they are identically zero. This is also true for algebraic functions. I'm not sure if it's true for elementary functions (note that Richardson's theorem doesn't apply to elementary functions because it uses abs(), which is not elementary). Aaron Meurer On Sun, Feb 9, 2014 at 1:31 PM, Harsh Gupta <[email protected]> wrote: > I think we need to have formal policy about including the code which can > potentially give wrong results. > > There can be two cases. > > 1. We don't know what use case leads to wrong to the wrong result but we are > not sure that there won't be any. As Sergey B Kirpichev in the discussion > on > the PR #2723, hack and pray is not a good strategy for maths related > softwares. Other than compulsory test coverage and code review, which are > already doing we can do two things. > > First we can might make it necessary to give a formal proof of the > algorithm used. > This way, given that the implementation is correct, we can be sure that > the > code will give correct output. But the cons are that it can be hard to > turn > up with a formal proof especially if the developer has come up with the > algorithm by himself. > > Second we can ask for a formal description and justification of the > algorithm. This way it will be easier to figure out logical fallacies and > as > a bonus we can add the formal description in the documentation. > > 2. This is the case where we know of certain use cases which give the wrong > result but allowing them helps us solve a larger set of usecases. > > For example while working on evaluating imageset we had an algorithm that > worked > well given that the input function is continuous and the solve returns > the all the > solutions of the derivative. But we don't have any easy method to check > for the continuity. > So ultimately we decided to restrict ourself to rational functions. > > But there can be cases where the safe set of inputs are either too hard > to > isolate or becomes too small to be of any use. For example the > oscillating nature of trigonometric functions at infinity leads to wrong > results in some of the cases of limit evaluation. But isolating the cases > where it will give wrong > result might turn to be harder problem than computing the limit itself. > And by > not allowing trigonometric functions or not allowing limit computation at > infinity will reduce the usefulness of limit to a great extent. > > Because I don't think we can avoid wrong results we should: > > - Document and tell users that this is what sympy cannot do and where can > silently go wrong. > > - Create a subset of sympy that is complete and reliable, backed by formal > proofs of correctness. I speculate that the common use cases of sympy are > teaching and homework of students. A reliable subset of sympy might find > more real world application, say in designing hybrid algorithms for > computation. We might go about implementing by first figuring out the > modules > and algorithms which are complete, then we can have an environment > variable > `ONLY_COMPLETE_MODULES` which when set to true will allow only complete > modules to be used. > > -- > Harsh Gupta > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at http://groups.google.com/group/sympy. > For more options, visit https://groups.google.com/groups/opt_out. -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out.
