This one is slowly but surely driving me crazy...
I am trying to get a template to define boolean symbolic functions, which could be used to translate some sympy or mathematica results back to Sage. Sage's symbolic logic module is irrelevant, being an implementation of propositional logic, whereas, the aim of this implementation is to manipulate variables-rich symbolic expressions, which would entail first-order predicate logic...
For a first try, I decided to use Sympy's boolean functions, which do what I think is the Right Thing (TM), using function
to wrap them in Sage symbolic functions.
My current attempt for And
is as follows :
import sympy
from sympy import sympify, And as SAnd, Or as SOr, Not as SNot
STrue=sympify(True)
SFalse=sympify(False)
def And_eval_func(self, *args):
R = SAnd(*map(sympify, args))
# To debug...
if R in {STrue, SFalse}:
print("Expect boolean...")
return bool(R._sage_())
if R.func is SAnd : return self(*R.args, hold=True)
return R._sage_()
And=function("And",
eval_func = And_eval_func,
conversions = {"sympy":"And", "mathematica":"And"},
print_latex_func=lambda self, *args:\
r" \wedge ".join(map(latex, args)))
setattr(sympy.And, "_sage_",
lambda self, *args:And(*map(lambda u:u._sage_(), args), hold=True))
That gives some nice results :
sage: And(x>2, 4>3, y<5)
And(x > 2, y < 5)
The constant 4>3
(which is True
) is correctkly eliminated, the symbolic inequations being respected :
But this one bugs me :
sage: And(x>2, 4<3, y<5)
Expect boolean...
0 # `False` expected...
The culprit seems to be the wrapping in a symbolic function ; without this wrappping, the expected results is obtained by And_eval_func
:
sage: And_eval_func(And, x>2, 4<3, y<5)
Expect boolean...
False # As expected...
However, the _sage_
conversions for inequalities might be responsible :
sage: And(x>2, 4>3, y<5).subs(x==4)
And(1, y < 5)
Correct, but the substitution does not trigger a reevaluation, and the constant 4>2
(which should print as True
) is not eliminated.
sage: And(x>2, 4>3, y<5).subs(x==4).subs(y==0)
1
Ditto, but this time, the second substitution somehow triggers a reevaluation which does not use And_eval_func
The problem might be more fundamental : from True?
:
The class bool is a subclass of the class int, and cannot be subclassed.
Hence two questions :
1) Do you see a workaround using function
?https://doc.sagemath.org/html/en/reference/logic/index.html
2) Are there special caution to,take against this shenanigan when writing a proper library function ?
Any hint is welcome. Mayday...