Assumptions history

Leonid Kovalev edited this page Jan 16, 2018 · 4 revisions
Clone this wiki locally

(The following is from a post by Aaron Meurer in the Google Groups thread https://groups.google.com/forum/#!msg/sympy/PHR136kdxc4/C2qs5obPGoMJ)

To really understand what should be done, you should understand what's already been tried, and why certain things haven't worked. So let me see if I can give a short history. this is from memory, so I'm sure I'll forget a lot of things. Hopefully in writing this down I can help you and others who have not been around for long enough to know all these things.

In the beginning, there were just the assumptions. This is what is today called the old assumptions. Assumptions were set on symbols and stored in the expressions. The syntax was Symbol('x', real=True) and x.is_real. The inference engine used a combination of a deduction system that computed all possible facts from a set of facts (sympy.core.facts and sympy.core.assumptions), and called eval_is* methods on objects.

There have been a lot of facts added to this system over the years, but the basic system itself has remained almost completely unchanged. So don't discount it. It's fast, reasonably extendable, and it gets the job done.

It was then seen that one of the biggest things that made the core slow. Part of this was that the core was doing too much with assumptions, slowing down basic operations, and part of it was simply that it made the core too complex, making some refactorings very difficult or impossible.

So some ideas were tossed around on how to separate the assumptions from the core. This predates me, but I believe https://github.com/sympy/sympy/issues/4146 was an important discussion here. This lead to Fabian Pedregosa's 2009 Google Summer of Code project, which implemented the so-called "new assumptions" (https://github.com/sympy/sympy/wiki/GSoC-2009-Report-Fabian-Pedregosa:-Assumptions).

The basic idea here is that assumptions would be separate from the objects that were being assumed about. So for instance, instead of Symbol('x', real=True), which puts the "real" fact on the 'x' object, you would just have Symbol('x'), and keep Q.real separate.

The syntax for this system was refined a bit by Ronan a little later, so that you could type Q.real(x), and that would represent the fact "x is real".

Some key aspects of Fabian's system:

  • ask(): Basically the same as it is today. A two argument function. The first argument is what you are asking about, and the second is what you are assuming (like ask(Q.real(x), Q.positive(x)), meaning "given that x is positive, is x real?"). Because assumptions are separate from the objects that they are on, you have to keep track of your assuming facts. I believe the notion of "global assumptions", which are just an implicit way to store some facts globally to be included in all ask() calls, were added later. Global assumptions have been a bit of a point of contention, and I'll talk about them a bit more later.

  • ask handlers: The deduction system for ask was two parted. First it would use some basic logic deduction using a SAT solver and some known facts (like Implies(Q.positive, Q.real)). Second, each fact would have a handler object, which defines methods on how to determine its truth for specific classes given some assumptions, like

class AskPositiveHandler(Handler): 
    @staticmethod 
    def Pow(expr, assumptions): 
        # Returns True, False, or None if expr, which is a Pow, is 
positive, given the facts in assumptions 
  • refine(): One of the key aspect of assumptions is simplification. The canonical example is sqrt(x**2). This simplifies to x if x is nonnegative, to abs(x) if x is real, and not at all otherwise. The traditional way this was done is in the core, meaning the simplification happens when the sqrt (i.e., Pow) object is created, by checking the assumptions on x. This has two disadvantages: it slows things down, since the checking happens every time any Pow object is created, and it makes it difficult to create sqrt(x**2) unsimplified if x is positive (there are other disadvantages too, see https://github.com/sympy/sympy/wiki/Automatic-Simplification).

The idea behind refine() is that since assumptions are separate from objects, the simplifications would need to be done in a function, which takes the object and the assumptions. So it would work like refine(sqrt(x**2), Q.positive(x)) -> x.

refine also has a handler system similar to ask to handle writing all these simplification routines.

Note that I am talking about a lot of this in the past tense, but most of it is still true today. The new assumptions have the same system that Fabian wrote (except with some syntax changes), and the core still simplifies assumptions at object creation time.

The next step after this project was to remove the old assumptions, so that only the new assumptions would be used. There have been several attempts at this. They all have failed. A (very incomplete) list of links follows:

https://github.com/sympy/sympy/issues/4983 https://github.com/sympy/sympy/pull/328 https://github.com/sympy/sympy/pull/343 https://github.com/sympy/sympy/pull/366 https://github.com/sympy/sympy/pull/1162 https://github.com/sympy/sympy/pull/1751 https://github.com/sympy/sympy/pull/2210 https://github.com/sympy/sympy/issues/5295 https://github.com/sympy/sympy/pull/2538 https://github.com/sympy/sympy/issues/6730 https://github.com/sympy/sympy/issues/6786 https://github.com/sympy/sympy/issues/6783 https://github.com/sympy/sympy/issues/6738 https://github.com/sympy/sympy/issues/6735 https://github.com/sympy/sympy/issues/6735 https://github.com/sympy/sympy/issues/6734 https://github.com/sympy/sympy/issues/6731 https://github.com/sympy/sympy/issues/3447 https://github.com/sympy/sympy/issues/5976 https://github.com/sympy/sympy/pull/8134 https://github.com/sympy/sympy/pull/8293 https://github.com/sympy/sympy/pull/7925 https://github.com/sympy/sympy/pull/7926

(I relink some specific ones of these that I talk about below)

Some issues/realizations that have come out of this:

  • Global assumptions, as I mentioned above, are something that should be considered. There's a tension between wanting to remove assumptions from the core and convenience (just as there's a tension between not wanting expressions to autoevaluate too much and convenience). Having a pure "new assumptions" philosophy means that if you want to assume something on one of your variables, you have to pass that assumption around everywhere. A fix for this is to have a global assumptions set, where ask() automatically reads from this set and includes it in the global assumptions.

The problem is, you don't want your assumptions to "leak" to other, unrelated functions that happen to use the same symbol names. There have been several suggestions on how to fix this. Matthew Rocklin introduced an assuming() context manager, which makes it easy to assume a fact and unassume it when you don't need it. Making something that uses function scopes has also been suggested (see issue 4983). The final suggestion is to effectively keep the old assumptions, i.e., allow symbols to have assumptions defined directly on them (more on this later).

  • The old assumptions are baked into the core pretty heavily. Ronan's pull requests I linked above help with this a bit, as them moved the assumptions into a single corner of the core, making them easier to remove. But still things like Mul.flatten use the assumptions heavily. Plus the simplification that is supposed to only happen in refine() is all in there too.

  • The assumptions are used everywhere. This is really the main issue. Even the smallest change to the old assumptions has a ripple effect requiring changes to the entire codebase. In many cases, the changes require understanding every piece of code that uses the assumptions, so that a fix would be correct.

  • At SciPy 2013, Matthew Rocklin and I decided to give the new assumptions a stab. Because previous attempts to remove the old assumptions had failed terribly, we decided that instead of removing the old and replacing them with the new, we should try to merge the two. That is, make the new assumptions call the old assumptions, and make the old assumptions call the new assumptions. This was pull request 2210. This lead to some important realizations.

  • The new assumptions and old assumptions differ. I noticed you put this as your item e. But really this has to be the first thing that is fixed. If one assumptions system uses "real" to mean one thing and another uses it to mean another (as is currently the case; in the old assumptions oo is real and in the new it is not), then changing code from is_real to Q.real is not a simple find and replace. Furthermore, if you want to interface the two systems, they have to have to agree everywhere, or you'll get contradictions that in the best case lead to confusing errors or wrong results and in the worst case prevent the code from working at all because of logical unsatisfiability.

I've stated this many times, but I'll reiterate. One of the most important things that needs to be done for the assumptions before any major refactoring can happen is to decide on precise definitions for each assumption, and document them (look at all the issues referenced at https://github.com/sympy/sympy/issues/5295 to get an idea of why this is so important). I started this at https://github.com/sympy/sympy/pull/2538, but it isn't finished.

The basic issue is this. Suppose we want to write a handler that says "if x is zero or y is zero, then x*y is zero" (I know you asked in a later message in this thread about this fact, but let's suppose for now that we do want this fact). You might write something like

class AskZeroHandler: 
    @staticmethod 
    def Mul(expr, assumptions): 
        if any(ask(Q.zero(x), assumptions) for x in expr.args): 
            return True 

Seems fine so far. This is roughly what the current AskZeroHandler.Mul does.

Now suppose we try to get ask to recompute the exact fact itself:

ask(Q.zero(x*y), Q.zero(x) | Q.zero(y))

This will get passed in to the handler, and it will return, basically

ask(Q.zero(x), Q.zero(x) | Q.zero(y)) or ask(Q.zero(y), Q.zero(x) | Q.zero(y))

("or" here should actually be fuzzy or, meaning it does the right thing with None)

But here's the catch. That will return None. The reason is that both ask(Q.zero(x), Q.zero(x) | Q.zero(y)) and ask(Q.zero(y), Q.zero(x) | Q.zero(y)) are None: we can't deduce that x is zero given that x or y is zero. We only know that one of the two is zero, but not which!

The core issue is that there are limitations to using Python logic to do symbolic logic. In Python logic, everything must be evaluated down to a single truth value. In symbolic logic, expressions may have unknown truth values. Another example of this is the law of the excluded middle. Python does not know that "stuff or not stuff" is always True without first evaluating "stuff". Symbolic logic can know this, even if the truth value of "stuff" is unknown.

The handler system is broken in other ways too. Suppose we want to do the reverse fact, "if x*y is zero, then x is zero or y is zero". How to even begin writing this is not clear. If we write AskZeroHandler.Symbol, we would somehow need to check for Q.zero(Mul) facts in the assumptions, where the Mul contains x. The best thing I can think of is to do the very stupid thing and made just ask(Q.zero(x), Q.zero(x*y)) work (i.e., the second argument of ask() has to be exactly Q.zero(Mul)).

class AskZeroHandler: 
    @staticmethod 
    def Symbol(expr, assumptions): 
        if isinstance(assumptions, Q.zero) and 
isinstance(assumptions.args[0], Mul) and expr in 
assumptions.args[0].args: 
            return True 

The current ask handler system does very roughly not much more than this very stupid thing (in addition to what I did above, it handles And). I don't want to get too sidetracked from the history, but the system I proposed in #2508 handles this fact, and it handles it now matter how you pose it to ask, because all the logic is done symbolically, and things are solved with the SAT solver.

  • The new assumptions are slow. As I said above, don't discount the old assumptions. The are quite fast, and considering how they are used in the core, it's somewhat impressive. The new assumptions, as they are now, couldn't be used as a drop in replacement for the old assumptions for performance reasons alone.

Now we get to the most recent parts. At https://groups.google.com/forum/#!msg/sympy/wlXB4jngnW0/8G5QNz3Kf0EJ, I proposed what I believe is a reasonable way forward with the assumptions. It boils down to:

  • Merge my 2508 stuff, since the handler system won't scale. My ideas also need improvement (especially regarding speed). I also want to get it merged so that people will use it and think about ways to make it better.

  • Find and fix all inconsistancies between the old and new assumptions. A lot of what I suggested there was already fixed at https://github.com/sympy/sympy/pull/8293, but I made a more extensive list of suggested changes at https://github.com/sympy/sympy/pull/8134. In particular, the nature of infinities and real and positive facts has not been ironed out (and indeed, I'm not entirely convinced which way it should be changed to). Most importantly of all, document everything rigorously, so that there is a definitive definition of each assumption.

  • Make the new assumptions call the old assumptions. This is much less intrusive than the reverse. I made a proof of concept on how it can be done at https://github.com/sympy/sympy/pull/7925. Sergey made an alternate suggestion at https://github.com/sympy/sympy/pull/7926. The important thing is that we can't do this until the two systems agree with one another. Otherwise the result of ask() would depend on whether it hits the old assumptions or the handlers system.

Longer term, we should:

  • Make the old assumptions expr.is_real syntax call the new assumptions, so that there is effectively one system.

  • Remove assumptions from the core as much as possible. If we can remove ManagedProperties (the core metaclass that holds the basic old assumptions logic) that would be awesome. Removing automatic simplification based on assumptions is also important (especially for performance).

  • Use a tiered handlers system. I'm currently of the opinion that this is the way to go. The more powerful a system is, the slower it is. 2508 is great, but slow. The old assumptions, facts.py system is fast, but limited in power. I think we should have a system where it asks one by one, from fastest to most powerful, until it gets an answer (optionally stopping early if getting a None is not that big of an issue, e.g., in the core it should do this).

This also would give us room to explore other ways to do deduction on facts than the ones that currently exist. For instance, I currently do not know what the best way to do deduction on inequalities is.

  • Change code to use the new assumptions style, i.e., keep the assumptions separate from the object, when it is most convenient. I don't believe this can be done everywhere, but there are things that can be done.

This is a lot of work to do, and for a GSoC project, I would not expect to get to the long term things, but I would keep them in mind as things that need to be done.

Aaron Meurer