Effectful Mealy Machines: Coalgebraic and Causal Traces (Invited Talk)

Bonchi, Filippo; Di Lavore, Elena; Román, Mario

doi:10.4230/LIPIcs.CALCO.2025.1

Effectful Mealy Machines:
Coalgebraic and Causal Traces

Filippo Bonchi

Universitá di Pisa, Italy Elena Di Lavore

University of Oxford, UK Mario Román

University of Oxford, UK

Abstract

We introduce effectful Mealy machines – a general notion of Mealy machine with global effects – and give them semantics in terms of both bisimilarity and traces. Bisimilarity of effectful Mealy machines is characterized syntactically, via free uniform feedback. Their traces are given a novel semantic coinductive universe in terms of effectful streams. We prove that this framework generalizes standard causal processes and captures existing flavours of Mealy machine, bisimilarity, and trace.

This is an extended abstract for the manuscript Effectful Mealy Machines: Bisimulation and Trace that will appear in the proceedings of LiCS 2025 [3]; an extended version with proofs is also available (arxiv.org/abs/2410.10627) [4]. We additionally characterise causal processes as lax-natural transformations.

Keywords and phrases:

Mealy machines, coinduction, copy-discard categories, premonoidal categories

Category:

Invited Talk

Funding:

Filippo Bonchi: supported by the the Italian Ministero dell’Università e della Ricerca, grant PRIN 2022, PNRR No. P2022HXNSC - RAP (Resource Awareness in Programming) and partially by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme. This study was carried out within the National Centre on HPC, Big Data and Quantum Computing - SPOKE 10 (Quantum Computing) and received funding from the European Union Next-GenerationEU - National Recovery and Resilience Plan (NRRP) – MISSION 4 COMPONENT 2, INVESTMENT N. 1.4 – CUP N. I53C22000690001.

Elena Di Lavore: supported by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme.

Mario Román: partially supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0038 and by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Categorical semantics ; Theory of computation

\rightarrow

Abstract machines

Editors:

Corina Cîrstea and Alexander Knapp

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Introduction

Mealy machines have a transition behaviour $U\otimes X\overset{}{\rightarrow}U\otimes Y$ that takes the current state in $U$ and an input in $X$ to transition to the next state and produce an output in $Y$ . This perspective naturally leads us to consider Mealy machines as morphisms in a category, and to define their sequential and parallel compositions [14]. Mealy machines may also be seen as coalgebras [18]. This perspective naturally leads us to interpret their behaviour as the mapping to a final coalgebra.

Learning from these two perspectives, we define effectful Mealy machines as morphisms in an appropriate category, and give them trace semantics in a final coalgebra. Homomorphisms of effectful Mealy machines generalise coalgebra morphisms, and determine bisimulations.

Effectful Mealy machines may produce effects when transitioning. These effects are determined by an effectful triple: a triple of categories, introduced by Jeffrey [13], that distinguishes between different kinds of computations. There are values, which are total and deterministic, and form a cartesian category $\mathbb{V}$ ; there are local computations, which do not affect the global state, and form a monoidal category $\mathbb{P}$ because local effects interchange; and there are global computations, which may affect the global state, and form a premonoidal category $\mathbb{C}$ [16]. These three categories share the same objects, meaning that the different types of computation affect the same resources. Formally, an effectful triple is a triple of categories, $(\mathbb{V}\overset{}{\rightarrow}\mathbb{P}\overset{}{\rightarrow}\mathbb{C})$ as above, with two identity-on-objects functors between them that strictly preserve the monoidal and premonoidal structures, respectively.

Mealy machines and bisimilarity

A Mealy machine has a transition function and an initial state. At each step, the machine takes an input and, depending on the current state, it transitions to the next state producing an output. An effectful Mealy machine follows the same pattern, but it may produce effects while transitioning.

Definition 1 (Effectful machine).

An effectful machine, taking inputs on $X$ and producing outputs in $Y$ , is a tuple $(U,i,f)$ consisting of a state object $U\in\mathbb{C}_{\hyperlink{linkStrictification}{\mathsf{str}}}$ , an initial state $i\in\mathbb{P}_{\hyperlink{linkStrictification}{\mathsf{str}}}(I;U)$ , and a transition morphism, $f\in\mathbb{C}_{\hyperlink{linkStrictification}{\mathsf{str}}}(U\otimes[X];U% \otimes[Y])$ , where $[X]$ denotes the strictification of the object $X\in\mathbb{C}$ . $\mathsf{Mealy}_{\mathbb{C}}(X;Y)$ denotes the set of effectful machines with inputs in $X$ and outputs in $Y$ .

