Associativity / Commutativity for Boolean operations in SymbolicUtils.jl

General Usage
,
1

I’m working on a Boolean Algebra Rewriter with SymbolicUtils.jl, and I’ve noticed that for some reason, associativity and commutativity are not being properly applied for Boolean operations, which makes defining rules painful. I’m wondering if I’m missing something or if there is some way to manually tell SymbolicUtils to apply associativity/commutativity to boolean operations.

To clarify: I need to write these rules

@acrule((~a & ~b) & ~a => ~a & ~b)

@acrule((~a & ~b) & ~b => ~a & ~b)

If I only write the first one, then (A & B) & B has no change.

Furthermore, I have to define:

@acrule((~a & ~b & ~c) & ~a => ~a & ~b & ~c)

@acrule((~a & (~b & ~c)) & ~a => ~a & ~b & ~c)

If I only define the first one, then (A & (B & C)) & A doesn’t simplify.

2

there was a discussion about it here: [ANN] SymbolicIntegration.jl - indefinite integration with Symbolics.jl symbols - #8 by CiccioPasticcio

maybe @CiccioPasticcio has any idea?

3

yes so the commutativity thing is still a bit messy. What I did was to implement in the normal rule macro commutativity for the + and * operation, and that works for almost all the cases (still some problems with many nested operations). Currentyl associativity and commutativity for & is not supported. also i am not 100% sure what acrule macro does, but I think is not different from the rule macro

4

also there is no way to manually tell that some operations are commutative. would be nice to implement is, whad do you think @cryptic.ax ?

5

Yes, currently there’s no way to add associative/commutative (AC) operations. + and * for scalars (and + for arrays) are manually implemented to leverage the AC representation. It’s not an implementation thing - we simply don’t have the ability to support arbitrary AC operations, somewhat by design. SymbolicUtils itself can’t easily implement an AC boolean algebra, since even if the representation for + was repurposed for | and * for &, there’s no structural difference between a + b and a | b when both a and b are booleans. One alternative might be to define a custom primitive type that mimics Bool and define the algebra on that symtype, though I’m not 100% sure how well this would work. Alternatively, define a wrapper type

struct BoolTerm
  x::BasicSymbolic{SymReal}
end

And define all boolean operations as operating on BoolTerm and returning BoolTerm. That way, you control all symbolic dispatches and can use the internal representation as you wish. This is the standard way of using SU to define a custom algebra.

6

How would I go about defining the boolean operations as operating on BoolTerm and returning BoolTerm?