New methods for building computer algebra systems

点击翻译按钮获取中文摘要

The main objective of this research is to fundamentally re-examine the methodology currently used to build Computer Algebra Systems, aiming to make substantial improvements.  Computer Algebra Systems (CAS) are well-known to be at the forefront of many new programming language technologies (generic programming, dependent types, first-class types, etc), as well adopting advanced software engineering techniques long before they are popular in the mainstream.  While the development of new, faster algorithms in the area of Computer Algebra has proceeded at a breakneck pace in the last few years, engineering issues have received less attention.  However, recent progress in such areas as type theory, denotational semantics for nominal languages, generative programming and automated testing can all be profitably applied to the construction of CASes.We propose to re-examine, the current state-of-the-art in CAS development, and adapt current techniques in adjoining fields.  Just as simple type theory was too weak for Computer Algebra, it is expected that similar leaps will be needed in many areas of programming language theory and software engineering to properly address the very complex needs of a CAS.  First, we intend to concentrate on ``generic efficiency'', or how to write algorithms once using generative techniques to produce highly efficient specialized versions.  In our MetaOCaml experiments, the correctness guarantees are much higher than in traditional settings, while obtaining very efficient results at a fraction of the effort of developing new optimizing compiler techniques.  Secondly, current notions of polymorphism are not sufficient to appropriately express the kinds of ``genericity'' found in mathematics.  Approaches that frankly embrace developments in category theory will hopefully bear fruit.  This approach has worked very well for the development of powerful specification languages, we hope it can do something similar for programming languages.