When the transition morphism and the initial state both belong to $\mathbb{P}$ or to $\mathbb{V}$ , we call the Mealy machine monoidal or cartesian, respectively. Cartesian, monoidal and effectful Mealy machines form an effectful triple [3, Proposition III.3].

Homomorphisms of Mealy machines are value morphisms between the state spaces that do not alter the input-output behaviour.

Definition 2.

A homomorphism between two effectful machines $(U,i,f),(V,j,g)\in\hyperlink{linkMealyCategory}{\mathsf{Mealy}}(X;Y)$ , is a cartesian morphism $\alpha\in\mathbb{V}_{\hyperlink{linkStrictification}{\mathsf{str}}}(U;V)$ that satisfies Equation 1.

\hskip-17.50002pt\begin{matrix}\includegraphics[scale={0.9}]{fig-mealy-% homomorphism.pdf2svg.svg}\end{matrix}

(1)

Homomorphisms of Mealy machines determine bisimulations, and bisimilarity is the equivalence relation generated by them [3, Proposition III.6].

Definition 3 .

A bisimulation between two effectful machines, $M$ and $N$ , with the same input and output types is a zig-zag of homomorphisms, $(\alpha_{i}\colon M_{i}\Rightarrow N_{i})_{i=0}^{k}$ and $(\beta_{i}\colon M_{i+1}\Rightarrow N_{i})_{i=0}^{k-1}$ ,

M_{0}\overset{\alpha_{0}}{\Rightarrow}N_{0}\overset{\beta_{0}}{\Leftarrow}M_{1% }\overset{\alpha_{1}}{\Rightarrow}\dots\overset{\beta_{k-1}}{\Leftarrow}M_{k}% \overset{\alpha_{k}}{\Rightarrow}N_{k},

where $M_{0}=M$ and $N_{k}=N$ . Two effectful machines, $M$ and $N$ , are bisimilar, written $M\hyperlink{linkBisimilarity}{\equiv}N$ , if there is a bisimulation between them.

Bisimilarity has a universal property: effectful Mealy machines quotiented by bisimilarity form the free uniform feedback structure over the effectful triple $(\mathbb{V},\mathbb{P},\mathbb{C})$ [3, Theorem III.19].

Example 4 (Coalgebraic Mealy machines [3, Section III.C]).

A strong monad, $T\colon\mathbb{V}\overset{}{\rightarrow}\mathbb{V}$ , has a premonoidal Kleisli category, $\mathsf{kl}(T)$ , and we will usually consider the effectful triple $(\mathbb{V},\mathbb{P},\mathsf{kl}(T))$ , for some monoidal subcategory $\mathbb{P}$ of $\mathsf{kl}(T)$ . Effectful machines on $(\mathbb{V},\mathbb{P},\mathsf{kl}(T))$ with inputs in $X$ and outputs in $Y$ are coalgebras for the endofunctor $\mathsf{M}_{T}\colon\mathbb{V}\overset{}{\rightarrow}\mathbb{V}$ defined by $\mathsf{M}_{T}={(T(-\times Y))}^{X}$ , together with an initial state: indeed, a transition morphism $f\in\mathsf{kl}(T)(U\otimes X;U\otimes Y)$ is, equivalently, a coalgebra $\hat{f}\colon U\overset{}{\rightarrow}{(T(U\times Y))}^{X}$ [18]. Similarly, machine homomorphisms are $\mathsf{M}_{T}$ -coalgebra homomorphisms preserving initial states.

In particular, the transition morphisms of deterministic, non-deterministic and probabilistic machines can be expressed as coalgebras for $\mathbf{Set}$ -endofunctors. Moreover, the notions of bisimilarity for the machines in Figure 1 in the literature [18, 19, 1, 15, 2, 6] coincide with the effectful bisimilarity of Definition 3 ([3, Corollaries III.13 and III.15]).

Deterministic	$U\times X\overset{}{\rightarrow}U\times Y$
Partial	$U\times X\overset{}{\rightarrow}U\times Y+1$
Non-deterministic	$U\times X\overset{}{\rightarrow}\mathcal{P}(U\times Y)$
Probabilistic [1]	$U\times X\overset{}{\rightarrow}\mathcal{D}(U\times Y)$
Quantum [7, 5]	$U\times X\overset{}{\rightarrow}\mathsf{Q}_{\mathcal{H}}(U\times Y)$
Shared state	$U\times X\overset{}{\rightarrow}(U\times Y\times S)^{S}$

