8 ms·
Towards a new SymPy
- 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?
- 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.
- 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
- 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/
- bmitc 3y agoMathlib is not nearly as complete as advertised. It is very much a collection of research projects with little cohesion.
- staunton 3y agoA CAS also covers only a tiny part of "an undergrad math degree" so that's beside the point here. Assuming it had appropriate tactics doing the job of a CAS using all theorems (which isn't happening any time soon), what math would be missing?
- deleted 3y ago[deleted]
- 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).
- 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.
- 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
- 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.
- 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.
- rowanG077 3y agoYes type checkers are a domain of study. Basically any domain where mathematica needs to integrated into the end result as is.
- sheepshear 3y agoImplying there's a technical reason it couldn't be used.
- 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