Moore and Mealy machines in CST [lcc-0012]

Recall the classic definitions:

Definition Mealy machine [lcc-0013]

A Mealy machine with input A, output B and state space S, is a function A \times S \to B \times S.

Definition Moore machine [lcc-0014]

A Moore machine with input A, output B and state space S, is a pair of functions S \to B, A \times S \to S

The dynamical systems considered in Categorical Systems Theory are Moore-type machines - the output depends on the present state, but not (directly) on the input.

However, we can actually account for Mealy machines as well - a mealy machine with interface A (which is now an arena, i.e a pair of sets in the simplest case) and state space S is a lens TS \otimes A \to I, where I is the monoidal unit (here we assume the dynamical systems doctrine has enough structure to make the category of lenses monoidal).

In the simplest case, arenas are pairs of sets - then we have a lens \binom {S \times A'}{S \times A} \to \binom {*}{*}, which amounts to a map S \times A \to S \times A' as desired. But note that the input/output pairing has changed - now A' is the output and A the input

  • Given a Mealy machine and a Moore machine with the same interface, we can pair them to obtain a closed dynamical system T(S \otimes S') \to I. In general we can plug the two types of machines into each others' interfaces
  • Mealy machines reindex along lenses, but in the opposite direction from Moore machines
  • Given Mealy machines TS \otimes A \to I and TS' \otimes A' \to I, and a chart A \rightrightarrows A', there is a set of "maps of systems over this chart", namely maps S \to S' and 2-cells filling the resulting square. Thus we get something very similar to the usual double category of systems, lenses and charts, but with the lenses working in the opposite direction from what they usually do

References

Reference Categorical Systems Theory [myers-cst]

 
 @misc
{myers-cst, title={Categorical Systems Theory}, author={Myers, David Jaz},language={en} , url={http://davidjaz.com/Papers/DynamicalBook.pdf}}

Backlinks

Mealy machines as contexts in categorical systems theory [lcc-001B]

(Inspired by a conversation with Dylan Braithwaite, Matteo Capucci, Toby Smythe)

A "context" is "something you can plug a system into, producing a closed system. Recall that, given a (monoidal) theory of dynamical systems, a closed system is a system with interface I. So we may say that, when A is an interface, a context of type A should give a functor \mathsf {Sys}(A) \to \mathsf {Sys}(I).

Given a Mealy machine TS \otimes A \to I (see Moore and Mealy machines in CST), plugging into it thus gives a context of type A. Moreover, given a morphism of Mealy machines S \to S', we find a natural transformation between the induced functors---thus, we have a functor \mathsf {Mealy}(A) \to [\mathsf {Sys}(A),\mathsf {Sys}(I)].

On the other hand, this functor is not in general full. To see this, suppose we're working with the theory \mathcal {C} = \mathsf {Set}, \mathcal {A}(X) = \mathsf {Set}_{/X}, T(X) = X \times X \to X, i.e of simple discrete-time discrete-space systems. For an interface \binom {B}{A}, let \operatorname {Stream}(\binom {B}{A}) be the terminal coalgebra of the functor S \mapsto \sum _{a \in A} S^{B_a}---the set of "input-output streams". Let TS \otimes \binom {B}{A} \to I, TS' \otimes \binom {B}{A} \to I be two Mealy machines. Let f_w: S \to S' be a family of morphisms between them indexed by w \in \operatorname {Stream}(\binom {B}{A}). Given a dynamical system TX \to \binom {B}{A}, consider the mapping X \times S \to X \times S' which carries (x,s) to (x,f_w(s)) where w is the behaviour of x. It's not hard to see that this is a mapping between the two closed systems, and since any map of dynamical systems X \to X' must preserve the behaviour of points, this construction is a natural transformation. But clearly unless all the f_x are constant, this does not come from a map of Mealy machines.

It should be possible to build this into a full subcategory of [\mathsf {Sys}(A),\mathsf {Sys}(I)] given by families of Mealy machines indexed by the set of streams. Since every Moore machine (dynamical system) is a quotient of a coproduct of systems that are "free on a point with a specific behaviour", it seems likely that this full subcategory consists exactly of the cocontinuous functors (all this is specific to the particular case of sets, discrete-time and discrete space). This is vaguely analogous to the way the cocontinuous functors R-\mathsf {Mod} \to S-\mathsf {Mod} are classified by S-R bimodules.

Mealy and Moore machines as coalgebras [lcc-0019]

Let F: \mathcal {C} \to \mathcal {C} be a strong monoidal endofunctor. Then there is a dynamical systems doctrine where the indexed category is the trivial fibration \mathcal {C} \times \mathcal {C} \to \mathcal {C} (so that the category of "lenses" is really the category of adaptors \mathcal {C}^\mathrm {op} \times \mathcal {C}), and where the section is given by T(X) = (F(X), X)

A dynamical system with interface \binom {A}{B} is then an object S \in \mathcal {C} and a pair of maps S \to A, S \otimes B \to F(S). Recall (Moore and Mealy machines in CST) that this is a generalized form of Moore machine.

Conversely, a Mealy machine consists of a single map S \otimes A \to F(S) \otimes B.

Suppose \mathcal {C} is closed. Then a Mealy machine is a coalgebra for the endofunctor of \mathcal {C} given by S \mapsto [A, F(S) \otimes B].

If \mathcal {C} is furthermore Cartesian closed, then a Moore machine (ie, an open dynamical system in the usual sense) is a coalgebra of the functor S \mapsto A \times F(-)^B.

This suggests that Mealy machines are "more coalgebra-like" than Moore machines - we need fewer assumptions on the category \mathcal {C} to make them into coalgebras of a functor.

Monoidal streams as Mealy machines [lcc-0018]

See Moore and Mealy machines in CST for a discussion of Mealy machines. Recall from there that we can model a Mealy machine with interface A, in some dynamical systems doctrine, as a map TS \otimes A \to I.

Recall also that, in a monoidal category \mathcal {C}, a monoidal stream from (X_n)_{n\in \mathbb {N}} to (Y_n) is a sequence of objects S_n and morphisms X_n \otimes S_{n-1} \to Y_n \otimes S_n (with the convention that S_{-1} = I).

These seem like they should fit together, and they almost do. The problem is that this is defined in terms of a shift-backwards functor \partial : \mathcal {C}^\mathbb {N} \to \mathcal {C}^\mathbb {N}. We would like to define T in our dynamical systems doctrine so that TS = \binom {\partial ^{-1}S}{S} - then a Mealy machine would indeed be a monoidal stream. The problem is that \partial generally doesn't have an inverse - there is no way to shift a sequence of objects backwards without simply destroying the beginning.

However, if the set of scalars \mathcal {C}(I,I) is a singleton, because \partial is then fully faithful, we can extend the domain and codomain to make it an equivalence. In the concrete situation, this means extending to the subcategory of \mathcal {C}^\mathbb {Z} spanned by the bounded-below sequences (those which are eventually I)

In this case, we compute \int ^S \mathcal {C}(X \otimes S, Y \otimes \partial ^{-1}S) \cong \int ^S \mathcal {C}(X \otimes \partial S, Y \otimes \partial ^{-1}\partial S) \cong \mathcal {C}(X \otimes \partial S, Y \otimes S), where the first isomorphism holds because we're just precomposing our coend with an equivalence of categories, \partial .

Given a tuple \phi : S \to S', X \otimes \partial S' \to Y \otimes S witnessing the identity of two stateful maps, \phi itself is a homomorphism of Mealy machines between them. However, it is not obvious that this relationship goes the other way.

But it does seem as though two Mealy machines will have the same observed behaviour if a morphism exists between them (note that such a morphism must preserve the initial state, i.e this diagram must commute:)

Building on the above observation, it seems quite likely that Mealy machines connected by a homomorphism produce observationally equivalent streams, as in Monoidal Streams for Dataflow Programming, Definition 4.