Hi Tim! Tim Daly <[email protected]> writes:
> The Hawaii Test. Ah, how dreams die. > If you haven't seen this you might find it amusing. > https://www.youtube.com/watch?v=Av0PQDVTP4A > Actually quite an inspiring talk, as the audience reaction readily attested. To me the struggle here has always been the mismatch between how the human brain naturally works, and the precision and determinism we so admire in the micproprocessors we construct. We want the 'right answer' of mathematics, indeed it is one of the few things in modern society we can 'trust'. For all the cacophony and division among humans, mathematics is taught essentially the same way everywhere throughout the world. Yet few, *very* few humans have the patience and determination to follow the bit operations behind any conclusion. We desperately need to shorten, abbreviate, generalize, construct mnemonics and heuristics, and, sadly but importantly, *flush* extraneous information. Even the compulsory sleep cycle of our biology attests to the importance of this process. So when humans look at code, it is to jog their memory as quickly as possible to a greatly admired monument of precise logic just long enough to spot a problem, or even simply wonder at its alien beauty. The code itself should be mostly self explanatory for this purpose. Occasionally we do have to consult a manpage or similar to explain in English what is in reality a flow of mathematical logic, but in general the verbosity and imprecision of human language limits the utility of this process. One commits to memory a grab bag of useful tools to maximize the range of our capability and ignores the rest. You are quite right that the size of the documentation is not relevant as long as we have a good indexing process, which we do -- today's internet in this sense is one large 'book'. So it is somewhat ironic but not all that surprising that the AI movement of today has our beloved precise mathematical computers spitting out vague, emotional dialogue suggestive of plausibility only to supposedly facilitate our next advance in productivity. We have reproduced all our human foibles in the new wave of computation -- the comment about trusting 'it' like you would a used car salesman is quite apropos. But you know, it works. One can retrieve an overlooked idea or relevant notion much more quickly with this tool. And it is constructed to never overtax our limited brains, providing only one page at a time, spitting out verbatim tasks we would consider tedious and uninteresting, and often flattering us to boot! There are very few scholars, precious, who of course need a thorough understanding of the algorithms to hopefully develop new ones. Then there are a few more who want to use their work in scientific and engineering applications, who basically need reliability. And there are many more who like pretty graphics and get excited about fantastic concepts related to technology. These, like most of us, need a "story" or "narrative". One might look down on the narrative as a hopeless sign of failure, but this would ignore its proven historical utility in preserving "the book" for thousands of years. Indeed the people on this list who have contributed countless hours maintaining and preserving the thing of beauty that is AXIOM operate in part on principles of religion, as any strictly utilitarian analysis would have us abandon anything forsaken by the herd. A "story" has to be concise, understandable even at a child's level, inspiring, and motivating of service, cooperation, and reciprocity. Please excuse the diatribe. On a practical matter, I would like to cleanup the regression test failures in the Debian axiom package at some point. A lot of work went into that suite, so I am not keen on truncating it. Might you field some questions in this regard? Take care, > It would be interesting to know what are the Fricas long term goals. > If you raise your eyes to the horizon, where are you going? Why? > > This is from (axiom/goals in git): > > 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. -- Camm Maguire [email protected] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/87tsrrxz7f.fsf%40maguirefamily.org.
