In this talk I will present a method for constructing Mealy machines from arithmetic bitstream specifications. This method was described by Jan Rutten in his FACS'05 paper. David Costa and myself have implemented this synthesis procedure in Haskell, and experimental results have led to a conjecture on the minimal size of Mealy machines which implement so-called rational 2-adic functions.

For given sets (alphabets) A and B, a Mealy machine with input in A and output in B is a (deterministic) finite state transducer whose input-output behaviour is the stream function f:A^omega -> B^omega it computes. The dynamics of a Mealy machine is easily seen to be coalgebraic, and the coalgebraic notion of behaviour coincides with the input-output behaviour. In fact, the set of all Mealy machine behaviours forms a final coalgebra by defining transitions in terms of derivatives of stream functions, a notion similar to the derivative of a regular language. As a consequence, given a stream function f, the subcoalgebra generated by f in the final coalgebra implements f. The synthesis method consists in a symbolic computation of the generated subcoalgebra in the syntax of the chosen specification language. The Haskell program realises this for specifications in two bitstream algebras, one based on modulo-2 arithmetic, and the other on 2-adic arithmetic. In order to guarantee termination of this least fixpoint computation, it is crucial that the syntax allows an effective decision procedure for semantic equivalence. For the two bitstream algebras this is achieved by reduction to normal forms. For rational 2-adic functions, the number of states in the minimal implementation can be determined directly from the specification, and this number is (essentially) exponential in the length of the specification, but linear in the numeric intepretation of 2-adic expressions.