[Axiom-developer] Axiom 2016 / 30 Year Horizon "State of the Union" review

[Tim Daly]

Axiom has a "30 Year Horizon" view. We are focused on goals with a
long term view. We discuss the goals, the current state, and the
challenges.

******************************************
       LONG TERM GOALS
******************************************

We plan to be the primary system for teaching Computational Mathematics.

We plan to be a highly reliable, verified implementation of Computation
Mathematics.

We plan to be a "living" system that can be easily maintained,
modified, and extended.

------------------------------------------
--- Teaching Computational Mathematics ---
------------------------------------------

We believe that Axiom is unique among systems. It has a strong
scaffold of mathematical theory used as an organizing force.  It is
free and open source, making it accessible to everyone.  It is a high
platform on which to build higher rather than starting from scratch.

Axiom is a large system, currently having over 1100 Categories,
Domains, and Packages and about 10,000 function signatures. In the
long term we hope to expand that by a factor of 10 or more.

There is a rich environment with growing trends that present a
challenge to Axiom to find ways to unify them into a body of knowledge
of Computational Mathematics that can be taught at both the
undergraduate and graduate level, as well as commercial use.

We need to "collect" and "connect" Axiom to the existing and
growing body of knowledge.  There are published papers describing
Axiom's implementation details.  There are hundreds of citations of
Axiom in the literature, some which describe implementation details.
There are shelves of books containing algorithms, some of which are
implemented in Axiom.  There are shelves of books containing formulas,
some of which are already in the Computer Algebra Test Suite but the
ability to ingest them needs to be automated.  There are proof systems
becoming capable of handling Axiom's Spad language and underlying
Lisp.  There are hundreds of citations of Axiom in the literature
related to Axiom's structure and function implementations.  There are
online courses that cover background material needed to understand the
theory underlying Axiom.  There are emerging standards allowing
portable implementations of the existing front-end.

------------------------------------------
--- A Living System ----------------------
------------------------------------------

We are not in competition with existing systems. There are structural
reasons to believe that Axiom will be a central platform in the long
term.

We target teaching Computational Mathematics because people tend to
use the system they know. We plan to structure Axiom so that it can be
maintained, modified, and extended as well as deeply connected to the
literature and course work.

We believe that Computational Mathematics has to be free and open
source giving the ability to understand algorithms. But this is not
enough; we need to communicate the knowledge as well as the code.

We believe that Axiom's implementation needs to be proven correct
where possible giving the ability to trust the results.

We believe that by setting standards for explaining algorithms we will
raise the bar for communicating Computational Mathematics.

We believe that a large, easily extended, and clearly explained system
will overcome the tendency to "start from scratch".

******************************************
         CURRENT STATE
******************************************

Currently there are three classes of existing systems with their
particular problems and long term weaknesses.

The PROPRIETARY systems have great functionality, well beyond what Axiom
implements in some cases. The critical flaw is that these systems are
backed by companies and companies die on average every 10-15 years.
Since software is now considered a capital asset, especially in a
software-only company, the software cannot be given away and released
as open source. When these companies die, such as happened to
Symbolics (Macsyma) or Soft Warehouse (Derive), the software will
disappear.

The START-FROM-SCRATCH system is everywhere. There was a collection of
over 100 systems distributed at ISSAC in the 90s.  Axiom represented
hundreds of person-years of effort and millions of dollars of
investment. It contains PhD level implementations of algorithms on a
variety of topics. This level of investment is unlikely to be
re-created in the current environment. Companies do not see such
effort as a good investment and the government will not invest in this
area. Thus there is no money and without money it is not possible to
"start from scratch" to build such a large system again.

The UNDOCUMENTED systems are everywhere. The commercial systems have
good external documentation but from first-hand conversations we know
that the internals are not. They suffer from the "PhD syndrome". In
order to create leading-edge algorithms one needs to hire recent
PhDs. The algorithm implementation works but there is a large
disconnect between the theory and the implementation, usually leaving
the implementation undocumented.

