Axiom – A scientific computation system | Hacker News Reader

Axiom – A scientific computation system

axiom-developer.org

73 pointsandai24 comments

Tim Daly here...

Axiom is alive, well, and under active development. The current effort is merging the LEAN [0] proof technology with the Axiom algebra. This involves some deep restructuring. The target result is proven algorithms, something missing in current CAS work.

(Note that this is project goal F on http://axiom-developer.org)

The effort involves building a parallel architecture to the current Axiom category / domain layout to enable functions to use LEAN's axioms, definitions, and tactics to prove existing algorithms.

In addition, Axiom now uses Common Lisp CLOS to enable work using dependent types, something not currently available in the legacy system. The algebra hierarchy is now a CLOS hierarchy which enables a lot of flexible extensions.

There is no point in publishing the work as open source since it is still in the active research phase. When released it will be announced on the http://axiom-developer.org website and uploaded to github.

One of the Axiom algorithms (Groebner basis[1]) has been proven in Coq.

Wikipedia contains the literate form of Axiom[2] , including the original book restored from the NAG files.

There is an active fork maintaining the legacy code as mentioned above.

[0] The LEAN Theorem Prover https://www.andrew.cmu.edu/user/avigad/Papers/lean_system.pd...

[1] Bruno Buchberger. Bruno buchberger’s phd thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Journal of Symbolic ComputationVolume 41, Issues 3-4, Logic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger (60th birthday),, 2006.

[2] Wikipedia Axiom https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system...

Hi Tim,

>There is no point in publishing the work as open source since it is still in the active research phase.

That sounds very interesting to me at least, I'd appreciate being able to take a peek.

Having experience with prior open source work I'm not likely to release the current effort until I'm much closer to completion. The whole idea of CAS and Proof has already generated a hostile reception from both areas in my email stream.

I've already proven that if I did release Axiom again I'm too socially inept to manage the process anyway. I'd release a technical paper or two but I'm no longer associated with CMU so I'm pretty much a "hobby researcher" I guess. The last Axiom presentation was the invited talk at Notre Dame prior to Covid.

There are a lot of interesting things "in the works" though. One is the idea of "proof down to the metal" (aka Proof Carrying Code[0]). The use of (FPGA) field programmable gate arrays[1] and the RISC-V[2] architecture soft-implemented in the FPGA means that I can run the LEAN proof in parallel with the algorithm at the hardware level. This not only proves the algorithm correct, it proves the implementation correct. I have a few FPGAs.

It's all fun and games but I have to wait to release it.

[0] https://en.wikipedia.org/wiki/Proof-carrying_code

[1] https://en.wikipedia.org/wiki/Field-programmable_gate_array

[2] https://en.wikipedia.org/wiki/RISC-V

Hi Tim,

So first of all thank you Axiom and all the work you have put in the system over the years. Second, the integration with LEAN seems like an amazing step forward. Is there anything on the internet I can read more about this? How would it work? Would it be beneficial for education purposes or mainly for research? Third, I am otherwise engaged in other projects these days, but a long life dream of mine is to build a CAS from scratch. That said, I wouldn't mind start collaborating with a team improving an existing one like Axiom. The "How to participate" link is just "TODO", is there any way I can get in touch with the development team?

Thanks for the "all the work" complement. Despite all, it is more fun than work.

Computer algebra algorithms are basically functions. Axiom is unique in that it organizes the functions based on a group theory scaffold. Thus you can know that certain matrices commute but rectangular ones don't. Algorithms that know how to commute live in the commutative "category" in Axiom. So the game is to distribute LEAN's commutative axioms in their proper place in the group theory inheritance scaffold so they are available when they apply.

Axiom arranges the world into "categories" (not category theory stuff) and "domains". The LEAN structure is a third structure (actually fourth but...) built in parallel so that a theorem that proves that certain matrices commute will only be available when it applies. When you try to prove your algorithm you have a collection of LEAN axioms, definitions, and tactics that are valid and apply to your particular function. If your algorithm used rectangular matrices the commutative theorems would not be visible and thus not available in a proof step. Due to the hierarchical nature, once you prove an algorithm you can also use it in other downstream proofs, for example, using proven data structures and their properties.

I have not published any papers on the subject. I'm no longer anywhere in the academic pipeline so a paper wouldn't get very far. Plus this is "in the cracks" kind of research that doesn't seem to fit into either camp.

As for the education or research question... I'm trying to do what I call "computational mathematics". It would have "real world impact" for Proof Systems so they would be able to depend on and use proven computer algebra results. Computer algebra systems would benefit by giving proven answers. Both areas would benefit.

Don't try to build a computer algebra system from scratch. Axiom has hundreds of years of PhD level research work embedded in its code. There is no way to reproduce some of it as the people have died. Researching just one of the algorithms could take the equivalent of a PhD effort. I tried to introduce literate programming so that people could learn to maintain, modify, and extend Axiom. The idea is that you could "read the docs" and both learn from the authors and have embedded pointers to the theory literature. Without literate programming I believe that the whole effort will eventually die as the learning curve is very steep. Literate programming was an attempt to keep Axiom "alive". Nobody wanted it. I gave a talk on it once: https://www.youtube.com/watch?v=Av0PQDVTP4A&ab_channel=NextD...

There is no "team". There is just me. Apparently I'm bad at "team". I have no desire to get forked again.

Thanks for the invaluable feedback! Looking forward to see the day Axiom and LEAN are integrated together. Good luck!

Im not in this field so this might not be a good question, but why integration with LEAN and not ACL2, which is already written in Common Lisp

I worked with Nqthm and ACL2. They seem best adapted to hardware verification.

LEAN is pushing the edge of undergrad mathematics.

"Faszinating" that a lot of these systems seem to be implemented from scratch in object-oriented C++ (?), instead of Prolog, SML, OCAML, Haskell, Lisp, ... what went wrong?

Thanks, I wasnt aware of the differences between various provers.

Doesn't seem like anybody is actively working on it: https://github.com/daly/axiom/commits/master/

The only open source CAS that has survived for half a century seems to be maxima. The development seems to be active: https://sourceforge.net/p/maxima/code/ci/master/tree/ But, yeah, it's still on sourceforge.

Scratchpad lives on in FriCAS https://github.com/fricas/fricas/commits/master/ which has commits 18 hours ago. Tim Daly worked diligently on Axiom for years. However some of his changes, like requiring every single file be literate code and complete refusal to compromise, turned decades of IBM research into an isolated dumpster fire; good luck getting it to build/run anywhere outside his Docker container. I'm reasonably happy with FriCAS since it's based on the same software and is much more open source normative, while possessing capabilities Maxima users could only dream of. See also https://lists.nongnu.org/archive/html/axiom-developer/2007-0... and https://lists.nongnu.org/archive/html/axiom-developer/2007-0... for evidence of his leadership style.

FriCas seems to be quite light in documentation?

There's a 990 page book linked on the home page: https://fricas.github.io/book.pdf

Also built-in help with ")help ...": https://fricas.github.io/help.html

Thanks! Somehow didn't find that.

Tried this command from their intro:

    draw(5*besselJ(0,sqrt(x^2+y^2)), x=-20..20, y=-20..20)

On macos, it says "transmitting data", but nothing shows. Will visit again if/when out of Beta, it would be great to have a working version of Axiom.

See https://fricas.github.io/, which includes a 990 page book and detailed documentation.

REDUCE is here: https://reduce-algebra.sourceforge.io

The first published paper about REDUCE is from 1967, work on REDUCE started slightly earlier: https://dl.acm.org/doi/10.1145/2402536.2402544

The first expressions of its Lisp implementation were written roughly 60 years ago.

I use Maxima regularly as it was what I was taught at university. It is updated regularly. It's cranky as hell but it works. Sometimes I use the CAS on my calculator, mostly to check my own work, because it hurts less. That's an HP Prime with Giac/Xcas on it.

The first few minutes of this video cover some of the history of Axiom at IBM: https://www.youtube.com/watch?v=Av0PQDVTP4A

https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system...

I like the idea of learning to use Axiom, but getting it to run has been a huge PITA, at least on PopOS using the distro packaged version. In fact, I never did get that to run. So I switched to using Tim's Docker image and even that failed at first:

    $> docker run -i -t daly/axiom axiom

yields

    personality change failure 1

But after a bit of digging, I finally found the solution for that. It's related to a seccomp setting, which can be toggled with a command lines switch.

So this will yield a running Axiom instance:

    $> docker run --security-opt seccomp=unconfined -i -t daly/axiom axiom

As a side note to all of that... when I first decided to take a stab at getting a CAS running on my laptop, I tried all of Maxima, Axiom, FriCAS, and, uh, probably some others I'm forgetting. And NONE of the distro packaged versions worked out of the box. All would fail on startup with some variation of:

The assertion realpath(s,o) on line 471 of main.c in function mbin failed: Invalid argument

** buffer overflow detected *: terminated

I finally got Maxima working somehow, and that's been my goto CAS ever since, just because it worked. Weird, but it is what it is.

I worked on/with CAS in the 1990s, mostly PARI/GP (as a researcher) and Maple (as an assistant/junior professor).

I remember watching a talk by one of the Axiom developers, maybe T. Daly himself, on the Jussieu University Campus in Paris, probably around 1998 or 1999. I remember being impressed by some of the ideas that were presented (I may even have asked 1 or 2 silly questions during the seminar), but unfortunately the system was not yet open source and so this was of little use for me.

Tim Daly here...

There were quite a few challenges before Axiom could be open sourced.

NAG released the Axiom sources to me around that time. I gave an invited talk in Paris.

There were many issues to solve. The primary one was that you needed a running Axiom to build Axiom. I was not allowed to distribute the NAG version of a running Axiom. It took a long time to restructure the system so it could be built from sources.

Portions of the NAG version were never distributed to me and I had to recreate some from scratch.

GNU hosting and Sourceforge hosting were new technologies I had to master. I also struggled to understand how to create and lead an open source effort. Obviously in hindsight I'm very bad at management.

The NAG version of the system removed the Common Lisp version of AKCL, (of which I'm a minor author). AKCL is now GNU GCL under Camm. IBM Research sponsored the creation of AKCL under contract which was developed by Bill Schelter. Bill and I were in constant contact and he used my office on his site visits. I had to re-host Axiom on AKCL from the NAG version but Bill was dead by then.

Back then I was working at City College of New York in the CAISS effort involving Infinite Group Theory (Magnus). I maintained, modified, and extended that effort and made it open source. Axiom was not part of my job effort until the last few months of my time there. Axiom was all after-hours / off-the-clock work. (I see my name has been "scrubbed" from the CAISS/Magnus work. They even mention Axiom but not me. Sigh.)

Axiom is now exploring new research ideas combining computer algebra and proof theory (aka computational mathematics). The computer algebra people don't do proofs and the proof people don't do computer algebra algorithms. In fact, of the few hundred papers I reviewed only James Davenport made the bibliography section in both areas. I'm not expecting any enthusiasm for this research. If I fail no one will notice. If I succeed ... no one will notice :-) But I'm having fun.

I was looking at their documentation:

> For example, Axiom's integrator gives you the answer when an answer exists. If one does not, it provides a proof that there is no answer. Integration is just one of a multitude of symbolic operations that Axiom provides.

What does "an answer exists" in this case? Is axiom able to prove that an integral does not have an answer mathematically, which seems impressive, or just that it can not be found using its own substitucion rules?

Reply on news.ycombinator.com