Glad to see you're taking this on. It's a pretty complicated task.
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 handler system isn't very good. This is the key realization I
came to when working on https://github.com/sympy/sympy/pull/2210,
which lead to me to stop working on it and develop the proposed system
at https://github.com/sympy/sympy/pull/2508.
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
On Mon, Mar 16, 2015 at 11:17 PM, Sudhanshu Mishra <mrsu...@gmail.com> wrote:
> Hi all,
>
> I want to work on this projects listed on the ideas page. I've been reading
> discussions on the assumptions system for quite some time and trying to
> understand what has already been done and what do we want before 1.0.
>
> From what I've understood, it should look something like this:
>
> a) Make new assumptions read old assumptions (So that API doesn't break)
> b) Replace use of old assumptions with new assumptions everywhere (Remove
> assumptions from core too)
> c) Let x.is_* API be there but handle it with new assumptions (Probably we
> do not have a consensus here)
> d) Improve performance of new assumptions
> e) Get rid of the conflicting assumptions
>
>
> Aaron has already done some work on 'a' here which makes the point clear.
> I need guidance on how to go about 'b'.
> I'm not sure about what has to be done in 'c' since ideas are conflicting at
> different places.
>
> For 'd', I think SAT solvers are way to go. SDB's GSoC project last year had
> some good things for assumptions.
>
> Please comment on the points that I've made so that l could start writing my
> proposal.
>
>
> Regards
> Sudhanshu Mishra
>
> --
> 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 sympy+unsubscr...@googlegroups.com.
> To post to this group, send email to sympy@googlegroups.com.
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/sympy/CAFW_KCSSFq7ot37szRnfWKF2QBwn3d7b2TSPBevQ7_2fEbVxVA%40mail.gmail.com.
> For more options, visit https://groups.google.com/d/optout.
--
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 sympy+unsubscr...@googlegroups.com.
To post to this group, send email to sympy@googlegroups.com.
Visit this group at http://groups.google.com/group/sympy.
To view this discussion on the web visit
https://groups.google.com/d/msgid/sympy/CAKgW%3D6JnJ3s6pwjOoxcmR9YsoGG9-y%3D6gd_KOi_4ZmQhsSnWLA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.
