Fix inconsistency of != with is_zero() and matrix symmetry

[cxzhong]

Problem Description

The Bug

When symbolic variables are declared with domain constraints (e.g., domain='real'), there was an inconsistency between the behavior of the != operator and the is_zero() method:

sage: var('x12', domain='real')
sage: bool(x12 != 0)
False                        # Incorrect: should be True
sage: x12.is_zero()
False                        # Correct

sage: bool(x12 != 0) == (not x12.is_zero())
False                        # Inconsistent!

Impact

This bug caused incorrect behavior in matrix operations. For example, a triangular matrix was incorrectly identified as symmetric:

sage: var('x11 x12 x22', domain='real')
sage: M = matrix([[x11, x12], [0, x22]])
sage: M.is_symmetric()
True                         # Wrong! Should be False

# The matrix was considered symmetric because:
# M[0,1] != M[1,0]  =>  x12 != 0  =>  bool(x12 != 0) = False
# So Sage incorrectly concluded x12 == 0

Root Cause

The _bool_ method in expression.pyx is not compatible with the check_relation_maxima function. When they deal with ne. Because maxima said a!=b is unknown, check_relation_maxima returns False. But when we use a!=b, python consider it as not a==b. so it return True.

Fix #41125

📝 Checklist

• The title is concise and informative.
• The description explains in detail what this PR is about.
• I have linked a relevant issue or discussion.
• I have created tests covering the changes.
• I have updated the documentation and checked the documentation preview.

⌛ Dependencies

[mantepse]

Why did you close this?

[cxzhong]

Why did you close this?

This bool method is very fragile

Some small changes will break doctests. And maybe will raise bugs I do not know

[mantepse]

For the record: the proposed fix leads to

sage: var("x y")
(x, y)
sage: bool(x != y)
False
sage: bool(x - y != 0)
True

The specification of __bool__ is

    Return ``True`` unless this symbolic expression can be shown by Sage
    to be zero.  Note that deciding if an expression is zero is
    undecidable in general.

So, in principle, returning a wrong True is OK, but returning a wrong False is not.

Is there documentation for decide_relational(self._gobj)?

[cxzhong]

For the record: the proposed fix leads to

sage: var("x y")
(x, y)
sage: bool(x != y)
False
sage: bool(x - y != 0)
True

The specification of __bool__ is

    Return ``True`` unless this symbolic expression can be shown by Sage
    to be zero.  Note that deciding if an expression is zero is
    undecidable in general.

So, in principle, returning a wrong True is OK, but returning a wrong False is not.

Is there documentation for decide_relational(self._gobj)?

But the fixes will break somethings, I think it will need to refactor the whole sage's lib

[mantepse]

Yes, that's what I said. The proposed fix is incorrect, but

sage: y = SR.var("y")
sage: bool(y != 0)
True
sage: y = SR.var("y", domain="real")
sage: bool(y != 0)
False

is simply a bug.

[cxzhong]

@mantepse I have fixed it minimally, and it do not affect other parts.

[cxzhong]

Just try to patch this in this way, it does not involved many changes. real complex integer do not provide information about whether it is zero or not.

[mantepse]

I think that the direction is good, but we are not quite there yet. I think it should depend on the operator which assumptions we have to take into account.

Currently (i.e., without your patch), do we reach return check_relation_maxima(self)?

[cxzhong]

CC: @orlitzky

[cxzhong]

I think that the direction is good, but we are not quite there yet. I think it should depend on the operator which assumptions we have to take into account.

Currently (i.e., without your patch), do we reach return check_relation_maxima(self)?

Yes, we reach this maxima part directly after it return NotImplement from gianc without this patch. Because the system think it is with assumptions. But these assumptions do not provide any informations

[cxzhong]

And you can see the domain assumptions are GenericDeclaration.

[cxzhong]

And I think it is also not a good ideal. Because it will not fix the root cause. And I believe there are new bugs we do not discover. This patch only patches for this case.

[mantepse]

