nLab Mealy machine

Idea

A Mealy machine (named after Mealy 1955) – traditionally understood as a particular type of finite state automaton – is a map (traditionally thought of as a pair of maps, see Def. below) which takes input data and a given “state” to output data and an update of that “state”. In modern language of monadic computational effects this just means that a Mealy machine is a stateful-map, namely a Kleisli morphisms for a state monad (see Rem. below).

Definition

Original definition

Definition

(traditional component definition)
A (finite) Mealy machine consists of (finite) sets

• $S$, of states;

• $I$, the input alphabet;

• $O$, the output alphabet;

and functions

• $trans \colon S \times I \to S$, a transition function;

• $out \colon S \times I \to O$, an output function

and often an element

• $s_0 \in S$, the initial state.

Remark

(Mealy machines as effectful maps)
More concisely, a Mealy machine as in Def. is (except for the specification of the initial state) just a map between Cartesian products of this form:

(1)$$(out, trans) \;\colon\; I \times S \longrightarrow O \times S$$

As such this makes sense in any cartesian monoidal category other than Sets.

In a closed cartesian monoidal category (such as Sets) with internal hom $[\text{-},\text{-}]$, such a map (1) is equivalent to (namely: is the “curried” internal hom-adjunct of) a map of the form

$$S \longrightarrow \big[I,\, O \times S\big] \,.$$

In this form Mealy machines are discussed as coalgebras of an endofunctor, for instance in [Pattinson 2003, 1.1.3], [Bonsangue, Rutten & Silva 2008, p. 1], [Ghica, Kaye & Sprunger 2022, Def. 25].

But of course, by the same token (1) is also adjunct to a map of the form

(2)$$I \longrightarrow \big[S ,\, S \times O \big] \,$$

which makes more manifest how a Mealy machine is a map sending input $i \in I$ to output $o \in O$ after also reading out a stated $s \in S$ and then also updating that state.

In fact, in this form (2) Mealy machines are exactly the $S$-effectful maps in these sense of monadic computational effects, namely the Kleisli morphisms for the $S$-state monad (mentioned as such for instance in Oliveira & Miraldo 2016, p. 462). For discussion of this perspective in Haskell: [github.com/orakaro/MonadicMealyMachine], [Perone & Karachalias 2023, p. 3].

As spans in monoidal categories

Instead of regarding the pair given by the transition- and output function of a Mealy machine (Def. ) as a single map from $I \times S$ into the Cartesian product $O \times S$ (1), one may, of course, regard them as a span:

In this form, a Cartesian product is not needed to pair these two operations, and hence it is tempting to consider a generalized notion of Mealy machines in (not-necessarily cartesian) symmetric monoidal categories $(\mathcal{C}, \otimes, \mathbb{1})$, given by spans of the above form, but using the given monoidal product to pair what are now $\mathcal{C}$-objects $I$ and $S$:

This definition is considered for instance in BLLL23a, Def. 2.1.

An evident notion of homomorphisms between such spans are maps $f \colon S \to S'$ such that the following diagram commutes (BLLL23a, Rem. 2.2):

The authors of [BLLL23a, Prop. 3.5] [BLLL23b, Def. 2.1] find it useful to rephrase this as follows:

Definition

A Mealy machine internal to a symmetric monoidal category $(\mathcal{C},\,\otimes,\,\mathbb{1})$ for

• input alphabet object $I \,\in\, Ob(\mathcal{C})$

• output alphabet object $O \,\in\, Ob(\mathcal{C})$

is an object of the following pullback $Mly(I,O)$ in Cat:

where:

• $Alg(-\otimes I)$ is the category of algebras over the endofunctor

  $$\array{ \mathllap{ (\text{-})\otimes I \,\colon\; } \mathcal{C} &\longrightarrow& \mathcal{C} \\ S &\mapsto& S\otimes I }$$

• $U$ is the forgetful functor,

• $(-\otimes I)/O$ is the comma category of morphisms $out \colon X\otimes I\to O$,

• $V$ is the forgetful functor $(X,out)\mapsto X$.

Remark

If $\mathcal{C}$ has countable coproducts, a semiautomaton $trans \colon S\otimes I \to S$ consists of an action of the free monoid on $I$, $\sum_{n=0}^\infty I^{\otimes n}$; this is well-explained ibi.

Concisely, there is an equivalence of categories

$$Alg(-\otimes I) \simeq EM(I^*)$$

between $I$-semiautomata and the Eilenberg-Moore category of the monad induced by the monoid $I^*$.

Then, a Mealy machine as in Def. consists indeed of a span

$$S \leftarrow S\otimes I \to O \,.$$

Related entries

• state monad

• Moore machine

• automata

• Mealy morphism

References

The notion is due to:

• George H. Mealy, A Method for Synthesizing Sequential Circuits, Bell System Technical Journal 34 5 (1955) 1045-1079 [doi:10.1002/j.1538-7305.1955.tb03788.x]

For discussion in the context of finite state automata see:

• Mark V. Lawson, Finite automata, CRC Press (2003) [webpage, course notes:pdf]

Discussion via category theory and as coalgebras of an endofunctor

• Dirk Pattinson, Section 1.1.3 in: An Introduction to the Theory of Coalgebras (2003) [pdf, pdf]

• M. M. Bonsangue, Jan Rutten & Alexandra Silva , Coalgebraic Logic and Synthesis of Mealy Machines, in: Foundations of Software Science and Computational Structures. FoSSaCS 2008, Lecture Notes in Computer Science, 4962 (2008) [doi:10.1007/978-3-540-78499-9_17]

• H. Hansen, Jan Rutten, Symbolic synthesis of Mealy machines from arithmetic bitstream functions, Scientific Annals of Computer Science 20 (2010) 97–130 [pub:16639, pdf]

• Dan R. Ghica, George Kaye, David Sprunger, Def. 25 in: A compositional theory of digital circuits [arXiv:2201.10456]

Discussion as stateful-maps:

• José Nuno Oliveira, Victor Cacciari Miraldo, A practical approach to state-based system calculi, Journal of Logical and Algebraic Methods in Programming 85 4 (2016) 449-474 [doi:10.1016/j.jlamp.2015.11.007]

• Marco Perone, Georgios Karachalias, Composable Representable Executable Machines [arXiv:2307.09090]

Discussion in symmetric monoidal categories:

• Guido Boccali, Andrea Laretto, Fosco Loregian, Stefano Luneia, Completeness for categories of generalized automata [arXiv:2303.03867]

• Guido Boccali, Bojana Femić, Andrea Laretto, Fosco Loregian, Stefano Luneia, The semibicategory of Moore automata [arXiv:2305.00272]