6 ms·
Towards a new SymPy
- kzrdude 3y agoI think banking on SymEngineX ("SEX") for the Sympy 2.0 release would be interesting branding. I'm also cheering for Sympy, I think it's longevity now still predicts success in the future.
- alanbernstein 3y agoExcited to hear about the new LaTeX+SEX stack
- eigenket 3y agoI love SymPy. Its so useful for doing calculations I don't want to do myself.
- mathisfun123 3y agoThe unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until such time, sympy will remain a toy. 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.
- StableAlkyne 3y agoNot an expert in SAT solvers, personally. What would the benefit be in using one? 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.
- abdullahkhalids 3y agoMiniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.
- StableAlkyne 3y agoMiniconda is faster (I prefer it, personally)... ...but Miniconda and Anaconda are the same package manager, the difference is that Anaconda comes batteries-inclused with a ton of common packages. The reason Miniconda is faster isn't the solver, it's because it doesn't have 250 packages to go through the long checking process on. If you have a large, complex environment in Miniconda, that environment will get slower and slower to resolve over time.
- taeric 3y ago250 is not a big number... :(
- VHRanger 3y agoThey have the same resolver (Conda) You just have fewer packages installed with miniconda, so the sat problem is much smaller
- scoresmoke 3y agoYes, this is a big disadvantage. But have you tried Mamba that aims at implementing Anaconda more efficiently? It works really well in most cases. https://mamba.readthedocs.io/ https://mamba.readthedocs.io/
- bouchard 3y agoYou can use mamba's much faster solver directly with conda. conda install -n base conda-libmamba-solver conda config --set solver libmamba
- StableAlkyne 3y agoMamba is great, and I use it when possible. It's probably the single best thing to happen to Anaconda in years. Nowadays it's installed automatically, but up until a month ago you had to deal with the slow solver to install it. And fortunately it will become the default by Q4! The point I was making is the old solver left an impression on me that SAT is slow and inefficient, that's all really :)
- toth 3y agoIs Mathematica built like this?
- mathisfun123 3y agoYes but I doubt they're using z3 or cvc5 or any other oss sat/smt solver.
- c-cube 3y agoDo you have any evidence for that? My impression is that Mathematica is built on a rewriting language along with thousands of built-in procedures (some of which are sat/smt). I don't think its core engine itself is smt.
- maple3142 3y agoI am not sure current SAT solver is good at solving things that a good CAS can do. It is fast at a lot of operations related to bits (xor, shift, and, or ...) but it performs way worse for things like solving a linear system in a finite field. (This is all from my personal experiences, so I may be wrong.)
- mathisfun123 3y ago> linear system in a finite field 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.
- abecedarius 3y agoIs there an existing CAS built on top of a SAT or SMT solver?
- mathisfun123 3y agooss? none that i'm aware of that use a SAT/SMT solver for the term rewriting (like i'm suggesting). closed source, my strong intuition is both mathematica and magma work this way.
- abecedarius 3y agoSounds like a great project idea to make a toy demo of this direction you'd like to see. Maybe comparable to https://github.com/norvig/paip-lisp/blob/main/docs/chapter15.md https://github.com/norvig/paip-lisp/blob/main/docs/chapter15... and https://github.com/norvig/paip-lisp/blob/main/docs/chapter8.md https://github.com/norvig/paip-lisp/blob/main/docs/chapter8.... which are a few hundred lines of Lisp each, but do enough to be interesting.
- deleted 3y ago[deleted]
- philzook 3y agoYou might enjoy ruler https://github.com/uwplse/ruler https://github.com/uwplse/ruler 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.
- c-cube 3y agoThere's a workshop exploring that: http://www.sc-square.org/CSA/welcome.html http://www.sc-square.org/CSA/welcome.html . They're trying to bridge cas and smt.
- Q6T46nT668w6i3m 3y agoToy? SymPy has room for improvement but it has made a tremendous impact in research and industry.
- sheepshear 3y ago"Toy" is solver jargon that sort of means there's an alternative that blows it out of the water.
- bmitc 3y ago> core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules Why is that? What are the alternatives?
- 7thaccount 3y agoI really liked the article and how it explained CAS vs Numerical solutions. 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.
- abdullahkhalids 3y agoIs there any comparison of their features anywhere? Last time I tried sympy a few years ago, it was quite a bit lacking compared to Mathematica.
- 7thaccount 3y agoI don't personally know, but assume it'll take many years to catch up with Mathematica which has symbolic computing as their bread and butter with a large amount of developers adding to that codebase since like the 80s.
- carapace 3y agoPart II made the front page yesterday: https://news.ycombinator.com/item?id=37426080 https://news.ycombinator.com/item?id=37426080 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 https://news.ycombinator.com/item?id=37430437 I don't know what might drive or foster such consolidation. Maybe Category Theory? Bridging syntax?
- viscousviolin 3y agoHow about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem. [0] https://leanprover-community.github.io/ https://leanprover-community.github.io/
- staunton 3y agoThat's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).
- viscousviolin 3y agoThat's not my point. In the comment I made below the other post I talked about how Mathlib is just a piece of the puzzle, the way I see it [0]. I don't want to see Lean do symbolic computation - although I'm sure that would be great as well - what I want to see is to have Mathlib's library of mathematics being used in a way that any CAS can read definitions and theorems from it. Then a significant part of the CAS codebase won't have to be manually written, and developers can spend time on things that are not re-inventing some wheel. [0] https://news.ycombinator.com/item?id=37435449 https://news.ycombinator.com/item?id=37435449
- roger_ 3y agoSymPy is pretty nice but every time I use it for a real problem I end up hitting a wall and have to dig through the source or look at old issue reports for a workaround. 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.
- HelloNurse 3y agoRegarding the issue of representing symbolic expression and controlling their evaluation or simplification, are there precedents of using e-graphs to memoize and reuse work rather than simple trees with destructive updates?
- philzook 3y agoThe herbie project using egraphs to explore different ways of rewriting floating point expressions. https://herbie.uwplse.org/ https://herbie.uwplse.org/ One can also write custom rulesets in egglog (a new egraph rewriting system / language / datalog) https://egraphs-good.github.io/egglog/?example=herbie https://egraphs-good.github.io/egglog/?example=herbie 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.
- qubex 3y agoI’ve tried to appreciate SymPy but I always find myself running home to Mathematica. There’s simply no comparison. SymPy is like a match and Mathematica has the power of a sizeable thermonuclear warhead.
- rowanG077 3y agoIt's true. Unfortunately Mathematica simply can't be used in many domains. I would really like to integrate mathematica with a type checker for automatic theorem proving. I think it could greatly alleviate the clunkiness of dependent types.
- nequo 3y agoDo you know of attempts to integrate SymPy in this way?
- rowanG077 3y agoI tried it with symengine as a GHC(Haskell) Type checker plugin. But it was just too limited to be worthwhile.
- sheepshear 3y agoWhat's preventing it from being used?
- rowanG077 3y agoI can hardly accept a cool $3230 per year license. I didn't even attempt to go this route. I doubt they would even allow it tbh. The site isn't exactly clear on that.
- sheepshear 3y agoI thought you meant "domain" like a field of work or study.
- bionhoward 3y agoIf you have fewer primitives and terminals than there are UTF-8 characters (1.1 million), then you could ditch OOP expression trees altogether and use simple strings in Polish notation with a mapping of utf-8 characters to operations (simple lambdas). That way you don’t need __dict__ on every node of every tree. However, you’d have to rewrite the stuff which expects the OOP trees to instead expect Polish notation strings. This approach scales a lot further than classes because you reduce the memory cost of the algebraic expressions down to the simplest string to represent them (and even smaller if you pack the bits into an ANS, that’s a performance hit to reduce memory more)
- pxeger1 3y agoAt that point it's hard to justify not just writing it in C directly
- amelius 3y agoPython is great in DL, so any chance we'll see a combination of neural nets and computer algebra in a new sympy?
- j2kun 3y agoIf the author is reading this: please add an rss feed to the blog! I'd love to follow along for updates
- haberman 3y agoI remember being a kid and fawning over the upgrade from a TI-86 (which could not do symbolic manipulation) to the TI-89 (which could). 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.
- taeric 3y agoDepends what you mean? Mathematica is quite impressive. Many symbolic options exist in lisps. https://stackoverflow.com/questions/10355112/why-is-lisp-so-often-connected-to-symbolic-computation https://stackoverflow.com/questions/10355112/why-is-lisp-so-... is a good answer that goes over some of the reason for that.
- haberman 3y agoMathematica is certainly as powerful as a TI-89, but not OSS.
- taeric 3y agoRight, though you can get a free license with raspberry pi, I think? https://www.wolfram.com/raspberry-pi/ https://www.wolfram.com/raspberry-pi/ I'm sure there are restrictions, but likely not a concern for hobby interests?