Community standards for mathematical expression trees

[algebraicjulia]

Community standards for mathematical expression trees

[jpfairbanks]

see also https://github.com/JuliaSymbolics/SymbolicUtils.jl and https://github.com/0x0f0f0f/Metatheory.jl for more modern approaches. We should also consider https://arxiv.org/abs/2012.01847 as a more general rewriting system with DPO.

[jpfairbanks]

Yeah, I think that the MT data type should be flexible enough for everyone to use and will eventually become a fully fledgd embedded computer algebra system.

[jpfairbanks]

I saw a TODO note about implementing a more complete rewriting system. I think that Harrison’s Rewrite.jl has some overlap with term rewriting used here. If I understand correctly, the GATs used here are like the Theories he is using, but with types?

[epatters]

Thanks @jpfairbanks, I did not know about Rewrite.jl. Based on my cursory examination, I agree that the theories in Rewrite.jl look similar to (untyped) algebraic theories, although I don't understand how the system handles arities. For working with categories, we need not just types but a minimal form of dependent typing, which is what GATs give you.

Still, this package could certainly be a source of inspiration or maybe even collaboration/interoperation. Another source of inspiration is the old language OBJ.

Taking a step back, I don't know how best to make a generic and useful rewriting system, which is partly why I haven't done much work in this direction yet. Having a concrete problem to solve would help. I am definitely open to ideas here.

[epatters]

Cross referencing HarrisonGrodin/Rewrite.jl#27.