基于Groebner基理论和距离不变量方法的指标多项式标准型及其应用研究

The simplification and normalization of algebraic expressions is an "ancient" research topic, which is both important and fundamental in computer algebra. However, indexed expressions obey Einstein summation convention which stands for a composition of multiplication and addition, making the algebraic structure of indexed expressions much more complex. And Groebner basis theory is not yet powerful enough to deal with such algebraic structure. Therefore, the simplification and normalization of indexed expressions remains to be a challenging problem. On the other hand, modern differential geometry and physics often involve massive manual calculations of indexed expressions which are tricky and cumbersome to perform. They call for both theoretical results and algorithms for simplifying and normalizing indexed polynomials. However, existing algorithms either have low efficiency or cannot be extended. To solve these problems, this project first develops a general normalization algorithm of indexed polynomials with respect to interior symmetries, and a normalization algorithm of indexed differentials, by extending Groebner basis theory due to the method of constructing minimal restricted monoid rings. Secondly, provides an index replacement algorithm based on multi-level distance invariants, which is then used to establish efficient normalization algorithms. Finally the algorithms are applied to mechanically solving tensor verification problem and the problem of finding transformation rules of indexed functions under coordinate transformation, and to mechanically proving and exploring formulas and theorems involving several important and fundamental tensors in differential geometry.

多项式的化简和标准型是计算机代数中的一个关键而基本的古老研究课题，然而指标多项式满足Einstein求和约定，其本质上是采用符号表示乘法与加法的复合，从而引起有关的代数结构发生根本变化。关于该代数结构的Groebner基等理论尚不存在，这成为计算机代数中一个挑战性问题。另一方面，现代微分几何和物理学中常常涉及指标多项式的大量复杂、技巧性计算和推导，迫切需要关于指标多项式化简和标准型的理论与算法。而现有算法效率较低或只面向特定指标多项式而不可推广。针对上述问题，本项目首先通过构造最小“限制”幺半群环，进而运用Groebner基理论建立指标多项式关于内部对称性标准型，以及微分指标多项式标准型一般性算法，其次提炼多层次距离不变量，发展基于距离不变量的指标赋值法，用于建立高效标准型算法。最后应用于微分几何中张量判定、坐标变换下的规律问题的自动求解，和关于多种重要而基本张量的公式及定理的自动证明。

Einstein求和约定下的指标多项式在微分几何、张量分析等研究中频繁出现，涉及大量的计算、推导，通常都需要较强的技巧。一个自然的符号计算问题是：如何完全判断任意两个指标多项式是否相等？然而，Einstein求和约定本质上是采用符号表示乘法与加法的复合，使得Einstein求和约定的形式乘法不再具有结合性，另外，由于哑指标的重命性，指标多项式环的定义合冲理想不可有限生成。关于这种代数结构的Groebner基理论，目前尚不存在。因此，研究和发展指标多项式标准型理论与算法，不仅将会推动非结合代数理想和无限生成理想的Groebner基问题研究，也会推动现代微分几何定理自动证明，甚而解决微分几何本身的一些难题。.本项目着眼于符号计算中指标多项式相等判定这一基本问题，以任意指标多项式关于内部对称性的高效标准型算法研究为基础，进而研究微分指标多项式和非普通张量指标多项式的化简和标准型理论与算法，并在计算机代数系统中实现相应算法，最后应用于研究n维微分几何中公式、定理自动证明和推导。.本项目重要结果如下：.一、建立了指标多项式关于内部对称性标准型的一般性理论和高效算法，具体如下：.(1) 提出了构造ST-限制环的研究方法，将Groebner基理论进行了推广，建立了指标多项式关于内部对称性标准型的（一般性）理论。.(2) 运用指标距离不变量、对称块距离不变量等方法发展了微分指标多项式、Riemann张量指标多项式高效标准型算法，其复杂性远低于现有算法。.二、建立了微分指标多项式标准型的一般性理论。基于Leibniz展开定义初等指标单项式集合上的等价关系，并找到了每个等价类中元素的sim-多项式的哑指标个数上限，据此上限构造出基础限制环，证明了多项式的标准型就是它在基础限制环中的标准型。.三、将上述标准型理论和算法应用于微分几何中张量判定、坐标变换下的规律问题自动推导，以及重要而基本的张量的公式、定理证明。