pygae
Add rule-based rewrite capacity in a coordinate-free way
Continuing from discussions on Slack with @abrombo and @hugohadfield :
Alan Bromborsky:
I think the biggest deficiency of galgebra is that it can only reduce multivector expressions in one direction. All results are in terms of the multivector basis. It would be useful to be able to go in the other direction and rewrite multivector expressions in terms of other multivector expressions.
utensil:
I have the same feeling. Actually I think as a symbolic library, GAlgebra should be able to manipulate GA expression without concerning the basis and simplify GA expressions using predefined rewrite rules. For that, I studied the internal of a few rule-based symbolic rewrite library and wish to be able to implement as such. As for the rewrite rule list, I find Eric Chisolm's https://arxiv.org/pdf/1205.5935.pdf is pretty good at listing the identities in GA exhaustively in Appendix A Summary of definitions and formulas. I also have verified many of them with GAlgebra.jl (for syntax sugar) at https://github.com/pygae/GAlgebra.jl/blob/master/test/runtests.jl#L67 .
Some of the rule-based symbolic rewrite library/code that I've noticed:
- https://github.com/sympy/sympy/commits/master/sympy/unify
- https://github.com/sympy/sympy/tree/master/sympy/strategies
- https://github.com/logpy/logpy/
- https://github.com/HarrisonGrodin/Rewrite.jl
- https://github.com/JuliaDiff/DiffRules.jl
- https://github.com/HarrisonGrodin/Simplify.jl
- https://rulebasedintegration.org/
- (update) https://github.com/egraphs-good/egglog
I think you missed matchpy, which is what SymPy plans to use for its implementation of RUBI.
@asmeurer Thanks for the heads up. I have checked out https://github.com/HPAC/matchpy , its papers and issues related to the RUBI integration into SymPy, but I fail to find discussion on why matchpy is used to for the job and comparison against alternatives.
I took a look into the internal of matchpy and its code generation from RUBI to a decision tree and I realize that due to language features, rewrite engines are designed and implemented in significantly different ways. So matchpy might not be an optimal choice with porting to Julia in mind.
BTW, I'm a little confused by the usage of rewrite mechanisms in SymPy, the situation was described in https://github.com/sympy/sympy/wiki/Proposal-for-a-new-pattern-matching and brought up during planning for RUBI integration but I can't find further discussion or plans on this matter which I think it's quite an important one. In https://github.com/sympy/sympy/issues/7330 (an older but open issue) unification was considerred and obviously fail to be chosen as the tool for the task since the author maintains it outside of SymPy and SymPy's policy is not to introduce a dependency lightly but I don't know why matchpy made it into SymPy.
GitHub
A library for pattern matching on symbolic expressions in Python. - HPAC/matchpy
A computer algebra system written in pure Python. Contribute to sympy/sympy development by creating an account on GitHub.
Some afterthought: https://arxiv.org/pdf/1205.5935.pdf is not ideal for such a list, there's no logical relationship designed between the formulas towards the usage of pattern matching and rewrite flow. A new design (based on the paper) is still very much required.
Actually I guess such a list should be backed by a formal proof programming language like coq etc. So the whole workflow behind the idea in Gajit that's complete is actually: formal proof -> symbolic -> numeric. Thus we have a solid ground all the way up to performance optimization. Although it's not a must for this issue.
Not sure if this will interest you but Hongbo Li is doing nice things using rewriting rules http://www.issac-conference.org/2017/assets/tutorial_slides/Li.pdf
It seems this phd thesis is dedicated to the same thing : https://mediatum.ub.tum.de/doc/1175107/1175107.pdf
