> If we decorate the Categories with their mathematical axioms can > > we prove anything about them? Can we do it automatically using ACL2? > > Can we extend the compiler to do the proof while it compiles? > > > Very difficult.
Clearly but I think that this is one of the most interesting areas of research. Axiom has an advantage over other systems like Maple and Mathematica because of our structure. In the long term it is important that we are able to trust the results of computations, especially when the results are beyond checking by hand. The only way to build trust will be proving the programs correct. Unlike random programs, computer algebra programs have a good theory behind them. I think it is vital that we develop a theory and a mechanism for proof of computer algebra programs. It's the old Legendre vs Gauss argument... we can't just assert that our programs are right, we need to prove it. Otherwise it hardly qualifies as a science. Also of interest is that computational math is not quite the same as math. Axiom has some categories, such as RNG, which don't seem to match those of regular math. One question is whether this is just a design flaw or does it expose a new computational object that we need to examine theoretically. The same issue arises in proofs. I often see statements that some algorithm works "over the integers" and is of order O(n^2) or some such. However, my computer does not have integers. It has fixnums and bignums. The algorithm may be O(n^2) for fixnums but become O(n^3) for bignum values. The standard methods of statements based "on the integers" often don't take this into account. Yeah, it's difficult but that's what makes it fun. t _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
