constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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).
(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
(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:
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
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
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].
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:
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
$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$.
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
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
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:
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]
Last revised on August 26, 2023 at 13:51:01. See the history of this page for a list of all contributions to it.