Figure 1: Machines for different

\mathbf{Set}

-monads.

Coalgebraic traces

The behaviour of effectful Mealy machines is a mapping to a final coalgebra that contains the possible execution traces. Effectful Mealy machines form an effectful triple, so their traces do too and the behaviour is functorial.

An execution trace of a machine takes a stream of inputs to a stream of outputs obtained by running it. Thus, execution traces of effectful Mealy machines are effectful stream transducers, or effectful streams (Definition 7). These are streams of morphisms, as in Definition 5, quotiented by an equivalence relation that allows local transformations of the memory (Definition 6).

Definition 5 (Raw effectful stream).

A raw effectful stream, $f\in\hyperlink{linkRawEffectfulStream}{\mathsf{rawStream}_{\mathbb{C}}}(% \mathbf{X};\mathbf{Y})$ , with inputs in $\mathbf{X}=(X{}_{0},X{}_{1}\makebox[6.13336pt][c]{.\hfil.\hfil.})$ and outputs in $\mathbf{Y}=(Y{}_{0},Y{}_{1},\makebox[6.13336pt][c]{.\hfil.\hfil.})$ is coinductively defined as a tuple consisting of

$\blacksquare$

$M_{f}\in{\mathbb{C}}_{\mathsf{obj}}$ , the memory;
$\blacksquare$

${f}^{\circ}\in\mathbb{C}({\mathbf{X}}^{\circ};M_{f}\otimes{\mathbf{Y}}^{\circ})$ , the head;
$\blacksquare$

${f}^{+}\in\hyperlink{linkRawEffectfulStream}{\mathsf{rawStream}_{\mathbb{C}}}(% M_{f}\hyperlink{linklatercomp}{\cdot}{\mathbf{X}}^{+};{\mathbf{Y}}^{+})$ , the tail.

We depict effectful streams as in the following diagram, interpreting that each step in the stream has its own runtime.

\begin{matrix}\includegraphics*[scale={0.9}]{fig-effectful-stream.pdf}\end{matrix}

Tensoring of an object is coinductively defined by ${(M\hyperlink{linklatercomp}{\cdot}\mathbf{X})}^{\circ}=M\otimes{\mathbf{X}}^{\circ}$ and ${(M\hyperlink{linklatercomp}{\cdot}\mathbf{X})}^{+}={\mathbf{X}}^{+}$ . Tensoring extends analogously to morphisms [3, Definition IV.2].

Definition 6 .

Stream dinaturality, $(\hyperlink{linkdinat}{\sim})$ , is the least equivalence relating two streams $(M_{f},{f}^{\circ},{f}^{+})\hyperlink{linkdinat}{\sim}(M_{g},{g}^{\circ},{g}^{% +})$ , whenever there exists a pure morphism $r\in\mathbb{P}(M_{g};M_{f})$ such that ${g}^{\circ}\fatsemi(r\otimes\mathrm{id})={f}^{\circ}$ and $r\hyperlink{linklatercomp}{\cdot}{f}^{+}\hyperlink{linkdinat}{\sim}{g}^{+}$ (Equation 2).

\begin{matrix}\includegraphics*[scale={0.9}]{fig-stream-dinaturality.pdf}\end{matrix}

(2)

Definition 7.

An effectful stream, $f\in\hyperlink{linkEffectfulStream}{\mathsf{Stream}_{\mathbb{C}}}(\mathbf{X};% \mathbf{Y})$ , with inputs in $\mathbf{X}=(X{}_{0},X{}_{1},\makebox[6.13336pt][c]{.\hfil.\hfil.})$ and outputs $\mathbf{Y}=(Y{}_{0},Y{}_{1},\makebox[6.13336pt][c]{.\hfil.\hfil.})$ , is an equivalence class of raw effectful streams under stream dinaturality.

Definition 7 can be recast in coalgebraic terms. The set $\hyperlink{linkEffectfulStream}{\mathsf{Stream}}(\mathbf{X};\mathbf{Y})$ of effectful streams from $\mathbf{X}$ to $\mathbf{Y}$ is the final fixpoint of the functor $\phi\colon[(\mathbb{C}^{\omega})^{\mathsf{op}}\times\mathbb{C}^{\omega},% \mathbf{Set}]\overset{}{\rightarrow}[(\mathbb{C}^{\omega})^{\mathsf{op}}\times% \mathbb{C}^{\omega},\mathbf{Set}]$ defined by

