Algebraic Specification and Coalgebraic Synthesis of Mealy Automata

We introduce the notion of functional stream derivative, generalising the notion of input derivative of rational expressions (Brzozowski 1964) to the case of stream functions over arbitrary input and output alphabets. We show how to construct Mealy automata from algebraically specified stream functions by the symbolic computation of functional stream derivatives. We illustrate this construction in full detail for various bitstream functions specified in the algebraic calculus of the 2-adic numbers. This work is part of a larger ongoing effort to specify and model component connector circuits in terms of (functions and relations on) streams.