I implemented the AnyArgs and AllArgs idea in the pull request (I haven't yet written down any facts using it, though).
Aaron Meurer On Sun, Oct 13, 2013 at 9:37 PM, Aaron Meurer <[email protected]> wrote: > As part of my work on the assumptions system in > https://github.com/sympy/sympy/pull/2508, I'd like to be able to > symbolically represent as many facts as possible. > > Some facts are easy to symbolically represent. For instance positive > implies real is represented as Implies(Q.positive, Q.real). Another > example is the fact that if x is zero and y is positive, then x**y is > zero, which can be represented as Implies(And(Q.zero(x), > Q.positive(y)), Q.zero(x**y)). > > However, some facts are not so easy to represent, because they involve > an arbitrary number of terms. An example is that a multiplication is > zero if and only if one of its terms is zero. We can create specific > instances of this fact for specific instances of Mul, for example, for > x*y, we would have Equivalent(Q.zero(x*y), Or(Q.zero(x), Q.zero(y))). > However, I want to be able to represent this fact generically, and > generate the specific instances from that. I'd like to do so > symbolically, so that it becomes possible to reason further about the > fact later on if we would like to, and also so that it is easier to > read. In other words, I could just write something like > > def generate_Mul_zero_fact(mul): > return Equivalent(Q.zero(mul), Or(*(Q.zero(x) for x in mul.args))) > > but that is not so easy to read, and it's impossible to extract the > general fact. > > So I'm wondering if anyone has any ideas about some new Basic object > that could be used to represent this. My thoughts so far were to > create an AnyArgs object (there would also be an AllArgs object) which > would work like Equivalent(Q.zero, AnyArgs(Q.zero)). > > One issue with this construction is that it doesn't contain an > explicit reference to the Mul part of the fact. In the system I've set > up so far this is not an issue, because I store that information > separately, but conceivably we might want to keep this fact on the > object itself. > > Any other thoughts? > > I also was thinking about introducing general quantifier objects, like > forall and exists, though I'm not sure if they would actually help > here (perhaps using ForAll(ArgsOf) instead of AllArgs). We do want to > have those at some point, though. > > 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out.
