Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Towards a new SymPy

oscarbenjamin.github.io

Post reply on HN
Print view View original

51–60 of 72 posts

Re: Towards a new SymPy

#51

Post by sheepshear »

Q6T46nT668w6i3m wrote: post #48
mathisfun123 wrote: post #3

The 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…

Toy? SymPy has room for improvement but it has made a tremendous impact in research and industry.

"Toy" is solver jargon that sort of means there's an alternative that blows it out of the water.

Re: Towards a new SymPy

#52

Post by westurner »

zozbot234 wrote: post #37
staunton wrote: post #34

Earlier quoted context omitted.

Lean does have a tactics system (very similar to Coq). However, there is no general tactic that will do, e.g., "sin^2 + cos^2 = 1" for you. (Writing a tactic specifically for that simplification is easy, of course, but that's not what a CAS is). (I doubt there is one in Coq that will do this, although I'm not sure). A symbolic algebra system is expected to do this simplification (and much more advanced ones) automati…

Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case. This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.

Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations,

All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2') or find_similar(expr, AxiomDB) would be useful.

How do CAS differ from Production Rule Systems? https://en.wikipedia.org/wiki/Production_system_(computer_sc...

CAS > Simplification: https://en.wikipedia.org/wiki/Computer_algebra#Simplificatio...

Rewriting: https://en.wikipedia.org/wiki/Rewriting

Because the rulesets are expected to change, rules engines have functionality to compile rules into a tree or better for performance.

eBPF is not a rules engine, but it does optimize filter sets IIRC?

Re: Towards a new SymPy

#53

Post by bmitc »

mathisfun123 wrote: post #3

The 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…

> 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?

Re: Towards a new SymPy

#54

Post by [deleted] »

mathisfun123 wrote: post #40
abecedarius wrote: post #31

Earlier quoted context omitted.

Is there an existing CAS built on top of a SAT or SMT solver?

oss? 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.

[deleted]

Re: Towards a new SymPy

#55

Post by bmitc »

viscousviolin wrote: post #12
carapace wrote: post #6

Part II made the front page yesterday: 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 I don't know what might drive or foster such consolidation. Maybe Category Theory? Bridging syntax?

How 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/

Mathlib is not nearly as complete as advertised. It is very much a collection of research projects with little cohesion.

Re: Towards a new SymPy

#56

Post by sheepshear »

rowanG077 wrote: post #36
qubex wrote: post #32

I’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.

It'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.

What's preventing it from being used?

Re: Towards a new SymPy

#57

Post by staunton »

westurner wrote: post #52
zozbot234 wrote: post #37

Earlier quoted context omitted.

Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case. This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.

Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations, All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2'…

Julia's Symbolics.jl allows users to easily add custom rewrite rules. However, it's not a state-of-the-art CAS. I don't have that much experience with others. Mathematica doesn't allow it, I think.

Re: Towards a new SymPy

#58

Post by c-cube »

mathisfun123 wrote: post #25
toth wrote: post #8

Earlier quoted context omitted.

Is Mathematica built like this?

Yes but I doubt they're using z3 or cvc5 or any other oss sat/smt solver.

Do 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.

Re: Towards a new SymPy

#59

Post by c-cube »

philzook wrote: post #42
mathisfun123 wrote: post #3

The 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…

You might enjoy 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 co…

There's a workshop exploring that: http://www.sc-square.org/CSA/welcome.html . They're trying to bridge cas and smt.

Re: Towards a new SymPy

#60

Post by staunton »

bmitc wrote: post #55
viscousviolin wrote: post #12

Earlier quoted context omitted.

How 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/

Mathlib is not nearly as complete as advertised. It is very much a collection of research projects with little cohesion.

A 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?
Post reply on HN