非交换变量形式级数的有效类及其应用中的可换性问题
The commutativity problem for effective varieties of formal series, and applications
摘要 Abstract
有理数域上的非交换变量$\Sigma$的形式级数是从$\Sigma^*$到$\mathbb Q$的映射。如果输出值不依赖于输入符号的顺序,则称该级数为可换的。对于一类级数的可换性问题,其输入是该类中一个(有限表示的)级数,并且目标是确定它是否是可换的。这是一个非常自然但并不平凡的问题,之前从未从算法的角度进行过考虑。我们证明了对于所有构成所谓有效预簇(generalizing Reutenauer的形式级数簇的概念)的级数类,可换性是可判定的。例如,Schützenberger在20世纪60年代引入的有理级数类,众所周知是一个有效的(预)簇,因此对于它来说可换性问题是可判定的。为了展示我们的结果的适用性,我们考虑了推广有理级数类的形式级数类。我们研究了多项式自动机、shuffle自动机和渗滤自动机,并证明每个模型都识别出一个有效预簇的形式级数。因此,它们的可换性问题是可判定的,这是一个新的结果。我们发现,对于如此不同的计算模型,可换性可以在统一的方式下被判定,这一点令人印象深刻。最后,我们将可换性问题的应用扩展到形式级数理论之外。我们展示了可以决定某些受限类代数差分和微分方程的序列和幂级数的可解性,对于这些问题在完全一般的情况下是不可判定的。通过这些,我们能够证明多元多项式递归序列和构造可微代数幂级数的语法是有效的,这些都是先前工作中遗留下的新结果。
A formal series in noncommuting variables $\Sigma$ over the rationals is a mapping $\Sigma^* \to \mathbb Q$. We say that a series is commutative if the value in the output does not depend on the order of the symbols in the input. The commutativity problem for a class of series takes as input a (finite presentation of) a series from the class and amounts to establishing whether it is commutative. This is a very natural, albeit nontrivial problem, which has not been considered before from an algorithmic perspective. We show that commutativity is decidable for all classes of series that constitute a so-called effective prevariety, a notion generalising Reutenauer's varieties of formal series. For example, the class of rational series, introduced by Sch\"utzenberger in the 1960's, is well-known to be an effective (pre)variety, and thus commutativity is decidable for it. In order to showcase the applicability of our result, we consider classes of formal series generalising the rational ones. We consider polynomial automata, shuffle automata, and infiltration automata, and we show that each of these models recognises an effective prevariety of formal series. Consequently, their commutativity problem is decidable, which is a novel result. We find it remarkable that commutativity can be decided in a uniform way for such disparate computation models. Finally, we present applications of commutativity outside the theory of formal series. We show that we can decide solvability in sequences and in power series for restricted classes of algebraic difference and differential equations, for which such problems are undecidable in full generality. Thanks to this, we can prove that the syntaxes of multivariate polynomial recursive sequences and of constructible differentially algebraic power series are effective, which are new results which were left open in previous work.