assumptions inference

[Andrey Torba]

Hi,

I'm working on the pull request.

A 1x1 matrix is always diagonal. Diagonal implies symmetric. I have fixed AskDiagonalHandler such that this assertion pass:

  V1 = MatrixSymbol('V1', 2, 1)

  V2 = MatrixSymbol('V2', 2, 1)

  expr = V1.T*(V1 + V2)

  assert ask(Q.diagonal(expr)) is True

Now I assume that inference module will deduce that this expression is also symmetric (since the expression is diagonal):

  assert ask(Q.symmetric(expr)) is True                  # it is None!

It returns None. Is anything missing? Can you show an example where this kind of inference works well?

-Andrey

[Aaron Meurer]

This is a downside of the handlers system. The deductions aren't made
based on facts that the handlers return. This is one of the main
deficiencies that the satask/sathandlers system tries to fix. I don't
know if there's an easy fix to make it work in the handlers system.
You could also manually modify the SymmetricHandler class to check for
diagonal (this is obviously annoying, because it blatantly duplicates
the general fact in get_known_facts
https://github.com/sympy/sympy/blob/5827cafb1e1840915b3e7c9f62cd0d58fff9fc48/sympy/assumptions/ask.py#L1517).

The better way to fix it is to implement it in the sathandlers system.
No matrix stuff is implemented there yet, so it may require some
ground work.

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 sympy+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at https://groups.google.com/group/sympy.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/sympy/d84286f8-9a6f-469b-ac95-4a3c8b21cda2%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Andrey Torba]

Aaron, what should be done in order to add new sat handlers?

I'm thinking where to start from? sympy/assumptions/sathandlers.py:

class IsEmptyOr1x1(UnevaluatedOnFree):

    def apply(self):

        return Equivalent(self.args[0], self.expr.shape == (0, 0) or self.expr.shape == (1, 1))

for klass, fact in [

    ...

    (MatrixExpr, IsEmptyOr1x1(Q.diagonal)),

    (MatrixExpr, Implies(Q.diagonal, Q.symmetric)),

    ...

    ]

[Aaron Meurer]

That looks good, although I might try to go for something more general. Maybe we just need a Shape class that we can combine with Eq, like Eq(Shape, (1, 1)) where Shape(A) evaluates as the shape of A. It wouldn't really be a predicate, though, so maybe some more thought is needed here. 

Aaron Meurer 

To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/1e2b221a-2b4a-48f5-b1dc-44ff6ab0db28%40googlegroups.com.

[Aaron Meurer]

Actually, using Eq for tuples seems problematic as well. Maybe just
something like ShapeEq((1, 1)), so the fact would be

Implies(ShapeEq((1, 1)) | ShapeEq((0, 0)), Q.diagonal)

That's just one idea. There's lots of ways you can equivalently write
the same thing. The goal is to make abstractions that make the facts
as readable as possible.

Aaron Meurer

[Aaron Meurer]

And a final thought, empty square and 1x1 matrices have multiple
trivial facts. So probably having EmptySquareMatrix and OneByOneMatrix
classes would be useful. I don't know if my Shape idea would be used
other than for them. This is basically your original idea, except I
think it would be useful to separate them out, since some more things
are true about empty matrices than 1x1 matrices (just glancing at the
existing facts, integer_elements and real_elements both apply, and if
we ever add some kind of Q.elements(fact) meta-predicate for matrices,
that would also apply by vacuous truth).

Aaron Meurer

[Andrey Torba]

How can I resolve "Inconsistent assumptions"? Any techniques how to find what exactly is inconsistent?

  File "sympy/assumptions/satask.py", line 44, in satask

    raise ValueError("Inconsistent assumptions")

  ValueError: Inconsistent assumptions

 I know what rules cause inconsistency, but I can't understand why

Example:

class CheckSquareMatrix(UnevaluatedOnFree):

    def apply(self):

        r, c = self.expr.shape

        return Equivalent(self.args[0], r == c)

class CheckEmptyMatrix(UnevaluatedOnFree):

    def apply(self):

        return Equivalent(self.args[0], self.expr.shape == (0, 0))

class CheckOneByOneMatrix(UnevaluatedOnFree):

    def apply(self):

        return Equivalent(self.args[0], self.expr.shape == (1, 1))

    (MatrixExpr, CheckSquareMatrix(Q.square)),

    (MatrixExpr, CheckOneByOneMatrix(Q.diagonal)),

    (MatrixExpr, CheckEmptyMatrix(Q.zero)),

    (MatrixExpr, Implies(Q.zero & Q.square, Q.diagonal)),

    (MatrixExpr, Implies(Q.diagonal, Q.symmetric)),

    (ZeroMatrix, Q.zero),

    (Identity, Q.diagonal),

[Aaron Meurer]

You have to bisect the facts. There's an open issue to do this
automatically https://github.com/sympy/sympy/issues/8029.

I played with it and I believe the facts
CheckOneByOneMatrix(Q.diagonal)) and CheckEmptyMatrix(Q.zero)) are
wrong. These compile to Equivalent(Q.diagonal(A), A.shape == (1, 1))
and Equivalent(Q.zero(A), A.shape == (0, 0)). But Equivalent is
incorrect here. It should just be reverse implication. Diagonal
matrices are not necessarily 1x1, and zero matrices are not
necessarily empty.

I'm assuming you modeled these after CheckIsPrime. Direct equivalence
handler classes like this should only be used to show the system that
an assumption is equivalent to some computation on an object (e.g.,
Q.prime is equivalent to the isprime() function). No doubt some better
naming, and perhaps some refactoring could make this clearer.

Something like EmptyMatrix would need to be a predicate, not a
handler. Something like

(MatrixExpr, CheckEmptyMatrix(Q.EmptyMatrix))

would be a correct fact.

Finally, your fact Implies(Q.diagonal, Q.symmetric)) is unnecessary
(it's already in the known_facts in ask.py), and Implies(Q.zero &
Q.square, Q.diagonal)) should go in ask.py, since it's a completely
free fact (it's true regardless of what expression you apply it to).

I also want to note that I'm a little worried about the use of Q.zero
to refer to zero matrices. That could lead to problems down the road,
since Q.zero means "real and zero" in the assumptions. However, just
looking at the existing known_facts, I see a lot of inconsistencies
and confusion of numbers and matrices (and operators) in the new
assumptions, so as long as things work, we can probably punt this to
another day.

Aaron Meurer

> https://groups.google.com/d/msgid/sympy/0ea41a27-64fb-4dfb-8ad0-bed1472c7b81%40googlegroups.com.