In addition one needs a wide range of skills. To maintain Axiom one
needs to be able to understand implementation details, large common
lisp systems, and have a depth and breadth of both theory and
computational mathematics. There are very few people who fit that
criteria. Indeed, that's the very problem we intend to cure by
teaching new Computational Mathematicians.

******************************************
        CURRENT EFFORTS
******************************************

Here we discuss details of ongoing efforts, some of which will likely
take years to complete if completion is even possible with
ever-expanding knowledge.

MERGING RELATED PAPERS: We have been collecting papers related to the
theory and implementation of Axiom. Various people have given
permission to use their material as chapters in the documentation
(e.g. Davenport, Grabmeier, Scheerhorn, Hammerling, etc.) The material
is added and adapted to the Axiom literate programming style. Citations
are made with hyperlinks between the chapters and the algebra code.

REVERSE ENGINEERING ALGORITHMS: We have been seeking algorithm
implementations that are clearly connected to published algorithms. We
are merging the algorithm details with the Spad implementation. This
will enable people to understand both the theory and the details as
well as highlight limitations and design decisions.

EXTENDING ALGEBRA: We have been working to replace the functionality
provided by the NAG library. Currently we are integrating BLAS and
LAPACK numerics with a plan for QUADPACK in the near future. We have
several Axiom algebra packages "stacked up" to be added at the
appropriate time, gated by the fact that we plan to provide them as
examples of "Literate Algebra". It is no longer sufficient to just
"throw the code in the pile" without the associated background.

MERGING SOURCE CODE: There are still about 250k lines of source code
to be merged into the books. The build system is being restructured
to remove the need for 'make'. The directories are disappearing.

COMPUTER ALGEBRA TEST SUITE (CATS): There is a growing body of test
suites for general areas of mathematics at the CATS website. These
test suites show the power and the limitations of the current Axiom
implementation. They point the way toward areas in need of
improvement.

AUTOMATED FORMULA INGESTION: There are many reference books that
contain mathematical formulas implemented in Latex. Fateman has shown
that Latex does not provide sufficient semantics to automatically read
them. We are working on a Latex "semantics markup" package to attack
this problem. The semantic markup does not change the print
representation but provides more semantics in the Latex formula tags
so they can be automatically read. This will open up a connection
between these hugh sources of formulas and Axiom.

IMPLEMENTING VERIFIED MATHEMATICS: Axiom is a Computational
Mathematics system. As such, it is a form of mathematics. Trusted
mathematical systems should strive to prove the implementation
correct. Axiom has implemented a build step that invokes ACL2 to prove
the Lisp implementation correct. Axiom has implemented a build step
that invokes COQ to prove the Spad implementation correct. We are
working toward putting more code into this proof pipeline.

BIBILOGRAPHY and CITATIONS: We are connecting Axiom to the
literature in several ways. We have a pipeline of documentation
of the theory and implementation details. We have an ongoing
literature search for citations related to the algebra source
code. Algebra code is being decorated with hyperlinks to the
bibliography included in each book. Ultimately we plan to link
to the actual papers.

ONLINE COURSES INTEGRATION: We are connecting Axiom to online courses
which provide the background necessary to understand the implementation
and use of Axiom's algebra. We have inserted hyperlinks to particular
videos and particular courses, such as Salomone's Abstract Algebra II
course. As more course material becomes available online we will
decorate Axiom with hyperlinks, making it easy to gain the necessary
background.

UNIFIED FRONT END: We are connecting Axiom to the browser as the
unified front end. Eventually the command line, hyperdoc, and the
graphics will all be available. Our focus on teaching means that we
will have a different orientation than the current set of front-ends.
We need a "curriculum" system that will provide guided understanding
and use of Axiom's algebra.

RESEARCH: We are implementing algebra, such as Gustafson's Universal
Numbers (UNUMs), to see if this can simplify the BLAS/LAPACK numerics.
We are examining "mixed" numerics that carry symbolic results in order
to control loss of precision.

A LIVING SYSTEM: Ultimately Axiom is striving to be a "living
system". Experience shows that most software dies. But Computational
Mathematics represents the collision of computers and mathematics and
is a timeless new subject area. We are striving to "be timeless" as
well. That is the reason for the "30 Year Horizon".

