nLab Mealy machine

Contents

Context

Computation

constructive mathematics,realizability,computability

intuitionistic mathematics

propositions as types,proofs as programs,computational trinitarianism

Constructive mathematics

Realizability

Computability

Idea
Definition

Original definition
As spans in monoidal categories

Related entries
References

Idea

AMealy machine (named afterMealy 1955) – traditionally understood as a particular type offinite state automaton – is amap (traditionally thought of as apair of maps, see Def. below) which takes input dataand a given “state” to output dataand an update of that “state”. In modern language ofmonadic computational effects this just means that a Mealy machine is astateful-map, namely aKleisli morphisms for astate monad (see Rem. below).

Definition

Original definition

Definition

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

$S S$ , ofstates;
$I I$ , theinput alphabet;
$O O$ , theoutput alphabet;

andfunctions

$trans : S \times I \to S trans \colon S \times I \to S$ , atransition function;
$out : S \times I \to O out \colon S \times I \to O$ , anoutput function

and often anelement

$s_{0} \in S s_0 \in S$ , theinitial 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 amap betweenCartesian products of this form:

(1)

(out, trans) : I \times S ⟶ O \times S (out, trans)  \;\colon\;   I \times S \longrightarrow O \times S

As such this makes sensein anycartesian monoidal category other thanSets.

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

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

In this form Mealy machines are discussed ascoalgebras 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 alsoadjunct to a map of the form

(2)

I ⟶ [S, S \times O] I \longrightarrow \big[S ,\, S \times O \big]  \,

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

In fact, in this form(2) Mealy machines are exactly the $S S$ -effectful maps in these sense ofmonadic computational effects, namely theKleisli morphisms for the $S S$ -state monad (mentioned as such for instance inOliveira & Miraldo 2016, p. 462). For discussion of this perspective inHaskell: [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 I \times S$ into theCartesian product $O \times S O \times S$ (1), one may, of course, regard them as aspan:

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

This definition is considered for instance inBLLL23a, Def. 2.1.

An evident notion ofhomomorphisms between such spans are maps $f : S \to S' f \colon S \to S'$ such that the followingdiagram 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 asymmetric monoidal category $(𝒞, \otimes, 𝟙) (\mathcal{C},\,\otimes,\,\mathbb{1})$ for

input alphabet object $I \in Ob (𝒞) I \,\in\, Ob(\mathcal{C})$
output alphabet object $O \in Ob (𝒞) O \,\in\, Ob(\mathcal{C})$

is an object of the followingpullback $Mly (I, O) Mly(I,O)$ inCat:

where:

$Alg (- \otimes I) Alg(-\otimes I)$ is the category ofalgebras over theendofunctor
$\begin{matrix} (-) \otimes I : 𝒞 & ⟶ & 𝒞 \\ S & \mapsto & S \otimes I \end{matrix} \array{ \mathllap{ (\text{-})\otimes I \,\colon\; } \mathcal{C} &\longrightarrow& \mathcal{C} \\ S &\mapsto& S\otimes I }$
$U U$ is the forgetful functor,
$(- \otimes I) / O (-\otimes I)/O$ is thecomma category of morphisms $out : X \otimes I \to O out \colon X\otimes I\to O$ ,
$V V$ is the forgetful functor $(X, out) \mapsto X (X,out)\mapsto X$ .

Remark

If $𝒞 \mathcal{C}$ hascountable coproducts, a semiautomaton $trans : S \otimes I \to S trans \colon S\otimes I \to S$ consists of anaction of thefree monoid on $I I$ , $\sum_{n = 0}^{∞} I^{\otimes n} \sum_{n=0}^\infty I^{\otimes n}$ ; this is well-explainedibi.

Concisely, there is anequivalence of categories

Alg (- \otimes I) ≃ EM (I^{*}) Alg(-\otimes I) \simeq EM(I^*)

between $I I$ -semiautomata and theEilenberg-Moore category of the monadinduced by the monoid $I^{*} I^*$ .

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

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

Related entries

References

The notion is due to:

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

For discussion in the context offinite state automata see:

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

Discussion viacategory theory and ascoalgebras 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 Science20 (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 asstateful-maps:

José Nuno Oliveira, Victor Cacciari Miraldo,A practical approach to state-based system calculi, Journal of Logical and Algebraic Methods in Programming85 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 thehistory of this page for a list of all contributions to it.

Edit DiscussPrevious revisionChanges from previous revision History (9 revisions)Cite Print Source

Movatterモバイル変換

nLab Mealy machine

Context

Computation

Constructive mathematics

Realizability

Computability

Contents

Idea

Definition

Original definition

Definition

Remark

As spans in monoidal categories

Definition

Remark

Related entries

References