\phi(\mathsf{Q})(\mathbf{X},\mathbf{Y})=\int^{M\in\mathbb{P}}\!\!\!\mathbb{C}(% {\mathbf{X}}^{\circ};M\otimes{\mathbf{Y}}^{\circ})\times\mathsf{Q}(M\hyperlink% {linklatercomp}{\cdot}{\mathbf{X}}^{+};{\mathbf{Y}}^{+}).

The integral sign denotes a kind of colimit, known as coend, that formalises the stream dinaturality quotient.

The effectful trace of an effectful Mealy machine is obtained by starting with the initial state and repeating the transition morphism at each time step.

Any object $X$ in $\mathbb{C}$ can be repeated to form a stream $\hyperlink{linkCorepeat}{\llparenthesis}X\hyperlink{linkCorepeat}{\rrparenthesis}$ , defined by ${\hyperlink{linkCorepeat}{\llparenthesis}X\hyperlink{linkCorepeat}{% \rrparenthesis}}^{\circ}=X$ and ${\hyperlink{linkCorepeat}{\llparenthesis}X\hyperlink{linkCorepeat}{% \rrparenthesis}}^{+}=\hyperlink{linkCorepeat}{\llparenthesis}X\hyperlink{% linkCorepeat}{\rrparenthesis}$ . Analogously, a transition morphism $f\in\mathbb{C}(U\otimes X;U\otimes Y)$ can be repeated to an effectful stream $\hyperlink{linkCorepeat}{\llparenthesis}f\hyperlink{linkCorepeat}{% \rrparenthesis}\colon U\hyperlink{linklatercomp}{\cdot}\hyperlink{linkCorepeat% }{\llparenthesis}X\hyperlink{linkCorepeat}{\rrparenthesis}\leadsto\hyperlink{% linkCorepeat}{\llparenthesis}Y\hyperlink{linkCorepeat}{\rrparenthesis}$ , defined as $M_{\hyperlink{linkCorepeat}{\llparenthesis}f\hyperlink{linkCorepeat}{% \rrparenthesis}}=U$ , ${\hyperlink{linkCorepeat}{\llparenthesis}f\hyperlink{linkCorepeat}{% \rrparenthesis}}^{\circ}=f$ and ${\hyperlink{linkCorepeat}{\llparenthesis}f\hyperlink{linkCorepeat}{% \rrparenthesis}}^{+}=\hyperlink{linkCorepeat}{\llparenthesis}f\hyperlink{% linkCorepeat}{\rrparenthesis}$ . The operation $(\hyperlink{linklatercomp}{\cdot})$ attaches the initial state to the execution of $f$ .

Definition 8 .

The trace of an effectful machine $(U,i,f)\in\hyperlink{linkMealyCategory}{\mathsf{Mealy}}(X;Y)$ is the effectful stream defined by $\hyperlink{linkTrace}{\mathsf{Trace}}(U,i,f)=i\hyperlink{linklatercomp}{\cdot}% \hyperlink{linkCorepeat}{\llparenthesis}f\hyperlink{linkCorepeat}{\rrparenthesis}$ . Two machines are trace-equivalent if their traces coincide.

Causal traces

In some cases, effectful streams have an explicit presentation as causal processes [3, Section V]. These generalise Raney’s causal functions [17] to copy-discard categories with conditionals.

Definition 9.

For a copy-discard category $(\mathbb{V},\mathbb{P})$ , a causal process, $f\colon\mathbf{X}\overset{}{\rightarrow}\mathbf{Y}$ , is a sequence of morphisms $\{f_{n}\colon X_{0}\otimes\cdots\otimes X_{n}\overset{}{\rightarrow}Y{}_{0}% \otimes\cdots\otimes Y_{n}\}_{n\in\mathbb{N}}$ in $\mathbb{P}$ such that there exist morphisms $\{d_{n}\colon Y{}_{0}\otimes\cdots\otimes Y_{n}\otimes X{}_{0}\otimes\cdots% \otimes X_{n+1}\overset{}{\rightarrow}Y_{n+1}\}_{n\in\mathbb{N}}$ satisfying that

