nLab Mealy machine

Redirected from "Mealy machines".
Contents

Contents

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

  • SS, of states;

  • II, the input alphabet;

  • OO, the output alphabet;

and functions

  • trans:S×IStrans \colon S \times I \to S, a transition function;

  • out:S×IOout \colon S \times I \to O, an output function

and often an element

  • s 0Ss_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):I×SO×S (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 “curriedinternal hom-adjunct of) a map of the form

S[I,O×S]. 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[S,S×O] I \longrightarrow \big[S ,\, S \times O \big] \,

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

In fact, in this form (2) Mealy machines are exactly the SS-effectful maps in these sense of monadic computational effects, namely the Kleisli morphisms for the SS-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×SI \times S into the Cartesian product O×SO \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 II and SS:

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

An evident notion of homomorphisms between such spans are maps f:SSf \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 IOb(𝒞)I \,\in\, Ob(\mathcal{C})

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

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

where:

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

    (-)I:𝒞 𝒞 S SI \array{ \mathllap{ (\text{-})\otimes I \,\colon\; } \mathcal{C} &\longrightarrow& \mathcal{C} \\ S &\mapsto& S\otimes I }
  • UU is the forgetful functor,

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

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

Remark

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

Concisely, there is an equivalence of categories

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

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

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

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

References

The notion is due to:

For discussion in the context of finite state automata see:

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:

Last revised on August 26, 2023 at 13:51:01. See the history of this page for a list of all contributions to it.