Automata, power series, and coinduction : taking input derivatives seriously (extended abstract)

Formal power series, which are functions from the set of words over an alphabet $A$ to a semiring $k$, are viewed coalgebraically. In summary, this amounts to supplying the set of all power series with a deterministic automaton structure, which has the universal property of being final. Finality then forms the basis for both definitions and proofs by coinduction, the coalgebraic counterpart of induction. Coinductive definitions of operators on power series take the shape of what we have called behavioural differential equations, after Brzozowski's notion of input derivative, and include many classical differential equations for analytic functions. The use of behavioural differential equations leads, amongst others, to easy definitions of and proofs about both existing and new operators on power series, as well as to the construction of finite (syntactic) nondeterministic automata, implementing them.