The commutativity problem for effective varieties of formal series, and applications

TL;DR

This work establishes that commutativity for broad classes of noncommutative formal series is decidable when the classes form an effective prevariety, unifying rational, Hadamard-finite, shuffle-finite, infiltration-finite, and related series under one algorithmic framework. It introduces Hadamard and shuffle automata (and their infiltrations) as syntactic representations whose finite-generation and derivative-closure yield decidability, including Ackermann- and 2-EXPSPACE complexities for key problems. The paper then applies these results to multivariate polynomial recursive sequences (polyrec) and constructible differentially algebraic power series (CDA), proving solvability/consistency questions are decidable in multivariate settings, often with high but precise complexity bounds. Extensions to mixed products and algebraic varieties of commutative series broaden the scope, enabling effective syntax and decision procedures for a wide range of models and applications. Overall, the work provides a uniform, algorithmic approach to longstanding open decidability questions in noncommutative and commutative series, with concrete implications for sequences, differential equations, and constructible power series.

Abstract

A formal series in noncommuting variables $Σ$ over the rationals is a mapping $Σ^* \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ü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.

Figures (1)

• Figure 1: The six constraints on the computation of $f(2, 2)$.

Theorems & Definitions (126)

• Theorem 1
• Theorem 2
• Example 1
• Example 2
• Lemma 1: Left and right derivatives commute
• Lemma 2: Characterisation of commutativity
• Theorem 2
• proof
• Remark 1
• Lemma 3