A comment there makes what I think is a very good point about "the lack of consolidation of computer algebra efforts": https://news.ycombinator.com/item?id=37430437
I don't know what might drive or foster such consolidation. Maybe Category Theory? Bridging syntax?
I will say though that symengine is a great project and congrats to that guy for pulling it off under the constraints of a phd.
Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.
On the one hand this is like comparing apples and oranges. On the other hand SAT is slow for dependency management not because the solver itself is slow (it might well be - I don't know which solver they packaged) but because it's an NP-complete problem.
Back to sympy: a computer algebra system (CAS) is primarily (IMHO) an algebra system, not a matrix manipulation library or a pde solver or whatever kitchen sink collection of things is in all of them. Algebra in this context means manipulating algebraic expressions and that's term rewriting and that's also NP-complete (well at least in some form or fashion, eg egraph extraction).
So in summary - there's no way out of using SAT/SMT here.
> slow, clunky, etc
Just to put a finer point on this - it's a very shallow thing to look at conda's or whomever's implementation and then paint over SAT/SMT with that same brush. The way that I usually describe z3 is that it is nuclear weapons grade industrial software. I mean jesus christ its stated goal is solving NP complete/hard problems and it frequently succeeds at this goal on problems with millions of decision variables and clauses. It is absolutely the highest tech piece of tech out there (XYZ pytorch/tensorflow ai ml thing pales in comparison) and we are all extremely lucky that it is licensed permissively and developed completely in the open (and basically by one guy!). And it is being used in many many places for very serious engineering.
It would be very interesting for SMT and CAS to converge a bit more. SMT in expressiveness and domains and CAS in rigor.
The modality of their usage is different. CAS tends to return some expressions of interest, which it is hard to get SMT to do. Either you get "unsat" or a particular model from an SMT solver, not a simplified expression (ok, z3 has a simplify command, which is pretty cool).
SMT today is not obviously expressive enough to handle most of the domains and questions that come up in CAS systems.
Most SMT solvers do not intrinsically handle transcendental functions or any notions of calculus, abstract algebra, etc.
CAS systems are largely interested in problems of equational reasoning, whereas SMT's bread and butter is gluing together "trivialities" like linear inequalities and congruence closure with SAT search.
I said it below, but I'll repeat it here: in my humble opinion, this is not what you want from a CAS. This is functionality better delegated to a BLAS (yes even with the finite field qualifier). And just because both CAS and BLAS have A in them, does not mean they are the same thing.
Why is that? What are the alternatives?
It also looks like SymPy or SymEngine is starting to catch up to Mathematica which also is pretty cool and does the same kind of expansion of an expression into a tree of sub expressions.
As an adult and OSS enthusiast, I've often wondered if there is an OSS option that can at least match, and ideally exceed, the TI-89's capabilities. Is SymPy it? I've had a few reasonably good experiences with SymPy, but I don't know much about the theoretical underpinnings of CAS, or how SymPy compares to competing offerings.
Many symbolic options exist in lisps. https://stackoverflow.com/questions/10355112/why-is-lisp-so-... is a good answer that goes over some of the reason for that.
The approach is not yet anywhere near being able to touch all the domains sympy can handle. Destructive term rewriting tends to be a bit more forgiving to unsoundness in the rules and still returning roughly meaningful results. EGraph rewriting (and other automated reasoning systems) tend to just return junk as soon as you aren't careful about your semantics. Associativity and commutativity are ubiquitous in CAS applications and encoding these concepts in general purpose terms is rather unsatisfying. The post above emphasizes specialty methods for polynomials, which it would be desirable to find a clean way to integrate into egraph techniques. Variable binding (which is treated in a rather mangled form in CAS systems) is seemingly important for treating summation, differentiation, and integration correctly. The status of doing variable binding efficiently and correctly in egraphs is also unclear imo.
Most recently I wanted to simplify a complex expression with terms like ‘diag(v1) * v2’ into Hadamard products, and found I’d need to implement custom rules to get it to work.
I'm also cheering for Sympy, I think it's longevity now still predicts success in the future.
