Several people have asked about Axiom's goals and about my opinions on other free and commercial systems.
I have no opinions about other free or commercial systems. Computational Mathematics is not a competition, it is a field of study. Do what you can to make it better for all. Axiom has several goals. 1) Axiom needs to live. Keeping Axiom alive is a primary goal. It is patently obvious that open source projects tend to die when the lead maintainer stops development for any reason. Github and Sourceforge have many thousands of examples. Commercial software dies when the company dies. Witness Symbolics (Macsyma), Soft Warehouse (Derive), or MapleSoft (Maple was sold to a Japanese company which currently supports it). Companies die, on average, after 15 years. Axiom is timeless in that it is computational mathematics. The algorithms and results will always be correct. So unlike other efforts, what we write can be used by later generations. This goal influences every decision about direction and purpose, in particular, driving some of the goals listed below. 2) Axiom needs to be better documented and better explained. The decision to deeply explain and document Axiom is based on the obvious need to make it possible for new people to maintain, modify, and extend it. Explanation needs structure so a new person can "linearly learn" what is needed. It also needs structure so information can be found easily through some search mechanism. It further needs structure to incorporate what is already known. Literate programming was chosen after a long search for possbile solutions. The book-like nature of a literate program focuses attention on people, not machines. It is a linear format which provides a way to communicate ideas using methods developed over history. Books are structure we understand. You can find information in the volume choice; there are currently 21; the table of contents, tables of figures and subjects, detailed indexes, a new "rich form bibliography" which includes abstracts, and the use of hyperlinks between volumes, to outside sources, and to youtube videos and courses. Experiments are being done to embed gifs to illustrate ideas. Algorithms, Categories, and Domains now have hyperlinks to published literature and there are some initial examples of deeper documentation of the algorithms. Ideally every algorithm will provide sufficient explanation of the implementation or links to explanations so the implementation can be understood in context. In additon, people have generously contributed material from other sources which directly explain details of Axiom, sometimes even written by the Axiom primary authors. There is a structured bibliography based on various sub-topics as well as a section on external references to Axiom (currently 636 have been found). There is an automated regression test suite that is being expanded and made uniform for testing all known functions. The Axiom code is now using a uniform syntax and has per-function help text, as well as automated generation of help files. Finally there is a literate bug document that points at known problems (with a plan for adding deeper explanations and possible solutions). 3) Axiom is RESEARCH software. It is exploring ways to push the boundaries of computational mathematics. 3A) Proving Axiom Correct Computational Mathematics IS Mathematics. It needs proofs, not handwaving. This effort involves adding proof technology to Axiom. Propositions are types and can be incorporated into the Category structure as "type signatures". Domains already have representations which is known in logic as the "carrier". Proofs of Propositions, using operations from the domain, will show that the Domain is properly designed and implemented. The three parts (signatures, representations, proofs) mirror the logic structure of "typeclasses" which have (signatures, carriers, proofs) so there is a solid formal basis in logic for Axiom's Category/Domain structure. Because Axiom uses Group Theory as a scaffold there is a solid formal basis for inheriting propositions so a Domain knows what it needs to prove and what operations are needed in the Domain to support that proof. Axiom currently can invoke Coq and ACL2 during the build process. An example of automatically proving a lisp algorithm using ACL2 exists. A Coq example is being worked on. In addition, we are looking in detail at a new system called LEAN. 3B) Number representations There are two research efforts. One involves "formal numbers" so that we can claim that the symbol 'x' is an 'Integer' without giving it a value. This was work originally performed under grant at City College of New York. The second involves work by Gustafson on a new representation of floats that can be dynamic in range and easier to reason about. The goal is to push this through the numeric libraries in order to eliminate some of the costly checking and arrive a reliable results. Some of this work is being done on a FPGA (which is now mainstream on some Intel chips). 3C) Provisos Provisos are a long-standing research question. Some work has been done, mostly using Cylindrical Algebraic Decomposition, to derive new ways to constrain the boundaries of valid computations. It is expected that this work will benefit greatly from the integration with formal methods listed above. 4) Teaching In order to keep Axiom alive we need to teach the next generation. Axiom is developing the coursework necessary for teaching computational mathematics. There are Universities planning to teach using Axiom and every effort will be made to support those efforts. In addition, there is a plan to teach at CMU. The end result will be course outlines, a set of slides for standard 28 lecture courses, and published youtube videos collected under a youtube channel for distance learning. Besides computational mathematics, one of the courses will focus on maintaining, modifying, and extending Axiom with new ideas. 5) Standards 5A) Axiom has done some work to automate the semantics of NIST's Digital Library of Mathematical Functions (DLMF). Macros translate the Latex sources to Axiom input based on additional decorations. 5B) Axiom has a Computer Algebra Test Suite (CATS) which uses published sources as test cases, finding bugs in Axiom as well as the publications. 5C) Axiom is moving to full browser-based HTML5 documentation, moving the Hypertex and Graphics packages to HTML and Canvas code. Dynamic Axiom input/output in HTML exists and works. 6) New Algorithms Research on new algorithms, such as a full implementation of Clifford algebra, are "in-process". Gustafson Floats will eventually be another Domain as a numeric category, useful for constructing things like POLY(GUST), that is, Polynomials over Gustafson floats. New algorithms are interesting but without proper explanation of the idea and the implementation detail they are just "soon-to-be-dead-code". Every effort is being made to ensure that new code provides the details needed to understand the algorithm and the implementation, along with proper testing, examples, help files, and associated external references. 7) The 30 Year Horizon Axiom has a "30 Year Horizon" focus. We will arrive at our goal in 30 years, starting today. Which is, in mathematical fashion, true for every given future day. Computational Mathematics is a huge field and we are only at the very beginning of this journey. Find an idea. Research the literature. Talk to a lot of people. Push the envelope just a little bit. In other words, do the equivalent of a PhD thesis. You already have a research platform. You don't need the degree, you just need the ambition. Collaborate, Cooperate, Contribute. Tim
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer