Steps and Traces

Bart Jacobs, Paul Levy, Jurriaan Rot

► To cite this version:

Bart Jacobs, Paul Levy, Jurriaan Rot. Steps and Traces. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.122-143, 10.1007/978-3-030-00389-0_8. hal-02044644

HAL Id: hal-02044644

https://inria.hal.science/hal-02044644

Submitted on 21 Feb 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Steps and Traces

Bart Jacobs¹ and Paul Levy² and Jurriaan Rot¹*

¹ Institute for Computing and Information Sciences, Radboud Universiteit, Nijmegen, The Netherlands

² University of Birmingham, UK bart@cs.ru.nl and P.B.Levy@cs.bham.ac.uk and jrot@cs.ru.nl

**Abstract.** In the theory of coalgebras, trace semantics can be defined in various distinct ways, including through algebraic logics, the Kleisli category of a monad or its Eilenberg-Moore category. This paper elaborates two new unifying ideas: 1) coalgebraic trace semantics is naturally presented in terms of corecursive algebras, and 2) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof, and allows to derive conditions under which some of them coincide.

## 1 Introduction

Traces are used in the semantics of state-based systems as a way of recording the consecutive behaviour of a state in terms of sequences of observable (input and/or output) actions. Trace semantics leads to, for instance, the notion of trace equivalence, which expresses that two states cannot be distinguished by only looking at their iterated in/output behaviour.

For many years already, trace semantics is a central topic of interest in the coalgebra community — and not only there, of course. One of the key features of the area of coalgebra is that states and their coalgebras can be considered in different universes, formalised as categories. The break-through insight is that trace semantics for a system in universe *A* can often be obtained by switching to a different universe *B*. More explicitly, where the (ordinary) behaviour of the system can be described via a final coalgebra in universe *A*, the trace behaviour arises by finality in the different universe *B*. Typically, the alternative universe *B* is a category of algebraic logics, the Kleisli category, or the category of Eilenberg-Moore algebras, of a monad on universe *A*.

This paper elaborates two new unifying ideas.

1. We observe that the trace map from the state space of a coalgebra to a carrier of traces is in all three situations the unique 'coalgebra-to-algebra' map to a *corecursive algebra* [6] of traces. This differs from earlier work which tries to describe traces as final coalgebras. For us it is quite natural to view languages as algebras, certainly when they consist of finite words/traces.

<footnote>* The research leading to these results has received funding from the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement nr. 320571.</footnote>
2. Next, these corecursive algebras, used as spaces of traces, all arise via a uniform construction, in a setting given by an adjunction together with a special natural transformation that we call a 'step'. We heavily rely on a basic result saying that in this situation, the (lifting of the) right adjoint preserves corecursive algebras, sending them from one universe to another. This is a known result [5], but its fundamental role in trace semantics has not be recognized before. For an arbitrary coalgebra there is then a unique map to the transferred corecursive algebra; this is the trace map that we are after.

The main contribution of this paper is the unifying step-based approach to coalgebraic trace semantics: it is shown that three existing flavours of trace semantics — logical, Eilenberg-Moore, Kleisli — are all instances of our approach. Moreover, comparison results are given relating two of these forms of trace semantics, namely logic-to-Eilenberg-Moore and logic-to-Kleisli. The other combinations involve subtleties which we do not fully grasp yet. Due to space limitations, we don't cover the whole field of coalgebraic trace semantics: we focus only on finite trace semantics, and also exclude at this stage the 'iteration' based approaches, e.g., in [25,22,8].

*Outline.* The paper is organised as follows. It starts in Section 1 with the abstract step-and-adjunction setting, and the relevant definitions and results for corecursive algebras. In the next three sections, it is explained how this setting gives rise to trace semantics, by presenting the above-mentioned three approaches to coalgebraic trace semantics in terms of steps and adjunctions: Eilenberg-Moore (Section 3), logical (Section 4) and Kleisli (Section 5). In each case, the relevant corecursive algebra is described. These sections are illustrated with several examples. The next section establishes a connection between the Eilenberg-Moore and the logical approach, and a connection between the Kleisli and logical approach (Section 6). In Section 7 we briefly show that our construction of corecursive algebras strengthens to a construction of completely iterative algebras. Finally, in Section 8 we provide some directions for future work.

*Notation.* In the context of an adjunction $F \dashv G$, we shall use overline notation $\overline{(-)}$ for adjoint transposition. The unit and counit of an adjunction are, as usual, written as $\eta$ and $\varepsilon$.

For an endofunctor $H$, we write $Alg(H)$ for its algebra category and $CoAlg(H)$ for its coalgebra category. For a monad $(T, \eta, \mu)$ on $C$, we write $\mathcal{EM}(T)$ for the Eilenberg-Moore category and $\mathcal{KL}(T)$ for the Kleisli category.

We recall that any functor $S: \mathbf{Sets} \to \mathbf{Sets}$ has a unique strength st. We write st: $S(X^A) \to S(X)^A$ for st(t)(a) = S(ev_a)(t), where ev_a = $\lambda f.f(a): X^A \to X$.

## 2 Coalgebraic semantics from a step

This section is about the construction of corecursive algebras and their use for semantics. The notion of corecursive algebra, studied in [9,6] as the dual of Taylor's notion of recursive coalgebra [10], is defined as follows.
**Definition 1.** Let $H$ be an endofunctor on a category $\mathbf{C}$.

1. A coalgebra-to-algebra morphism from a coalgebra $c: X \to H(X)$ to an algebra $a: H(A) \to A$ is a map $f: X \to A$ such that the diagram

$$ \begin{array}{ccc} X & \xrightarrow{f} & A \\ \bigcirc_c \downarrow & & \uparrow_a \\ H(X) & \xrightarrow{H(f)} & H(A) \end{array} $$

commutes. Equivalently: such a morphism is a fixpoint for the endofunction on the homset $\mathbf{C}(X, A)$ sending $f$ to the composite

$$ X \xrightarrow{c} H(X) \xrightarrow{H(f)} H(A) \xrightarrow{a} A $$

2. An algebra $a: H(A) \to A$ is corecursive when for every coalgebra $c: H \to H(X)$ there is a unique coalgebra-to-algebra morphism $(X, c) \to (A, a)$.

Here is some intuition.

- As explained in [14], the specification of a coalgebra-to-algebra morphism $f$ is a “divide-and-conquer” algorithm. It says: to operate on an argument, first decompose it via the coalgebra $c$, then operate on each component via $H(f)$, then combine the results via the algebra $a$.

- For each final $H$-coalgebra $\zeta: A \stackrel{\sim}{\to} H(A)$, the inverse $\zeta^{-1}: H(A) \to A$ is a corecursive algebra. For most functors of interest, this final coalgebra gives semantics up to bisimilarity, which is finer than trace equivalence. So trace semantics requires a different corecursive algebra.

In all our examples, we use the same procedure for obtaining a corecursive algebra, which we shall now explain. Our basic setting consists of an adjunction, two endofunctors, and a natural transformation:

