Unwanted conversions by function wrapping ?

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...

edit retag close merge delete

Sort by ยป oldest newest most voted

Hello, @Emmanuel Charpentier! I tried various approaches to your code, added print() commands to every line in order to see what is happening internally, studied the code for function, which lead me to FunctionFactory, which lead me to SymbolicFunction, which lead me too your code again, etc., etc., etc. It took me hours, but I couldn't resist the challenge. It bugs me that I couldn't solve your problem. However, in the end, I do believe that I could find an explanation for why you don't get boolean results. Here is my theory: If you make

print(type(And(x>2, 4>3, y<5)))


you will get <class 'sage.symbolic.expression.Expression'>, which makes sense if you think about it, because you are creating a new symbolic function. Anyway, it seems that booleans cannot be coerced to Expressions without being converted to Integers first. For example,

Expression(SR, True)


will return 1, and the similar applies to False and 0.

My appreciation is that this mechanism you use should allow the construction of boolean functions like your And, so I think this should be classified as a bug (?), but I am going beyond my attributions here.

Perhaps a solution to your problem could be make a wrapper function for the wrapper symbolic function. Another solution I can think of is to go low level and try to use something more elementary than function(), e.g., function_factory or perhaps even inherit from BuiltinFunction.

If I make some progress, I'll let you know.

I hope this helps!

EDIT 1: Hello, @Emmanuel Charpentier! Sorry to ping you twice with this question, but, as I promised, I am letting you know that I made some progress in this matter, although it is very anticlimactic.

I've been studying the source code for function(), SymbolicFunction, BuiltinFunction, function_factory and Function. I have tried various approaches at various levels, and nothing worked. I believe the problem is in the class Function, from which the others mentioned inherit. It has a method called __call__, which takes care of the evaluation (you can find it at sage.symbolic.function.pyx; in Sage 9.2, it is at line 436). Unfortunately, this method coerces the arguments to the Symbolic Ring SR, which, as indicated in my text above, converts True and False to 1 and 0, respectively.

You will observe that this method has the arguments coerce and hold. This hold seems to be the same as the one you used in your code, so my best guess is that this method takes care of the low level evaluation of the function (And in your case). You will see the following lines in that method:

if coerce:
try:
args = [SR.coerce(a) for a in args]
...


This seems to what is causing the True-->1 and False-->0 conversion. Unfortunately, setting coerce to False wrecks havoc in the computation, so I have no idea how to solve this.

As I told you, I am just guessing that this __call__ method is indeed the one taking care of the low level evaluation; however, at the very least, it is correct that the true problem is that your code is somehow coercing to the Symbolic Ring.

I only see two solutions: (1) Somehow modify the Function class so that it doesn't coerce boolean arguments, or (2) define your own class BoolFunction that mimics Function (which should inherit from SageObject) or SymbolicFunction (which should inherit from Function), but uses a different evaluation method for boolean arguments. (Perhaps this requires to open a ticket?)

Sorry for not bringing a definitive solution to your problem!

more