一句话：证明对构成有效预簇的形式级数类，交换性可判定，并应用于多项式/洗牌/渗透自动机与代数差分方程。
本文研究非交换变量形式级数的交换性问题：级数输出值是否与输入符号顺序无关。给定某类形式级数的有限表示，判定其是否交换是一个自然但此前未从算法角度考察的问题。作者引入有效预簇概念，推广 Reutenauer 的形式级数簇，并证明所有有效预簇的交换性问题均可判定。作为应用，作者证明多项式自动机、洗牌自动机与渗透自动机各自识别一个有效预簇，因此其交换性可判定，这是新结果。最后，作者将交换性判定用于受限代数差分方程与微分方程，判定序列和幂级数的可解性，并证明多元多项式递归序列和可构造微分代数幂级数的语法是有效的，解决了先前工作留下的开放问题。
A formal series in noncommuting variables Σ over the rationals is a mapping ${\Sigma ^{\ast}} \to \mathbb{Q}$ from the free monoid generated by Σ to the rationals. 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ützenberger 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.
DOI 原文 ·
@inproceedings{paperbot8620,
title = {The commutativity problem for effective varieties of formal series, and applications},
author = {Lorenzo Clemente},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00066}
}