$$ H \mathrel{\substack{\rightleftarrows \\ \leftarrow\, \\ \bigcirc \\ G}} C \underset{\bigcirc}{\stackrel{F}{\rightleftarrows}} \mathbf{D} \underset{\bigcirc}{\mathrel{\substack{\rightleftarrows \\ \leftarrow\, \\ L}}}} \quad \text{with} \quad HG \stackrel{\rho}{\Longrightarrow} GL \quad (1) $$

The natural transformation $\rho: HG \Rightarrow GL$ will be called a step. Here $H$ is the *behaviour functor*: we study $H$-coalgebras and give semantics for them in a corecursive $H$-algebra. This arrangement is well-known in the area of coalgebraic modal logic [3,27,20,7,24], but we shall see that its application is wider.

A step can be formulated in several equivalent ways [18,23].

**Theorem 2.** In the situation (1), there are bijective correspondences between natural transformations $\rho_1: HG \Rightarrow GL$, $\rho_2: FH \Rightarrow LF$, $\rho_3: FHG \Rightarrow L$ and $\rho_4: H \Rightarrow GLF$.

Moreover, if $H$ and $L$ happen to be monads, then $\rho_1$ is an $\mathcal{EM}$-law (map $HG \Rightarrow GL$ compatible with the monad structures) iff $\rho_2$ is a $\mathcal{KL}$-law (map $FH \Rightarrow$
Thus, by analogy with the familiar statement that “right adjoints preserves limits”, we have “step-induced algebra liftings of right adjoints preserve corecursiveness”. Now we give the complete construction for semantics of a coalgebra.

**Theorem 5.** Suppose that $L$ has a final coalgebra $\zeta: \Psi \cong L(\Psi)$. Then for every $H$-coalgebra $(X, c)$ there is a unique coalgebra-to-algebra map $c^\dagger$ as on the left below:

$$ \begin{array}{ccc} X & - & c^\dagger \\ \begin{array}{c} c \\ \downarrow \end{array} & - & G(\Psi) \\ \begin{array}{c} H(X) \\ \downarrow \end{array} & - & HG(\Psi) \end{array} $$

$$ \begin{array}{ccc} F(X) & - & \overline{c^\dagger} \\ \begin{array}{c} F^\rho(X,c) \\ \downarrow \end{array} & - & \Psi \\ \begin{array}{c} LF(X) \\ \downarrow \end{array} & - & L(\Psi) \end{array} $$

The map $c^\dagger$ on the left can alternatively be characterized via its adjoint transpose $\overline{c^\dagger}$ on the right, which is the unique coalgebra-to-algebra morphism. The latter can also be seen as the unique map to the final coalgebra $\Psi \cong L(\Psi)$. $\square$

Note that Theorem 5 generalises final coalgebra semantics: taking in (1) $F = G = \text{Id}_C$ and $H = L$, the map $c^\dagger$ in the above theorem is the unique homomorphism to the final coalgebra. In the remainder of this paper we focus on instances where $c^\dagger$ captures traces, and we therefore refer to it as the trace semantics map.

## 3 Traces via Eilenberg-Moore

We recall the approach to trace semantics developed in [17,29,4], putting it in the framework of the previous section. The approach deals with coalgebras for the composite functor $BT$, where $T$ is a monad that captures the ‘branching’ aspect. The following assumptions are required.

$$ \begin{array}{ccc} \mathcal{EM}(T) & \xrightarrow{\bar{B}} & \mathcal{EM}(T) \\ \begin{array}{c} U \\ \downarrow \end{array} & - & \begin{array}{c} U \\ \downarrow \end{array} \\ \mathbf{C} & - & \mathbf{C} \end{array} \quad (2) $$

1. An endofunctor $B: \mathbf{C} \to \mathbf{C}$ with a final coalgebra $\zeta: \Theta \cong B(\Theta)$.

2. A monad $(T, \eta^T, \mu^T)$, with the standard adjunction $\mathcal{F} \dagger U$ between categories $\mathbf{C} \simeq \mathcal{EM}(T)$, where $U$ is ‘forget’ and $\mathcal{F}$ is for ‘free algebras’.

3. A lifting $\bar{B}$ of $B$, as in (2), or, equivalently, an $\mathcal{EM}$-law $\kappa: TB \Rightarrow BT$.

**Example 6.** To briefly illustrate these ingredients, we consider non-deterministic automata. These are $BT$-coalgebras with $B: \mathbf{Sets} \to \mathbf{Sets}$, $B(X) = 2 \times X^A$ with $2 = \{\perp, \top\}$ and $T$ the finite powerset monad. The functor $B$ has a final coalgebra carried by the set $2^{A^*}$ of languages. Further, $\mathcal{EM}(T)$ is the category of join semi-lattices (JSL). The lifting is defined by product in $\mathcal{EM}(T)$, using the JSL on 2 given by the usual ordering $\perp \le \top$. By the end of this section, we revisit this example and obtain the usual language semantics.
These assumptions give rise to the following instance of our general setting (1):

$$ BT \xrightarrow{\mathcal{C}} \xleftarrow[\mathcal{U}]{\mathcal{F}} \xrightarrow{\perp} \mathcal{E}\mathcal{M}(T) \xrightarrow{\bar{\mathcal{B}}} \mathcal{B} \quad \text{with} \quad \rho: BTU \Longrightarrow U\bar{B} \text{ where} \\ \rho_{(X,a)} = (BTX \xrightarrow{Ba} BX) $$

Actually — and equivalently, by Theorem 2 — the step $\rho$ is most easily given in terms of $\rho_4: BT \Rightarrow U\bar{B}\mathcal{F}$: since $\bar{B}$ lifts $B$, we have $U\bar{B}\mathcal{F} = B\mathcal{U}\mathcal{F} = BT$, so that $\rho_4$ is then defined simply as the identity.

The following result is well-known, and is (in a small variation) due to [30].

**Lemma 7.** There is a unique algebra structure $\mathcal{a}$: $T(\Theta) \to \Theta$ making $((\Theta, a), \zeta)$ a $\bar{B}$-coalgebra. Moreover, this coalgebra is final. □

We apply the step-induced algebra lifting $G_\rho$: $\text{Alg}(\bar{B}) \to \text{Alg}(BT)$ to the inverse of this final $\bar{B}$-coalgebra, obtaining a $BT$-algebra:

$$ (BT(\Theta) \xrightarrow{\ell_{em}} \Theta) := G_{\rho}((\Theta, a), \zeta^{-1}) = (BT(\Theta) \xrightarrow{B(a)} B(\Theta) \xrightarrow{\zeta^{-1}} \Theta). $$

By Theorem 5, this algebra is corecursive, giving us trace semantics of $BT$-coalgebras. More explicitly, given a coalgebra $c: X \to BT(X)$, the trace semantics is the unique map, written as $em_c$, making the following square commute.

$$ \begin{tikzcd} & X - \text{\textbf{--}}^{\text{em}_c} - \text{\textbf{--}} \arrow[r] & \Theta \arrow[d, "c"] \arrow[r, "\ell_{em}"] & \Theta \\ BT(X) \text{\textbf{--}} \arrow[r, "\text{BT}(em_c)"'] & BT(\Theta) & & \end{tikzcd} \quad (3) $$

The unique map $em_c$ in (3) appears in the literature as a 'coiteration up-to' or 'unique solution' theorem [1]. Examples follow later in this section (Theorem 8, Example 9).

In [17,29], the above trace semantics of $BT$-coalgebras arises through 'de-terminisation', which we explain next. Given a coalgebra $c: X \to BT(X)$, one takes its adjoint transpose:

$$ \frac{c: X \to BT(X) = B\mathcal{U}\mathcal{F}(X) = U\bar{B}\mathcal{F}(X)}{\bar{c}: \mathcal{F}(X) \to \bar{B}\mathcal{F}(X)} $$

It follows from Theorem 2 and our definition of $\rho$ that this transpose coincides with the application of the step-induced coalgebra lifting $\mathcal{F}^\rho$: $\text{CoAlg}(BT) \to \text{CoAlg}(\bar{B})$ from the previous section, i.e., $\mathcal{F}^\rho(X, c) = (\mathcal{F}(X), \bar{c})$. The functor $\mathcal{F}^\rho$ thus plays the role of determination, see [17]. By Theorem 5, the trace semantics $em_c$ can equivalently be characterised in terms of $\mathcal{F}^\rho$, as the unique map $\overline{em}_c$ making (4) commute. This

$$ \begin{tikzcd} & T(X) - \text{\textbf{--}}^{\overline{em}_c} - \text{\textbf{--}} \arrow[r] & \Theta \arrow[d, "\bar{c}"] \arrow[r, "\text{--}", "\text{--} \to \zeta^{-1}"] & \Theta \\ BT(X) \text{\textbf{--}} \arrow[r, "\text{BT}(\overline{em}_c)"'] & BT(\Theta) & & \end{tikzcd} \quad (4) $$
is how the trace semantics via Eilenberg-Moore is presented in [17,29]: as the transpose $\overline{em}_c = \overline{em}_c \circ \eta_X^T$.

We conclude this section by recalling a canonical construction of a distributive law [15] for a class of ‘automata-like’ examples.

**Theorem 8.** Let $\Omega$ be a set, $T$ a monad on **Sets** and $t: T(\Omega) \to \Omega$ an $\mathcal{E}\mathcal{M}$-algebra. Let $B: \mathbf{Sets} \to \mathbf{Sets}$, $B(X) = \Omega \times X^A$, and $\kappa: TB \Rightarrow BT$ given by

$$ \kappa_X := \left( T(\Omega \times X^A) \xrightarrow{\langle T(\pi_1), T(\pi_2) \rangle} T(\Omega) \times T(X^A) \xrightarrow{t \times \mathrm{st}} \Omega \times T(X)^A \right). $$

Then $\kappa$ is an $\mathcal{E}\mathcal{M}$-law. Moreover, the final $B$-coalgebra $(\Omega^{A^*}, \zeta)$ together with the algebra structure $T(\Omega^{A^*}) \xrightarrow{\mathrm{st}} T(\Omega)^{A^*} \xrightarrow{t^{A^*}} \Omega^{A^*}$ is a final $\overline{B}$-coalgebra. $\square$

**Example 9.** By Theorem 8, we obtain an explicit description of the trace semantics arising from the corecursive algebra (3): for any $\langle o, f \rangle: X \to \Omega \times T(X)^A$, the trace semantics is the unique map $em$ in

$$ \begin{array}{ccc} X & \xrightarrow{\text{em}} & \Omega^{A^*} \\ \langle o, f \rangle \downarrow & & \uparrow^{\zeta^{-1}} \\ BT(X) \xrightarrow{\text{st}} BT(\Omega^{A^*}) & \xrightarrow{\text{em}} & B(T(\Omega)^{A^*}) \xrightarrow{\text{st}} BT(\Omega^{A^*}) \end{array} $$

We instantiate the trace semantics $em$ for various choices of $\Omega$, $T$ and $t$. Given a coalgebra $\langle o, f \rangle: X \to \Omega \times T(X)^A$, we have $em(x)(\varepsilon) = o(x)$ independently of these choices. The table below lists the inductive case $em(x)(aw)$ respectively for non-deterministic automata (NDA) where branching is interpreted as usual (NDA-∃), NDA where branching is interpreted conjunctively (NDA-∀) and (reactive) probabilistic automata (PA). Here $P_f$ is the finite powerset functor, and $D_{\mathrm{fin}}$ the finitely supported distribution functor.

<table><thead><tr><th></th><th><i>T</i></th><th><i>Ω</i></th><th><i>t</i>: <i>T</i>(<i>Ω</i>) &rarr; <i>Ω</i></th><th><b>em</b>(<i>x</i>)(<i>aw</i>)</th></tr></thead><tbody><tr><td>NDA-∃</td><td><i>P</i><sub>f</sub></td><td>2 = {⊥, ⊤}</td><td><i>S</i> &mapsto; ∨ <i>S</i></td><td>∨<sub><i>y</i>∈<i>f</i>(<i>x</i>)(<i>a</i>)</sub> <b>em</b>(<i>y</i>)(<i>w</i>)</td></tr><tr><td>NDA-∀</td><td><i>P</i><sub>f</sub></td><td>2 = {⊥, ⊤}</td><td><i>S</i> &mapsto; ∧ <i>S</i></td><td>∧<sub><i>y</i>∈<i>f</i>(<i>x</i>)(<i>a</i>)</sub> <b>em</b>(<i>y</i>)(<i>w</i>)</td></tr><tr><td>PA</td><td><i>D</i><sub>fin</sub></td><td>[0, 1]</td><td><i>ϕ</i> &mapsto; &sum;<sub><i>p</i>∈[0,1]</sub> <i>p</i> &middot; <i>ϕ</i>(<i>p</i>)</td><td>∑<sub><i>y</i>∈<i>X</i></sub> <b>em</b>(<i>y</i>)(<i>w</i>) &middot; <i>f</i>(<i>x</i>)(<i>a</i>)(<i>y</i>)</td></tr></tbody></table>

For other examples, and a concrete presentation of the associated determination constructions, see [17,29].

# 4 Traces via Logic

This section illustrates how the ‘logical’ approach to trace semantics of [21], started in [27], fits in our general framework. In essence, traces are built up from logical formulas, also called tests, which are evaluated for states. These tests are obtained via an initial algebra of a functor $L$. The approach works both for $TB$ and $BT$-coalgebras (and could, in principle, be extended to more general combinations). We start by listing our assumptions in this section.
It is instructive to characterise this trace semantics in terms of the transpose and the step-induced coalgebra liftings $F^{\delta_{\tau}}$ and $F^{\delta_{\tau}'}$, showing how they arise as unique maps from an initial algebra:

$$ \begin{array}{ccc} F(X) & \leftarrow & -\overline{\log_c} - \Phi \\ F^{\delta_{\tau}}(X,c) \uparrow & & \downarrow \alpha^{-1} \\ LF(X) & \leftarrow & L(\overline{\log_c}) - L(\Phi) \end{array} \qquad \begin{array}{ccc} F(Y) & \leftarrow & -\overline{\log_d} - \Phi \\ F^{\delta_{\tau'}}(Y,d) \uparrow & & \downarrow \alpha^{-1} \\ LF(Y) & \leftarrow & L(\overline{\log_d}) - L(\Phi) \end{array} \qquad (9) $$

In the remainder of this section, we show two classes of examples of the logical trace semantics. With these descriptions we retrieve most of the examples from [21] in a smooth manner.

**Proposition 11.** Let $\Omega$ be a set, $T$: **Sets** $\to$ **Sets** a functor and $t$: $T(\Omega) \to \Omega$ a map. Then the set of languages $\Omega^{A^*}$ carries a corecursive algebra for the functor $\Omega \times T(-)^A$. Given a coalgebra $\langle o, f \rangle$: $X \to \Omega \times T(X)^A$, the unique coalgebra-to-algebra morphism $\log$: $X \to \Omega^{A^*}$ satisfies

$$ \log(x)(\varepsilon) = o(x) \qquad \log(x)(aw) = t(T(ev_w \circ \log)(f(x)(a))) $$

for all $x \in X$, $a \in A$ and $w \in A^*$.

*Proof.* We instantiate the assumptions in the beginning of this section by $\mathbf{C} = \mathbf{D} = \mathbf{Sets}$, $F = G = \Omega^{-}$, $B(X) = \Omega \times X^{A}$, $L(X) = A \times X + 1$ and $T$ the functor from the statement. The initial $L$-algebra is $\alpha: A \times A^* + 1 \cong A^*$. The map $t$ extends to a modality $\tau$: $TG \Rightarrow G$, given on components by

$$ \tau_X := (T(\Omega^X) \xrightarrow{\text{st}} T(\Omega)^X \xrightarrow{t^X} \Omega^X). $$

The logic $\delta$: $BG \Rightarrow GL$ is given by the isomorphism $\Omega \times (\Omega^{-})^{A} \cong \Omega^{(A \times -)+1}$. Instantiating (7) we obtain the corecursive $BT$-algebra

$$ \Omega \times T(\Omega^{A^*})^A \xrightarrow{\text{id} \times (\text{st})^A} \Omega \times (T(\Omega)^{A^*})^A \xrightarrow{\text{id} \times (t^{A^*})^A} \Omega \times (\Omega^{A^*})^A \xrightarrow{\Omega^{\alpha^{-1}} \circ \delta} \Omega^{A^*}. $$

The concrete description of $\log$ follows by spelling out the coalgebra-to-algebra diagram that characterises it. $\square$

**Example 12.** We instantiate the trace semantics $\log$ from Proposition 11 for various choices of $\Omega$, $T$ and $t$. Similar to the instances in Example 9, we consider a coalgebra $\langle o, f \rangle$: $X \to \Omega \times T(X)^A$, and we always have $\log(x)(\varepsilon) = o(x)$. The cases of non-deterministic automata (NDA-∃, NDA-∀) and probabilistic automata (PA) are the same as in Example 9. However, in constrast to the Eilenberg-Moore approach and other approaches to trace semantics, a monad structure on $T$ is not required here. This is convenient as it also allows to treat
alternating automata (AA), where $T = \mathcal{P}_f\mathcal{P}_f$; it is unclear whether $T$ carries a suitable monad structure in that case.

<table><thead><tr><th></th><th>T</th><th>Ω</th><th>t: T(Ω) → Ω</th><th>log(x)(aw)</th></tr></thead><tbody><tr><td>NDA-∃</td><td>\mathcal{P}_f</td><td>2 = {⊥, ⊤}</td><td>S ↦ ∨S</td><td>∑<sub>y∈f(x)(a)</sub> log(y)(w)</td></tr><tr><td>NDA-∀</td><td>\mathcal{P}_f</td><td>2 = {⊥, ⊤}</td><td>S ↦ ∧S</td><td>∧<sub>y∈f(x)(a)</sub> log(y)(w)</td></tr><tr><td>PA</td><td>\mathcal{D}_{fin}</td><td>[0, 1]</td><td>ϕ ↦ ∑<sub>p∈[0,1]</sub> p · ϕ(p)</td><td>∑<sub>y∈X</sub> log(y)(w) · f(x)(a)(y)</td></tr><tr><td>AA</td><td>\mathcal{P}_f\mathcal{P}_f</td><td>2 = {⊥, ⊤}</td><td>S ↦ ∨<sub>T∈S</sub> ∧<sub>b∈T</sub> b</td><td>∑<sub>T∈f(x)(a)</sub> ∧<sub>y∈T</sub> log(y)(w)</td></tr></tbody></table>

We also describe a logic for polynomial functors constructed from a signature. Here, we model a signature by a functor $\Sigma: \mathbb{N} \to \mathbf{Sets}$, where $\mathbb{N}$ is the discrete category of natural numbers. This gives rise to a functor $H_\Sigma: \mathbf{Sets} \to \mathbf{Sets}$ as usual by $H_\Sigma(X) = \coprod_{n \in \mathbb{N}} \Sigma(n) \times X^n$. We abuse notation and write $\sigma(x_1, \dots, x_n)$ instead of $(\sigma, x_1, \dots, x_n)$. The initial algebra of $H_\Sigma$ consists of closed terms (or finite node-labelled trees) over the signature.

**Proposition 13.** Let $\Omega$ be a meet semi-lattice with top element $\top$ as well as a bottom element $\bot$, let $T: \mathbf{Sets} \to \mathbf{Sets}$ be a functor, and $t: T(\Omega) \to \Omega$ a map. Let $\Phi$ be the initial $H_\Sigma$-algebra. The set $\Omega^\Phi$ of ‘tree’ languages carries a corecursive algebra for the functor $TH_\Sigma$. Given a coalgebra $c: X \to TH_\Sigma(X)$, the unique coalgebra-to-algebra map $\log: X \to \Omega^\Phi$ is given by

$$ \log(x)(\sigma(t_1, \dots, t_n)) = t(T(m) \circ c(x)), \text{ where} $$

$$ m = \left( t \mapsto \left\{ \begin{array}{ll} \bigwedge_i \log(x_i)(t_i) & \text{if } \exists x_1 \dots x_n \cdot t = \sigma(x_1, \dots, x_n) \\ \bot & \text{otherwise} \end{array} \right. \right): H_\Sigma(X) \to \Omega $$

for all $x \in X$ and $\sigma(t_1, \dots, t_n) \in \Phi$.

*Proof.* We use $\mathbf{C} = \mathbf{D} = \mathbf{Sets}$, $F = G = \Omega^-$, $B = L = H_\Sigma$. The map $t$ extends to a modality $\tau: TG \Rightarrow G$ as in the proof of Proposition 11. The logic $\delta: H_\Sigma\Omega^- \Rightarrow \Omega^{H_\Sigma(-)}$ is:

$$ \delta_X(\sigma(\phi_1, \dots, \phi_n))(t) = \begin{cases} \bigwedge_i \phi_i(x_i) & \text{if } \exists x_1 \dots x_n \cdot t = \sigma(x_1, \dots, x_n) \\ \bot & \text{otherwise} \end{cases} $$

The corecursive algebra $\ell_{\log}$ is then given by:

$$ TH_{\Sigma}(\Omega^{\Phi}) \xrightarrow{T(\delta)} T(\Omega^{H_{\Sigma}(\Phi)}) \xrightarrow{\text{st}} T(\Omega)^{H_{\Sigma}(\Phi)} \xrightarrow{t^{H_{\Sigma}(\Phi)}} \Omega^{H_{\Sigma}(\Phi)} \xrightarrow{\cong} \Omega^{\Phi}. $$

The explicit characterisation of $\log$ is a straightforward computation. $\square$

<figure><img src="image_2.png" /></figure>

*Example 14.* Given a signature $\Sigma$, a coalgebra $f: X \to \mathcal{P}_f H_\Sigma(X)$ is a (top-down) tree automaton. With $\Omega = \{\bot, \top\}$ and $t(S) = \bigvee S$, Proposition 13 gives:

$$ \log(x)(\sigma(t_1, \dots, t_n)) = \top \text{ iff } \exists x_1 \dots x_n. \sigma(x_1, \dots, x_n) \in f(x) \wedge \bigwedge_{1 \le i \le n} \log(x_i)(t_i) $$

for every state $x \in X$ and tree $\sigma(t_1, \dots, t_n)$. This is the standard semantics of tree automata. It is easily adapted to weighted tree automata, see [21].
By Theorem 5, this algebra is corecursive, i.e., for every coalgebra $c: X \to TB(X)$, there is a unique map $kl_c$ as below:

$$ \begin{array}{ccc} X & \to & T(\Psi) \\ \multicolumn{3}{c}{\text{---} \xrightarrow{kl_c} \text{---}} \\ c & \leftarrow & \text{---} \xrightarrow{TB(kl_c)} \text{---} \xrightarrow{\ell_{kl}} \\ \text{---} & \to & TBT(\Psi) \end{array} $$

The trace semantics is exactly as in [12], to which we refer for examples.

# 6 Comparison

The presentation of trace semantics in terms of corecursive algebras allows us compare the different approaches by constructing algebra morphisms between them. In this section, we compare the Eilenberg-Moore against the logical approach, and the Kleisli against the logical approach as well. For a comparison between Kleisli and Eilenberg-Moore we refer to [17]. The latter is not in terms of corecursive algebras; we leave such a reformulation for future work. In [21], logical traces are also compared to determinisation constructions. But the technique is different, with the primary difference that no corecursive algebras are used there.

## 6.1 Eilenberg-Moore and Logic

To compare the Eilenberg-Moore approach to the logical approach, we combine their assumptions. This amounts to an adjunction $F \vdash G$, endofunctors $B, L$ and a monad $T$ as follows:

<figure><img src="image_3.png" /></figure>

together with:

1. A final $B$-coalgebra $\zeta: \Theta \cong B(\Theta)$.

2. An $\mathcal{EM}$-law $\kappa: TB \Rightarrow BT$, or equivalently, a lifting $\bar{B}$ of $B$.

3. An initial algebra $\alpha: L(\Phi) \cong \Phi$.

4. A step $\delta: BG \Rightarrow GL$.

5. A step $\tau: TG \Rightarrow G$, whose components are $\mathcal{EM}$-algebras (a *monad action*).

The map $\tau$ is an assumption of the logical approach, but the compatibility with the monad structure was not assumed before (in the logical approach, $T$ is not assumed to be a monad). We note that $\tau$ being a monad action is the same thing as $\tau$ being an $\mathcal{EM}$-law (involving the monad $T$ on the left and the identity monad on the right). Therefore, by Theorem 2:
**Theorem 17.** If the equivalent conditions in Lemma 16 hold, then the map $e$ defined in (11) is an algebra morphism from $\ell_{em}$ to $\ell^{\log}$, as on the left below.

<figure><img src="image_4.png" /></figure>

In that case, for any coalgebra $X \xrightarrow{\sim} BT(X)$ the triangle on the right commutes.

*Proof.* We use that $\ell_{em} = \zeta^{-1} \circ B(a): BT(\Theta) \to \Theta$, where $((\Theta, a), \zeta)$ is the final $\overline{B}$-coalgebra, see Section 3. We need to prove that the outside of the following diagram commutes.

<figure><img src="image_5.png" /></figure>

The rectangle on the right commutes by definition of $e$. For the square on the left, it suffices to show $e \circ a = \tau_1 \circ T(e)$; this is equivalent to $F(a) \circ \bar{e} = \tau_2 \circ \bar{e}$ in:

$$ \Phi \xrightarrow{\bar{e}=F(e) \circ \epsilon} F(\Theta) \xrightarrow{F(a)} \tau_2 \xrightarrow{FT(\Theta)} $$

Indeed, by transposing we have on the one hand:

$$ \bar{e} \circ \bar{a} = F(a \circ e) \circ \epsilon_{\Phi} = F(a) \circ F(e) \circ \epsilon_{\Phi} = F(a) \circ \bar{e} $$

And on the other hand, using that $\tau_2 = F(\tau_1 \circ T(\eta)) \circ \epsilon$,

$$ \begin{align*} \tau_2 \circ \bar{e} &= F(\tau_1 \circ T(\eta)) \circ \epsilon \circ F(e) \circ \epsilon \\ &= F(\tau_1 \circ T(\eta)) \circ FG(F(e) \circ \epsilon) \circ \epsilon \\ &= F(G(F(e) \circ \epsilon) \circ \tau_1 \circ T(\eta)) \circ \epsilon \\ &= F(\tau_1 \circ TG(F(e) \circ \epsilon) \circ T(\eta)) \circ \epsilon \\ &= F(\tau_1 \circ T(G(\epsilon) \circ GF(e) \circ \eta)) \circ \epsilon = F(\tau_1 \circ T(e)) \circ \epsilon = \overline{\tau_1 \circ T(e)}. \end{align*} $$

By transposing the maps in (11), it follows that $\bar{e}: \Phi \to F(\Theta)$ is the unique morphism from the initial $L$-algebra to $F(\zeta) \circ \delta_2: LF(\Theta) \to F(\Theta)$. Hence, for the desired equality $F(a) \circ \bar{e} = \tau_2 \circ \bar{e}$, it suffices to prove that $F(a)$ and $\tau_2$ are
both algebra homomorphisms from $F(\zeta) \circ \delta_2$ to a common algebra, which in turn
follows from commutativity of the following diagram.

<figure><img src="image_6.png" /></figure>

Using the translation $(-)_1 \leftrightarrow (-)_2$ (of Theorem 2), one shows that the upper-
left rectangle is equivalent to the assumption (12). To see this, we use that
$(\delta^\tau)_2 = (\delta_1 \circ B\tau_1)_2 = \delta_2 T \circ L\tau_2$ and $(\delta_\tau)_2 = (\tau_1 L \circ T\delta_1)_2 = \tau_2 B \circ \delta_2$ (as stated,
e.g., in [21]); moreover, it is easy to check that $(\delta_1 \circ B\tau_1 \circ \kappa G)_2 = F_\kappa \circ (\delta_1 \circ B\tau_1)_2$.
The lower-right rectangle commutes since $((\Theta, a), \zeta)$ is a $\bar{B}$-coalgebra. The other
two squares commute by naturality.

For the second part of the theorem, let $c: X \to BT(X)$ be a coalgebra. Since $e$ is an algebra morphism, the equation $e \circ em_c = \log_c$ follows by uniqueness of morphisms from $c$ to the corecursive algebra on $G(\Phi)$. $\square$

The equality $e \circ em_c = \log_c$ means that equivalence wrt Eilenberg-Moore
trace semantics implies equivalence wrt the logical trace semantics. The converse
is, of course, true if $e$ is monic. For that, it is sufficient if $\delta: BG \Rightarrow GL$ is
expressive. Here expressiveness is the property that for any $B$-coalgebra, the
unique coalgebra-to-algebra morphism to the corecursive algebra on $G(\Phi)$ factors
as a $B$-coalgebra homomorphism followed by a mono. This holds in particular if
the components $\delta_A: BG(A) \to GL(A)$ are all monic (in $C$) [20].

**Lemma 18.** If $\delta: BG \Rightarrow GL$ is expressive, then $e$ is monic. Moreover, if $\delta$ is an isomorphism, then $e$ is an iso as well.

*Proof.* Expressivity of $\delta$ means that we have $e = m \circ h$ for some coalgebra homomorphism $h$ and mono $m$. By finality of $\zeta$ there is a $B$-coalgebra morphism $h'$ such that $h' \circ h = \text{id}$. It follows that $h$ is monic (in $C$), so that $m \circ h = e$ is monic too. For the second claim, if $\delta$ is an isomorphism, then $G(\alpha^{-1}) \circ \delta: BG(\Phi) \to G(\Phi)$ is an invertible corecursive $B$-algebra, which implies it is a final coalgebra (see [5, Proposition 7], which states the dual). It then follows from (11) that $e$ is a coalgebra morphism from one final $B$-coalgebra to another, which means it is an isomorphism. $\square$

Previously, we have seen both a class of examples of the Eilenberg-Moore
approach (Theorem 8), and the logical approach (Proposition 11). Both arise
from the same data: a monad $T$ (just a functor in the logical approach) and an
$\mathcal{EM}$-algebra $t$. We thus obtain, for these automata-like examples, both a logical
trace semantics and a matching 'Eilenberg-Moore' semantics, where the latter essentially amounts to a determinisation procedure. The underlying distributive laws satisfy (12) by construction, so that the two approaches coincide (as already seen in the concrete examples).

**Theorem 19.** Let $\Omega$ be a set, $T$: **Sets** $\rightarrow$ **Sets** a monad and $t$: $T(\Omega) \rightarrow \Omega$ an $\mathcal{EM}$-algebra. The $\mathcal{EM}$-law $\kappa$ of Theorem 8, together with $\delta, \tau$ as defined in the proof of Proposition 11, satisfies (12). For any coalgebra $c$: $X \rightarrow \Omega \times T(X)^A$, the map $\log_c$ coincides (up to isomorphism) with the map $em_c$.

*Proof.* To prove (12), i.e., $\delta^\tau \circ \kappa = \delta_\tau$, we first compute, following (6),

$$ (\delta^\tau)_X = \delta_X \circ (\mathrm{id} \times \tau_X^A) = \delta_X \circ (\mathrm{id} \times (t^X \circ \mathrm{st})^A) : \Omega \times (T(\Omega^X))^A \rightarrow \Omega^{A \times X+1} \\ (\delta_\tau)_X = \tau_{A \times X+1} \circ T(\delta_X) = t^{A \times X+1} \circ \mathrm{st} \circ T(\delta_X) : T(\Omega \times (\Omega^X)^A) \rightarrow \Omega^{A \times X+1} $$

Hence, we need to show that

$$ \delta_X \circ (\mathrm{id} \times (t^X \circ \mathrm{st})^A) \circ (t \times \mathrm{st}) \circ \langle T(\pi_1), T(\pi_2) \rangle = t^{A \times X+1} \circ \mathrm{st} \circ T(\delta_X) \quad (13) $$

for every set $X$. To this end, let $S \in T(\Omega \times (\Omega^X)^A)$ and $t \in (A \times X + 1)$. We first spell out the right-hand side:

$$ \begin{align*} & (t^{A \times X+1} \circ \mathrm{st} \circ T(\delta_X)(S))(t) \\ &= t((\mathrm{st} \circ T(\delta_X)(S))(t)) \\ &= t(T(\mathrm{ev}_t \circ \delta_X)(S)) \\ &= \begin{cases} t(T(\pi_1)(S)) & \text{if } t = * \in 1 \\ t(T(\mathrm{ev}_x \circ \mathrm{ev}_a \circ \pi_2)(S)) & \text{if } t = (a, x) \in A \times X \end{cases} \end{align*} $$

In the last step, we used the definition of $\delta$:

$$ \begin{align*} \mathrm{ev}_* \circ \delta_X(\omega, f) &= \delta_X(\omega, f)(*) = \omega = \pi_1(\omega, f), \\ \mathrm{ev}_{(a,x)} \circ \delta_X(\omega, f) &= \delta_X(\omega, f)(a, x) = f(a)(x) = \mathrm{ev}_x \circ \mathrm{ev}_a \circ \pi_2(\omega, f). \end{align*} $$

For the left-hand side of (13), distinguish cases $* \in 1$ and $(a, x) \in A \times X$.

$$ \begin{align*} & (\delta_X \circ (\mathrm{id} \times (t^X \circ \mathrm{st})^A) \circ (t \times \mathrm{st}) \circ \langle T(\pi_1), T(\pi_2) \rangle(S))(*) \\ &= \pi_1(\mathrm{id} \times (t^X \circ \mathrm{st})^A) \circ (t \times \mathrm{st}) \circ \langle T(\pi_1), T(\pi_2) \rangle(S) \\ &= t(T(\pi_1)(S)) \end{align*} $$
which matches the right-hand side of (13). For $(a, x) \in A \times X$, we have:

$$ 
\begin{align*}
& (\delta_X \circ (\mathrm{id} \times (t^X \circ \mathrm{st})^A) \circ (t \times \mathrm{st}) \circ \langle T(\pi_1), T(\pi_2) \rangle(S))(a, x) \\
&= (((t^X \circ \mathrm{st})^A \circ \mathrm{st})(T(\pi_2)(S)))(a)(x) \\
&= (((t^X)^A \circ \mathrm{st}^A \circ \mathrm{st})(T(\pi_2)(S)))(a)(x) \\
&= (t^X \circ \mathrm{st}(\mathrm{st}(T(\pi_2)(S))(a))(x) \\
&= (t^X \circ \mathrm{st}(T(\mathrm{ev}_a)(T(\pi_2)(S)))(x) \\
&= (t^X \circ \mathrm{st}(T(\mathrm{ev}_a \circ \pi_2)(S))(x) \\
&= t(\mathrm{st}(T(\mathrm{ev}_a \circ \pi_2)(S))(x)) \\
&= t(T(\mathrm{ev}_x) \circ T(\mathrm{ev}_a \circ \pi_2)(S)) \\
&= t(T(\mathrm{ev}_x \circ \mathrm{ev}_a \circ \pi_2)(S))
\end{align*}
$$

which also matches the right-hand side, hence we obtain (13) as desired.

Since (12) is satisfied, it follows from Theorem 17 that $e \circ em_c = \log_c$. Since $\delta$ is an iso, $e$ is an iso as well by Lemma 18. $\square$

## 6.2 Kleisli and Logic

To compare the Kleisli approach to the logical approach, we combine their assumptions. This amounts to an adjunction $F \vdash G$, endofunctors $B, L$ and a monad $T$ as follows:

<figure><img src="image_7.png" /></figure>

together with:

1. An initial algebra $\beta: B(\Psi) \stackrel{\sim}{\Rightarrow} \Psi$.

2. A $Kl$-law $\lambda: BT \Rightarrow TB$, or equivalently, an extension $\bar{B}$ of $B$.

3. $(\Psi, J(\beta^{-1}))$ is a final $\bar{B}$-coalgebra.

4. An initial algebra $\alpha: L(\Phi) \stackrel{\sim}{\Rightarrow} \Phi$.

5. A step $\delta: BG \Rightarrow GL$.

6. A step $\tau: TG \Rightarrow G$, whose components are $\mathcal{EM}$-algebras (a *monad action*).

Again, we assume $\tau$ to be compatible with the monad, satisfying the equivalent conditions in Lemma 15. Since $\delta$ is a step, we obtain the following unique coalgebra-to-algebra morphism $k$ from the initial $B$-algebra:

$$ 
\begin{tikzcd}
& \Psi \arrow[r, "k"] \arrow[d, "\beta^{-1}"] & G(\Phi) \arrow[d, "\uparrow_{G(\alpha^{-1})}"] \\
B(\Psi) \arrow[r, "B(k)"'] & BG(\Phi) \arrow[r, "\delta"] & GL(\Phi)
\end{tikzcd}
\quad (14)
$$

Since $\tau$ is a monad action, for every $X$, $G(X)$ carries an Eilenberg-Moore algebra $\tau_X$. Thus we can take the adjoint transpose $\bar{k} = \tau_\Phi \circ T(k): T(\Psi) \to G(\Phi)$. We have the following analogue of Theorem 17.
Everything commutes: the upper right rectangle by assumption (15), the rightmost square in the middle row since $\tau$ is an action, the outer shapes by definition of $\ell_{kl}$ and $\ell_{log}$, the lower left rectangle by (14) and the rest by naturality. $\square$

The above result gives a sufficient condition under which 'Kleisli' trace equivalence implies logical trace equivalence. However, contrary to the case of traces in Eilenberg-Moore, in Lemma 18, we currently do not have a converse. If $\delta$ has monic components, then it is easy to use corecursiveness to define a map from $\ell_{log}$ to $\ell_{kl}$, but this surprisingly is not sufficient to show $\bar{k}$ to be monic, as confirmed by Example 22 below. In the comparison between Eilenberg-Moore and Kleisli traces [17], a similar difficulty arises: it is unclear under what conditions the map from the final coalgebra in Kleisli to the final coalgebra in Eilenberg-Moore obtained there is mono (and hence, if Eilenberg-Moore trace equivalence implies Kleisli trace equivalence).

**Example 22.** We give an example where $\delta: BG \Rightarrow GL$ is monic and (15) commutes, but where nevertheless logical equivalence is stronger than 'Kleisli' trace equivalence. Let $C = D = \mathbf{Sets}$, $F = G = 2^{-}$, $B = L = (A \times -) + 1$, $T = \mathcal{P}$, $\tau: \mathcal{P}2^{-} \Rightarrow 2^{-}$ given by union as before, and define the step $\delta$ by $\delta_X(a, \varphi)(t) = \top$ iff $\exists x.t = (a, x) \wedge \varphi(x)$, and $\delta_X(*)(t) = \top$ (the latter differs from the step in Proposition 13). Notice that $\delta$ indeed has monic components.

Let $\lambda: BT \Rightarrow TB$ be the distributive law from [12], given by $\lambda_X(a, S) = \{(a, x) | x \in S\}$ and $\lambda(*) = \{*\}$. Then (15) is satisfied:

$$ \begin{array}{ccc} A \times \mathcal{P}(2^X) + 1 & \xrightarrow{\lambda} & \mathcal{P}(A \times 2^X + 1) \\ \multicolumn{2}{c}{\text{id} \times \tau+1 \downarrow} & \downarrow \mathcal{P}(\delta) \\ A \times 2^X + 1 & \xrightarrow{\delta} & 2^{A \times X+1} \leftarrow \tau \quad \mathcal{P}(2^{A \times X+1}) \end{array} $$

It is straightforward to check that this commutes. However, given a coalgebra $f: X \to TB(X)$, the induced logical semantics $\log: X \to 2^{A^*}$ is: $\log(x)(w) = \top$ iff $* \in f(x)$ or $\exists a \in A, v \in A^*, y \in X.w = av \wedge (a, y) \in f(x) \wedge \log(y)(v) = \top$. In particular, this means that if $* \in f(x)$ and $* \in f(y)$ for some states $x, y$, then they are trace equivalent. This differs from the Kleisli semantics, which amounts to the usual language semantics of non-deterministic automata [12].

Cîrstea [8] compares logical traces to a 'path-based semantics', which resembles the Kleisli approach (as well as [22]) but does not require a final $\bar{B}$-coalgebra. In particular, given a commutative monad $T$ on $\mathbf{Sets}$ and a signature $\Sigma$, she considers a canonical distributive law $\lambda: H_{\Sigma}T \Rightarrow TH_{\Sigma}$, which coincides with the one in [12]. Cîrstea shows that, with $\Omega = T(1)$, $t = \mu_1: TT(1) \to T(1)$ and $\delta$ from the proof of Proposition 13 (assuming $T1$ to have enough structure to define that logic), the triangle (15) commutes (see [8, Lemma 5.12]).

# 7 Completely Iterative Algebras

In this paper, we constructed several corecursive algebras. We briefly show that they all satisfy the following stronger property [26].
**Definition 23.** For an endofunctor $H$ on $\mathbf{C}$, an $H$-algebra $a: HA \to A$ is completely iterative when $[id, a]$ is a corecursive $A + H$-coalgebra. Explicitly: when for every $c: X \to A + HX$ there is a unique $f: X \to A$ such that the following diagram commutes.

$$ \begin{tikzcd} X \arrow[r, "f"] \arrow[d, "c"] & A \arrow[d, "[id,a]"'] \\ A + HX \arrow[r, "A+Hf"'] & A + HA \end{tikzcd} $$

Following [14,26], we have two ways of constructing such algebras.

**Proposition 24.**

1. If $\zeta: A \to HA$ is a final $H$-coalgebra, then $(A, \zeta^{-1})$ is completely iterative.

2. Given a step as in Section 2, the functor $G_\rho$ preserves complete iterativity.

We may thus say: “step-induced algebra liftings of right adjoints preserve complete iterativity”. Consequently, by analogy with Theorem 5, if $L$ has a final coalgebra $(\Psi, \zeta)$ then $G_\rho(A, \zeta^{-1})$ is completely iterative. For our examples, this may be seen as a trace semantics for a coalgebra $c$ that may sometimes stop following the behaviour functor and instead provide semantics directly.

## 8 Future work

The main contribution of this paper is a general treatment of trace semantics via corecursive algebras, constructed through an adjunction and a step, covering the ‘Eilenberg-Moore’, ‘Kleisli’ and ‘logic’ approaches to trace semantics. It is expected that our framework also works for other examples, such as the ‘quasi-liftings’ in [2], but this is left for future work. In [19], several examples of adjunctions are discussed in the context of automata theory, some of them the same as the adjunctions here, but with the aim of lifting them to categories of coalgebras, under the condition that what we call the step is an iso. In our case, it usually is not an iso, since the behaviour functor is a composite $TB$ or $BT$; however, it remains interesting to study cases in which such adjunction liftings appear, as used for instance in the aforementioned paper and [28,21]. Further, our treatment in Section 3 (Eilenberg-Moore) assumes a monad to construct the corecursive algebra, but it was shown by Bartels [1] that this algebra is also corecursive when the underlying category has countable coproducts (and dropping the monad assumption). We currently do not know whether this fits our abstract approach. Finally, the Eilenberg-Moore/logic and Kleisli/logic comparisons (Section 6) seem to share certain aspects (the conditions look very similar), but so far we have been unable to derive a general perspective on such comparisons that covers both, and possibly also the Eilenberg-Moore/Kleisli comparison of [17].

*Acknowledgement.* We are grateful to the anonymous referees for various comments and suggestions.
References

1. F. Bartels. Generalised coinduction. *Mathematical Structures in Computer Science*, 13(2):321–348, 2003.

2. F. Bonchi, A. Silva, and A. Sokolova. The power of convex algebras. In R. Meyer and U. Nestmann, editors, *28th International Conference on Concurrency Theory, CONCUR 2017*, volume 85 of LIPICS, pages 23:1–23:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.

3. M. Bonsangue and A. Kurz. Duality for logics of transition systems. In *Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005*, pages 455–469, 2005.

4. M. Bonsangue, S. Milius, and A. Silva. Sound and complete axiomatizations of coalgebraic language equivalence. *ACM Trans. Comput. Log.*, 14(1):7:1–7:52, 2013.

5. V. Capretta, T. Uustalu, and V. Vene. Recursive coalgebras from comonads. *Inf. Comput.*, 204(4):437–468, 2006.

6. V. Capretta, T. Uustalu, and V. Vene. Corecursive algebras: A study of general structured corecursion. In M. Vinicius Medeiros Oliveira and J. Woodcock, editors, *Formal Methods: Foundations and Applications*, number 5902 in Lect. Notes Comp. Sci., pages 84–100. Springer, Berlin, 2009.

7. L-T. Chen and A. Jung. On a categorical framework for coalgebraic modal logic. *Electr. Notes Theor. Comput. Sci.*, 308:109–128, 2014.

8. C. Cîrstea. A coalgebraic approach to quantitative linear time logics. CoRR, abs/1612.07844, 2016.

9. A. Eppendahl. Coalgebra-to-algebra morphisms. *Electr. Notes Theor. Comput. Sci.*, 29:42–49, 1999.

10. J. Y. Girard, Y. Lafont, and P. Taylor. *Proofs and Types*. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1988.

11. I. Hasuo. Generic weakest precondition semantics from monads enriched with order. *Theor. Comput. Sci.*, 604:2–29, 2015.

12. I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via coinduction. *Log. Meth. Comp. Sci.*, 3(4), 2007.

13. W. Hino, H. Kobayashi, I. Hasuo, and B. Jacobs. Healthiness from duality. In *Logic in Computer Science*. IEEE, Computer Science Press, 2016.

14. R. Hinze, N. Wu, and J. Gibbons. Conjugate hylomorphisms - or: The mother of all structured recursion schemes. In Sriram K. Rajamani and David Walker, editors, *Proceedings of the Symposium on Principles of Programming Languages, POPL 2015*, pages 527–538. ACM, 2015.

15. B. Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In *Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday*, pages 375–404, 2006.

16. B. Jacobs. A recipe for state and effect triangles. *Log. Meth. Comp. Sci.*, 13(2), 2017. See https://lmcs.episciences.org/3660.

17. B. Jacobs, A. Silva, and A. Sokolova. Trace semantics via determinization. *Journ. of Computer and System Sci.*, 81(5):859–879, 2015.

18. G. M. Kelly and R. Street. Review of the elements of 2-categories. In Gregory M. Kelly, editor, *Category Seminar: Proceedings Sydney Category Seminar 1972/1973*, number 420 in Lecture Notes in Mathematics. Springer-Verlag, 1974.

19. H. Kerstan, B. König, and B. Westerbaan. Lifting adjunctions to coalgebras to (re)discover automata constructions. In M. Bonsangue, editor, *Coalgebraic Methods in Computer Science (CMCS 2014), Revised Selected Papers*, volume 8446 of Lect. Notes Comp. Sci., pages 168–188. Springer, 2014.
20. B. Klin. Coalgebraic modal logic beyond sets. In M. Fiore, editor, *Math. Found. of Programming Semantics*, number 173 in Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 2007.

21. B. Klin and J. Rot. Coalgebraic trace semantics via forgetful logics. *Log. Meth. Comp. Sci.*, 12(4:10), 2016. See https://lmcs.episciences.org/2622.

22. A. Kurz, S. Milius, D. Pattinson, and L. Schröder. Simplified coalgebraic trace equivalence. In *Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering*, pages 75–90, 2015.

23. T. Leinster. *Higher Operads, Higher Categories*, volume 298 of *London Mathematical Society Lecture Notes*. Cambridge University Press, 2004.

24. P. Levy. Final coalgebras from corecursive algebras. In L. Moss and P. Sobocinski, editors, *Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)*, volume 35 of *LIPIcs*, pages 221–237. Schloss Dagstuhl, 2015.

25. S. Milius, D. Pattinson, and L. Schröder. Generic trace semantics and graded monads. In *6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands*, pages 253–269, 2015.

26. Stefan Milius. Completely iterative algebras and completely iterative monads. *Inf. Comput.*, 196(1):1–41, 2005.

27. D. Pavlović, M. Mislove, and J. Worrell. Testing semantics: Connecting processes and process logics. In M. Johnson and V. Vene, editors, *Algebraic Methods and Software Technology*, number 4019 in Lect. Notes Comp. Sci., pages 308–322. Springer, Berlin, 2006.

28. J. Rot. Coalgebraic minimization of automata by initiality and finality. *Elect. Notes in Theor. Comp. Sci.*, 325:253–276, 2016.

29. A. Silva, F. Bonchi, M. Bonsangue, and J. Rutten. Generalizing determinization from automata to coalgebras. *Log. Meth. Comp. Sci.*, 9(1), 2013.

30. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In *Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997*, pages 280–291. IEEE Computer Society, 1997.