Riding the research waves

--000000000000d0ea4305f59aa60b
Content-Type: text/plain; charset="UTF-8"

I want to synthesize and organize prior discussions into a research
statement.

Scratchpad was born as a research platform. Axiom is the commercial
version that was forcibly birthed due to IBM's business decisions. Axiom
has never been, and was not intended to be, a "commercial competitor
to Mathematica and Maple".

If your goal in developing a new algorithm is to have people use it
then it makes more sense to write it in Mathematica and Maple.
If your goal is to research an extension of existing theory, write it in
Axiom.
Completing the Risch algorithm would be a perfect Axiom-style goal.

There are 3 interesting streams of research that are currently active and
of interest to Axiom. These are computer algebra, proof theory, and type
theory.
All three have been active since the last century. The interesting research
question is "What does this have to do with Axiom research?"

Computer Algebra stream

Axiom differs from other computer algebra systems because it has a
scaffold of group theory guiding the structure. This has defined the whole
category / domain organization.

Because of the group theory structure, Axiom is an ideal platform for
organizing and optimizing algorithms within the web of existing ideas.

One research question is the impact of dependent types on the potential
for re-organizing the Axiom structure. Another question is how to adapt
Lean proofs to proving Axiom's algorithms.

Proof theory stream

Lean is the latest version of decades-long research in proof assistants.
It is effectively a from-scratch implementation of the ideas, implemented
within a programming language that will self-host.

Lean has inspired a large body of proofs ranging from undergraduate to
leading edge research.

Lean contains proofs related to group theory, thus making it a compatible
match to Axiom. A second scaffold that contains the definitions and theorems
along side Axiom's group theory structure would make it possible to inherit
the definitions and theorems when trying to prove Axiom algorithms.

In addition, since Lean is pushing into areas of proof that could usefully
be
implemented in Axiom, it opens a stream of new areas of algorithms. An
exciting version of this would be automatic generation of algorithms from
proofs.


Type Theory stream

Type theory has the notion of a "dependent type". This allows a type to be
specialized based on the arguments of the type. Axiom would take "types"
beyond the programming language domain and into mathematics.

Axiom does this in rather limited ways at the moment. For example, there
is the general GCD algorithm. Axiom contains about 20 implementations based
on the place in the type hierarchy they reside.

Using dependent types, the GCD algorithm could be written once
and specialized as needed. Further, the proof of the algorithm is not really
dependent on the proof of the instance if done properly. This has the
potential
of collapsing the many existing Axiom specializations, such as packages,
into a
single instance.

Peak wave, Peak trough

The Axiom research platform sits where these three waves come together.

The Lean proof of the GCD in a dependent type implementation restructures
the Axiom algorithm hierarchy. The goal is proven algorithms in a general
setting
that specialize for a given algorithm.

Such a "computational mathematics" platform would bring together disparate
existing streams. That's the goal of the SANE (rational, coherent,
judicial, sound)
branch of Axiom research.

--000000000000d0ea4305f59aa60b
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div><br></div><div><br></div><div>I want to synthesize an=
d organize prior discussions into a research statement.<br></div><div><br><=
/div><div>Scratchpad was born as a research platform. Axiom is the commerci=
al</div><div>version that was forcibly birthed due to IBM&#39;s business de=
cisions. Axiom</div><div>has never been, and was not intended to be, a &quo=
t;commercial competitor</div><div>to Mathematica and Maple&quot;.</div><div=
><br></div><div>If your goal in developing a new algorithm is to have peopl=
e use it</div><div>then it makes more sense to write it in Mathematica and =
Maple.</div><div>If your goal is to research an extension of existing theor=
y, write it in Axiom.</div><div>Completing the Risch algorithm would be a p=
erfect Axiom-style goal.<br></div><div><br></div><div>There are 3 interesti=
ng streams of research that are currently active and</div><div>of interest =
to Axiom. These are computer algebra, proof theory, and type theory.<br></d=
iv><div>All three have been active since the last century. The interesting =
research</div><div>question is &quot;What does this have to do with Axiom r=
esearch?&quot;</div><div><br></div><div>Computer Algebra stream<br></div><d=
iv><br></div><div>Axiom differs from other computer algebra systems because=
 it has a <br></div><div>scaffold of group theory guiding the structure. Th=
is has defined the whole</div><div>category / domain organization. <br></di=
v><div><br></div><div>Because of the group theory structure, Axiom is an id=
eal platform for <br></div><div>organizing and optimizing algorithms within=
 the web of existing ideas.</div><div><br></div><div>One research question =
is the impact of dependent types on the potential</div><div>for re-organizi=
ng the Axiom structure. Another question is how to adapt</div><div>Lean pro=
ofs to proving Axiom&#39;s algorithms. <br></div><div><br></div><div>Proof =
theory stream</div><div><br></div><div>Lean is the latest version of decade=
s-long research in proof assistants.</div><div>It is effectively a from-scr=
atch implementation of the ideas, implemented</div><div>within a programmin=
g language that will self-host.</div><div><br></div><div>Lean has inspired =
a large body of proofs ranging from undergraduate to</div><div>leading edge=
 research.</div><div><br></div><div>Lean contains proofs related to group t=
heory, thus making it a compatible</div><div>match to Axiom. A second scaff=
old that contains the definitions and theorems</div><div>along side Axiom&#=
39;s group theory structure would make it possible to inherit</div><div>the=
 definitions and theorems when trying to prove Axiom algorithms.</div><div>=
<br></div><div>In addition, since Lean is pushing into areas of proof that =
could usefully be</div><div>implemented in Axiom, it opens a stream of new =
areas of algorithms. An</div><div>exciting version of this would be automat=
ic generation of algorithms from proofs.<br></div><div><br></div><div><br><=
/div><div>Type Theory stream</div><div><br></div><div>Type theory has the n=
otion of a &quot;dependent type&quot;. This allows a type to be</div><div>s=
pecialized based on the arguments of the type. Axiom would take &quot;types=
&quot;</div><div>beyond the programming language domain and into mathematic=
s.<br></div><div><br></div><div>Axiom does this in rather limited ways at t=
he moment. For example, there</div><div>is the general GCD algorithm. Axiom=
 contains about 20 implementations based</div><div>on the place in the type=
 hierarchy they reside.</div><div><br></div><div>Using dependent types, the=
 GCD algorithm could be written once <br></div><div>and specialized as need=
ed. Further, the proof of the algorithm is not really</div><div>dependent o=
n the proof of the instance if done properly. This has the potential</div><=
div>of collapsing the many existing Axiom specializations, such as packages=
, into a</div><div>single instance.</div><div><br></div><div>Peak wave, Pea=
k trough</div><div><br></div><div>The Axiom research platform sits where th=
ese three waves come together.</div><div><br></div><div>The Lean proof of t=
he GCD in a dependent type implementation restructures</div><div>the Axiom =
algorithm hierarchy. The goal is proven algorithms in a general setting<br>=
</div><div>that specialize for a given algorithm.<br></div><div><br></div><=
div>Such a &quot;computational mathematics&quot; platform would bring toget=
her disparate</div><div>existing streams. That&#39;s the goal of the SANE (=
rational, coherent, judicial, sound)</div><div>branch of Axiom research.<br=
></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br=
></div><div><br></div></div>

--000000000000d0ea4305f59aa60b--