******************************************
        CHALLENGES
******************************************

A fundamental challenge is a lack of time. The tasks are large, some
impossibly so. We hope to set the standard for future work by future
authors in the belief that we can achieve a living system. It is by no
means certain, but then, neither is tomorrows breakfast.

MERGING RELATED PAPERS: Finding related papers takes time.
We have to understand an area, find "canonical" introductory
papers, obtain permission, re-implement the papers into Axiom's
books, and sew the papers and algebra together with hyperlinks.

REVERSE ENGINEERING ALGORITHMS: Trying to find the formula
or algorithm that matches the implementation is difficult. In one
cases we have found 20 formulas, none of which match the algorithm
used by Axiom. Even when we know what is being implemented some
of the algorithms are special "helper" functions that are part
of a much larger algorithm such as integration. These have to be
explained in a context that itself needs an explanation. It takes
time.

EXTENDING ALGEBRA: Both time and thought constrain this task.
We want the algebra to "be teachable" which means that we need to
provide much more than the code. There should be some theory,
some algorithmic design details, help files, a range of examples
with a good canonical use example. There needs to be literature
citations and, potentially, links to videos explaining the
background and use, either in courses or stand-alone.

MERGING SOURCE CODE: It takes time to rewrite 250k of Lisp into
a more structured and better documented form. It takes time to
"tree shake" the code to remove unused functions. The data
structures need to be reshaped, rationalized, and explained.
The build machinery simplification is "in-process". Axiom is,
after all, just a Lisp program with a Domain-Specific Language
(Spad) sitting on top so it shouldn't need a build system.

COMPUTER ALGEBRA TEST SUITE (CATS): Each of the test suites
have taken between half a year and a year of effort to implement.
This effort tends to uncover bugs or mismatches between the
formula and Axiom's algebra. Understanding the issue slows down
the work. For example, integration can differ by a constant but
sometimes the fact that the answer is constant is not obvious
or Axiom cannot prove it algorithmically. Occasionally we have
found bugs in the published literature.

AUTOMATED FORMULA INGESTION: Understanding what to mark,
what are the needed semantics, and how to write the Latex macros
takes time. Axiom needs to know, for example, which symbol is
being used as the variable of integration. This is obvious to
the human but not to the machine. This makes semantic markup
an iterative process that is defined by the target reader.

IMPLEMENTING VERIFIED MATHEMATICS: ACL2 and COQ are large
and impressive systems that take time to master. They do not
cover every aspect of what would be useful to prove. They do
provide a good platform for constraining the choice of an
implementation so it is easier (or even possible) to prove.
As such they improve the quality of Axiom.

BIBILOGRAPHY and CITATIONS: This year has been devoted to
the literature. We have collected papers and citations. We have
chosen papers to target for inclusion, for reference, and for
providing background on Axiom. We have made the bibliographic
citations robust. We have been decorating the algebra with
hyperlinks to background material. All of this is in pursuit
of "academic quality", making teaching easier.

ONLINE COURSES INTEGRATION: Online courses provide excellent
material, either as a full course or as a targeted lecture on a
single topic. We are working to find, link, and integrate the
online lectures with the algebra. Citations are now hyperlinked
at the appropriate places.

UNIFIED FRONT END: We have moved the structure of hyperdoc into
html. We have moved the front-end into interactive input/output. We
are looking at moving the graphics to the browser canvas. It all
takes time, especially since "the browser" is a moving target that
tends to break after every upgrade.

RESEARCH: Acton has examples of rewriting formulas to minimize
numeric issues, some of which involve substitution of symbolic
quantities. This allows for exact cancellation rather than
underflow. It looks like a fertile area for symbolic/numeric
cooperation. UNUMs look like they could greatly simplify numeric
code. We have been working on an FPGA implementation as the new
Intel processors have an embedded FPGA.

A LIVING SYSTEM: Ultimately Axiom is striving to be a "living
system". Experience shows that most software dies. But
Computational Mathematics represents the collision of computers
and mathematics and is a timeless new subject area. We are
striving to "be timeless" as well. That is the reason for
the "30 Year Horizon".

Tim