sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.43k stars 479 forks source link

Boolean symbolic expressions #31911

Open mkoeppe opened 3 years ago

mkoeppe commented 3 years ago

As proposed in https://groups.google.com/g/sage-devel/c/U_WGbYG2zOE/m/yq-EDEXDAgAJ

We add symbolic functions and_symbolic, or_symbolic, not_symbolic; the first two are also accessible by repurposing the operators bitwise-and & and bitwise-or |.

By extending the expression parser to also handle & (equivalently, infix and), | (equivalently, infix or), and ~ (equivalently, prefix not), these constructions can also be obtained as a conversion from maxima and giac expression strings.

One application is for the coordinate restrictions of a Chart.

Depends on #32383

CC: @EmmanuelCharpentier @nbruin @egourgoulhon @fchapoton @spaghettisalat @kcrisman

Component: symbolics

Work Issues: Parser: Use a make_... function instead of importing and_symbolic...

Author: Matthias Koeppe

Branch/Commit: u/mkoeppe/boolean_symbolic_expressions @ e9eac61

Issue created by migration from https://trac.sagemath.org/ticket/31911

7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:43

Something is fishhy in the maxima__>Sage conversion :

sage: maxima("(a>0) and (b<0)")                                                 
a>0andb<0
sage: maxima("(a>0) and (b<0)")._sage_()                                        
and_symbolic(a > 0, 0 < 0)
mkoeppe commented 3 years ago
comment:44

Yes, see comment:10 -- I have not figured out maxima conversion -- hoping for help from the experts

mkoeppe commented 3 years ago
comment:45
sage: maxima("(a>0) and (b<0)")                                                 
a>0andb<0

Didn't you fix the whitespace-eating behavior some time recently?

mkoeppe commented 3 years ago
comment:46

Note

sage: sage.calculus.calculus.symbolic_expression_from_string("a>0andb<0", accept_sequence=True)                          
and_symbolic(a > 0, 0 < 0)
sage: sage.calculus.calculus.symbolic_expression_from_string("a>0and b<0", accept_sequence=True)                         
and_symbolic(a > 0, b < 0)
sage: sage.calculus.calculus.symbolic_expression_from_string("0andb", accept_sequence=True)                              
0
mkoeppe commented 3 years ago
comment:47

Our expression parser has poor error checking and silently ignores unexpected trailing tokens in some situations:

sage: sage.calculus.calculus.symbolic_expression_from_string("0fffffif", accept_sequence=True)                           
0
mkoeppe commented 3 years ago
comment:48

Actually, this is just implicit multiplication 0*fffffif, which gets simplified to 0.

mkoeppe commented 3 years ago
comment:49

Replying to @mkoeppe:

sage: maxima("(a>0) and (b<0)")                                                 
a>0andb<0

Didn't you fix the whitespace-eating behavior some time recently?

I see, that's #31796, which appears to be stuck

mkoeppe commented 3 years ago

Changed dependencies from #32315 to #32315, #31796

7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:51

Replying to @mkoeppe:

sage: maxima("(a>0) and (b<0)")                                                 
a>0andb<0

Didn't you fix the whitespace-eating behavior some time recently?

I tried. But this patch entailed other bugs, which I hanven't yet understood == back to the old drawing board...

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from bb06156 to 644d831

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

b5e4168Trac #32315: support iteration and enumerated sets
e0a8145Merge #32315
767e89aTicket #31796 : make maxima output parseable.
d7abbe6MaximaAbstract._commands: Remove whitespace in apropos output before breaking it apart
644d831Merge #31796
mkoeppe commented 3 years ago
comment:53

Now, with the repaired #31796 merged, the problem is fixed:

sage: maxima("(a>0) and (b<0)")                                                                                    
a > 0 and b < 0
sage: maxima("(a>0) and (b<0)")._sage_()                                                                           
and_symbolic(a > 0, b < 0)
mkoeppe commented 3 years ago
comment:54

I'm setting this again to needs_review so that the patchbot runs; obviously more work is needed.

7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:55

Replying to @mkoeppe:

Now, with the repaired #31796 merged, the problem is fixed:

sage: maxima("(a>0) and (b<0)")                                                                                    
a > 0 and b < 0
sage: maxima("(a>0) and (b<0)")._sage_()                                                                           
and_symbolic(a > 0, b < 0)