\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{\lower 4.46773pt\hbox{% {\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.latexml-% figure0.pdf}}}}=\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 14.78% 835pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.la% texml-figure1.pdf}}}}{}.

(3)

Equation 3 imposes a causality condition: the first $n$ outputs of $f_{n+1}$ can only be influenced by the first $n$ inputs, but not by the input $n+1$ .

Existence of conditionals is a property of a copy-discard category: it captures the notion of conditioning in categories of probabilistic processes [8, 12, 10]. Conditionals ensure that every morphism with two outputs, $f\colon X\overset{}{\rightarrow}A\otimes B$ , splits as its marginal $f\mathbin{\fatsemi}\pi_{A}$ with some conditional $c\colon A\otimes X\overset{}{\rightarrow}B$ as below.

\forall\ f\colon X\overset{}{\rightarrow}A\otimes B\quad\exists\ c\colon A% \otimes X\overset{}{\rightarrow}B\qquad\leavevmode\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\hbox{\lower 4.46773pt\hbox{{\leavevmode\includegraphics{}% {}{dagpub-tikzpictures/p001-Bonchi.latexml-figure2.pdf}}}}=\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{\lower 8.73546pt\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.latexml-figure% 3.pdf}}}}{}

Causal processes over a copy-discard category with conditionals form a monoidal category with component-wise compositions and monoidal products [3, Proposition V.7]. When the base copy-discard category, $(\mathbb{V},\mathbb{P})$ , additionally verifies the existence of morphism ranges [3, 9], then causal processes over $(\mathbb{V},\mathbb{P})$ are monoidally isomorphic to effectful streams over $(\mathbb{V},\mathsf{Tot}(\mathbb{P}),\mathbb{P})$ [3, Theorem V.8], where $\mathsf{Tot}(\mathbb{P})$ indicates the subcategory of $\mathbb{P}$ of total morphisms, i.e. those that commute with the discard maps.

Examples of copy-discard categories with conditionals and ranges include the Kleisli categories of the monads described in Example 4 [3, Proposition V.5]. Causal processes in these categories give explicit descriptions for traces of deterministic, partial, non-deterministic and probabilistic Mealy machines.

We conclude with a novel characterisation of causal processes as lax-natural transformations. We fix a copy-discard category $(\mathbb{V},\mathbb{P})$ with conditionals. Conditionals determine a preorder-enrichment [11, Theorem 3.3] that yields the desired lax-naturality condition.

Each infinite sequence of objects $\mathbf{X}=(X_{0},X_{1},\dots)$ determines a functor $\underline{\mathbf{X}}\colon(\mathbb{N},\geq)\overset{}{\rightarrow}\mathbb{P}$ that maps each natural number $n$ to the object $X_{0}\otimes\cdots\otimes X_{n}$ , and each inequality $n\geq m$ to the projection $\pi_{n,m}\colon X_{0}\otimes\cdots\otimes X_{n}\overset{}{\rightarrow}X_{0}% \otimes\cdots\otimes X_{m}$ given by the copy-discard structure. A causal process $f\colon\mathbf{X}\overset{}{\rightarrow}\mathbf{Y}$ is a lax-natural transformation from the functor $\underline{\mathbf{X}}$ to the functor $\underline{\mathbf{Y}}$ . Explicitly, the components of $f$ are morphisms $f_{n}\colon X_{0}\otimes\cdots\otimes X_{n}\overset{}{\rightarrow}Y_{0}\otimes% \cdots\otimes Y_{n}$ , and the lax-naturality condition imposes that, for $n\geq m$ , $f_{n}\mathbin{\fatsemi}\pi_{n,m}\leq\pi_{n,m}\mathbin{\fatsemi}f_{m}$ .

Finally, we show that lax-naturality is equivalent to the causality condition in Equation 3.

Proposition 10.

For a copy-discard category $(\mathbb{V},\mathbb{P})$ with conditionals, the monoidal category of causal processes is isomorphic to the monoidal category of functors of the form $\underline{\mathbf{X}}$ , for infinite sequences $\mathbf{X}$ of objects in $\mathbb{P}$ , and lax-natural transformations between them.

Proof sketch.

Lax-natural transformations $f\colon\underline{\mathbf{X}}\overset{}{\rightarrow}\underline{\mathbf{Y}}$ and $g\colon\underline{\mathbf{Y}}\overset{}{\rightarrow}\underline{\mathbf{Z}}$ compose sequentially. With the identity natural transformation, they form a category. Lax-natural transformations also have a monoidal product defined component-wise, which makes them a monoidal category.

