On Tue, Aug 26, 2014 at 12:32 AM, Chris Smith <[email protected]> wrote:
>
> Where is it clearly stated what the difference is in the two systems?
It's not written down anywhere, that's why I suggested my first few
bullet points. Ideally there should be no differences, at least
mathematically.
>
> One thing I have noted is what a fog it is writing the routines since it is
> not clear what the routine must do and what will mathemagically be handled by
> the inference system -- and that, especially, I do not understand the
> difference in the two. I know they keep evaluating propositions until a clear
> answer is found but I don't know if there is a significant difference in the
> two in that regard. I know that the new system can handle "is_true"
> expressions and can handle assumptions involving Or (while the old
> assumptions only allow And-based assumptions: var('x', integer=True,
> positive=True).
>
The new system is, ironically, less smart about inferences. It only
actually makes automatic deductions based on the simple known facts at
https://github.com/sympy/sympy/blob/56b613c1394e7b86646574133c0cdfdb7a4cf064/sympy/assumptions/ask.py#L327-L374
(which are compiled into ask_generated.py).
The old assumptions always make deductions from the facts at
https://github.com/sympy/sympy/blob/56b613c1394e7b86646574133c0cdfdb7a4cf064/sympy/core/assumptions.py#L68-L102.
The main difference (aside from the difference in the facts
themselves) is that the old assumptions always compute every fact
every time any assumptions are used on an object. The new assumptions
compute known_facts from the SAT solver, but this is only the very
simple facts in that known_facts dict. Most of it is in the handlers
module, which doesn't use the SAT solver at all.
The new assumptions handlers don't (and really can't) use any
inference, which is why I feel that they are broken. They do do some
recursive calling of ask and other handlers, but this is not
inference. Inference works with any kind of logical expression.
The example of this I like to use is ask(Q.zero(x*y), Q.zero(x) |
Q.zero(y)). It is impossible for the handlers to give True for this,
even though that is the correct answer, because the Mul zero handler
has something like any(ask(Q.zero(i)) for i in expr.args). But given
the assumption Q.zero(x) | Q.zero(y), both Q.zero(x) and Q.zero(y) are
None. You know that one is zero, but you don't know which one.
That's what my branch does better. To write down a fact, you need to
understand it as a logical statement, like (Mul, Equivalent(Q.zero,
AnyArgs(Q.zero))) (for a Mul object, the expression being zero is
logically equivalent to any of the args being zero).
There is a cost to understanding assumptions as precise logical
expressions, but the advantage is that *all* possible inferences are
done. If satask doesn't reach a conclusion, it means that it cannot be
deduced from the facts that it has.
There are other advantages as well, like automatic detection of
logical inconsistencies and clear separation of the facts (data) and
the operations on those facts (code).
>
> One thing I noted today was that the old system can make a calculation based
> on arg(expression) which depends on the old assumptions. I don't know how
> that could be done in the new system. Specifically, I needed to compute, for
> a power, arg(base)*exponent/pi and see whether that was an integer or half
> integer. But arg() needs assumptions to return a value and that's where the
> problem arises. arg uses the old assumptions so if you try to do the
> calculation in the new assumption system (where the symbolic assumptions are
> not available with the symbols) it fails.
This is what I am suggesting to fix with my last bullet point above.
The new assumptions handlers should pull in facts from the old
assumptions, so that ask(Q.real(Symbol('x', real=True))) gives True.
The satask system from my branch handles this at
https://github.com/sympy/sympy/pull/2508/files#diff-e0f95401c86d07d90903363122990de0R172,
although that could be made much more streamlined (especially if the
old and new assumptions had the same definitions!).
>
> As far as passing symbol-based assumptions along to the old system from the
> new, wouldn't something like this be a start?
I'm not clear where these functions would be used. My suggestion is to
add code to sympy/assumptions/handlers so that expr.is_integer would
be checked for ask(Q.integer(expr)).
Aaron Meurer
>
> >>> def assumption(a):
> ... if a.func is Not:
> ... b = False
> ... a = a.args[0]
> ... else:
> ... b = True
> ... if isinstance(a, AppliedPredicate):
> ... return a.func.name, a.args[0], b
> ...
> >>> def update(k, v, d):
> ... if v is not None:
> ... if k in d:
> ... assert v == d[k]
> ... else:
> ... d[k] = v
> ...
> >>> def know(a):
> ... s = {}
> ... d = {}
> ... if a.func is And:
> ... p = a.args
> ... elif isinstance(a, AppliedPredicate):
> ... p = [a]
> ... else:
> ... raise NotImplementedError(a)
> ... for i in p:
> ... k, x, v = assumption(i)
> ... if x not in s:
> ... s[x] = {}
> ... update(k, v, s[x])
> ... return s
> ...
> >>> know(Q.positive(x)&Q.negative(y))
> {x: {'positive': True}, y: {'negative': True}}
>
> --
> You received this message because you are subscribed to the Google Groups
> "sympy" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To post to this group, send email to [email protected].
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/sympy/63b54e60-6538-4c7e-8f1f-155990dd6ac1%40googlegroups.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 [email protected].
To post to this group, send email to [email protected].
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%3D6KWofC6CmaJ5FUxRZkHG4z1ZwhO%2B4NhAs4-1wvbH2kMJA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.