The guideline we've been striving for (and which maxima generally tries as well) is that bool(A==B) should be true if it can be shown that equality hold for all free variables (hopefully taking into account assumptions on them). The "safe" thing is that we return false when we don't succeed in showing that.

I thought so until yesterday, when I learned on the maxima mailing list that this is not the case:

Does this mean that is(equal(a, b)) is false if and only if the function (a, b) \mapsto a-b does not have any zeros?

Yes.

I now see that I was not as precise as I should have been. What I meant to say is that

is(equal(a, b)) is false if and only if a-b, considered as a function from the variables appearing in a and b, does not have any zeros

In particular, this explains why the maxima manual contains

(%i8) is (equal (x, y));
(%o8)                        unknown

However, with our specification, bool(x == y) should clearly be false.

[cxzhong]

It seems Ok. Do not affect other parts doctests

[nbruin]

In particular, this explains why the maxima manual contains

(%i8) is (equal (x, y));
(%o8)                        unknown

Interesting! Indeed even is(equal(x,x^2)) returns unknown and is(equal(x,x+1))does returnfalse. So their trueis still useful for us, but theirunknownreally does include many cases where we definitely wantfalse. Note that their is(notequal(x,x^2))is equally picky and returns a lot ofunknown. Indeed, it's documented as the negation of equal, but then in tristate logic, where unknown` is its own negation.

[cxzhong]

In particular, this explains why the maxima manual contains

(%i8) is (equal (x, y));
(%o8)                        unknown

Interesting! Indeed even is(equal(x,x^2)) returns unknown and is(equal(x,x+1))does returnfalse. So their trueis still useful for us, but theirunknownreally does include many cases where we definitely wantfalse. Note that their is(notequal(x,x^2))is equally picky and returns a lot ofunknown. Indeed, it's documented as the negation of equal, but then in tristate logic, where unknown` is its own negation.

In fact, many mathematical software use tristate logic, including mathematica sympy and so on.

But our sagelib codes have many != and they use if !=. python if only accept bool. So it will affect the whole sagelib. It need much work.

[nbruin]

In fact, many mathematical software use tristate logic, including mathematica sympy and so on.

But our sagelib codes have many != and they use if !=. python if only accept bool. So it will affect the whole sagelib. It need much work.

In that case it may make sense to make a (partial) inventory of != occurrences that lead to wrong behaviour with SR, like the is_symmetric test for matrices here. If that inventory gets long enough then that makes the case stronger that != on SR should be made into the logical negation of ==. Perhaps strong enough to overrule the otherwise reasonable argument that the tristate logic of equal and notequal in maxima should round unknown to false in either case.

This would definitely require discussion on sage-devel: the current behaviour in sage has been around for quite a while, so there are going to be people out there who rely on that behaviour. For the change to happen, one would need to argue that correct behaviour throughout the sagemath library is more important than the convenience of backwards compatibility. The thing is: a lot of the functionality in sagemath doesn't work well with SR anyway, so there is little use in increasing correctness for this particular thing. That's why a convincing inventory will help make a case.

[cxzhong]

In fact, many mathematical software use tristate logic, including mathematica sympy and so on.

But our sagelib codes have many != and they use if !=. python if only accept bool. So it will affect the whole sagelib. It need much work.

In that case it may make sense to make a (partial) inventory of != occurrences that lead to wrong behaviour with SR, like the is_symmetric test for matrices here. If that inventory gets long enough then that makes the case stronger that != on SR should be made into the logical negation of ==. Perhaps strong enough to overrule the otherwise reasonable argument that the tristate logic of equal and notequal in maxima should round unknown to false in either case.

This would definitely require discussion on sage-devel: the current behaviour in sage has been around for quite a while, so there are going to be people out there who rely on that behaviour. For the change to happen, one would need to argue that correct behaviour throughout the sagemath library is more important than the convenience of backwards compatibility. The thing is: a lot of the functionality in sagemath doesn't work well with SR anyway, so there is little use in increasing correctness for this particular thing. That's why a convincing inventory will help make a case.

My idea is that the == behavior in expression is clear, which means we can verify its equal as expressions clearly. So we can write in document that we define != by not ==.