Finally, we prove that lax-naturality is equivalent to the causality condition (Equation 3). For two morphisms $f,g\colon X\overset{}{\rightarrow}Y$ in a copy-discard category with conditionals, the preorder $f\leq g$ is defined by the existence of $r\colon Y\otimes X\overset{}{\rightarrow}I$ satisfying

\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{\lower 4.46773pt\hbox{% {\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.latexml-% figure4.pdf}}}}=\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 8.735% 46pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.lat% exml-figure5.pdf}}}}.

Consider a causal process $f\colon\mathbf{X}\overset{}{\rightarrow}\mathbf{Y}$ . By discarding the second output in Equation 3, we obtain witnesses $d_{n}\mathbin{\fatsemi}\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.latexml-figure% 6.pdf}}}$ of the inequalities $f_{n+1}\mathbin{\fatsemi}\pi_{n+1,n}\leq\pi_{n+1,n}\mathbin{\fatsemi}f_{n}$ . By transitivity, these inequalities are enough to prove that $f_{n}\mathbin{\fatsemi}\pi_{n,m}\leq\pi_{n,m}\mathbin{\fatsemi}f_{m}$ for all $n\geq m$ .

For the converse, consider a lax-natural transformation $f\colon\underline{\mathbf{X}}\overset{}{\rightarrow}\underline{\mathbf{Y}}$ . Lax-naturality implies that $f_{n+1}\mathbin{\fatsemi}\pi_{n+1,n}\leq\pi_{n+1,n}\mathbin{\fatsemi}f_{n}$ , which means that there are morphisms $r_{n+1}\colon Y_{0}\otimes\cdots\otimes Y_{n}\otimes X_{0}\otimes\cdots\otimes X% _{n+1}\overset{}{\rightarrow}I$ satisfying the equation below.

\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{\lower 4.46773pt\hbox{% {\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.latexml-% figure7.pdf}}}}=\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 11.58% 092pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.la% texml-figure8.pdf}}}}

Using (i) conditionals and (ii) lax-naturality, we find morphisms $d_{n+1}\colon Y_{0}\otimes\cdots\otimes Y_{n}\otimes X_{0}\otimes\cdots\otimes X% _{n+1}\overset{}{\rightarrow}Y_{n+1}$ that satisfy the causality condition (Equation 3).

	$\displaystyle\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 4.467% 73pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.lat% exml-figure9.pdf}}}}\overset{(i)}{=}\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 8.7359pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p001-Bonchi.latexml-figure10.pdf}}}}$	$\displaystyle\overset{(ii)}{=}\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 21.13954pt\hbox{{\leavevmode\includegraphics{}{}{dagpub% -tikzpictures/p001-Bonchi.latexml-figure11.pdf}}}}$
		$\displaystyle=\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 22.96% 227pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.la% texml-figure12.pdf}}}}{}$

Thus, we can take $d_{n+1}=\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 4.467% 73pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p001-Bonchi.lat% exml-figure13.pdf}}}}\mathbin{\fatsemi}(r_{n+1}\otimes c_{n+1})$ . $\hfill\blacktriangleleft$

We believe that this more abstract characterisation of causal processes, other than simplifying some proofs, may shed some light on the nature of processes that evolve in time respecting a causality condition.

References