Thanks a lot ; I was searching in that direction, but missed the target you reached masterfully. Kudos !

BTW : "something" translating Maxima's is would be as useful as a translation of Maxima's and, or and not, necessary for the present ticket :

(%i3) is(a>2);
(%o3)                               unknown
(%i4) is(subst([a=3],a>2));
(%o4)                                true

Not coincidentally, it has the same Sage syntax collision problem...

Shouldn't it be added to this ticket ? Alternatively, we could create a new ticket for this and and depend on it.

mkoeppe commented 3 years ago
comment:56

Could you elaborate on is? What collides with what?

mkoeppe commented 3 years ago

Changed dependencies from #32315, #31796 to #32315, #31796, #32379

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

f1e2fe0NotSymbolic, not_symbolic: New
f492321src/sage/symbolic/expression_conversions.py: Make a docstring raw
4aec1e8Merge #32379
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from 644d831 to 4aec1e8

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

175e523src/sage/functions/boolean.py: Remove unused imports
218b2d6and_symbolic, or_symbolic, not_symbolic: Add global bindings
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from 4aec1e8 to 218b2d6

mkoeppe commented 3 years ago

Description changed:

--- 
+++ 
@@ -1,4 +1,7 @@
 As proposed in https://groups.google.com/g/sage-devel/c/U_WGbYG2zOE/m/yq-EDEXDAgAJ

+We add symbolic functions `and_symbolic`, `or_symbolic`, `not_symbolic`; the first two are also accessible by repurposing the operators bitwise-and `&` and bitwise-or `|`.

-One application is for the restrictions of a `Chart`.
+By extending the expression parser to also handle `&` (equivalently, infix `and`) and `|` (equivalently, infix `or`), these constructions can also be obtained as a conversion from `maxima` and `giac` expression strings.
+
+One application is for the coordinate restrictions of a `Chart`.
7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:61

Replying to @mkoeppe:

Could you elaborate on is? What collides with what?

is is a Sage operator, roughly equivalent to Lisp's eq :

sage: x.parent() is SR
True

Therefore, the Maxima's is can't be translated by the mechanism used for Maxima's functions :

sage: maxima.is(x>0)
  File "<ipython-input-6-e177b9fc4016>", line 1
    maxima.is(x>Integer(0))
           ^
SyntaxError: invalid syntax

sage: maxima_calculus.is(x>0)
  File "<ipython-input-7-dea1cf49bee0>", line 1
    maxima_calculus.is(x>Integer(0))
                    ^
SyntaxError: invalid syntax
mkoeppe commented 3 years ago
comment:62

A simple workaround for this is:

sage: getattr(maxima, 'is')(x>0)                                                                                         
unknown
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

4094035src/sage/interfaces/sympy.py: Handle Not
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from 218b2d6 to 4094035

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

a9302a6NotSymbolic: Add sympy test
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from 4094035 to a9302a6

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

d202804src/sage/functions/boolean.py: Add conversions to giac
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from a9302a6 to d202804

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

700e84bsrc/sage/functions/boolean.py: Add conversions to maxima
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from d202804 to 700e84b

mkoeppe commented 3 years ago
comment:67

Replying to @mkoeppe:

For converting to maxima, some help would be welcome.

I think I figured a solution

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Changed commit from 700e84b to 392926c

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 3 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

392926cParser.p_eqn: Handle 'not', '~'
7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:69

Still problematic :

sage: not_symbolic((a>0) & ((b<0) | (x!=0))).simplify()
a <= 0

Worse :

sage: ((a>0) | (x!=0)).simplify()
1

BTW :

sage: ~((a>0) & ((b<0) | (x!=0)))
1/and_symbolic(a > 0, or_symbolic(b < 0, x != 0))
mkoeppe commented 3 years ago
comment:70

Indeed:

sage: var('a,b')                                                                                                         
(a, b)
sage: ((a>0) | (x!=0)).simplify()                                                                                        
1
sage: ((a>0) | (x!=0))._maxima_()                                                                                        
true
sage: ((a>0) | (x!=0))                                                                                                   
or_symbolic(a > 0, x != 0)
sage: f = ((a>0) | (x!=0))                                                                                               
sage: f._maxima_init_()                                                                                                  
'(_SAGE_VAR_a > 0) or (_SAGE_VAR_x # 0)'
sage: maxima(_)                                                                                                          
true
sage: (x!=0)._maxima_()                                                                                                  
_SAGE_VAR_x # 0
sage: (a>0)._maxima_()                                                                                                   
_SAGE_VAR_a > 0
sage: maxima('(a>0) or (x # 0)')                                                                                         
true