Then I think it is a uniform way to define nonequal. we should make each part to define in this way.

[cxzhong]

This would definitely require discussion on sage-devel: the current behaviour in sage has been around for quite a while, so there are going to be people out there who rely on that behaviour. For the change to happen, one would need to argue that correct behaviour throughout the sagemath library is more important than the convenience of backwards compatibility. The thing is: a lot of the functionality in sagemath doesn't work well with SR anyway, so there is little use in increasing correctness for this particular thing. That's why a convincing inventory will help make a case.

It only affects the behavior of expression. It is the cost that we need to be compatible for bool system in fact it is a tristate logic system. sometimes we need to be stricter.

[nbruin]

I agree that defining != as the logical negation of == is clear and quite defensible. It's just that it requires a non-compatible change in behaviour for SR. I've tried to search the sagemath documentation for != usage on SR elements and found surprisingly little! Perhaps the design choice around this hasn't been made so consciously. We'd still have to check with the community on sage-devel, but I wasn't able to find any documentation that defines the != semantics for SR. That's at least a little less friction.

I do think it's cleaner to implement the changed behaviour in

sage/src/sage/symbolic/expression.pyx

Lines 3437 to 3441 in 5c8d9e9

	from sage.symbolic.relation import check_relation_maxima
	if self.variables():
	return check_relation_maxima(self)
	else:
	return False

rather than maxima_check_relation (because that routine is well-documented and does what it claims). There is some shenanigans with == vs. != earlier on in the file already, so perhaps that can be used to straighten out the code.

[nbruin]

Particularly this fragment:

sage/src/sage/symbolic/expression.pyx

Lines 3391 to 3401 in 5c8d9e9

	if self.operator() == operator.ne:
	# this hack is necessary to catch the case where the
	# operator is != but is False because of assumptions made
	m = self._maxima_()
	s = m.parent()._eval_line('is (notequal(%s,%s))' % (repr(m.lhs()),repr(m.rhs())))
	if s == 'false':
	return False
	else:
	return True
	else:
	return True

It deals with a similar problem but does its own conversion to/from maxima. That's not a smart idea: the purely strings-based conversion there is significantly less sophisticated than what our standard to/from maxima interface does (and probably a bit slower too!). I'd expect this can be refactored together with the invocation of maxima further down below.

[cxzhong]

I agree that defining != as the logical negation of == is clear and quite defensible. It's just that it requires a non-compatible change in behaviour for SR. I've tried to search the sagemath documentation for != usage on SR elements and found surprisingly little! Perhaps the design choice around this hasn't been made so consciously. We'd still have to check with the community on sage-devel, but I wasn't able to find any documentation that defines the != semantics for SR. That's at least a little less friction.

I do think it's cleaner to implement the changed behaviour in

sage/src/sage/symbolic/expression.pyx

Line 3437 in 5c8d9e9

from sage.symbolic.relation import check_relation_maxima

rather than maxima_check_relation (because that routine is well-documented and does what it claims). There is some shenanigans with == vs. != earlier on in the file already, so perhaps that can be used to straighten out the code.

But one problem is that the check_relation_maxima we use in this bool function has already violate the document of bool function. It said that only we can verify it is zero return False. the behavior of check_relation_maxima and bool will be contradict in the documents with only bool system. @nbruin @mantepse

[cxzhong]

Another way is that we can add a check_maxima_relation_2 function or other names is only for bool on expression used

[cxzhong]

bool want to check != by not ==. But check_maxima want to check != if it is really noequal at all. It is contradict in bool system we just have True and False.

[cxzhong]

@nbruin Do you think it is OK to add a new function such that regards != as not ==

[mantepse]

I think it would be important to do this systematically, rather than fiddling around.

Let expr be an expression in n variables x, y, .... I think we first need to check whether the following definitions and conventions are currently used in SageMath:

• the default domain of a variable is currently $\mathbb C$, see assumptions.py, line 22.
• we regard expr as a map from a subset of $\mathbb C^n$ - defined by assumptions() - to $\mathbb C$.
• we do not make any assumptions like continuity or even stronger assumptions.
• by definition bool(expr != 0) is the same as bool(expr), which is False only if SageMath can show that expr is the zero map, i.e., vanishes for all values of the variables in the specified domain.
• there is currently no definition for bool(expr == 0).

