[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Symbolic Algorithms Standards
From: |
kp |
Subject: |
Re: [Axiom-developer] Symbolic Algorithms Standards |
Date: |
Mon, 11 Aug 2014 23:00:14 +0200 |
User-agent: |
Mozilla/5.0 (Windows NT 6.1; WOW64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0 |
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
(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.
Kurt
Am 10.08.2014 04:54, schrieb Tim Daly:
> The time has come, it seems to me, to organize an effort to
> collect and standardize symbolic algorithms, similar in spirit
> to the NIST Handbook of Mathematical Functions.
>
> It should be possible to order algorithm development for things
> like integration, starting with Liouville's work, then Risch, etc.
> The idea is to provide the algorithm and a series of improvements
> in some reasonably accessible pseudocode, perhaps with some
> agreed-upon benchmark of time and space complexity. There should
> also be an associated website with a cache of the papers for each
> algorithm. The book would be updated yearly with new developments.
>
> I have been collecting bibliographic references as part of the
> Axiom project and have recently started organizing them by topic.
> http://axiom-developer.org/axiom-website/bookvolbib.pdf
>
> Is a NIST-like algorithm collection reasonable? Opinions welcome.
>
> Tim Daly
> address@hidden
>
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>