- Algebra hierarchy -- build up monoids, groups, fields etc and develop the basic theory of these structures also give concrete implementations of things like integers, reals (isomorphisms with efficient representations would be nice too!)
- Algebraic algorithms -- produce algorithms that can be used to help me do mathematics (e.g. factoring, transformations, solving classes of equations)
- Wiki -- Dependently typed programming in the large has already been done, they came up with FTA and FTC -- this is a constructive proof that it works!
There are some projects already working on this kind of thing, http://c-corn.cs.ru.nl/, http://github.com/Eelis/new-alg-hierarchy, http://www.lix.polytechnique.fr/coq/contribs/Algebra.html, http://hlombardi.free.fr/liens/constr.html, http://www.lix.polytechnique.fr/~assia/rech-eng.html, help make this list bigger!.
Ignoring these would be so dammed stupid I am not even going to think about it, but I want to point out that unless we make the most use of these projects as is possible then anything we create will be an anti-social library that nobody can use except me -- that is not desirable.
I think the only way to get this done is by collaborating with other people in a formally checked wiki (http://www.vdash.org/, http://code.google.com/p/hol-online/, http://prover.cs.ru.nl/login.php, http://www.cs.ru.nl/~herman/afstud.html, more?). These projects are all 'beta' that don't let everyone get involved so that's not very useful. Lets write it in Ur perhaps, using Coq as a subprocess. The directory structure of the Coq libraries would reflect that of the wiki. Edits will be accepted if they are checked and correct. I think once you have a spinal chord implemented, people will be able to add on parts quite easily.
I see no reason why someone with a bit of time wouldn't pick up Disquisitiones Arithmeticae or whatever and fold it into the wiki. With a bit of work getting everything set up correctly I think we could make a useful (basic) algebra system.
No comments:
Post a Comment