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.