Is this a maxima bug?

mkoeppe commented 3 years ago
comment:71

Replying to @EmmanuelCharpentier:

BTW :

sage: ~((a>0) & ((b<0) | (x!=0)))
1/and_symbolic(a > 0, or_symbolic(b < 0, x != 0))

Yes, this is as discussed in comment:29, comment:38.

mkoeppe commented 3 years ago
comment:72

Replying to @mkoeppe:

Is this a maxima bug?

Minimal example in plain maxima 5.45.0:

(%i8) (x#0);
(%o8)                                x # 0
(%i9) (x#0) or (x#0);
(%o9)                                true
mkoeppe commented 3 years ago
comment:73

I think our translation of Python's == and != to = and # on the Maxima side is wrong, and we should use equal and notequal instead - see https://maxima.sourceforge.io/docs/manual/maxima_169.html (Special operator: if)

7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:74

Replying to @mkoeppe:

Replying to @mkoeppe:

Is this a maxima bug?

Minimal example in plain maxima 5.45.0:

(%i8) (x#0);
(%o8)                                x # 0
(%i9) (x#0) or (x#0);
(%o9)                                true

Did you (or do you plan to) report it in Maxima's bug report system ?

BTW : Sympy's logical functions seem exempt from this bug :

sage: foo = x!=0
sage: sympy.And(*map(lambda u:u._sympy_(), (foo, foo)))._sage_()
x != 0
sage: sympy.Or(*map(lambda u:u._sympy_(), (foo, foo)))._sage_()
x != 0
sage: sympy.Not(foo._sympy_())._sage_()
x == 0

Wrapping Sympy's functions may be a quick way out (that was my initial plan...).

7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:75

Replying to @mkoeppe:

I think our translation of Python's == and != to = and # on the Maxima side is wrong, and we should use equal and notequal instead - see https://maxima.sourceforge.io/docs/manual/maxima_169.html (Special operator: if)

Doesn't seem to be a question of precedence :

(%i9) x#0 or x#0;

(%o9) true
(%i10) (x#0) or (x#0);

(%o10) true
mkoeppe commented 3 years ago
comment:76

No, I no longer think this is a Maxima bug.

I think it is a bug in our interface sage.interfaces.maxima_abstract. There are already two places that work around it (by using equal, notequal): Expression._maxima_init_assume_ and test_relation_maxima.

mkoeppe commented 3 years ago
comment:77

See the early tickets #1163, #2218

7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:79

Replying to @mkoeppe:

No, I no longer think this is a Maxima bug.

I think it is a bug in our interface sage.interfaces.maxima_abstract. There are already two places that work around it (by using equal, notequal): Expression._maxima_init_assume_ and test_relation_maxima.

Indeed, the documentation is quite clear : = and # : syntactic (in)equality (i. e. isomorphic structures) ; equal and unequal : value (= structural) (in)equality.

This might be a heavy change. Separate ticket, separately tested ?

mkoeppe commented 3 years ago

Changed dependencies from #32315, #31796, #32379 to #32315, #31796, #32379, #32383

mkoeppe commented 3 years ago
comment:80

Yes, I agree. There is a big potential for breakage. I've opened #32383 for it.

7822f248-ba56-45f1-ab3d-4de7482bdf9f commented 3 years ago
comment:81

A possible plan B (independent of the Maxima snag) is to wrap Sympy's symbolic functions And, Or and Not, possibly leaving the logical operators to a later ticket. This is easy, the only problem being Maxima (1+back)translation, which you have solved.

Wrapping a Python method (imptementation of these functions in Sympy) shouldn't be as heavy as invoking a function in another interpreter : we stay in Python.

This is new functionality, after all : we don't (yet) have to worry about backwards compatibility. Introducing it with limited syntax (possibly extended later) isn't a drawback to anybody.

Thoughts ?

mkoeppe commented 3 years ago
comment:82

Sympy translation already works, in both directions.

mkoeppe commented 3 years ago
comment:83

And there is no remaining issue with "syntax".

mkoeppe commented 3 years ago

Changed dependencies from #32315, #31796, #32379, #32383 to #32315, #31796, #32383