Symbolic synthesis of Mealy machines from arithmetic bitstream functions

In this paper, we describe a \emph{symbolic} synthesis method which given an algebraic expression that specifies a bitstream function $f$, constructs a (minimal) Mealy machine that realises $f$. The synthesis algorithm can be seen as an analogue of Brzozowski's construction of a finite deterministic automaton from a regular expression. It is based on a coinductive characterisation of the operators of 2-adic arithmetic in terms of stream differential equations.