axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Symbolic Algorithms Standards


From: daly
Subject: [Axiom-developer] Symbolic Algorithms Standards
Date: Mon, 11 Aug 2014 18:17:23 -0500

> Such a collection would be indeed desirable as there is none - at least
> not comprehensive enough. Most favourable of course would be a library
> of formally verified algorithms like CoqEAL

I have an initial effort on a wider bibliography
http://axiom-developer.org/axiom-website/bookvolbib.pdf
which I have started to lay out by year
http://axiom-developer.org/axiom-website/lattice.html
Hover over the numbers for the title.
The citation is in the source code for the web page.

I'm not sure what a good way to show the information might be.
If you hover over a number should it also show lines to the papers
it references? That info is in the page source but not used yet.
I am not the best person to do user interface design, as you can see.
Ideally clicking on a link would open the actual paper.

Half of the standards problem is the citation lattice, shown above.
This will be foundational information for when and where an algorithm
first arose. It will also show improvements and their history. Densely
referenced nodes are certainly important. 

The other half of the standards problem is what is actually
implemented in existing systems. I'm instrumenting Axiom to give a
trace of the algorithms used in the solution of an input. This will
allow me to build up a tower of the algorithms. Then I need to relate
the implementations to the published papers. A similar instrumentation
of Maxima would show what algorithms are implemented there.

The third half of the standards problem is getting it supported :-)

We're 40+ years into computational mathematics.
This needs to be done.



> (http://www.maximedenes.fr/content/coqeal-coq-effective-algebra-library)
> taking advantage of the relatively new SSReflect (tutorial ->
> http://hal.archives-ouvertes.fr/docs/00/40/77/78/PDF/RT-367.pdf).
> The implementation of Bourbaki's "Elements of Mathematics" by Jose Grimm
> (http://www-sop.inria.fr/marelle/gaia/index.html) demonstrates in an
> impressive way the feasibility to create such a mathematical firm
> collection of algorithms.

> Regarding 'pseudocode' it might be better (imho) to use the language of
> one of the available proof assistants of which Coq is only one suitable
> to do the task (http://en.wikipedia.org/wiki/Proof_assistant). Although
> I have no profund knowledge of the others (than Coq and Isabelle), it
> would be surely preferable to choose one that is capable of 'code
> generation' as it might be easier (one day ;) than expected to write a
> generator for spad/aldor.

I'm not sure what the "pseudocode" might be but I can't actually
advocate writing Spad code. The standards idea is supposed to be
somewhat more general, not a self-serving effort.

I am looking at COQ for a different reason, namely that I'm trying
to prove an Axiom algorithm correct. See
http://axiom-developer.org/axiom-website/bookvol13.pdf
for the place-holder document. I started with the euclidean algorithm.
There are "layers" of the problem so I'm looking at COQ for a
Spad-to-Lisp proof, ACL2 for a Lisp-to-C proof, and my own research on
Conditional Concurrent Assignments for C-to-Intel semantics. This is
a "thin-thread" approach, trying to take one algorithm all the way
from Spad to the machine.

It would be really useful if the standard algorithms could be proven
correct. Code generation from COQ would be ideal. 

Tim









reply via email to

[Prev in Thread] Current Thread [Next in Thread]