[HN Gopher] Things I would like to see in a computer algebra system
___________________________________________________________________
Things I would like to see in a computer algebra system
Author : panic
Score : 95 points
Date : 2022-04-20 18:54 UTC (1 days ago)
(HTM) web link (fredrikj.net)
(TXT) w3m dump (fredrikj.net)
| practal wrote:
| Very good points. It helps to list the requirements of a system
| before you actually build it! I did something very similar when I
| wrote about what I would like to see in an interactive theorem
| proving (ITP) system: https://doi.org/10.47757/practal.1
|
| This worked out great so far in that I managed to come up with a
| logic which I believe is actually the BEST logic for mathematics,
| Abstraction Logic (AL): https://doi.org/10.47757/pal.2
|
| Furthermore, I think the ideal ITP system and the ideal Computer
| Algebra System (CAS) are actually the same thing. Many will
| dispute that, but this is just because they cannot look further
| than the shortcomings of current incarnations of both concepts. I
| actually think that AL will help to unify those two concepts, as
| an AL term is a very simple thing, and much easier to manipulate
| than a typed term of some complicated type theory!
|
| A lot of the points you list are really just saying that you want
| your CAS to be an ITP system: a) Inert expressions b) Based on
| math c) Based on typed math d) Type-integrated symbolics and
| enclosures e) Good for Inequalities g) Large but lean h) Text-
| friendly (and human-friendly)
|
| Your other points are points that people want for ITP systems,
| too: i) Integers j) Good math display k) Well-named
|
| As for types, I believe now that a static type system just does
| not cut it. I believe something like Practical Types (which led
| me to AL) is the right way to go, such that you have semantic
| types, which are basically like sets, without requiring that
| everything is a set: https://doi.org/10.47757/practical.types.1
| JoeyBananas wrote:
| > Pretty much the only systems that more or less get math right
| are the mathematical libraries for proof assistants (Lean, Coq,
| etc.). The mathematical structures and interfaces in Lean's
| MathLib are actually pretty close to what I'd like to see in a
| CAS.
|
| This comes with HUGE practical disadvantages. Yes, it would be
| possible to use type theory to make a mathematically rigorous
| CAS, but it would never be practical. Anyone who has ever tried
| knows that even proving something trivial like a+b+c+d=d+b+c+a in
| a theorem prover requires a suprising amount of ingenuity. There
| are few people in the world who have the skills to define and
| prove something more advanced like Buchberger's algorithm, and a
| task like that would probably require several math papers worth
| of new research just to produce the slowest implementation known
| to mankind. And it would take years.
| kmill wrote:
| It's pretty easy in Lean/mathlib: import tactic
| example (R : Type*) [comm_ring R] (a b c d : R) : a + b
| + c + d = d + b + c + a := by ring
|
| It takes about 50ms to parse, process, and type check this
| example, with the ring tactic running using some VM-compiled
| Lean code (in Lean 4, tactics will be compiled to native code).
|
| The way the ring tactic works is that it puts both sides of the
| equality into some kind of normal form, and hopefully the
| normal forms are the same. And, honestly, even without the ring
| tactic, it's easy to use just the simplifier for this if you
| know the incantation: simp [add_assoc, add_left_comm,
| add_comm]. (The simplifier is not a simple piece of software,
| but it's built-in and it's able to run a rewrite system while
| being able to normalize things when the rewrites enter loops.)
|
| To write CAS-like tactics, in principle "all you have to do" is
| write algorithms that simultaneously operate on expressions and
| construct proofs that the expressions represent what you need
| them to represent.
|
| One example of this in mathlib is the norm_num tactic, which is
| supposed to take expressions involving numbers, operators, and
| other functions, then evaluate everything as far as possible.
| It's something like Mathematica's evaluator, though it only
| evaluates using rules specifically developed for norm_num. It
| turns out that norm_num, even though it is operating on
| expressions and constructing proofs the whole way, tends to be
| _much_ faster than using kernel reductions (the gold standard
| for correctness). That 's because it's able to use faster
| algorithms for various functions rather than the mathematically
| pristine ones, for example it does multiplication using a
| base-2 representation of a natural number rather than in terms
| of its unary representation, which is the definition for the
| natural numbers as an inductive type.
|
| In fact, by using these sorts of tactics it's possible to
| calculate things that the kernel can't calculate itself. Here
| are some examples using top-level commands to invoke kernel
| reduction and the norm_num tactic: #reduce
| 1000000 * 1000000 -- deep recursion was detected
| #norm_num 1000000 * 1000000 -- 1000000000000
|
| (This is something that lets you use Lean as a calculator with
| a "repl".)
|
| Lean also has #eval to VM-compile an expression and evaluate it
| there, but what's interesting about #norm_num is that while
| evaluating it's also constructed a proof that the answer is
| correct. The VM compiler and VM are considered to be untrusted
| code, and they certainly have not been proved to be correct in
| any way.
| themulticaster wrote:
| Similar story in Isabelle/HOL - no special tactics required
| for this example: lemma fixes a ::
| "'a::comm_ring" shows "a + b + c + d = d + b + c + a"
| by fastforce
|
| Just for fun, I wrote up an equivalent but completely manual
| proof where every proof step consist of just on application
| of an existing fact - this is extremely verbose, but still
| quite short for this example: lemma
| fixes a :: "'a::comm_ring" shows "a + b + c + d = d +
| b + c + a" proof - note assoc =
| ab_semigroup_add_class.add_ac(1) have "a + b +
| c + d = a + (b + c + d)" unfolding assoc[of a] by
| rule also have "... = a + (d + (b + c))"
| unfolding add.commute[of d "b + c"] by rule
| also have "... = d + (b + c) + a" unfolding
| add.commute[of a "d + (b + c)"] by rule also
| have "... = d + b + c + a" unfolding assoc by rule
| finally show ?thesis . qed
| fdej wrote:
| Author here. I'm only talking about using formalizable and
| mathematically consistent type definitions in a CAS, not
| requiring formal proofs in the implementations of types.
|
| For example, if you want to prove a+b+c+d=d+b+c+a, you will
| define a, b, c, d as elements of a type R implementing the
| "additive abelian group" interface (or an extension of this
| interface, like "ring"); R = integers, for example. The CAS can
| then use builtin techniques for abelian additive groups to
| prove the property efficiently. It will not have to prove those
| properties from first principles.
|
| In the distant future there could perhaps be some kind of
| convergence between CASes and proof assistants to completely
| rule out implementation errors, but this would require
| breakthroughs in proof automation for the reason you mentioned.
| zozbot234 wrote:
| > A CAS worth its name ought to be able to represent structures
| like transcendental number fields, rings of holomorphic
| functions, differential fields, transseries, and so on.
|
| Doing this in a principled way requires implementing constructive
| analysis, which is not easy. Even something as simple as equality
| of real numbers is not constructively defined, one has to work
| with constructive apartness relations instead.
| practal wrote:
| No. Constructive analysis is not needed for this. Classical
| mathematics will do just fine. Stating nonsense like this is
| what gives constructivism a bad name. That's not saying that
| there is no room for constructivism in an ideal ITP/CAS system,
| there certainly is!
| colanderman wrote:
| > For example, 6 has an additive inverse in Z but not in N [...]
| (this is the reason why int often makes more sense than unsigned
| int in C, even when you have an unsigned value)
|
| `unsigned int` isn't actually N though, it's Z/ _n_ Z [1], i.e.,
| the integers modulo _n_ , which _does_ have an additive inverse
| of 6 (being _n_ -6).
|
| The reason `int` often makes more sense is because it's a useful
| property that the additive inverse of 6 actually be less than 6
| -- or more generally, that `int` _isn 't_ modular.
|
| Agree with the overall point though, that 6 is an element of many
| "types". Of the CAS-adjacent languages I'm experienced with, TLA+
| gets this right; SMTLIBv2 does not.
|
| [1]
| https://en.wikipedia.org/wiki/Modular_arithmetic#Integers_mo...
| zozbot234 wrote:
| I don't think modulo arithmetic per se includes any notion of
| "less". Typical definitions of "order" for an algebraic
| structure would require the order to be translation invariant,
| which isn't true in modulo arithmetic.
| ianbooker wrote:
| We are currently evaluating SymPy in Jupyter Notebooks as tool
| for teaching and from that experience I would add both simplicity
| for beginners as well as explicitness to the laundry list. Python
| and SymPy for example will simplify things they think is
| "trivial" (not so simple for teaching basics). Yet while you can
| be very explicit to counter such behavior, this will take away
| the simplicity.
| JabavuAdams wrote:
| Thanks for writing this! It's interesting and useful to me. I've
| been thinking about a personal "math helper". My context is that
| I have an engineering background and am currently studying
| physics.
|
| Your "inert expressions" point really resonated. I'd like for my
| helper not to do anything to expressions I'm working with, at
| least initially. I want to micromanage and literally tell it what
| operations to do. I just want to remove the typos and -1/+1
| etcetera mistakes that I tend to make. I also tend to get a bit
| lost in just simple algebra, so I'd like to be able to massage an
| expression multiple ways and keep ones that are making progress.
___________________________________________________________________
(page generated 2022-04-21 23:01 UTC)