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.
