Commutative algebras of series
Pith reviewed 2026-05-16 10:37 UTC · model grok-4.3
The pith
Polynomial product rules completely characterise all bilinear associative commutative products on noncommuting series and make P-automaton equivalence decidable.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The central claim is a complete and decidable characterisation of all polynomial product rules P such that the coinductively defined P-product is bilinear, associative and commutative. The paper further proves that whenever P satisfies this characterisation, the equivalence problem for P-automata is decidable. This result subsumes and extends prior decidability theorems for Hadamard, shuffle and infiltration automata.
What carries the argument
The P-product, defined coinductively by a polynomial product rule P that gives a recursive recipe for building the product of two series from the series themselves and their derivatives.
If this is right
- There are infinitely many bilinear associative commutative products on noncommuting series.
- Equivalence of P-automata is decidable for every P-product satisfying the characterisation.
- Decidability results for Hadamard, shuffle and infiltration automata are special cases of the general theorem.
- P-automata form an infinite-state model whose states are terms built from the series.
Where Pith is reading between the lines
- The characterisation opens the possibility of constructing new product operations tailored to specific concurrency models.
- The coinductive presentation may allow coalgebraic techniques to prove further properties of P-automata beyond equivalence.
- Similar recursive rule-based characterisations could apply to products over other algebraic structures such as semirings.
Load-bearing premise
The product is defined coinductively by a polynomial product rule P on formal power series in noncommuting indeterminates.
What would settle it
A polynomial product rule P that produces a bilinear, associative and commutative product yet lies outside the characterised class, or a P inside the class for which P-automaton equivalence turns out to be undecidable.
Figures
read the original abstract
We consider a large family of product operations of formal power series in noncommuting indeterminates, the classes of automata they define, and the respective equivalence problems. A $P$-product of series is defined coinductively by a polynomial product rule $P$, which gives a recursive recipe to build the product of two series as a function of the series themselves and their derivatives. The first main result of the paper is a complete and decidable characterisation of all product rules $P$ giving rise to $P$-products which are bilinear, associative, and commutative. The characterisation shows that there are infinitely many such products, and in particular it applies to the notable Hadamard, shuffle, and infiltration products from the literature. Every $P$-product gives rise to the class of $P$-automata, an infinite-state model where states are terms. The second main result of the paper is that the equivalence problem for $P$-automata is decidable for $P$-products satisfying our characterisation. This explains, subsumes, and extends previous results on Hadamard, shuffle, and infiltration automata. We have formalised most results in the proof assistant Agda.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper defines a family of P-products on formal power series in noncommuting indeterminates via coinductive polynomial rules P. It gives a complete and decidable characterization of those P yielding bilinear, associative, and commutative products (including Hadamard, shuffle, and infiltration as special cases). It proves that equivalence of the induced P-automata is decidable precisely when P satisfies the characterization, and reports an Agda formalization of most results.
Significance. The results unify and extend prior work on specific products and automata by supplying an exhaustive classification together with machine-checked evidence. The decidability theorem for equivalence directly subsumes earlier results on Hadamard, shuffle, and infiltration automata while revealing that infinitely many such products exist. The coinductive approach and Agda development provide a solid foundation for further study of commutative algebras of series.
minor comments (2)
- The abstract states that the characterization is complete and decidable but does not indicate the syntactic form of the admissible rules P; a one-sentence description would improve immediate readability.
- Section 2 introduces the coinductive definition of the P-product; an explicit small example (e.g., the rule for the shuffle product) immediately after the general definition would help readers verify the recursive construction.
Simulated Author's Rebuttal
We thank the referee for their positive assessment of the manuscript and for recommending acceptance. We are pleased that the complete decidable characterization of P-products and the decidability result for P-automata equivalence, along with the Agda formalization, were viewed favorably as unifying and extending prior work.
Circularity Check
No significant circularity; derivation is self-contained
full rationale
The central result is a mathematical classification of polynomial product rules P such that the coinductively defined P-product is bilinear, associative and commutative. This characterisation is obtained directly by inspecting the recursive structure of the coinductive definition and enumerating the admissible coefficient patterns; the Agda formalisation supplies machine-checked evidence that the listed properties hold exactly for the rules satisfying the characterisation. No equation reduces to a fitted parameter, no uniqueness theorem is imported from prior self-work, and no ansatz is smuggled via citation. The decidability of P-automaton equivalence is a direct consequence of the same finite characterisation rather than a re-statement of the input. The derivation is therefore independent of its own outputs.
Axiom & Free-Parameter Ledger
axioms (2)
- domain assumption Formal power series in noncommuting indeterminates form a coinductive structure equipped with derivatives.
- domain assumption The product rule P is a polynomial in the appropriate variables.
Reference graph
Works this paper leans on
-
[1]
Henning Basold, Helle Hvid Hansen, Jean-Éric Pin, and Jan Rutten
-
[2]
Newton series, coinductively: a comparative study of composi- tion.Mathematical Structures in Computer Science, 29, 1, (June 2017), 38–66. doi:10.1017/s0960129517000159
-
[3]
M. Benedikt, T. Duff, A. Sharad, and J. Worrell. 2017. Polynomial automata: zeroness and applications. InProc. of LICS’17. (June 2017), 1–12. doi:10.1109/LICS.2017.8005101
-
[4]
François Bergeron and Christophe Reutenauer. 1990. Combinatorial resolution of systems of differential equations iii: a special class of differentially algebraic series.European Journal of Combinatorics, 11, 6, 501–512. doi:10.1016/S0195-6698(13)80035-2
-
[5]
J. Berstel and C. Reutenauer. 2010.Noncommutative rational series with applications. CUP.isbn: 0521190223
work page 2010
-
[6]
Bonsangue, Helle Hvid Hansen, Alexander Kurz, and Jurriaan Rot
Marcello M. Bonsangue, Helle Hvid Hansen, Alexander Kurz, and Jurriaan Rot. 2015. Presenting distributive laws.Logical Methods in Computer Science, Volume 11, Issue 3, (Aug. 2015). doi:10.2168/lmcs- 11(3:2)2015
-
[7]
Michele Boreale, Luisa Collodi, and Daniele Gorla. 2024. Products, polynomials and differential equations in the stream calculus.ACM Trans. Comput. Logic, 25, 1, Article 7, (Jan. 2024), 26 pages. doi:10.11 45/3632747
work page 2024
-
[8]
Michele Boreale and Daniele Gorla. 2021. Algebra and Coalgebra of Stream Products. InProc. of CONCUR’21(Leibniz International Pro- ceedings in Informatics (LIPIcs)). Serge Haddad and Daniele Varacca, editors. Vol. 203. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 19:1–19:17.isbn: 978-3-95977-203-7. doi:10.4230 /LIPIcs.CONCUR.2021.19
work page 2021
-
[9]
Michaël Cadilhac, Filip Mazowiecki, Charles Paperman, Michał Pilipczuk, and Géraud Sénizergues. 2021. On polynomial recursive sequences. Theory of Computing Systems.isbn: 1433-0490. doi:10.1007/s00224-0 21-10046-9
-
[10]
Kuo-Tsai Chen, Ralph H. Fox, and Roger C. Lyndon. 1958. Free Differ- ential Calculus, IV. The Quotient Groups of the Lower Central Series. The Annals of Mathematics, 68, 1, (July 1958), 81. doi:10.2307/1970044
-
[11]
Lorenzo Clemente. 2025. The commutativity problem for effective varieties of formal series, and applications. InIn Proc. of LICS’25. IEEE, (June 2025), 804–817. doi:https://dx.doi.org/10.1109/lics65433 .2025.00066
-
[12]
Lorenzo Clemente. 2025. The commutativity problem for effective varieties of formal series, and applications. (2025). doi:https://dx.doi .org/10.48550/arxiv.2503.21697
-
[13]
Lorenzo Clemente. 2024. Weighted Basic Parallel Processes and Com- binatorial Enumeration. In35th International Conference on Concur- rency Theory (CONCUR 2024)(Leibniz International Proceedings in Informatics (LIPIcs)). Rupak Majumdar and Alexandra Silva, edi- tors. Vol. 311. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 18:1–18:2...
work page 2024
-
[14]
Cox, John Little, and Donal O’Shea
David A. Cox, John Little, and Donal O’Shea. 2015.Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. (4th ed.).Undergraduate Texts in Math- ematics. Springer International Publishing.isbn: 978-3-319-16720- 6,978-3-319-16721-3. http://gen.lib.rus.ec/book/index.php?md5=003a db5eacf2735a849e496c5f16ed26
work page 2015
-
[15]
2009.Hand- book of Weighted Automata.Monographs in Theoretical Computer Science
Manfred Droste, Werner Kuich, and Heiko Vogler, eds. 2009.Hand- book of Weighted Automata.Monographs in Theoretical Computer Science. Springer
work page 2009
-
[16]
Michel Fliess. 1981. Fonctionnelles causales non linéaires et indéter- minées non commutatives.Bulletin de la Société mathématique de France, 79, 3–40. doi:10.24033/bsmf.1931
-
[17]
Michel Fliess. 1974. Sur divers produits de séries formelles. fr.Bulletin de la Société Mathématique de France, 102, 181–191. doi:10.24033/bs mf.1777
work page doi:10.24033/bs 1974
-
[18]
Michel Fliess. 1976. Un outil algebrique: les series formelles non commutatives. InMathematical Systems Theory. Giovanni Marchesini and Sanjoy Kumar Mitter, editors. Springer Berlin Heidelberg, Berlin, Heidelberg, 122–148.isbn: 978-3-642-48895-5. doi:10.1007/978-3-64 2-48895-5_9
-
[19]
Helle Hvid Hansen, Clemens Kupke, and Jan Rutten. 2017. Stream Differential Equations: Specification Formats and Solution Methods. Logical Methods in Computer Science, Volume 13, Issue 1, (Feb. 2017). doi:10.23638/LMCS-13(1:3)2017
-
[20]
Bart Jacobs. 2006. A bialgebraic review of deterministic automata, regular expressions and languages. InAlgebra, Meaning, and Com- putation. Springer Berlin Heidelberg, 375–404. doi:10.1007/11780274 _20
-
[21]
1957.An Introduction to Differential Algebra
Irving Kaplansky. 1957.An Introduction to Differential Algebra. (1st ed.). Actualites Scientifiques Et Industrielles, 1251. Hermann
work page 1957
-
[22]
Manuel Kauers and Peter Paule. 2011.The Concrete Tetrahedron: Sym- bolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. (1st ed.).Texts and Monographs in Symbolic Computation. Springer-Verlag Wien.isbn: 978-3-7091-0444-6,978-3-7091-0445-3
work page 2011
-
[23]
Bartek Klin. 2011. Bialgebras for structural operational semantics: an introduction.Theoretical Computer Science, 412, 38, 5043–5069. CMCS Tenth Anniversary Meeting. doi:10.1016/j.tcs.2011.03.023
- [24]
- [25]
-
[26]
Ernst Mayr. 1989. Membership in polynomial ideals over Q is ex- ponential space complete. InIn Proc. of STACS’89. B. Monien and R. Cori, editors. Springer Berlin Heidelberg, Berlin, Heidelberg, 400– 406.isbn: 978-3-540-46098-5. doi:10.1007/BFb0029002
-
[27]
Masakazu Nasu and Namio Honda. 1969. Mappings induced by PGSM-mappings and some recursively unsolvable problems of finite probabilistic automata.Information and Control, 15, 3, (Sept. 1969), 250–273. doi:10.1016/s0019-9958(69)90449-5
-
[28]
Dmitri Novikov and Sergei Yakovenko. 1999. Trajectories of poly- nomial vector fields and ascending chains of polynomial ideals. en. Annales de l’Institut Fourier, 49, 2, 563–609. doi:10.5802/aif.1683
-
[29]
1971.Introduction to Probabilistic Automata.Computer Science and Applied Mathematics
Azaria Paz. 1971.Introduction to Probabilistic Automata.Computer Science and Applied Mathematics. Elsevier Inc, Academic Press Inc. isbn: 978-0-12-547650-8,0125476507
work page 1971
-
[30]
J. J. M. M. Rutten. 2005. A coinductive calculus of streams.Math- ematical Structures in Computer Science, 15, 1, (Feb. 2005), 93–147. doi:10.1017/s0960129504004517
-
[31]
J. J. M. M. Rutten. 2003. Behavioural differential equations: a coin- ductive calculus of streams, automata, and power series.Theoretical Computer Science, 308, 1, 1–53. doi:10.1016/S0304-3975(02)00895-2
-
[32]
Marcel-Paul Schützenberger. 1961. On the definition of a family of automata.Information and Control, 4, 2–3, (Sept. 1961), 245–270. doi:https://dx.doi.org/10.1016/s0019-9958(61)80020-x
-
[33]
Daniele Turi and Gordon Plotkin. 1997. Towards a mathematical operational semantics. InProc. of LICS’97. IEEE Comput. Soc, 280–
work page 1997
-
[34]
doi:10.1109/lics.1997.614955. Conference acronym ’XX, June 03–05, 2018, Woodstock, NY Lorenzo Clemente A ADDITIONAL PROOFS In this section we present some additional proofs which were omitted from the main text. A.1 Associativity We show that a bilinear product rule 𝑃 (bilinear form) is associative if, and only if, the parameters 𝛼, 𝛽 1, 𝛽2, 𝛾∈Q satisfy t...
-
[35]
· ¤𝑥𝑦𝑧+ (𝛽 1𝛽2 −𝛽 2𝛽1) ·𝑥¤𝑦𝑧+ (𝛽 2 1 −𝛽 1 −𝛾𝛼) ·𝑥𝑦¤𝑧+ (𝛾 𝛽2 −𝛽 2𝛾) · ¤𝑥¤𝑦𝑧+ (𝛾 𝛽1 −𝛾 𝛽 2) · ¤𝑥𝑦¤𝑧+ (𝛽 1𝛾−𝛾 𝛽 1) ·𝑥¤𝑦¤𝑧+ (𝛾2 −𝛾 2) · ¤𝑥¤𝑦¤𝑧=0. By equating each coefficient to zero and simplifying, we obtain (4). A.2 Simulating the constant term Let 𝑋= {𝑥1, . . . , 𝑥𝑘 } be a finite set of variables. We show that polynomial 𝑃-automata over Q[𝑋] can be simula...
work page 2018
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.