Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
goals -- a newly added file to explain current goals
- Loading branch information
Showing
4 changed files
with
191 additions
and
15 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,186 @@ | ||
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. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,16 +1,2 @@ | ||
books/bookvolbib Axiom References in External Literature | ||
|
||
Goal: Axiom References in External Literature | ||
|
||
\index{Smith, Robert} | ||
\begin{chunk}{axiom.bib} | ||
@misc{Smit12, | ||
author = "Smith, Robert", | ||
title = "Excursions in Mathematics Using Lisp", | ||
link = "\url{https://www.youtube.com/watch?v=nTI_d-jS6dI}", | ||
year = "2012", | ||
keywords = "axiomref" | ||
} | ||
|
||
\end{chunk} | ||
goals -- a newly added file to explain current goals | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters