Metatheory.jl for clean simplify rules on non-commutative groups

[akirakyle]

I mostly wanted to put this here as a reminder that Metatheory.jl exists and has a bunch of conveniently defined rules for working with rules that apply to non-commutative groups (or more generally monoids or other such general structures). While it's always possible to express such rules using the primitive @rule macro, sometimes correctly matching all the cases it should apply to can be tricky (e.g. https://github.com/JuliaSymbolics/SymbolicUtils.jl/issues/110). Furthermore, while the SymbolicUtils.jl rewriter is quite fast, I think it's performance is mostly aimed at associative-commutative simplifications, thus it would be interesting to see whether Metatheory.jl's approach could be faster for the non-commutative algebras that QuantumSymbolics.jl works with, especially since it seems there's been recent work on getting massive speedups in the 3.0 branch.

[Krastanov]

I am not particularly well aware of (1) whether Metatheory.jl is being revived and (2) what is the interoperability story these days between Metatheory and SymbolicUtils.

However, if you would like to define a bounty around the bigger picture you are describing here, please do. This is something we can reasonably fund.

[akirakyle]

I'm also not sure what the goals are for the future of Metatheory and SymbolicUtils as it's a bit difficult to glean purely based on whats written on each's github project. However it seems like the 3.0 branch has been receiving some attention in the past year.

As I'm still getting a better big picture overview of how the julia Symbolics system works, I'm not sure I have anything super concrete to pursue implementing, but rather thoughts for avenues that may be interesting to further explore.

For example, I think a bigger picture idea for QuantumSymbolics.jl would be to define more abstract simplify rules based on the mathematical structure of the operator algebras encountered in quantum systems. The goal would be to have a clearer separation between the rules themselves and the way in which they are applied in a rewrite system. This would help ensure the rules themselves are correct in the mathematical sense, and that the implementation of the rewrite system preserves the relevant mathematical structure. One example of where this may help is when working with the generalized Pauli group in dimension $d$ (sometimes called clock and shift style matrices). This group is non-commutative, however its index group is commutative with the very simple structure of being isomorphic to $\mathbb{Z}_d\times \mathbb{Z}_d$. A rewrite system that's aware of the fact that the index group is albelian can use it to more quickly reduce products of elements, especially when containing powers, then one that treats the rules more "locally" by defining the rules just on the two generators $X$ and $Z$. (I know I left out the complex phase in this phrasing of the group product, but I think the same argument holds there by understating this phase is isomorphic to the symplectic group over $\mathbb{Z}_d$.