I got around to making a very lightweight Proof-of-Concept
in https://github.com/sympy/sympy/pull/8664
On Friday, December 19, 2014 10:02:04 PM UTC-6, Aaron Meurer wrote:
>
> On Thu, Dec 18, 2014 at 5:47 PM, Richard Fateman <fat...@gmail.com
> <javascript:>> wrote:
> > Please forgive me if this is off track -- I've never used assumptions in
> > sympy, and
> > don't know much about sympy implementation.
> >
> > But here's a problem that has come up in a number of other computer
> algebra
> > system
> > that are (in some way) linked to a programming language.
> >
> > If you say something about a symbol s, are you saying something about
> > the locally lexically bound symbol s, a binding of the symbol s as the
> > result of
> > (say) pattern matching, a globally bound symbol (in some global symbol
> > table)
> > or something else.
>
> Something to note here is that because SymPy is built on top of
> Python, which is already a programming language in its own right,
> there is a clear distinction between a SymPy Symbol and a Python
> variable. A SymPy Symbol is an object with a string attached to it. A
> Python variable is the name of an identifier used in code to point to
> some Python object. So
>
> a = 1
> a = "hello"
> a = Symbol('a')
> a = Symbol('x')
>
> are all valid ways of assigning different things to the Python
> variable a. In the last two cases, a will point to a SymPy Symbol. In
> the second to last, the name of the Symbol will be the same as the
> Python variable name, but this will be a coincidence. In fact, there's
> not even a way for Symbol to know what variable name it is attached
> to, and the question doesn't even make sense since any object in
> Python can be bound to any number of variable names (including 0).
>
> So there is no binding question. Two Symbol objects are considered the
> same if they have the same name and assumption, regardless of how or
> where they were created. And indeed, since they are immutable and
> SymPy has caching, it's possible (though not guaranteed) that they may
> even end up being the exact same object in memory (this can be tested
> with the Python "is" operator).
>
> It's an important distinction to make semantically, as it's a very big
> point of confusion for new users to SymPy, especially ones who are
> also new to Python, or who may be coming from a language where this
> distinction is not made (i.e., most other computer algebra systems).
> I'm not entirely clear which you meant by "symbols" and "vars" in your
> question. I prefer to refer to SymPy Symbol with a capital S, since
> that is the name of the object in the code, and "Python variable" to
> make it clear that it has nothing to do with SymPy as a Python
> library.
>
> I'd say SymPy is better for being able to make this distinction. SymPy
> Symbols aren't scoped. They are just objects that float around. They
> don't even know where they live. Python variables, which are what
> actually comprise the code, are what are scoped.
>
> If in a language like Lisp I were to take any quoted atom and think of
> that as a mathematical variable, that would lead to a lot of
> confusion. What is 'a? Is it a real number? Is it a complex number? Is
> it a string? Is it a list of lists? It can be any of those things,
> depending on what scope it is in in the language.
>
> > Can any program variable in python have assumptions?
> > Or are declared vars what can have assumptions?
> > Are vars bound in some nice discipline in which they can be shadowed and
> > layered in
> > some way? Are there trees of contexts in which assumptions live (which
> is
> > what Maxima does, but only if you ask.)
>
> The answer is not so easy because as Sergey notes, there are two
> independent systems in SymPy, the so-called old assumptions, which are
> almost as old as SymPy itself (at least as far as I can tell), and the
> new assumptions, which aren't really new anymore, but still lack the
> ability to deduce most things, since most development effort has gone
> into improving the old system.
>
> In the old system, to *apply* an assumption, you put it on a Symbol,
> like Symbol('x', positive=True). You cannot apply an assumption to
> anything other than a symbol in the old assumptions. This creates a
> distinct symbol from Symbol('x'). To ask about an assumption, you
> check an attribute of the object, like x.is_real or
> (2*x).is_nonnegative. This gives True if it is known to be true, False
> if it is known to be False, or None if it can't be deduced (either
> because the algorithms aren't implemented or because it could be
> either). The possible assumptions are hard-coded into the system, and
> the deduction system is fairly simple (though quite fast). Basically,
> deductions are made by computing all possible facts more or less from
> a "transitive closure" of the inferences (it's alpha and beta
> deduction).
>
> In the new assumptions, the assumptions are not really applied. They
> are just facts that you can write down about an expression. You can
> write down a fact about any kind of expression, not just a symbol.
> These facts are like Q.positive(x), Q.negative(x + 1), or
> And(Q.positive(x), Q.negative(x)). To ask about an assumption, you use
> something like ask(Q.negative(x), Q.positive(-x)). This translates to
> "is x negative given that -x is positive?". The output is
> True/False/None again. This uses a combination of some hard-coded
> lookups and a SAT solver.
>
> Note that writing down Q.positive(x) doesn't assume that x is
> positive. It just creates an object that represents that logical
> predicate. That object can later be used in the appropriate places to
> assume this, or to ask about it, or to create large predicates.
>
> There is also some very simple notion of "global" assumptions, i.e.,
> if you use assume(Q.positive(x)), it will enter the fact into some
> global assumptions table, which is used automatically by ask(). You
> can also nest these contexts with with blocks like
>
> with assuming(Q.positive(x)):
> with assuming(Q.whatever(x)):
> ...
>
> This is still proof-of-concept more than anything though. In fact,
> anything "new assumptions" is more or less proof of concept, because
> the actual code in SymPy that implements facts and the code that uses
> the assumptions, e.g., in the solvers, all use the old assumptions
> system.
>
> >
> > There is a whole crowd of people. Well, not such a big crowd really,
> but a
> > bunch
> > of people who write about MKM mathematical knowledge manipulation.
> >
> > If you are embarking on a path to (in effect) re-invent this stuff,
> probably
> > it is
> > a good idea to read about other peoples' (sometimes quite ineffective)
> > approaches.
>
> Some of these approaches have already been reinvented by SymPy, I'm
> sure. This is part of the reason we have two assumptions systems
> (three if you count my approach in
> https://github.com/sympy/sympy/pull/2508, which effectively takes the
> new assumptions system and uses the SAT solver exclusiviely, which
> gives some very powerful possibilities).
>
> >
> > But I may be all wet on whether this is related to sympy.
> >
> > RJF
> >
> > On Wednesday, December 17, 2014 10:20:12 AM UTC-8, Aaron Meurer wrote:
> >>
> >> I agree that the new assumptions can be cumbersome. We should
> >> definitely keep support for old style assumptions syntax (Symbol('x',
> >> positive=True). The downside to it is that that doesn't work for
> >> expressions. Your idea, of basically tying assumptions to an
> >> expression, is interesting. How would Guard (which probably needs a
> >> better name) work in Python? Would it subclass the expression type? If
> >> so, we'd need to fix https://github.com/sympy/sympy/issues/6751.
> >>
> >> OTOH, it is also often very useful to keep assumptions completely
> >> separate from expressions, and we should not disallow that use-case.
> >>
> >> Also, I should point out that you can't use "with" as a method name as
> >> it's a reserved keyword in Python.
> >>
> >> > x.with(Q.positive(x)) + x.with(Q.real(x))
> >> > ---> Guard(2*x,Q.positive(x) & Q.real(x))
> >>
> >> This seems problematic to me. Currently, the way the old assumptions
> >> work, which is fairly sane, is that symbols with the same name but
> >> different assumptions compare different. So Symbol('x', positive=True)
> >> + Symbol('x', real=True) will result in x + x, with the two x's being
> >> distinct symbols.
> >>
> >> I think figuring out the correct thing to do in this case is the key
> >> to getting something like this to work.
> >>
> >> Aaron Meurer
> >>
> >>
> >> On Wed, Dec 17, 2014 at 11:32 AM, Dan Buchoff <daniel....@gmail.com>
> >> wrote:
> >> > This proposal is a little far-reaching, but I think it solves some
> real
> >> > issues with the ease of use of refine and provides a reasonable way
> >> > forward
> >> > for typed symbols.
> >> >
> >> > The problem with refine is that:
> >> > (1) It's wordy. Assumptions on symbols are succinct and easy.
> >> > (2) It requires explicit invocation so it requires the developer to
> >> > refine
> >> > before simplifying and simplify can't take advantage of refinements.
> >> > (3) You must track your simplifying assumptions and since these are
> >> > separate
> >> > from the expression, it's too easy to refine on assumptions that
> later
> >> > don't
> >> > apply.
> >> >
> >> > Introduce a new type: Guard
> >> > Guard(expr,axiom) - an expression which has meaning if the axiom is
> true
> >> > Expr.with(axiom) - turns an expression into a Guard based on the
> given
> >> > axiom
> >> >
> >> > This solves the problem by:
> >> > (1) still allowing assumptions attached to symbols, handling them in
> a
> >> > sane
> >> > way
> >> > (2) tracking your assumptions so they can be used while simplifying
> >> > (3) requiring you to explicitly detach an expression from its
> >> > assumptions
> >> >
> >> > For the simplest case, this provides typed expressions:
> >> > (x**2).with(Q.integer(x))
> >> > ---> Guard(x**2, Q.integer(x))
> >> >
> >> > Axioms distribute over application, so each expression only needs one
> >> > set of
> >> > axioms
> >> > a1.with(p1) + a2.with(p2)
> >> > ---> Guard(a1 + a2, p1 & p2)
> >> >
> >> > x.with(Q.positive(x)) + x.with(Q.real(x))
> >> > ---> Guard(2*x,Q.positive(x) & Q.real(x))
> >> >
> >> > Axioms are taken to be the current assumption context, so rewrite
> rules
> >> > can
> >> > be applied more immediately.
> >> > sqrt(x**2).with(Q.nonnegative(x))
> >> > ---> Guard(x,Q.nonnegative(x))
> >> >
> >> > This elegantly solves the issue of typed expressions by unifying
> their
> >> > assumptions, possibly resulting in a contradiction (which may be
> >> > implemented
> >> > as a special value or a ContradictionError)
> >> > Q.positive(x)+Q.negative(x)
> >> > ---> x.with(Q.positive(x) & Q.negative(x))
> >> > simplify(_)
> >> > ---> Contradiction
> >> >
> >> > Thoughts?
> >> >
> >> > --
> >> > 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/2179e8b1-a241-44ca-a479-3fe2c0f35e4f%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 sympy+un...@googlegroups.com <javascript:>.
> > To post to this group, send email to sy...@googlegroups.com
> <javascript:>.
> > 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/40c5819a-273b-4e33-b697-1db5dde29a73%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 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/b6bc8419-77a1-4092-8ebf-7d446076acd8%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