Assuming that the above is true (which I somewhat doubt), we have two possibilities for a definition of bool(expr == 0).

1.) it could be the same as not bool(expr != 0) - in this case, it would be True only if SageMath can show that expr is the zero map, or
2.) it could be False only if SageMath can show that expr is not the zero map.

I think it would be good to make this consistent with lazy power series, where we cannot test for zero either:

    def __bool__(self):
        """
        Test whether ``self`` is not zero.

        When the halting precision is infinite, then any series that is
        not known to be zero will be ``True``.

Apart from that, we also need to decide what is_symmetric is supposed to return:

a) return True only if SageMath can show that the matrix is symmetric, or
b) return False only if SageMath can show that the matrix is not symmetric.

(Note that this has no relevance to the original bug report, because in that case SageMath should have no trouble deciding that the matrix is non-symmetric.)

Finally, is it possible to have a general policy for methods like is_symmetric? Or is it better to decide on a per method basis? If we decide on the latter, this would need to be documented in every method!

[cxzhong]

Apart from that, we also need to decide what is_symmetric is supposed to return:

a) return True only if SageMath can show that the matrix is symmetric, or b) return False only if SageMath can show that the matrix is not symmetric.

We can not do that. Because like this issue

sage: X.is_symmetric()

Do you expect it is True or False. In fact because x in RR, It can be True and can be False. It is undecided.
We can not do that True is for mathematical ==, and False is for mathematical !=. unless we do not use bool system
The thing we only can do is

Return ``True`` if this is a symmetric matrix. 

This is said in the document of matrix0.pyx, it is equivalent with
Return True if and only if this is a symmetric matrix.
I think this version makes more sense. In fact we do not want it to return True for such case.

[cxzhong]

some strange things, In this https://groups.google.com/g/sage-devel/c/hGOw9X2X9xQ/m/UpsjvNfOBQAJ

sage: R.<t> = QQ[[]]
sage: f = t.add_bigoh(5) - t
sage: f
O(t^5)
sage: not f
True
sage: bool(O(t^5)) == False
True
sage: bool(t + O(t^5))
True
sage: t + O(t^5)==0
False
sage: O(t^5)==0
True
sage: not O(t^5)
True
sage: not O(t^5)==0
False
sage: O(t^5)
O(t^5)
sage: bool(O(t^5)) == False
True

It is also preserve that != is not ==. But the mathemtical behavior looks like strange

[fchapoton]

just my little grain of sand: maybe #38707 is relevant

[cxzhong]

just my little grain of sand: maybe #38707 is relevant

Thank you very much.

[nbruin]

just my little grain of sand: maybe #38707 is relevant

I think that's a different issue. symbolic.expression.__bool__ already has code to convert to equal. The problem is that the mathematical meaning of notequal in maxima is not compatible with our definition if we round unknown to false. For our definition, we need to round unknown to `true.

There are some further issues, particularly in sage.symbolic.relation.test_relation_maxima that are not specifically math-related:

• the relation is first coarsely translated to maxima to check some trivial cases. There = and # are encountered but they are only used for a string check. This seems like a very expensive first step to optimize for some very questionable cases
• later on it uses maxima's _eval_line, which means expressions get translated to maxima purely via string representation. Our standard conversion-to-maxima is much more sophisticated (taking care to translate subtly different function names, avoiding clashes in variable names, etc) and possibly faster too.
• by doing these conversion stringwise, we end up with variables like x, whereas the sage assumption management system probably converts those variables to _SAGE_VAR_x. So it's not clear to me that test_relation_maxima can even take assumptions into consideration properly.

On top of that, sage.symbolic.expression.__bool__ has some logic that should be straightened out:

• if it finds a '!=" relation it goes to maxima in its own, hand-crafted block.
• then it checks if assumptions are needed because a false result from pynac may not have taken assumptions into account. But that's basically the same reason why != needs more care! So that part needs to be refactored.

So I think three things need to happen:

• community consultation on changing when A != B returns true in sage (I don't think we have a choice, but people may need warning)
• clean up test_relation_maxima to do conversion between sage and maxima properly
• refactor __bool__ to better express intent. At that point, I suspect we might as well only do == and hard-wire != to be the logical negation.

So @cxzhong : no I don't think just adding another version of test_relation_maxima is sufficient.

[cxzhong]

maybe the code is written very long ago. I try to make it more clear and readable and speed up it. @nbruin Thank you very much

[cxzhong]

I found that we do not have compare equal and inequal in the maxima interface. we have to use _eval_line to do this.

[cxzhong]

@nbruin Thank you for your reviewing. I found that pynac can deal with assumptions too. and it will True for the absolutely right case. So we can delete such maxima logic in pynac. But and if pynac return notimplement (for this bug issue it will return notimplement instead of False or True, I just check this), then turn to assumption check, if no assumption, turn to interval field check logic. Otherwise turn to maxima path. I do not use special cases like before. they all turn to by maxima_init logic. I think in this way we can deal with assumptions better. But I do not find how to deal with equal and inequal in maxima interface. I have to use _eval_line. I think now is better. and it just broke a doctest in expression. If we need bool(a!=b) == not bool(a==b), the doctest is wrong.

[nbruin]

I found that pynac can deal with assumptions too.

Make sure to check some more complicated examples! Blame shows that the more elaborate handling of != goes back to #1163. There are many interesting cases discussed there that didn't make it into the doctests. I think particularly: #1163 (comment) may be relevant.

I expect the code can be refactored, but it looks like they had a particular reason to give extra attention to != through Pynac (which hasn't developed very much since, so I expect that whatever issue existed then would still exist now).

Avoiding string parsing for maxima is a matter of reaching into maxima_lib a little more. That's straightforward. I can do that in a few weeks, when I may have a bit more time.

EDIT: Here's a quick fragment for doing the equality tests without relying on string conversions (mostly). Part of this code would probably be best incorporated in maxima_lib, where it would live most comfortably. Then you can just import test_max_equal and test_max_notequal from there.

The code just uses the ECL interface to construct the appropriate lisp structure for the desired maxima operation and then calls the maxima evaluator on that. We're doing this construction via the basic (and hopefully fast) lisp library constructors. The wrapper objects of lisp functions (this is what maxima_eval is) automatically try to transform their arguments into EclObjects and the nested (python) list structure is encoding the right thing for that.

from sage.interfaces.maxima_lib import maxima_eval, max_to_sr, sr_to_max
from sage.libs.ecl import EclObject
max_equal = EclObject("$EQUAL")
max_notequal = EclObject("$NOTEQUAL")
max_is = EclObject("$IS")
test_max_equal = lambda A,B: maxima_eval([[max_is],[[max_equal],sr_to_max(A),sr_to_max(B)]]).python()
test_max_notequal = lambda A,B: maxima_eval([[max_is],[[max_notequal],sr_to_max(A),sr_to_max(B)]]).python()

#example
test_max_equal(x,x^2)
test_max_notequal(x,x+1)

As background info, maxima_lib interface objects have their ecl representation accessible. That gives you some insight into how maxima represents its expressions internally:

sage: maxima_calculus(sin(x^2)).ecl()
<ECL: ((%SIN SIMP) ((MEXPT SIMP) |$_SAGE_VAR_x| 2))>

[cxzhong]

I found that pynac can deal with assumptions too.

Make sure to check some more complicated examples! Blame shows that the more elaborate handling of != goes back to #1163. There are many interesting cases discussed there that didn't make it into the doctests. I think particularly: #1163 (comment) may be relevant.

I just test #1163 It is right now. I think some bugs in gianc and maxima have been fixed.
Edit: Note that:

sage: assume(x > 0)
sage: sqrt(x^2)
x
sage: assume(x < 0)
sage: sqrt(x^2)
x

is wrong. we can not assume(x>0) and assume(x<0).