Formal power series over an alphabet $α$ are functions from words $List α$ to the rationals. They carry the pointwise vector-space structure, the left and right derivatives (the series analogues of language quotients), the reversal, the support, and the Parikh image. A series is commutative when it is constant on words with the same Parikh image. This module records the basic definitions of §2 of the paper together with the elementary facts about derivatives and reversal that the later sections use.

The commutativity problem asks whether a series is commutative, i.e. constant on words with the same Parikh image. The key observation (paper §3) is that commutativity is characterised by two finite families of equations, swap and rotate, which makes it decidable for effective prevarieties (the meta-theorem). Conversely, the zeroness problem reduces to commutativity: given $f$, one builds a series $g$ over a two-letter-enlarged alphabet, supported on words beginning with the two fresh letters, such that $g$ is commutative exactly when $f = 0$.

A series is linearly finite if it lies in a finitely generated $ℚ$-space of series closed under left derivatives; it is recognisable if it is recognised by a linear representation $(k, x, y, M)$, i.e. $f (w) = x · M(w) · y$. The two notions coincide (a classical result). The class of recognisable series is an effective prevariety — equality is decidable by linear algebra — and hence the commutativity problem is decidable for it (paper §4). This is the only chain in the proof network that does not depend on the ideal-membership statement.

A series is Hadamard-finite if it lies in the Hadamard algebra generated by a finite tuple of series that is closed under left derivatives (paper §5): the Hadamard product is the pointwise product of the underlying functions, so the Hadamard algebra is just the (pointwise) ring of series. Equivalently (the coincidence), it is recognised by a Hadamard automaton $(k, F, Δ)$: a configuration space $ℚ[X_1, …, X_k]$, a final-weight functional $F$, and a transition $Δ_a$ that extends to an endomorphism of the configuration space. The Hadamard-finite series form an effective prevariety, so equality and the commutativity problem are decidable for them; the equality decision reduces to ideal membership in the configuration polynomial ring (the ideal-membership statement).

A multivariate polynomial recursive sequence (polyrec sequence) in $d$ variables is a $k$-tuple of sequences $f : ℕ^d → ℚ$ satisfying polynomial equations $shift_j f_i = p^{(j)}_i(f_1, …, f_k)$ (paper §5.4), where $shift_j$ is the shift in the $j$-th coordinate and $p^{(j)}_i$ are polynomials evaluated pointwise in the sequences. The consistency problem asks whether, given the equations and an initial condition $f_i(0) = c_i$, a solution exists. This is decidable (paper §5.4, theorem $polyrec consistency$): the polyrec system is isomorphic to a Hadamard system over the $d$-letter alphabet, so a solution exists exactly when the companion Hadamard series are commutative, which is decidable.

A series is shuffle-finite if it belongs to a finitely generated differential shuffle algebra (paper §6.2.2): it is a shuffle polynomial in a finite tuple of series that is closed under left derivatives. Equivalently (the coincidence), it is recognised by a shuffle automaton $(k, F, Δ)$: a configuration space $ℚ[X_1, …, X_k]$, a final-weight functional $F$, and a transition $Δ_a$ that extends to a derivation of the configuration space (the paper's differential- algebra structure, §6). The shuffle-finite series form an effective prevariety, so equality and the commutativity problem are decidable for them; the equality decision reduces to ideal membership in the configuration polynomial ring (the ideal-membership statement), via the same ideal-chain argument as for the Hadamard and infiltration automata.