GSoC 15: Improving Assumptions
508 views
Skip to first unread message
Sudhanshu Mishra
Mar 17, 2015, 12:17:56 AM3/17/15
to sy...@googlegroups.com
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
Joachim Durchholz
Mar 17, 2015, 3:46:05 AM3/17/15
to sy...@googlegroups.com
Am 17.03.2015 um 05:17 schrieb Sudhanshu Mishra:
> c) Let x.is_* API be there but handle it with new assumptions
> (Probably we do not have a consensus here)
Actually I see two reasons to do that:
> c) Let x.is_* API be there but handle it with new assumptions
> (Probably we do not have a consensus here)
1) Compatibility
2) New assumptions can be clunky:
from sympy.abc import x, y, z
ask(Q.even(x*y*(y + z)),
Q.integer(x) & Q.integer(y) & Q.even(z))
Old is much more straightforward, though at the price of some set-up
verbosity:
x = Symbol('x', integer=True)
y = Symbol('y', integer=True)
m = Symbol('m', even=True)
(x*y*(y + z)).is_even
(Note that the API for new assumptions may improve, so this is a weaker
argument than it might seem at first)
Compatibility is very important if the old assumptions system is being
used by SymPy users.
Sudhanshu Mishra
Mar 17, 2015, 4:11:19 AM3/17/15
to sy...@googlegroups.com
Compatibility is very important if the old assumptions system is being used by SymPy users.
This is also not clear. The idea says that the project aims to completely replace old assumptions system with the new one.
So, do we remove the API of old assumptions or do we let it stay?
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+unsubscribe@googlegroups.com.
To post to this group, send email to sy...@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/5507DBB9.10205%40durchholz.org.
For more options, visit https://groups.google.com/d/optout.
Joachim Durchholz
Mar 17, 2015, 5:21:38 AM3/17/15
to sy...@googlegroups.com
Am 17.03.2015 um 09:10 schrieb Sudhanshu Mishra:
>>
>>
>> Compatibility is very important if the old assumptions system is being
>> used by SymPy users.
>
>
> This is also not clear. The idea says that the project aims to completely
> replace old assumptions system with the new one.
>
> So, do we remove the API of old assumptions or do we let it stay?
I had that sentence interpreted as "we want to remove the old
>>
>>
>> Compatibility is very important if the old assumptions system is being
>> used by SymPy users.
>
>
> This is also not clear. The idea says that the project aims to completely
> replace old assumptions system with the new one.
>
> So, do we remove the API of old assumptions or do we let it stay?
implementation".
I didn't read that as relating to the user-facing API at all.
Particularly considering that all discussion so far has been about
getting the new assumptions to fly at all, I've been assuming that
interface consideration would come later.
Sudhanshu Mishra
Mar 17, 2015, 6:02:17 AM3/17/15
to sy...@googlegroups.com
Makes sense. Thanks for commenting!
IMO we can keep the old assumptions' user facing API as long as we reach 1.0 because maintaining both systems might be counterproductive at times.
I still have a lot more to read about assumptions.
--
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+unsubscribe@googlegroups.com.
To post to this group, send email to sy...@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/5507F21F.2070002%40durchholz.org.
Sudhanshu Mishra
Mar 19, 2015, 6:17:43 AM3/19/15
to sy...@googlegroups.com
Since we are trying to move to the new assumptions, wouldn't it be good if new additions in the codebase use new assumptions? It would help refine the module and make the transition easy IMO.
Joachim Durchholz
Mar 19, 2015, 9:11:28 AM3/19/15
to sy...@googlegroups.com
Am 19.03.2015 um 11:17 schrieb Sudhanshu Mishra:
> Since we are trying to move to the new assumptions, wouldn't it be good if
> new additions in the codebase use new assumptions?
Yes, but as far as I can tell, new assumptions aren't ready for that
> Since we are trying to move to the new assumptions, wouldn't it be good if
> new additions in the codebase use new assumptions?
kind of use yet. There have been discussions of integrating a SAT solver
(which would be cool but I think that's experimental if it exists at
all), I recall performance problems being discussed but not yet resolved
(but some very nice performance figures as well so it's promising), and
I bet that there are some kinks that still need ironing out.
My current understanding is that it still needs the SAT solver either
coded or maybe just finished, and after that, integration can happen as
soon as there are a few people around who are confident that they can
use their expertise and time to solve any problems before they can block
a release.
So I guess we'll have to support both systems for a while.
Sudhanshu Mishra
Mar 19, 2015, 2:08:19 PM3/19/15
to sy...@googlegroups.com
> Yes, but as far as I can tell, new assumptions aren't ready for that
kind of use yet.
kind of use yet.
That's exactly why it will be fruitful for the new assumptions.
> There have been discussions of integrating a SAT solver
(which would be cool but I think that's experimental if it exists at
all), I recall performance problems being discussed but not yet resolved
(but some very nice performance figures as well so it's promising), and
I bet that there are some kinks that still need ironing out.
(which would be cool but I think that's experimental if it exists at
all), I recall performance problems being discussed but not yet resolved
(but some very nice performance figures as well so it's promising), and
I bet that there are some kinks that still need ironing out.
> My current understanding is that it still needs the SAT solver either
coded or maybe just finished, and after that, integration can happen as
soon as there are a few people around who are confident that they can
use their expertise and time to solve any problems before they can block
a release.
coded or maybe just finished, and after that, integration can happen as
soon as there are a few people around who are confident that they can
use their expertise and time to solve any problems before they can block
a release.
Since we only know of heuristic approaches to build SAT solvers there
always be chances of improvements. Lately, I read the blog posts by Fabian(He
wrote the logic module and new assumptions), it seems that we have a good enough
SAT solver(DPLL). Anyway, Aaron can comment better as he mentored a project on logic
last year.
> So I guess we'll have to support both systems for a while.
We'll support the user facing API anyway. However, I was just asking if the developers start using
new assumptions under the hood.
Joachim Durchholz
Mar 19, 2015, 2:21:32 PM3/19/15
to sy...@googlegroups.com
Am 19.03.2015 um 19:08 schrieb Sudhanshu Mishra:
> We'll support the user facing API anyway. However, I was just asking if the
> developers start using
> new assumptions under the hood.
Well, question is: Is is ready for that yet?
> We'll support the user facing API anyway. However, I was just asking if the
> developers start using
> new assumptions under the hood.
Sudhanshu Mishra
Mar 20, 2015, 8:56:48 AM3/20/15
to sy...@googlegroups.com
> Well, question is: Is is ready for that yet?
Perhaps not. It might be after merging 2508.
--
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+unsubscribe@googlegroups.com.
To post to this group, send email to sy...@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/550B13A8.6090904%40durchholz.org.
Sudhanshu Mishra
Mar 20, 2015, 8:57:16 AM3/20/15
to sy...@googlegroups.com
I have a question.
This one is fine.
In [9]: x = Symbol('x', zero=True)
In [10]: (x*y).is_zero
Here we didn't give facts about y then why ask returned True?
In [3]: ask(Q.zero(x*y), Q.zero(x))
Out[3]: True
Joachim Durchholz
Mar 20, 2015, 5:06:50 PM3/20/15
to sy...@googlegroups.com
Am 20.03.2015 um 13:56 schrieb Sudhanshu Mishra:
> I have a question.
>
> This one is fine.
>
> In [9]: x = Symbol('x', zero=True)
>
> In [10]: (x*y).is_zero
>
> ------------------------------
> I have a question.
>
> This one is fine.
>
> In [9]: x = Symbol('x', zero=True)
>
> In [10]: (x*y).is_zero
>
>
> Here we didn't give facts about y then why ask returned True?
>
> In [3]: ask(Q.zero(x*y), Q.zero(x))
> Out[3]: True
I'd assume that x*zero is always zero regardless of the value of x, so
> Here we didn't give facts about y then why ask returned True?
>
> In [3]: ask(Q.zero(x*y), Q.zero(x))
> Out[3]: True
this result seems correct.
This assumes that x is a number, of course. If we allow anything
involving limits for x, then the result should not be True.
Sudhanshu Mishra
Mar 20, 2015, 5:11:08 PM3/20/15
to sy...@googlegroups.com
I think, just like the old assumptions it should also consider the cases where the product might be NaN.
--
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+unsubscribe@googlegroups.com.
To post to this group, send email to sy...@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/550C8BE5.3010209%40durchholz.org.
Sudhanshu Mishra
Mar 20, 2015, 6:14:33 PM3/20/15
to sy...@googlegroups.com
I think the handler just treats it as following but don't know why.
Q.zero(Mul(*args)) -> Or(*[Q.zero(arg) for arg in args])
By the way, here's the link to the proposal which I've started writing: https://github.com/sympy/sympy/wiki/GSoC-2015-Application-Sudhanshu-Mishra:-Assumptions
It doesn't have much information about the project and implementation yet. Please take a look on it.
Aaron Meurer
Mar 20, 2015, 7:23:36 PM3/20/15
to sy...@googlegroups.com
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
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
> --
> 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+un...@googlegroups.com.
> 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
> To post to this group, send email to sy...@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.
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
Aaditya Nair
Mar 21, 2015, 4:08:44 AM3/21/15
to sy...@googlegroups.com
- 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.
What kind of changes are we taking about ? Is it about the API changes or the assumptions that are returned ?
- 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.
Cant we just update the symbol` to directly update assumptions in `global_assumptions`.
That will help solve any unsatisfiablity as all assumptions are stored in one place.
- 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.
Intrusive in what sense ?
Again, I think using `global_assumptions` is the answer.
- 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).
I think that does some of the work towards that. doesn't it?
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.
Can we divide up the project , as Sudhanshu and me want to work on the same thing ?
Aaditya M Nair
Joachim Durchholz
Mar 21, 2015, 7:18:10 AM3/21/15
to sy...@googlegroups.com
Am 21.03.2015 um 00:23 schrieb Aaron Meurer:
> 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).
I have another suggestion: Turn assumption contexts into first-class
> 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).
objects (and give them a better name).
Have a global assumption context, let the context manager manage another
one, or add contexts into expressions. IOW let the user decide what
contexts he needs or wants.
Do not have any kind of fallback between these context objects; if
there's a global_assumptions object, make assuming() not pull it in by
default, but allow writing
with assuming(global_assumption):
so people can pull in their global assumptions (and they can also keep
different sets of assumptions around, e.g. to test different hypotheses).
> - 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.
If we want to merge the two, and if it's an ongoing effort, then this
must be heavily guarded with unit tests.
> 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.
You can't infer True vom A | !A on a per-symbol basis, you need a less
local view.
Also, an inference engine can do strategy. E.g. in an expression like
x*(hugely_complicated_thing), and you find that x is zero, you don't
need to infer much about hugely_complicated_thing except that it will
not diverge towards infinity.
I still see a place for per-symbol assumptions and rules. They are the
basic facts that the inference engine needs to work with.
> 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.
years of refinement.
To catch up, the solver would have to get smart about strategy quickly,
which means it should be easy to hack on.
> - 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.
from the old assumption, instead of trying to recreate facts in the new
assumptions.
Trouble is: old assumption have their facts and rules as executable code
in handlers. Solvers in new assumptions need them as proposition objects
that they can recombine.
So my approach would be to look at the old-assumptions code, identify
structural preconditions and ensuing inferences, recode these as rules
for new assumptions, and replace the old-assumption handler code with a
series of calls to the "apply THIS rule to THAT Basic AFTER checking
that it is valid" function.
Nice thing with that is that the old-assumption code is pretty
well-covered by tests, so most mistakes in the recoding will be caught.
> - Make the new assumptions call the old assumptions.
SAT solver (new assumptions) handler (old assumptions)
| |
v v
elementary rules
Elementary rules consisting of a structural pattern ("this rule applies
to Add nodes with all operands being integral"), possibly a predicate
("number of known-to-be-odd operands is even"), and a resulting
predicate ("Add node is known to be even") and/or structural
transformation ("move the even operands to the head of the list" - okay,
that's sill, you need that for sine/cosine transforms and such, and
maybe transformation is beyond the scope of assumptions anyway).
I do not think the new assumptions should call the old assumptions. The
new assumptions work by manipulating data structures, not by executing code.
> - 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.
metaclass system (which is there for the Singleton stuff).
I.e. Singleton and assumptions stuff get mixed in the metaclass
hierarchy, and separating that from each other would be really great.
> - 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).
and in what circumstances they get activated.
Otherwise, users will be constantly surprised about rules and when
they'll get applied and when not, and what to do to get a specific rule
applied.
Another way to get users a say would be to allow them to specify an
assumption *as something to verify*. This would force the solver into
chasing those rules that lead to the specified assumption, and trigger
those rules that the user want to see triggered.
Hope I didn't ramble too much :-)
Regards,
Jo
Aaron Meurer
Mar 21, 2015, 2:32:42 PM3/21/15
to sy...@googlegroups.com
On Sat, Mar 21, 2015 at 3:08 AM, Aaditya Nair <aaditya...@gmail.com> wrote:
>> - 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.
>
>
> What kind of changes are we taking about ? Is it about the API changes or
> the assumptions that are returned ?
Almost any change you make. If you change the API, you'll have to
>> - 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.
>
>
> What kind of changes are we taking about ? Is it about the API changes or
> the assumptions that are returned ?
modify everywhere that API is used. If you change what an assumption
means (e.g., if you change oo.is_real), you'll have to go through
everywhere that assumption and make sure that its use is still
correct. Even just making the assumptions more powerful (able to
return True or False as opposed to None more often) can require some
changes, because some code may take different paths.
>
>>
>> - 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.
>
>
> Cant we just update the symbol` to directly update assumptions in
> `global_assumptions`.
> That will help solve any unsatisfiablity as all assumptions are stored in
> one place.
This doesn't fix unsatisfiability. I was maybe a bit unclear what that
means. It means if two facts are inconsistent in their definition
(like oo.is_real vs. Q.real(oo)), then you will get logical
contradictions if you try to merge the two, because some code will use
one and some will use the other. For unsatisfiability, I mean that
this logical contradiction can bubble up to an exception from he SAT
solver, so that instead of getting a wrong result or something like
that, the assumptions system just completely fails. The system I
propose at 2508 is very good at failing with contradictory
assumptions.
>
>>
>> - 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.
>>
> Intrusive in what sense ?
> Again, I think using `global_assumptions` is the answer.
SymPy uses the new assumptions. Except for a few isolated modules,
everything is using the old assumptions. So changing the way the new
assumptions works will not affect many thing. On the other hand, even
small changes to the old assumptions can affect the entire code base,
and a change as huge as making them use the new assumptions leads to
effects that are unmanageable.
>>
>>
>> - 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).
>
>
> I think that does some of the work towards that. doesn't it?
>
>>
>> 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.
>
>
> Can we divide up the project , as Sudhanshu and me want to work on the same
> thing ?
make sure your proposals can be completed independently of one another
(i.e., even if the other student is not accepted, you should be able
to do your proposal). Even if you both are accepted, we've learned in
the past that it's a bad idea to have one student's work depend on
another's. I would discuss this with Sudhanshu.
A suggested way to split things (and there are other ways) would be
for one person to work on the steps I outlined here to "merge" the old
and new assumptions, and for another person to work on improving the
new assumptions (a la 2508 and similar ideas).
Aaron Meurer
>
> Aaditya M Nair
>
> --
> 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+un...@googlegroups.com.
> To post to this group, send email to sy...@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/fe011c10-0364-4553-b5ae-b56cffc258bb%40googlegroups.com.
> --
> 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+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
Aaron Meurer
Mar 21, 2015, 2:54:47 PM3/21/15
to sy...@googlegroups.com
outlined. Actually, the two pull requests I mentioned only make the
new assumptions read the old assumptions on Symbol. The next step
would be to make them read the old assumptions on every expression.
> Trouble is: old assumption have their facts and rules as executable code in
> handlers. Solvers in new assumptions need them as proposition objects that
> they can recombine.
possible written down as in 2508, so that they can be used with the
inference system.
But before we can do that, we have to figure out how to make that
approach faster.
>
> So my approach would be to look at the old-assumptions code, identify
> structural preconditions and ensuing inferences, recode these as rules for
> new assumptions, and replace the old-assumption handler code with a series
> of calls to the "apply THIS rule to THAT Basic AFTER checking that it is
> valid" function.
> Nice thing with that is that the old-assumption code is pretty well-covered
> by tests, so most mistakes in the recoding will be caught.
system. Although the assumptions tests themselves could be translated
to the new assumptions syntax.
But another advantage of a full inference system is that it catches
contradictions. So mistakes can often be caught that way. Another
advantage is that facts written down declaritively tend to be terse
(see https://github.com/sympy/sympy/pull/2508/files#diff-e0f95401c86d07d90903363122990de0R287,
each oneline fact would be several lines in the old assumptions). So
mistakes are harder just for that. I'm also thinking of syntactic
sugar that can be used to make those facts even easier to read.
>
>> - Make the new assumptions call the old assumptions.
>
>
> I think the transitional structure would have to be this:
>
> SAT solver (new assumptions) handler (old assumptions)
> | |
> v v
> elementary rules
>
> Elementary rules consisting of a structural pattern ("this rule applies to
> Add nodes with all operands being integral"), possibly a predicate ("number
> of known-to-be-odd operands is even"), and a resulting predicate ("Add node
> is known to be even") and/or structural transformation ("move the even
> operands to the head of the list" - okay, that's sill, you need that for
> sine/cosine transforms and such, and maybe transformation is beyond the
> scope of assumptions anyway).
>
> I do not think the new assumptions should call the old assumptions. The new
> assumptions work by manipulating data structures, not by executing code.
The final goal is to not have multiple assumptions systems, at least
from a user perspective. We will probably have multiple inference
layers, but these should be hidden from the user. To do this, we
either need to remove one of the existing systems (already tried and
failed), or merge the two, so that one calls the other and they just
become different layers in the inference stack.
>
>> - 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.
>
>
> ManagedProperties isn't just for assumptions, it's integrated with the
> metaclass system (which is there for the Singleton stuff).
> I.e. Singleton and assumptions stuff get mixed in the metaclass hierarchy,
> and separating that from each other would be really great.
>
>> - 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).
>
>
> That would require naming each tier, and telling users what tiers exist and
> in what circumstances they get activated.
> Otherwise, users will be constantly surprised about rules and when they'll
> get applied and when not, and what to do to get a specific rule applied.
different tiers should be, how they should be named, and when they
should be used. The main focus is performance, i.e., calling faster
things first, and potentially not calling slower things. So before we
think too hard about it we would also need to benchmark things. This
is why I put it in my longer term list, as other things would need to
settle down a bit first before doing this. Or maybe we can find a way
to make the most powerful system really fast and this will become
completely unnecessary.
>
> Another way to get users a say would be to allow them to specify an
> assumption *as something to verify*. This would force the solver into
> chasing those rules that lead to the specified assumption, and trigger those
> rules that the user want to see triggered.
were to make a graph where the nodes are the assumptions (real,
positive, even, etc.) and there are edges if two assumptions are
related by a fact (like positive -> real), the graph would have a very
large connected component containing all the standard assumptions
(there are about twenty of them). Also, a good SAT solver should be
pretty good at ignoring useless facts.
And every edge has to point in both directions. You can't just say
positive -> real and I know something about real, so I don't need to
care about positive. The reason is the contrapositive rule, !real ->
!positive. If what I know about real ends up being that real is False,
then I can deduce something about positive.
Aaron Meurer
>
> Hope I didn't ramble too much :-)
>
> Regards,
> Jo
>
> --
> 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+un...@googlegroups.com.
> To post to this group, send email to sy...@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/550D536D.8020806%40durchholz.org.
> 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+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
Joachim Durchholz
Mar 21, 2015, 3:57:10 PM3/21/15
to sy...@googlegroups.com
Am 21.03.2015 um 19:54 schrieb Aaron Meurer:
>> Trouble is: old assumption have their facts and rules as executable code in
>> handlers. Solvers in new assumptions need them as proposition objects that
>> they can recombine.
>
> Yes this is true. Long term, I would like to see as many facts as
> possible written down as in 2508, so that they can be used with the
> inference system.
>
> But before we can do that, we have to figure out how to make that
> approach faster.
+1
>> Trouble is: old assumption have their facts and rules as executable code in
>> handlers. Solvers in new assumptions need them as proposition objects that
>> they can recombine.
>
> Yes this is true. Long term, I would like to see as many facts as
> possible written down as in 2508, so that they can be used with the
> inference system.
>
> But before we can do that, we have to figure out how to make that
> approach faster.
>> So my approach would be to look at the old-assumptions code, identify
>> structural preconditions and ensuing inferences, recode these as rules for
>> new assumptions, and replace the old-assumption handler code with a series
>> of calls to the "apply THIS rule to THAT Basic AFTER checking that it is
>> valid" function.
>> Nice thing with that is that the old-assumption code is pretty well-covered
>> by tests, so most mistakes in the recoding will be caught.
>
> Only if the translated code is actually used by the assumptions
> system.
calls go into the new assumption system.
THAT one could, for the transition period, try first new, then old
assumptions. And issue diagnostics if it detects inconsistencies other
than the new system missing some fact.
> Although the assumptions tests themselves could be translated
> to the new assumptions syntax.
> But another advantage of a full inference system is that it catches
> contradictions. So mistakes can often be caught that way. Another
> advantage is that facts written down declaritively tend to be terse
> (see https://github.com/sympy/sympy/pull/2508/files#diff-e0f95401c86d07d90903363122990de0R287,
> each oneline fact would be several lines in the old assumptions). So
> mistakes are harder just for that. I'm also thinking of syntactic
> sugar that can be used to make those facts even easier to read.
>>> - Make the new assumptions call the old assumptions.
>>
>>
>> I think the transitional structure would have to be this:
>>
>> SAT solver (new assumptions) handler (old assumptions)
>> | |
>> v v
>> elementary rules
>>
>> Elementary rules consisting of a structural pattern ("this rule applies to
>> Add nodes with all operands being integral"), possibly a predicate ("number
>> of known-to-be-odd operands is even"), and a resulting predicate ("Add node
>> is known to be even") and/or structural transformation ("move the even
>> operands to the head of the list" - okay, that's sill, you need that for
>> sine/cosine transforms and such, and maybe transformation is beyond the
>> scope of assumptions anyway).
>>
>> I do not think the new assumptions should call the old assumptions. The new
>> assumptions work by manipulating data structures, not by executing code.
>
> They do execute code. See sympy.assumptions.handlers.
But what data is the SAT solver working with, then?
>>> - 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.
>>
>> ManagedProperties isn't just for assumptions, it's integrated with the
>> metaclass system (which is there for the Singleton stuff).
>> I.e. Singleton and assumptions stuff get mixed in the metaclass hierarchy,
>> and separating that from each other would be really great.
>
> OK, I didn't know that.
properties that the assumptions system requires.
(I think that the metaclass should have been split out into a
ManagedPropertiesMeta metaclass.)
> The main focus is performance, i.e., calling faster
> things first, and potentially not calling slower things.
to know how badly.
Maybe some cost-based optimization (CBO). Associate each rule with some
info on how much evaluating it would cost (probably depending on the
structure of the expression the rule applies to, e.g. something that
tries permutations could be fast enough for up to four operands or
something), and let the solver decide what to try first.
>> Another way to get users a say would be to allow them to specify an
>> assumption *as something to verify*. This would force the solver into
>> chasing those rules that lead to the specified assumption, and trigger those
>> rules that the user want to see triggered.
>
> Sadly, the facts are all tied to one another pretty closely. If you
> were to make a graph where the nodes are the assumptions (real,
> positive, even, etc.) and there are edges if two assumptions are
> related by a fact (like positive -> real), the graph would have a very
> large connected component containing all the standard assumptions
> (there are about twenty of them). Also, a good SAT solver should be
> pretty good at ignoring useless facts.
The old assumptions establish heaps and heaps of useless fact and still
are faster...
Does the solver use backwards chaining?
I.e. start with facts and chain forward, start with the final conclusion
it's trying to prove and chain backwards, find overlaps between the two
sets of facts as they grow. That's still O(N^k), but at least that
halves N, which is still a huge win.
Having an intermediate hypotheses gives the solver another point that it
can chain forward and backwards from. So we're dividing N by
(number-of-intermediate-points * 2) now, which can help as well.
HTH
Jo
Aaron Meurer
Mar 21, 2015, 8:04:56 PM3/21/15
to sy...@googlegroups.com
(https://github.com/sympy/sympy/blob/5507c86e70f816f95f87b868615502a44cac5853/sympy/assumptions/ask.py#L329-L377).
In my branch, everything in that file. The known_facts are what I
like to call the "free" facts, in that they can be written down
completely free of the expression they apply to. For instance,
Implies(Q.positive, Q.real). Facts that depend on the kind of
expression they apply to (like, if all terms in an Add are positive,
then the whole expression is positive), aren't expressible
symbolically in the current new assumptions (but they are in 2508).
Aaron Meurer
> --
> 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+un...@googlegroups.com.
> To post to this group, send email to sy...@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/550DCD11.6030708%40durchholz.org.
> 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+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
Joachim Durchholz
Mar 22, 2015, 5:40:51 AM3/22/15
to sy...@googlegroups.com
Am 22.03.2015 um 01:04 schrieb Aaron Meurer:
> On Sat, Mar 21, 2015 at 2:57 PM, Joachim Durchholz <j...@durchholz.org> wrote:
>> Am 21.03.2015 um 19:54 schrieb Aaron Meurer:
>>>>
>>>> I do not think the new assumptions should call the old assumptions. The
>>>> new
>>>> assumptions work by manipulating data structures, not by executing code.
>>>
>>> They do execute code. See sympy.assumptions.handlers.
>>
>>
>> Oh. I've been thinking that that was part of the old assumptions system.
>> But what data is the SAT solver working with, then?
>
> Currently, the known_facts
> (https://github.com/sympy/sympy/blob/5507c86e70f816f95f87b868615502a44cac5853/sympy/assumptions/ask.py#L329-L377).
> In my branch, everything in that file. The known_facts are what I
> like to call the "free" facts, in that they can be written down
> completely free of the expression they apply to. For instance,
> Implies(Q.positive, Q.real). Facts that depend on the kind of
> expression they apply to (like, if all terms in an Add are positive,
> then the whole expression is positive), aren't expressible
> symbolically in the current new assumptions (but they are in 2508).
Oh, I see.
> On Sat, Mar 21, 2015 at 2:57 PM, Joachim Durchholz <j...@durchholz.org> wrote:
>> Am 21.03.2015 um 19:54 schrieb Aaron Meurer:
>>>>
>>>> I do not think the new assumptions should call the old assumptions. The
>>>> new
>>>> assumptions work by manipulating data structures, not by executing code.
>>>
>>> They do execute code. See sympy.assumptions.handlers.
>>
>>
>> Oh. I've been thinking that that was part of the old assumptions system.
>> But what data is the SAT solver working with, then?
>
> Currently, the known_facts
> (https://github.com/sympy/sympy/blob/5507c86e70f816f95f87b868615502a44cac5853/sympy/assumptions/ask.py#L329-L377).
> In my branch, everything in that file. The known_facts are what I
> like to call the "free" facts, in that they can be written down
> completely free of the expression they apply to. For instance,
> Implies(Q.positive, Q.real). Facts that depend on the kind of
> expression they apply to (like, if all terms in an Add are positive,
> then the whole expression is positive), aren't expressible
> symbolically in the current new assumptions (but they are in 2508).
I'd want go full length towards making all rules into data structures,
no code execution at all (except for generic code to apply rules,
obviously).
I can't even give a hard reason for that, except that I know from
experience that data is far easier to analyze and do something new and
initially unexpected than code where this is essentially impossible.
Also, all solvers that I know work that way.
I don't know whether that would be a wise approach for SymPy, or the
right thing to do right now.
I'm slightly worried that we might want to go full length to data-based
solving after we get the SAT solver, and then have *three* solvers to
deal with (because the old assumptions system won't die that quickly),
so I still see a small advantage to going that direction right now.
Downside of "right now" would be "who's going to do it" and "that's
going to be even more work"... so I don't know enough to have a real
position about what's the best way forward.
Sudhanshu Mishra
Mar 23, 2015, 8:52:56 PM3/23/15
to sy...@googlegroups.com
I've updated the wiki. (Still far from complete)
Please provide feedback on the matter so far.
Places to look at:
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+unsubscribe@googlegroups.com.
To post to this group, send email to sy...@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/550E8E1E.3060701%40durchholz.org.
Joachim Durchholz
Mar 24, 2015, 5:39:33 AM3/24/15
to sy...@googlegroups.com
Just a heads-up: I'm in a bit of a squeeze and won't be able to review
the application.
the application.
Aaron Meurer
Mar 24, 2015, 12:13:37 PM3/24/15
to sy...@googlegroups.com
You should also mention my approach from
https://github.com/sympy/sympy/pull/7925 to make the new assumptions
read the old assumptions (add handlers). Also, technically,
https://github.com/sympy/sympy/pull/2508/files#diff-e0f95401c86d07d90903363122990de0R227
is a way of doing this as well. I'm undecided on which of these
(including adding to global assumptions) is the best. If you have a
preference, you should argue in the application why you think it's the
best one.
In the execution section, can you give your impression of how
long/hard each item would be (or maybe the timeline is the appropriate
place to do this).
What is the difference between "Making API of old assumptions call new
assumptions internally. The target would be to achieve minimum ripple
effect throughout the codebase as the changes are made." and "Once the
new assumption is ready to handle things, start modifying the codebase
so that expr.is_* syntax calls the new assumptions."?
Regarding the last bullet point, what exactly would the find and replace be?
Aaron Meurer
>> email to sympy+un...@googlegroups.com.
https://github.com/sympy/sympy/pull/7925 to make the new assumptions
read the old assumptions (add handlers). Also, technically,
https://github.com/sympy/sympy/pull/2508/files#diff-e0f95401c86d07d90903363122990de0R227
is a way of doing this as well. I'm undecided on which of these
(including adding to global assumptions) is the best. If you have a
preference, you should argue in the application why you think it's the
best one.
In the execution section, can you give your impression of how
long/hard each item would be (or maybe the timeline is the appropriate
place to do this).
What is the difference between "Making API of old assumptions call new
assumptions internally. The target would be to achieve minimum ripple
effect throughout the codebase as the changes are made." and "Once the
new assumption is ready to handle things, start modifying the codebase
so that expr.is_* syntax calls the new assumptions."?
Regarding the last bullet point, what exactly would the find and replace be?
Aaron Meurer
>> To post to this group, send email to sy...@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/550E8E1E.3060701%40durchholz.org.
>>
>> For more options, visit https://groups.google.com/d/optout.
>
>
>> 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/550E8E1E.3060701%40durchholz.org.
>>
>> 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+un...@googlegroups.com.
> 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
> To post to this group, send email to sy...@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_KCS-B%3D2_bs%2BKJakG3fBucmPVB%2BsFfyYffF8G-RfWvndy%2Bg%40mail.gmail.com.
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
Sudhanshu Mishra
Mar 25, 2015, 2:28:29 PM3/25/15
to sy...@googlegroups.com
Thanks for pointing these out. I'm a bit slow here because of exams.
You should also mention my approach from
https://github.com/sympy/sympy/pull/7925 to make the new assumptions
read the old assumptions (add handlers). Also, technically,
https://github.com/sympy/sympy/pull/2508/files#diff-e0f95401c86d07d90903363122990de0R227
is a way of doing this as well. I'm undecided on which of these
(including adding to global assumptions) is the best. If you have a
preference, you should argue in the application why you think it's the
best one.
Seems like a good plan. I've to say that, I also like this(
https://github.com/sympy/sympy/pull/7926)
approach.But it has a blocking issue of weakref issue in the cache.
I'm adding my views on these in my proposal.
In the executionsection, can you give your impression of how
long/hard each item would be (or maybe the timeline is the appropriate
place to do this).
I though of discussing this with you before writing it. Anyway, I'll write it according to me. We can always alter it later.
What is the difference between "Making API of old assumptions call new
assumptions internally. The target would be to achieve minimum ripple
effect throughout the codebase as the changes are made." and "Once the
new assumption is ready to handle things, start modifying the codebase
so that expr.is_* syntax calls the new assumptions."?
As I've been maintaining two copies of my proposal, this one got duplicated while syncing. Sorry about that. I'll remove one of them.
Regarding the last bullet point, what exactly would the find and replace be?
Replacing the use of old assumptions with the new one.
Sudhanshu Mishra
To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAKgW%3D6LRH3j2ofpbg_PvH0Qf0qoRKJdebk2mL0%2BXEjj5x5vMfg%40mail.gmail.com.
Aaron Meurer
Mar 25, 2015, 6:53:35 PM3/25/15
to sy...@googlegroups.com
Don't forget to submit your proposal in Melange. I don't see it there yet.
Aaron Meurer
> https://groups.google.com/d/msgid/sympy/CAFW_KCRYCx379a3YW82QyJF8gEMnKgfABSVEuiGi3izj%3Dx9ELQ%40mail.gmail.com.
Aaron Meurer
Sudhanshu Mishra
Mar 25, 2015, 6:59:13 PM3/25/15
to sy...@googlegroups.com
Yeah. I'll submit them right now. I'll keep editing later.
I'm submitting my proposal to PSF and NumFOCUS only as it is related to SymPy only.
Sudhanshu Mishra
To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAKgW%3D6%2Br6CtjEQ7j59%3D5d_TiaQ7Q_%2BOn%3DwFpGX6WE4SSg8AdaQ%40mail.gmail.com.
Sudhanshu Mishra
Mar 25, 2015, 7:24:29 PM3/25/15
to sy...@googlegroups.com
I've submitted the proposals(PSF and NumFOCUS). Please confirm if it's visible to you.
Title: "SymPy: Improving assumptions in SymPy"
Sudhanshu Mishra
Aaron Meurer
Mar 25, 2015, 7:42:59 PM3/25/15
to sy...@googlegroups.com
Yep, I see them. You should be able to edit them up to the deadline.
Aaron Meurer
> https://groups.google.com/d/msgid/sympy/CAFW_KCQaURSuFkheAySeqUrhw%3DRdy6Uqtr%3DVvY45zq%2B0PbzRmw%40mail.gmail.com.
Aaron Meurer
Sudhanshu Mishra
Mar 27, 2015, 11:39:59 AM3/27/15
to sy...@googlegroups.com
Aaron,
I've updated(Added more description about execution and added timeline) my proposal on wiki as well as on melange. Please have a look and let me know if it looks good.
Sudhanshu Mishra.
To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAKgW%3D6KfXFCw22PJfc6RZig5ydr2reTR%2BpweR1MeBEX6SrZs9w%40mail.gmail.com.
Aaron Meurer
Mar 27, 2015, 11:53:14 AM3/27/15
to sy...@googlegroups.com
I won't have a chance to look at this until after the deadline.
Aaron Meurer
> https://groups.google.com/d/msgid/sympy/CAFW_KCTc03b0U9Edm%3Dh2qMQUgGu8%2BALMnrwFidn-Fh0PiJUwbw%40mail.gmail.com.
Aaron Meurer
Sudhanshu Mishra
Mar 27, 2015, 11:56:58 AM3/27/15
to sy...@googlegroups.com
Ok no problem. We can discuss that later over here if you have any question for me.
Sudhanshu Mishra
To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAKgW%3D6JMZh6O16%2BvjcW52ESRRAjcczguL2Rouk3k7jubHC0aoA%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages