/
goals
186 lines (138 loc) · 7.41 KB
/
goals
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
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.