[1] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[2] Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 149–158, 1997. doi:10.1109/LICS.1997.614943.
[3] Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy machines: bisimulation and trace. In Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science (to appear), 2025.
[4] Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy machines: bisimulation and trace (extended version), 2025. arXiv:2410.10627.
[5] Lorenzo Ceragioli, Elena Di Lavore, Giuseppe Lomurno, and Gabriele Tedeschi. A coalgebraic model of quantum bisimulation, 2024. to appear in the preceedings of Applied Category Theory 2024.
[6] Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Quantum bisimilarity via barbs and contexts: Curbing the power of non-deterministic observers. Proceedings of the ACM on Programming Languages, 8(POPL):1269–1297, 2023. doi:10.1145/3632885.
[7] Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Effect semantics for quantum process calculi, 2024. to appear in the preceedings of CONCUR 2024.
[8] Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29(7):938–971, 2019. doi:10.1017/S0960129518000488.
[9] Elena Di Lavore, Giovanni de Felice, and Mario Román. Monoidal streams for dataflow programming. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3531130.3533365.
[10] Elena Di Lavore and Mario Román. Evidential decision theory via partial Markov categories. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14, 2023. doi:10.1109/LICS56636.2023.10175776.
[11] Elena Di Lavore, Mario Román, Paweł Sobociński, and Márk Széles. Order in partial Markov categories. In Proceedings of the 41st Conference on Mathematical Foundations of Programming Semantics (to appear), 2025.
[12] Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020.
[13] Alan Jeffrey. Premonoidal categories and a graphical view of programs, 1997.
[14] Piergiulio Katis, Nicoletta Sabadini, and Robert F. C. Walters. Bicategories of processes. Journal of Pure and Applied Algebra, 115(2):141–178, 1997. doi:10.1016/S0022-4049(96)00012-6.
[15] Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 344–352. ACM Press, 1989. doi:10.1145/75277.75307.
[16] John Power and Edmund Robinson. Premonoidal categories and notions of computation. Math. Struct. Comput. Sci., 7(5):453–468, 1997. doi:10.1017/S0960129597002375.
[17] George N Raney. Sequential functions. Journal of the ACM (JACM), 5(2):177–180, 1958. doi:10.1145/320924.320930.
[18] Jan Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3–80, 2000. Modern Algebra. doi:10.1016/S0304-3975(00)00056-6.
[19] Sam Staton. Relating coalgebraic notions of bisimulation. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 191–205. Springer, 2009. doi:10.1007/978-3-642-03741-2_14.

[bib.bib1] [1] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.

[bib.bib2] [2] Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 149–158, 1997. doi:10.1109/LICS.1997.614943.

[bib.bib3] [3] Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy machines: bisimulation and trace. In Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science (to appear), 2025.

[bib.bib4] [4] Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy machines: bisimulation and trace (extended version), 2025. arXiv:2410.10627.

[bib.bib5] [5] Lorenzo Ceragioli, Elena Di Lavore, Giuseppe Lomurno, and Gabriele Tedeschi. A coalgebraic model of quantum bisimulation, 2024. to appear in the preceedings of Applied Category Theory 2024.

[bib.bib6] [6] Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Quantum bisimilarity via barbs and contexts: Curbing the power of non-deterministic observers. Proceedings of the ACM on Programming Languages, 8(POPL):1269–1297, 2023. doi:10.1145/3632885.

[bib.bib7] [7] Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Effect semantics for quantum process calculi, 2024. to appear in the preceedings of CONCUR 2024.

[bib.bib8] [8] Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29(7):938–971, 2019. doi:10.1017/S0960129518000488.

[bib.bib9] [9] Elena Di Lavore, Giovanni de Felice, and Mario Román. Monoidal streams for dataflow programming. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3531130.3533365.

[bib.bib10] [10] Elena Di Lavore and Mario Román. Evidential decision theory via partial Markov categories. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14, 2023. doi:10.1109/LICS56636.2023.10175776.

[bib.bib11] [11] Elena Di Lavore, Mario Román, Paweł Sobociński, and Márk Széles. Order in partial Markov categories. In Proceedings of the 41st Conference on Mathematical Foundations of Programming Semantics (to appear), 2025.

[bib.bib12] [12] Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020.

[bib.bib13] [13] Alan Jeffrey. Premonoidal categories and a graphical view of programs, 1997.

[bib.bib14] [14] Piergiulio Katis, Nicoletta Sabadini, and Robert F. C. Walters. Bicategories of processes. Journal of Pure and Applied Algebra, 115(2):141–178, 1997. doi:10.1016/S0022-4049(96)00012-6.

[bib.bib15] [15] Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 344–352. ACM Press, 1989. doi:10.1145/75277.75307.

[bib.bib16] [16] John Power and Edmund Robinson. Premonoidal categories and notions of computation. Math. Struct. Comput. Sci., 7(5):453–468, 1997. doi:10.1017/S0960129597002375.

[bib.bib17] [17] George N Raney. Sequential functions. Journal of the ACM (JACM), 5(2):177–180, 1958. doi:10.1145/320924.320930.

[bib.bib18] [18] Jan Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3–80, 2000. Modern Algebra. doi:10.1016/S0304-3975(00)00056-6.

[bib.bib19] [19] Sam Staton. Relating coalgebraic notions of bisimulation. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 191–205. Springer, 2009. doi:10.1007/978-3-642-03741-2_14.

Effectful Mealy Machines: Coalgebraic and Causal Traces