|
|
|
last edited 8 months ago by test1 |
Edit detail for Axiom Strengths revision 1 of 7
| 1 2 3 4 5 6 7 | ||
|
Editor:
Time: 2008/03/20 13:48:58 GMT-7 |
||
| Note: | ||
changed: - This page's purpose is to collect strengths of Axiom in comparison to other CAS. Please add your thoughts. Mathematical Abilities: - elementary integration, see http://www.math.univ-montp2.fr/FODESIT/SemJuin2004/Bronstein/bronstein.pdf - Real Algebraic Closure, see RealClosure [Axiom Language] and Library: - domains and categories provide an extensive library of generic algorithms that are easily extended to new domains - object-oriented programming methodology User Interface: - Axiom's 2-d and 3-d graphics are quite advanced and very flexible. - HyperDoc provides online reference and tutorial examples - TeXmacs interface - web interface [MathAction] Documentation: - more available documentation than any other open source computer algebra system - active [Axiom Wiki] - excellent Help browser Development: - full source code available through common open source channels such as Savannah and SourceForge - source code is evolving towards full [literate programming] documentation - command interpreter, library compiler and stand-alone compiler [aldor] is available From TimDaly Sun Apr 23 03:50:15 -0500 2006 From: Tim Daly Date: Sun, 23 Apr 2006 03:50:15 -0500 Subject: Strengths Message-ID: <20060423035015-0500@wiki.axiom-developer.org> Fundamentally I see Axiom as a research platform in computational mathematics. I believe that we are at the very beginning of the collision of mathematics with computers. There are whole areas of mathematics that need to be explored and computer algebra systems provide a place to do this research. When we implement a new algorithm we not only "reduce to practice" a useful idea we also prove, in some very fundamental way, that our algorithm is correct. Most mathematical proofs are social events where you try to convince another person that your statements are correct. Convincing a computer to generate the correct answers is the ultimate proof that you understand the problem and are generating the correct solution. Axiom is the strongest of the computer algebra systems for research purposes. You have complete control of all of the mathematics and, now that it is open source, you have the ability to reshape it in any way necessary. Axiom stands head and shoulders above all of the other existing systems because it is strongly based on theory. I believe that this is necessary in order to make systems that can scale. Without a good theoretical scaffolding it is very difficult to build ever-larger systems. Much more research remains to be done to explore computational mathematics. The computational aspect of mathematics can shed light on fundamental representation questions (like constructing rings over monoids using multiple inheritance) which do not arise in hand-manipulated math. Provisos (e.g. 1/x provided x <> 0) go directly to the heart of some very difficult and unsolved computational mathematical questions. If the proviso for 1/x is represented as intervals then we can write that 1/x \in [-infinity,0) AND 1/x \in (0,+infinity]. This implies that the computation has split into two parallel paths. We need to develop control algorithms that can handle such splits (there are 8 known possible control solutions). Furthermore, we need to consider several hard questions like the mathematics of combining intervals (and thus control branches). Hard questions arise if we make the endpoints symbolic such as f(x) \in [y,z]. We need to add conditions like f(x) \in [y,z] AND y <= z. So there are computations WITH provisos and computations IN provisos. A correct solution for provisos involves a complete rewrite of Axiom's algebra system. There are other equally hard computational mathematics problems. Consider the 'indefinites' issue. We know how to raise a matrix to a fixed power, say 3. Do we know how to raise a matrix to an indefinite power, say N? Or do polynomial arithmetic of p^n + ... * q^m + ... For fixed n and m we can compute any term in the resulting product. For arbitrary n and m what is the general term? How is it represented? Another outstanding question is the combination of proof technology (such as ACL2) and Axiom. What happens if we decorate the axiom algebra hierarchy with the theorems that apply, say, to monoids. Can we constructively prove that the algorithms in axiom that apply to monoids are formally correct? A further issue is the fact that formulas in textbooks are "iconic". That is, they represent "pictures" of ideas. Once you've studied E=mc^2 you view the formula as a picture rather than an equation. In fact, if you study the question you will eventually discover that all of the meaning of the equation resides in the surrounding paragraphs. Axiom carries this meaning in the type associated with each object. However there needs to be a formal sematic calculus developed which can represent and manipulate this "paragraph sematics" rather than just the equations. Even apparently easy ideas like simplification are very, very hard in general. Consider the question of simplification when using interval arithmetic. Interval bounds are provably tight if the equations are linear but not otherwise. Intervals that contain zero get very wide when they are squared. So the chosen representation of an equation can have a very large impact on the computed result. Automatic simplification that ignores this effect can cause previously stable computations to become unstable. This is only one of the many hard issues that automatic simplification introduces. Axiom is pushing the boundaries of literate programming. Hopefully the long term effect will be that researchers start publishing detailed implementations of their algorithms in a form that allows them to be "dragged and dropped" onto a running system and be immediately useful. This would allow detailed checking of results. It would also make programming be a legitimate activity for tenure track research consideration. Yet more interesting research problems arise if we consider machines which will be available on the 30 year horizon. These essentially infinite computing resources will have to be able to fully model not only the computational mathematics but model the problem being confronted by the researcher and even be aware of the researcher's "intensional stance" (their current approach to the problem) so that relevant research can be suggested from by the automatic literature searches. Tim From CliffYapp Sun Apr 23 11:15:08 -0500 2006 From: Cliff Yapp Date: Sun, 23 Apr 2006 11:15:08 -0500 Subject: Strengths Message-ID: <20060423111508-0500@wiki.axiom-developer.org> I am not sufficiently fluent in Axiom to give a concrete description of its strengths compared to those of other systems, but I can describe what motivated me to switch my attention from Maxima to Axiom. 1. Axiom provides a much better platform for the inclusion of new concepts such as Units and Dimensions. An attempt to incorporate those ideas into Maxima highlighted several weaknesses in that system, including the difficulty of treating units as something "different" from regular numbers. Axiom's type system allowed Martin Rubey to write very quickly a prototype units environment which sidestepped some extremely difficult display problems encountered in the Maxima effort. Although this isn't the final version of that environment, it was a compelling demonstration of the advantages of Axiom's display logic and type system for adding new concepts to Axiom. 2. Axiom's dedication to correctness and literate programming, e.g. the complete documentation of not just the programming code needed to solve a problem but the research, algorithms, and reasoning behind that algorithm, make the Axiom project something more than just a program - they make it a research project whose results are immediately practical for real world development, use, and interactive exploration. From BillPage Sun Apr 23 13:24:33 -0500 2006 From: Bill Page Date: Sun, 23 Apr 2006 13:24:33 -0500 Subject: hyperdoc Message-ID: <20060423132433-0500@wiki.axiom-developer.org> Martin wrote: > excellent Help browser Although Axiom's hyperdoc browser does do some things that other systems can't - such as navigate Axiom's complex type/domain system - I would hardly call it "excellent" in comparison to similar facilities in commercial products such as Maple and Mathematica.
This page's purpose is to collect strengths of Axiom in comparison to other CAS. Please add your thoughts.
Mathematical Abilities:
- elementary integration, see http://www.math.univ-montp2.fr/FODESIT/SemJuin2004/Bronstein/bronstein.pdf
- Real Algebraic Closure, see RealClosure?
[Axiom Language]? and Library:
- domains and categories provide an extensive library of generic algorithms that are easily extended to new domains
- object-oriented programming methodology
User Interface:
- Axiom's 2-d and 3-d graphics are quite advanced and very flexible.
- HyperDoc? provides online reference and tutorial examples
- TeXmacs? interface
- web interface [MathAction]?
Documentation:
- more available documentation than any other open source computer algebra system
- active [Axiom Wiki]?
- excellent Help browser
Development:
- full source code available through common open source channels such as Savannah and SourceForge?
- source code is evolving towards full [literate programming]? documentation
- command interpreter, library compiler and stand-alone compiler [aldor]? is available
I believe that we are at the very beginning of the collision of mathematics with computers. There are whole areas of mathematics that need to be explored and computer algebra systems provide a place to do this research. When we implement a new algorithm we not only "reduce to practice" a useful idea we also prove, in some very fundamental way, that our algorithm is correct. Most mathematical proofs are social events where you try to convince another person that your statements are correct. Convincing a computer to generate the correct answers is the ultimate proof that you understand the problem and are generating the correct solution.
Axiom is the strongest of the computer algebra systems for research purposes. You have complete control of all of the mathematics and, now that it is open source, you have the ability to reshape it in any way necessary.
Axiom stands head and shoulders above all of the other existing systems because it is strongly based on theory. I believe that this is necessary in order to make systems that can scale. Without a good theoretical scaffolding it is very difficult to build ever-larger systems. Much more research remains to be done to explore computational mathematics. The computational aspect of mathematics can shed light on fundamental representation questions (like constructing rings over monoids using multiple inheritance) which do not arise in hand-manipulated math.
Provisos (e.g. 1/x provided x <> 0) go directly to the heart of some very difficult and unsolved computational mathematical questions. If the proviso for 1/x is represented as intervals then we can write that 1/x \in [-infinity,0) AND 1/x \in (0,+infinity]?. This implies that the computation has split into two parallel paths. We need to develop control algorithms that can handle such splits (there are 8 known possible control solutions). Furthermore, we need to consider several hard questions like the mathematics of combining intervals (and thus control branches). Hard questions arise if we make the endpoints symbolic such as f(x) \in [y,z]?. We need to add conditions like f(x) \in [y,z]? AND y <= z. So there are computations WITH provisos and computations IN provisos. A correct solution for provisos involves a complete rewrite of Axiom's algebra system.
There are other equally hard computational mathematics problems.
Consider the indefinites issue. We know how to raise a matrix
to a fixed power, say 3. Do we know how to raise a matrix to an
indefinite power, say N? Or do polynomial arithmetic of p^n + ...
* q^m + ... For fixed n and m we can compute any term in the
resulting product. For arbitrary n and m what is the general
term? How is it represented?
Another outstanding question is the combination of proof technology (such as ACL2) and Axiom. What happens if we decorate the axiom algebra hierarchy with the theorems that apply, say, to monoids. Can we constructively prove that the algorithms in axiom that apply to monoids are formally correct?
A further issue is the fact that formulas in textbooks are "iconic". That is, they represent "pictures" of ideas. Once you've studied E=mc^2 you view the formula as a picture rather than an equation. In fact, if you study the question you will eventually discover that all of the meaning of the equation resides in the surrounding paragraphs. Axiom carries this meaning in the type associated with each object. However there needs to be a formal sematic calculus developed which can represent and manipulate this "paragraph sematics" rather than just the equations.
Even apparently easy ideas like simplification are very, very hard in general. Consider the question of simplification when using interval arithmetic. Interval bounds are provably tight if the equations are linear but not otherwise. Intervals that contain zero get very wide when they are squared. So the chosen representation of an equation can have a very large impact on the computed result. Automatic simplification that ignores this effect can cause previously stable computations to become unstable. This is only one of the many hard issues that automatic simplification introduces.
Axiom is pushing the boundaries of literate programming. Hopefully the long term effect will be that researchers start publishing detailed implementations of their algorithms in a form that allows them to be "dragged and dropped" onto a running system and be immediately useful. This would allow detailed checking of results. It would also make programming be a legitimate activity for tenure track research consideration.
Yet more interesting research problems arise if we consider machines which will be available on the 30 year horizon. These essentially infinite computing resources will have to be able to fully model not only the computational mathematics but model the problem being confronted by the researcher and even be aware of the researcher's "intensional stance" (their current approach to the problem) so that relevant research can be suggested from by the automatic literature searches.
Tim
I am not sufficiently fluent in Axiom to give a concrete description of its strengths compared to those of other systems, but I can describe what motivated me to switch my attention from Maxima to Axiom.- Axiom provides a much better platform for the inclusion of new concepts such as Units and Dimensions. An attempt to incorporate those ideas into Maxima highlighted several weaknesses in that system, including the difficulty of treating units as something "different" from regular numbers. Axiom's type system allowed Martin Rubey to write very quickly a prototype units environment which sidestepped some extremely difficult display problems encountered in the Maxima effort. Although this isn't the final version of that environment, it was a compelling demonstration of the advantages of Axiom's display logic and type system for adding new concepts to Axiom.
- Axiom's dedication to correctness and literate programming, e.g. the complete documentation of not just the programming code needed to solve a problem but the research, algorithms, and reasoning behind that algorithm, make the Axiom project something more than just a program - they make it a research project whose results are immediately practical for real world development, use, and interactive exploration.
excellent Help browser
Although Axiom's hyperdoc browser does do some things that other systems can't - such as navigate Axiom's complex type/domain system - I would hardly call it "excellent" in comparison to similar facilities in commercial products such as Maple and Mathematica.