Nie jesteś zalogowany | Zaloguj się

We study an expressive syntax in which one can coinductively define product operations on series.

For instance, we can model the known Hadamard, shuffle, and infiltration products,

and in fact any binary operation obeying a so called "product rule" w.r.t. left derivatives

(e.g., shuffle obeys the well-known Leibniz rule from calculus).

Our main result is a complete equational characterisation of coinductively defined products which are bilinear, associative, and commutative.

In this way, we recover such properties for the notable products above,

but also for other infinite families of products of which we were not previously aware.

For each such well-behaved coinductive product, we obtain a corresponding "generalised polynomial automaton" model,

where states are polynomials and transitions follow the product rule.

As an unexpected consequence, generalised polynomial automata have a decidable zeroness, equivalence, and commutativity problems.

As a special case, we recover known decidability results for polynomial, shuffle and infiltration automata.

Bonus: The characterisation can be carried over with small effort in the Agda proof assistant.

Commutative algebras of series