New methods for building computer algebra systems

这项研究的主要目标是从根本上重新审视目前用于构建计算机代数系统的方法，旨在做出实质性的改进。 众所周知，计算机代数系统（CAS）是许多新的编程语言技术（泛型编程，依赖类型，第一类类型等）的前沿，以及采用先进的软件工程技术，早在主流流行之前。 虽然在过去的几年里，计算机代数领域新的、更快的算法的发展以惊人的速度进行，但工程问题却受到较少的关注。 然而，最近的进展，如类型理论，命名语言的指称语义，生成式编程和自动化测试等领域都可以有利地适用于建设CASes.We建议重新审视，目前的国家的最先进的CAS开发，并适应当前的技术在相邻领域。 正如简单类型理论对于计算机代数来说太弱一样，预计在编程语言理论和软件工程的许多领域都需要类似的飞跃，以适当地解决CAS的非常复杂的需求。 首先，我们打算专注于“通用效率”，或者如何使用生成技术编写算法以产生高效的专用版本。 在我们的MetaOCaml实验中，正确性保证比传统设置高得多，同时获得非常有效的结果，只需开发新的优化编译器技术的一小部分。 其次，目前的多态性概念不足以恰当地表达数学中的“一般性”。 坦率地接受范畴论发展的方法有望取得成果。 这种方法对于开发功能强大的规范语言非常有效，我们希望它可以为编程语言做类似的事情。

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.