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: (i) coalgebraic,draftrules trace semantics is naturally presented in terms of corecursive algebras, and (ii) 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.
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, formalized 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.
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 [7] 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.
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 [6], but its fundamental role in trace semantics has not been 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 and Kleisli—are all instances of our approach. Moreover, comparison results are given relating theses. We focus only on finite trace semantics and also exclude at this stage the ‘iteration’ based approaches, e.g. in [9, 10, 31, 38].
Outline. The paper is organized 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. In Section 6, we study partial traces for coalgebras with input and output [5], as another instance of the step-and-adjunction setting, but it is helpful to express that setting in the language of bimodules, which we do in Appendix B.
The next section establishes a connection between the Eilenberg–Moore and the logical approach, between the Kleisli and logical approach and between the Kleisli and Eilenberg–Moore approach (Section 7). In Section 8, we show that our construction yields algebras that are not merely corecursive but completely iterative, a stronger property that provides more general trace semantics. Finally, in Section 9, 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 |$ {\textrm {Alg}}(H)$| for its algebra category and |$ {\textrm {CoAlg}}(H)$| for its coalgebra category. For a monad |$(T,\eta ,\mu )$| on |$ {\textbf {C}} $|, we write |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)$| for the Eilenberg–Moore category and |${\mathcal {K}}{\kern -.4ex}\ell (T)$| for the Kleisli category.
We recall that any functor |$S \colon {\textbf {Sets}} \rightarrow {\textbf {Sets}} $| has a unique strength |$ {\textrm {st}}$|. We write |$ {\textrm {st}} \colon S(X^A) \rightarrow S(X)^A$| for |$ {\textrm {st}}(t)(a) = S(\textrm {ev}_a)(t)$|, where |$\textrm {ev}_a = \lambda f. f(a) \colon X^A \rightarrow 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 [7, 11] as the dual of Taylor’s notion of recursive coalgebra [12], is defined as follows.
Let |$H$| be an endofunctor on a category |$ {\textbf {C}} $|.
A coalgebra-to-algebra morphism from a coalgebra |$c\colon X \rightarrow H(X)$| to an algebra |$a\colon H(\varTheta )\rightarrow \varTheta $| is a map |$f\colon X \rightarrow \varTheta $| such that the diagram
commutes. Equivalently: such a morphism is a fixpoint for the endofunction on the homset |$ {\textbf {C}} (X,\varTheta )$| sending |$f$| to the composite
An algebra |$a \colon H(A) \rightarrow A$| is corecursive when for every coalgebra |$c \colon X \rightarrow H(X)$| there is a unique coalgebra-to-algebra morphism |$(X,c) \to (\varTheta ,a)$|.
Here is some intuition.
- –
As explained in [18], 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
, the inverse |$\zeta ^{-1} \colon H(\varTheta ) \rightarrow \varTheta $| 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. It makes frequent use of the following so-called mate correspondence [26, 34]; also see, e.g. [23, 28, 29, 35] for special cases.
Given adjunctions and functors
In the situation (1), there are bijective correspondences between natural transformations |$\rho _1 \colon HG \Rightarrow GL$|, |$\rho _2 \colon FH \Rightarrow LF$|, |$\rho _3 \colon FHG \Rightarrow L$| and |$\rho _4 \colon H \Rightarrow GLF$|, as in Theorem 2.2.
Moreover, if |$H$| and |$L$| happen to be monads, then |$\rho _1$| is an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law (map |$HG \Rightarrow GL$| compatible with the monad structures) iff |$\rho _2$| is a |${\mathcal {K}}{\kern -.4ex}\ell $|-law (map |$FH \Rightarrow LF$| compatible with the monad structures) iff |$\rho _4$| is a monad map; and two further equivalent characterizations are respectively a lifting of |$G$| or an extension of |$F$|:
Steps give rise to liftings to categories of algebras and coalgebras, as follows.
In the setting (1), the step natural transformation |$\rho $| gives rise to both:
a lifting |$G_\rho $| of the right adjoint |$G$|, called the step-induced algebra lifting:
dually, a lifting |$F^{\rho }$| of the left adjoint |$F$|, called the step-induced coalgebra lifting:
Our approach relies on the following basic result.
In the setting (1), for a corecursive |$L$|-algebra |$a \colon L(\varTheta ) \to \varTheta $|, the transferred |$H$|-algebra |$G_{\rho } (\varTheta ,a) \colon HG(\varTheta ) \to G(\varTheta )$| is also corecursive.
Let |$c\colon X \rightarrow H(X)$| be an |$H$|-coalgebra. Then |$F^{\rho }(X,c)$| is an |$L$|-coalgebra, which gives rise to a unique coalgebra-to-algebra map |$f\colon F(X) \rightarrow \varTheta $| with |$a \mathrel {\circ } L(f) \mathrel {\circ } \rho \mathrel {\circ } F(c) = f$|. The adjoint-transpose |$g\colon X \rightarrow G(\varTheta )$| of |$f$| is then the unique coalgebra-to-algebra map from |$(X,c)$| to |$G_{\rho }(\varTheta ,a)$|.
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.
Suppose that |$L$| has a final coalgebra 
. Then for every |$H$|-coalgebra |$(X,c)$| there is a unique coalgebra-to-algebra map |$c^\dagger $| as on the left below:
.Note that Theorem 2.6 generalizes final coalgebra semantics: taking in (1) |$F = G = \textrm {Id}_{ {\textbf {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 |$c^\dagger $| as the trace semantics map.
Given steps |$\rho \colon HG \Rightarrow GL$| and |$\theta \colon KG \Rightarrow GM$|, we can form a new step by composition, written as |$\theta \circledcirc \rho $| in:
We conclude with a lemma that relates the mate construction to composition of steps. See Appendix A for a proof.
Let |$\rho \colon HG \Rightarrow GL$|, |$\theta \colon KG \Rightarrow GM$| be steps. Then |$\big (\theta \circledcirc \rho \big )_2 = M \rho _2 \mathrel {\circ } \theta _2 H$|.
3 Traces via Eilenberg–Moore
We recall the approach to trace semantics developed in [4, 22, 43], 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.
In this section, we assume the following:
An endofunctor |$B \colon {\textbf {C}} \rightarrow {\textbf {C}} $| with a final coalgebra
.A monad |$(T,\eta ,\mu )$|, with the standard adjunction |${\mathcal {F}} \dashv U$| between categories |$ {\textbf {C}} \leftrightarrows {\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)$|, where |$U$| is ‘forget’ and |${\mathcal {F}}$| is for ‘free algebras’.
- A lifting |$\overline {B}$| of |$B$|, as in
or, equivalently, an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law |$\kappa \colon TB \Rightarrow BT$|.(3)$$\ $$
To briefly illustrate these ingredients, we consider non-deterministic automata. These are |$BT$|-coalgebras with |$B\colon {\textbf {Sets}} \rightarrow {\textbf {Sets}} $|, |$B(X) = 2 \times X^A$| where |$2 = \{\bot ,\top \}$| and |$T$| the finite powerset monad. The functor |$B$| has a final coalgebra carried by the set |$2^{A^*}$| of languages. Further, |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)$| is the category of join semilattices (JSLs). The lifting is defined by products in |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)$|, using the JSL on |$2$| given by the usual ordering |$\bot \leq \top $|. By the end of this section, we revisit this example and obtain the usual language semantics.
The following result is well known and is (in a small variation) due to [45].
There is a unique algebra structure |$a \colon T(\varTheta ) \rightarrow \varTheta $| making |$((\varTheta ,a),\zeta )$| a |$\overline {B}$|-coalgebra. Moreover, this coalgebra is final in |$ {\textrm {CoAlg}}(\overline {B})$|.
We conclude this section by recalling a canonical construction of a distributive law [19] for a class of ‘automata-like’ examples that we will spell out in Example 3.5.
Let |$\varOmega $| be a set, |$T$| a monad on |$ {\textbf {Sets}} $| and |$t \colon T(\varOmega ) \rightarrow \varOmega $| an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-algebra. Let |$B \colon {\textbf {Sets}} \rightarrow {\textbf {Sets}} $|, |$B(X) = \varOmega \times X^A$|, and |$\kappa \colon TB \Rightarrow BT$| given by
3.1 Eilenberg–Moore trace semantics for |$TA$|-coalgebras
We now extend the above treatment of trace semantics of |$BT$|-coalgebras via Eilenberg–Moore categories, to cover coalgebras for a composite functor |$TA$| as well, where |$A$| is another endofunctor on the base category |$ {\textbf {C}} $|. This integrates the extension semantics of [22] in the present setting; the latter covers examples such as non-deterministic automata (as in Example 3.9) and probabilistic systems in generative form. The approach to trace semantics of |$TA$|-coalgebras in this section extends Assumption 3.1, making use of a lifting |$\overline {B}$| of a functor |$B$| to obtain traces as a suitable final coalgebra. Note that |$A$| itself is not lifted but is connected to |$B$| via a step |$\rho $| as stipulated in the global assumptions of this subsection, described next.
In addition to Assumption 3.1, we assume a functor |$A \colon {\textbf {C}} \rightarrow {\textbf {C}} $|, and a step |$\rho $| in
The counit |$\varepsilon \colon {\mathcal {F}} U \rightarrow U$| is given by |$\varepsilon _{(X,a)} = a$|; notice that |${\mathcal {F}} U (X,a) = (T(X), \mu _X)$|. Applying the forgetful functor to |$\varepsilon $| gives another step |$U \varepsilon \colon TU \Rightarrow U$|, where the ‘|$L$|’ (from (1)) in the codomain is the identity functor. We can compose the steps |$U\varepsilon $| and |$\rho $| in two ways. First, we get a step for |$AT$| by composing as follows:
We turn to the other composition of |$U\varepsilon $| and |$\rho $|, which gives a step for |$TA$|:
There is a one-to-one correspondence between
By Theorem 2.3, the natural transformation |$\rho = \rho _{1} : AU \Rightarrow U\overline {B}$| corresponds to |$\mathfrak {e} = \rho _{2} : {\mathcal {F}} A \Rightarrow \overline {B}{\mathcal {F}}$|; the latter is a natural transformation |$TA \Rightarrow BT$| whose components are maps of algebras |$\mu _{X} \rightarrow \overline {B}(\mu _{x})$|, as expressed by Diagram (9). This covers the first correspondence in the proposition.
By Theorem 2.3, a natural transformation |$\mathfrak {e} : TA \Rightarrow BT$| further corresponds to a natural transformation |$A \Rightarrow U\overline {B} {\mathcal {F}} = BU {\mathcal {F}} = BT$|. The latter is simply a natural transformation on the base category |$ {\textbf {C}} $|, which means no further coherence axioms like (9) need to be checked.
The composed step |$U\varepsilon \circledcirc \rho \colon TAU \Rightarrow U\overline {B}$| gives a corecursive algebra, by applying the step-induced algebra lifting |$G_{U\varepsilon \circledcirc \rho } \colon {\textrm {Alg}}(\overline {B}) \rightarrow {\textrm {Alg}}(TA)$| to the final |$\overline {B}$|-coalgebra |$((\varTheta , a), \zeta )$|, from Lemma 3.3. We call this corecursive algebra |$\ell _{\textrm {em}}^A \colon TA(\varTheta ) \rightarrow \varTheta $| to distinguish it from |$\ell _{\textrm {em}} \colon BT(\varTheta ) \rightarrow \varTheta $|. It is given by
We describe |$\ell _{\textrm {em}} \mathrel {\circ } U(\rho _2)$| as south-east and |$\ell _{\textrm {em}}^A$| as east-south in
We illustrate the situation with a simple example: non-deterministic automata, viewed as coalgebras of the form |$c \colon X \rightarrow {\mathcal {P}}_{\textrm {f}}(\varSigma \times X + 1)$|. To this end, we instantiate the setting with |$ {\textbf {C}} = {\textbf {Sets}} $|, |$T = {\mathcal {P}}_{\textrm {f}}$| the finite powerset monad and |$A(X) = \varSigma \times X + 1$|. Moreover, we let |$B(X) = 2 \times X^\varSigma $|. Note that there is a difference between |${\mathcal {P}}_{\textrm {f}} A$|-coalgebras and |$B {\mathcal {P}}_{\textrm {f}}$|-coalgebras, if |$\varSigma $| is infinite: the former are finitely branching non-deterministic automata (that is, finitely many successors) whereas the latter are image-finite non-deterministic automata (that is, finitely many successors for every alphabet letter).
4 Traces via logic
This section illustrates how the ‘logical’ approach to trace semantics of [29], ultimately based on the testing framework introduced in [40], fits in our general framework. In this approach, traces are viewed as 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 and continue by showing how these assumptions lead to a corecursive algebra giving trace semantics in the general framework of Section 2.
In this section, we assume
An adjunction |$F\dashv G$| between categories |$ {\textbf {C}} \leftrightarrows {\textbf {D}} ^{\textrm {op}}$|.
A functor |$T$| on |$ {\textbf {C}} $| with a step |$\tau \colon TG \Rightarrow G$|.
A functor |$B\colon {\textbf {C}} \rightarrow {\textbf {C}} $| and a functor |$L\colon {\textbf {D}} \rightarrow {\textbf {D}} $| with a step |$\delta \colon BG \Rightarrow GL$|.
An initial algebra
.
We deviate from the convention of writing |$\rho $| for ‘step’, since the above map |$\tau $| gives rise to multiple steps |$\tau \circledcirc \delta $| and |$\delta \circledcirc \tau $| in (11) below, in the sense of Definition 2.3; here we use ‘delta’ instead of ‘rho’ notation since it is common in modal logic.
We take |$ {\textbf {C}} = {\textbf {D}} = {\textbf {Sets}} $|, and |$F,G$| both the contravariant powerset functor |$2^{-}$|. Non-deterministic automata are obtained either as |$BT$|-coalgebras with |$B(X) = 2 \times X^A$| and |$T$| the finite powerset functor, or as |$TB$|-coalgebras, with |$B(X) = A \times X + 1$| and |$T$| again the finite powerset functor. In both cases, |$L$| is given by |$L(X) = A \times X + 1$|, which has the set of words |$A^*$| as carrier of an initial algebra. The map |$\tau \colon T2^- \Rightarrow 2^-$| is defined by |$\tau _X(S)(x) = \bigvee _{\varphi \in S} \varphi (x)$| and intuitively models the existential choice in the semantics of non-deterministic automata. The step |$\delta $| and the language semantics are defined later in this section.
In the remainder of this section, we show two classes of examples of the logical approach to trace semantics. With these descriptions, we retrieve most of the examples from [29] in a smooth manner.
We instantiate the assumptions in the beginning of this section by |$ {\textbf {C}} = {\textbf {D}} = {\textbf {Sets}} $|, |$F = G = \varOmega ^{-}$|, |$B(X) = \varOmega \times X^A$|, |$L(X) = A \times X + 1$| and |$T$| the functor from the statement. The initial |$L$|-algebra is 
. The map |$t$| extends to a modality |$\tau \colon TG \Rightarrow G$|, given on components by
We also describe a logic for polynomial functors constructed from a signature. Here, we model a signature by a functor |$\varSigma \colon \mathbb {N} \rightarrow {\textbf {Sets}} $|, where |$\mathbb {N}$| is the discrete category of natural numbers. This gives rise to a functor |$H_\varSigma \colon {\textbf {Sets}} \rightarrow {\textbf {Sets}} $| as usual by |$H_\varSigma (X) = \coprod _{n\in \mathbb {N}} \varSigma (n) \times X^n$|. The initial algebra of |$H_\varSigma $| consists of closed terms (or finite node-labelled trees) over the signature.
5 Traces via Kleisli
In this section, we briefly recall the ‘Kleisli approach’ to trace semantics [16] and cast it in our abstract framework. It applies to coalgebras for a composite functor |$TA$|, where |$T$| is a monad modelling the type of branching and |$A$| is a functor. For example, a coalgebra |$X \to \mathcal {P}(\varSigma \times X +S)$| has an associated map |$X \to \mathcal {P}(\varSigma ^{*} \times S)$| that sends a state |$x \in X$| to the set of its complete traces. (Taking |$S=1$|, this is the usual language semantics of a nondeterministic automaton.) To fit this to our framework, the monad |$T$| is |$\mathcal {P}$| and the functor |$A$| is |$(\varSigma \times -) + S$|. In general, the following assumptions are used.
In this section, we assume
An endofunctor |$A \colon {\textbf {C}} \rightarrow {\textbf {C}} $| with an initial algebra
.A monad |$(T,\eta ,\mu )$|, with the standard adjunction |$J \dashv U$| between categories |$ {\textbf {C}} \leftrightarrows {\mathcal {K}}{\kern -.4ex}\ell (T)$|, where |$J(X) = X$| and |$U(Y) = T(Y)$|.
- An extension |$\overline {A}$| of |$A$|, as below:
or, equivalently, a |${\mathcal {K}}{\kern -.4ex}\ell $|-law |$\lambda \colon AT \Rightarrow TA$|.(15)$$\ $$ |$(\varPsi , J(\beta ^{-1}))$| is a final |$\overline {A}$|-coalgebra.
In the case that |$A$| is the functor |$(\varSigma \times -) + S$|, its initial algebra is carried by |$\varSigma ^{*}\times S$|, and the canonical |${\mathcal {K}}{\kern -.4ex}\ell $|-law is given at |$X$| by
The above assumptions give rise to the following instance of our setting (1):
The above map |$\ell _{\textrm {kl}} \colon TAT(\varPsi ) \rightarrow T(\varPsi )$| is a map of Eilenberg–Moore algebras |$\mu _{AT(\varPsi )} \rightarrow \mu _{\varPsi }$|.
This follows by an easy calculation:
6 Partial traces for input/output
6.1 Introduction
To illustrate the versatility of our framework, we show next that it underpins a trace example quite different from the previous ones, one that arises in programming language semantics and involves both input and output actions [5].
To avoid confusion, it must be noted that the word ‘trace’ is used with a different meaning in the automata and semantics communities, as follows.
In the automata literature and the previous sections, a ‘trace’ ends in acceptance. Semanticists would call this a ‘complete trace’.
By contrast, in the semantics literature [5, 24, 32, 33, 36, 41] and this section, a ‘trace’ need not end in acceptance. For example, a program that prints Hello and then diverges (hangs) must be distinguished from one that simply diverges, even though—since neither terminates—neither has a complete trace. Accordingly, the string Hello is said to be a ‘trace’ of the former program (but not the latter), and so is each prefix. Automata theorists would call these ‘partial traces’.
This section applies our framework to traces of the second kind, but before doing that, we need two pieces of background. The first (Section 6.2) explains that, in a transition system for I/O, a state’s set of traces form a strategy. The second (Section 6.3) characterizes the poset of all strategies as a final coalgebra. This is a result that appeared in [5].
6.2 Trace sets as strategies
A strategy (more precisely, nondeterministic finite trace strategy) is a set |$\sigma $| of passive-ending plays such that |$sik \in \sigma $| implies |$s \in \sigma $|. Again, this terminology is based on the game idea, as a strategy tells proponent (nondeterminstically) how to play. The poset of all strategies, ordered by inclusion (|$\subseteq $|), is written |$\mathsf {Strat}$|.
6.3 Strategies form a final coalgebra
A complete semilattice is a poset with all suprema. Hence it also has all infima, which allows it to be called a ‘complete lattice’. Clearly, the poset |$\mathsf {Strat}$| of all strategies, ordered by inclusion (|$\subseteq $|), is a complete semilattice. Let |$\textbf {CSL}$| be the category of complete semilattices and homomorphisms, i.e. monotone functions that preserve suprema. It was shown in [5] that |$\mathsf {Strat}$| is a final coalgebra for a certain endofunctor on |$\textbf {CSL}$|, which we shall describe in several steps.
Firstly, an almost complete semilattice is a poset where every nonempty subset has a supremum. Hence, every lower-bounded subset has an infimum, but binary meets |$a \wedge b$| need not exist in general. Let |$\textbf {ACSL}$| be the category of almost complete semilattices and homomorphisms, i.e. monotone functions that preserve suprema of nonempty sets. Informally, our motivation for using this category is the fact that, up to trace equivalence, an I/O action such as printing commutes with binary nondeterminism, and more generally with |$I$|-ary nondeterministic choice for any nonempty set |$I$|. This point (and the special role of the empty set) is developed in more detail in [5].
For any set |$J$|, we define two functors:
For a family |$(A_j)_{j \in J}$| of complete semilattices, let |$\prod _{j \in J}A_j$| be the cartesian product. Endowed with pointwise order, it is an almost complete (in fact complete) semilattice.
For a family |$(f_{j} \colon A_{j} \to B_{j})_{j \in J}$| of complete semilattice homomorphisms, let |$\prod _{j \in J}f_j \colon \prod _{j \in J}A_j \to \prod _{j \in J} B_j$| be the map sending |$(a_j)_{j \in J}$| to |$(f_ja_j)_{j \in J}$|.
For a family |$(A_j)_{j \in J}$| of almost complete semilattices, let |$\bigoplus ^{\bot }_{j \in J}A_j$| be the set of pairs |$(U,(a_j)_{j \in U})$| where |$U \in {\mathcal {P}} J$| and |$a_j \in A_j$| for all |$j \in U$|. It is a complete semilattice when endowed with the following order: we have |$(U,(a_j)_{j \in U}) \leqslant (V,(b_j)_{j \in V})$| when |$U \subseteq V$| and |$a_j \leqslant b_j$| for all |$j \in U$|.
For a family |$(f_{j} \colon A_{j} \to B_{j})_{j \in J}$| of almost complete semilattice homomorphisms, let |$\bigoplus ^{\bot }_{j \in J}f_j \colon \bigoplus ^{\bot }_{j \in J}A_j \to \bigoplus ^{\bot }_{j \in J} B_j$| be the map sending a pair |$(U,(a_j)_{j \in U})$| to |$(U,(f_ja_j)_{j \in U})$|.
6.4 The step
With the background completed, we now want to instantiate our general setting to form an account of traces. Our adjunction and endofunctors are as follows:
Our step is formulated using bimodules and 2-cells, which are explained in the Appendix. Any functor |$U \colon {\textbf {D}} \to {\textbf {C}} $| gives rise to a bimodule |${U}^{\mathsf {Right}} \colon {\textbf {C}} \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textbf {D}} $| by Definition B.4(2), and then, for any set |$J$|, to a bimodule |$({U}^{\mathsf {Right}})^{J} \colon {\textbf {C}} ^{J} \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textbf {D}} ^{J}$| by Definition B.3. Central to our story are the following 2-cells (in the sense of Definition B.2(2)) defined for any set |$J$|.
Given a family of functions |$(f_j \colon X_j \to B_j)_{j \in J}$|, where |$X_j$| is a set and |$B_j$| a complete semilattice, the function |$\prod _{j \in J}f_j \colon \prod _{j \in J}X_j \to \prod _{j \in J} B_j$| sends |$(x_j)_{j \in J}$| to |$(fx_j)_{j \in J}$|.
- Given a family of functions |$(f_j \colon X_j \to A_j)_{j \in J}$|, where |$X_j$| is a set and |$A_j$| an almost complete semilattice, the function |$\sum ^{\sharp }_{j \in J} f_j \colon {\mathcal {P}} \sum _{j \in J} X_j \to \bigoplus ^{\bot }_{j \in J}A_j$| sends |$R$| to |$(L,(y_j)_{j \in L})$| where$$ \begin{eqnarray*} L & = & \{{j \in J \mid \exists x \in X_j.\,\mathsf{in}_j\,x \in R}\} \\ y_j & = & \bigvee_{x \in X_j \,:\, \mathsf{in}_j\,x \in R} f_j(x) \hspace{1em} \text{ for {$j \in L$}.} \end{eqnarray*}$$
From Theorem 6.1 with Proposition B.9(1), we see that, for every coalgebra |$c \colon X \to {\mathcal {P}}\sum _{k \in K} \prod _{i \in \mathsf {Ar}({k})}X$|, there is a unique morphism to |$(\mathsf {Strat},\varPsi )$|. Specifically, [5, Theorem 6.6] tells us that what this morphism sends |$x \in X$| to its set of traces. Finally, by Proposition B.9(2), |$U_{\rho }(\mathsf {Strat},\varPsi )$| is corecursive, and the map from |$(X,c)$| to it is the same, i.e. it sends |$x \in X$| to its set of traces.
Note that, as in Section 3, we can use |${\mathcal {P}}^{\rho }$| to determinize a transition system |$(X,c)$|. This is applied in [5, Section 6.2] to obtain a bisimulation method for trace equivalence.
6.5 Input, then output
A play is a finite or infinite sequence |$k_0,i_0,k_1,i_1,\ldots $|, where |$k_r \in K$| and |$i_r \in \mathsf {Ar}({k_r})$|. A play of odd length is active ending and one of even length is passive ending.
A strategy is a set |$\sigma $| of passive-ending plays such that |$\varepsilon \in \sigma $| (where |$\varepsilon $| is the empty play) and |$ski \in \sigma $| implies |$s \in \sigma $|.
- Let |$(X,c)$| be a transition system, and |$x \in X$| a state. A passive-ending play |$k_0,i_0,\ldots ,k_n,i_{n}$| is said to be a trace of |$x$| when there is a sequenceThe set of all such traces form a strategy.$$ \begin{align*} & x = x_0 \;\,\qquad x_0@k_0 \stackrel{i_0}{\Longrightarrow} x_1 \;, \qquad x_1@k_1 \stackrel{i_1}{\Longrightarrow} x_2 \;, \; \cdots \end{align*}$$
The poset |$\mathsf {Strat}$| of all strategies, ordered by inclusion |$(\subseteq )$|, forms an almost complete (in fact complete) semilattice. We adjust Theorem 6.1 to say that |$\mathsf {Strat}$| carries a final coalgebra for the endofunctor |$\prod _{k \in K} \bigoplus ^{\bot }_{i \in \mathsf {Ar}({k})}$| on |$\textbf {ACSL}$|.
Finally, we have the same results as in Section 6.4, but instead of (19) we use the following 2-cell:
7 Comparison
The presentation of trace semantics in terms of corecursive algebras allows us to compare the different approaches by constructing algebra morphisms between them. In three subsections, we compare the Eilenberg–Moore approach with the logical approach, the Kleisli approach with the logical approach, and finally we compare the Kleisli and Eilenberg–Moore approaches.
7.1 Eilenberg–Moore and logic
To compare the Eilenberg–Moore approach with the logical approach, we combine their assumptions, as follows.
In this subsection, we assume an adjunction |$F \dashv G$|, endofunctors |$B,L$| and a monad |$T$| as follows:
A final |$B$|-coalgebra
.An |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law |$\kappa \colon TB \Rightarrow BT$|, or equivalently, a lifting |$\overline {B}$| of |$B$|.
An initial algebra
.A step |$\delta \colon BG \Rightarrow GL$|.
A step |$\tau \colon TG \Rightarrow G$|, whose components are |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-algebras (a monad action).
Here we have assumed slightly more than the union of the assumptions of the two approaches. The step |$\tau $| is an assumption of the logical approach in Section 4, but there the compatibility with the monad structure was not assumed—simply because |$T$| was not assumed to be a monad before. Here, we use this assumption as a first compatibility requirement between the logical and Eilenberg–Moore approaches.
We note that |$\tau $| being a monad action is the same thing as |$\tau $| being an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law, involving the monad |$T$| on the left and the identity monad on the right. The next result is therefore an instance of Theorem 2.3.
The following are equivalent:
a monad action |$\tau _1 \colon TG \Rightarrow G$|;
a map |$\tau _2 \colon F \Rightarrow FT$|, satisfying the obvious dual action equations;
a monad morphism |$\tau _4 \colon T \Rightarrow GF$|;
an extension |$\widehat {F} \colon {\mathcal {K}}{\kern -.4ex}\ell (T) \rightarrow {\textbf {D}} ^{\textrm {op}} \;(\,= {\mathcal {K}}{\kern -.4ex}\ell (\textrm {Id}))$| of |$F$|.
a lifting |$\widehat {G} \colon {\textbf {D}} ^{\textrm {op}} \rightarrow {\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)$| of |$G$|.
The existence of such a |$\widehat {\delta }$| amounts to the property that each component |$\delta _X \colon BG(X) \rightarrow GL(X)$| is a |$T$|-algebra homomorphism from |$\overline {B}\widehat {G}(X)$| to |$\widehat {G}L(X)$|, i.e. the following diagram commutes:
If the equivalent conditions in Lemma 7.3 hold, then the map |$\mathsf {e}$| defined in (20) is a |$BT$|-algebra morphism from |$\ell _{\textrm {em}}$| to |$\ell ^{\textrm {log}}$|, as on the left below.
to |$F(\zeta ) \mathrel {\circ } \delta _{2} \colon LF(\varTheta ) \rightarrow F(\varTheta )$|. Hence, for the desired equality |$F(a) \mathrel {\circ } \overline {\mathsf {e}} = \tau _2 \mathrel {\circ } \overline {\mathsf {e}}$|, it suffices to prove that |$F(a)$| and |$\tau _2$| are both algebra homomorphisms from |$F(\zeta ) \mathrel {\circ } \delta _2$| to a common algebra, which in turn follows from commutativity of the following diagram. 
For the second part of the theorem, let |$c \colon X \rightarrow BT(X)$| be a coalgebra. Since |$\mathsf {e}$| is an algebra morphism, the equation |$\mathsf {e} \mathrel {\circ } \mathsf {em}_c = \mathsf {log}_c$| follows by uniqueness of coalgebra-to-algebra morphisms from |$c$| to |$\ell ^{\textrm {log}}$|.
The equality |$\mathsf {e} \mathrel {\circ } \mathsf {em}_c = \mathsf {log}_c$| means that equivalence w.r.t. Eilenberg–Moore trace semantics implies equivalence w.r.t. the logical trace semantics. The converse is, of course, true if |$\mathsf {e}$| is monic. For that, it is sufficient if |$\delta \colon 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 |$G_{\delta }(\varPhi , \alpha ^{-1})$| factors as a |$B$|-coalgebra homomorphism followed by a mono. This holds in particular if the components |$\delta _{A} \colon BG(A) \rightarrow GL(A)$| are all monic (in |$ {\textbf {C}} $|) [28].
If |$\delta \colon BG \Rightarrow GL$| is expressive, then |$\mathsf {e}$| is monic. Moreover, if |$\delta $| is an isomorphism, then |$\mathsf {e}$| is an iso as well.
Expressivity of |$\delta $| means that we have |$\mathsf {e} = m \mathrel {\circ } h$| for some coalgebra homomorphism |$h$| and mono |$m$|. By finality of |$\zeta $| there is a |$B$|-coalgebra morphism |$h^{\prime}$| such that |$h^{\prime} \mathrel {\circ } h = \textrm{id} $|. It follows that |$h$| is monic (in |$ {\textbf {C}} $|), so that |$m \mathrel {\circ } h = \mathsf {e}$| is monic too.
For the second claim, if |$\delta $| is an isomorphism, then |$G(\alpha ^{-1}) \mathrel {\circ } \delta \colon BG(\varPhi ) \rightarrow G(\varPhi )$| is an invertible corecursive |$B$|-algebra, which implies it is a final coalgebra (see [6, Proposition 7], which states the dual). It then follows from (20) that |$\mathsf {e}$| is a coalgebra morphism from one final |$B$|-coalgebra to another, which means it is an isomorphism.
Previously, we have seen both a class of examples of the Eilenberg–Moore approach (Theorem 3.4) and the logical approach (Proposition 4.3). Both arise from the same data: a monad |$T$| (just a functor in the logical approach) and an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-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 determinization procedure. The underlying distributive laws satisfy (21) by construction, so that the two approaches coincide (as already seen in the concrete examples).
Let |$\varOmega $| be a set, |$T \colon {\textbf {Sets}} \rightarrow {\textbf {Sets}} $| a monad and |$t \colon T(\varOmega ) \rightarrow \varOmega $| an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-algebra. The |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law |$\kappa $| of Theorem 3.4, together with |$\delta , \tau $| as defined in the proof of Proposition 4.3, satisfies (21). For any coalgebra |$c \colon X \rightarrow \varOmega \times T(X)^A$|, the map |$\mathsf {log}_c$| coincides (up to isomorphism) with the map |$\mathsf {em}_c$|.
Since (21) is satisfied, it follows from Theorem 7.4 that |$\mathsf {e} \mathrel {\circ } \mathsf {em}_c = \mathsf {log}_c$|. Since |$\delta $| is an iso, |$\mathsf {e}$| is an iso as well by Lemma 7.5.
7.2 Kleisli and logic
To compare the Kleisli approach to the logical approach, we combine their assumptions. Further, similar to the comparison between Eilenberg–Moore and logic in the previous section, we assume a first compatibility criterion by requiring the components |$\tau $| to be componentwise Eilenberg–Moore algebras.
In this subsection, we assume an adjunction |$F \dashv G$|, endofunctors |$A,L$| and a monad |$T$| as follows:
An initial algebra |$\beta \colon A(\varPsi ) \xrightarrow{\cong} \varPsi $|.
A |${\mathcal {K}}{\kern -.4ex}\ell $|-law |$\lambda \colon AT \Rightarrow TA$|, or equivalently, an extension |$\overline {A}\colon {\mathcal {K}}{\kern -.4ex}\ell (T) \rightarrow {\mathcal {K}}{\kern -.4ex}\ell (T)$| of |$A\colon {\textbf {C}} \rightarrow {\textbf {C}} $|.
|$(\varPsi ,J(\beta ^{-1}))$| is a final |$\overline {A}$|-coalgebra.
An initial algebra |$\alpha \colon L(\varPhi ) \xrightarrow{\cong} \varPhi $|.
A step |$\delta \colon AG \Rightarrow GL$|.
A step |$\tau \colon TG \Rightarrow G$|, whose components are |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-algebras (a monad action).
The condition |$\widehat {\delta } J = \delta $| simply means that |$\widehat {\delta }_X = \delta _X$| for every object |$X$| in |$ {\textbf {C}} $|. Naturality of |$\widehat {\delta }$| amounts to commutativity of the outside of the diagram below, for every map |$f \colon X \rightarrow T(Y)$|.
If the equivalent conditions in Lemma 7.8 hold, then the map |$\overline {\mathsf {k}} = \tau _\varPhi \mathrel {\circ } T(\mathsf {k}) \colon T(\varPsi ) \rightarrow G(\varPhi )$| is a |$TA$|-algebra morphism from |$\ell _{\textrm {kl}}$| to |$\ell _{\textrm {log}}$|, as on the left below.
Consider the following diagram.
For the second part of the theorem, since |$\overline {\mathsf {k}}$| is an algebra morphism, we have that |$\overline {\mathsf {k}} \circ \mathsf {kl}_c$| is a coalgebra-to-algebra morphism from |$c$| to the corecursive algebra |$\ell _{\textrm {log}}$|. Hence, |$\overline {\mathsf {k}} \circ \mathsf {kl}_c = \mathsf {log}_c$| by uniqueness of such morphisms.
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 7.5, we currently do not have a converse. The condition that |$\delta $| has monic components is, surprisingly, not sufficient for |$\overline {\mathsf {k}}$| to be monic, as confirmed by Example 7.10 below. In the comparison between Eilenberg–Moore and Kleisli traces in Section 7.3, a similar difficulty arises.
We give an example where |$\delta \colon AG \Rightarrow GL$| is monic and (24) commutes, but where nevertheless logical equivalence does not imply Kleisli trace equivalence. Let |$ {\textbf {C}} = {\textbf {D}} = {\textbf {Sets}} $|, |$F = G = 2^{-}$|, |$A = L = (-) + 1$|, |$T = {\mathcal {P}}_{\textrm {f}}$|, |$\tau \colon {\mathcal {P}}_{\textrm {f}} 2^{-} \Rightarrow 2^{-}$| given by union as before, and define the step |$\delta $|, for |$\varphi \in 2^X$|, by |$\delta _X(\varphi )(t) = \top $| iff |$t \in X \wedge \varphi (t)$|, and |$\delta _X(\ast )(t) = \top $| (the latter differs from the step in Proposition 4.5). Notice that |$\delta $| indeed has monic components. (In the conference version [21], we used a more general setting with |$A = L = (\varSigma \times -) + 1$|, where |$\varSigma $| is a fixed set. However, the associated |$\delta $| is not monic if |$\varSigma $| contains more than one element, contrary to what is stated there. Indeed, we need to choose |$\varSigma $| to be a singleton for the example to go through.)
Let |$\lambda \colon AT \Rightarrow TA$| be the distributive law from [16], given by |$\lambda _X(S) = \{x \mid x \in S\}$| for |$S \in {\mathcal {P}}_{\textrm {f}}(X)$|, and |$\lambda (\ast ) = \{\ast \}$|. Then (24) is satisfied:
Cîrstea [9] compares logical traces to a ‘path-based semantics’, which resembles the Kleisli approach (as well as [31]) but does not require a final |$\overline {A}$|-coalgebra. In particular, given a commutative monad |$T$| on |$ {\textbf {Sets}} $| and a signature |$\varSigma $|, she considers a canonical distributive law |$\lambda \colon H_\varSigma T \Rightarrow T H_\varSigma $|, which coincides with the one in [16]. Cîrstea shows that, with |$\varOmega = T(1)$|, |$t = \mu _1 \colon TT(1) \rightarrow T(1)$| and |$\delta $| from the proof of Proposition 4.5 (assuming |$T1$| to have enough structure to define that logic), the triangle (24) commutes (see [9, Lemma 5.12]).
7.3 Kleisli and Eilenberg–Moore
To compare the Eilenberg–Moore and Kleisli approaches, we first combine their assumptions. The Kleisli approach applies to |$TA$|-coalgebras; to match this, we make use of the variant of the Eilenberg–Moore approach for |$TA$|-coalgebras presented in Section 3.1. The latter approach uses a lifting of a functor |$B$| as well as a step relating |$A$| and |$B$|.
In this subsection, we assume to endofunctors |$A,B$| and a monad |$T$|, on a base category |$ {\textbf {C}} $|, and liftings |$\overline {A}, \overline {B}$| to Kleisli and Eilenberg–Moore-categories as follows:
An initial algebra |$\beta \colon A(\varPsi ) \xrightarrow{\cong}\varPsi $|.
A |${\mathcal {K}}{\kern -.4ex}\ell $|-law |$\lambda \colon AT \Rightarrow TA$|, or equivalently, an extension |$\overline {A}\colon {\mathcal {K}}{\kern -.4ex}\ell (T) \rightarrow {\mathcal {K}}{\kern -.4ex}\ell (T)$| of the functor |$A$|.
|$(\varPsi ,J(\beta ^{-1}))$| is a final |$\overline {A}$|-coalgebra.
An |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law |$\kappa \colon TB \Rightarrow BT$|, or equivalently, a lifting |$\overline {B} \colon {\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T) \rightarrow {\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)$|.
A final coalgebra |$\zeta \colon \varTheta \xrightarrow{\cong} B(\varTheta )$|.
A step |$\rho \colon AU \Rightarrow U\overline {B}$|.
The step |$\rho \colon AU \Rightarrow U\overline {B}$| is an assumption of the Eilenberg–Moore approach for |$TA$|-coalgebras in Section 3.1, defined on top of the assumptions for the Eilenberg–Moore approach for |$BT$|-coalgebras. Under a further assumption such a law corresponds to an extension natural transformation as in [22], see Proposition 7.12.
Taking the adjoint transpose, w.r.t. the Eilenberg–Moore adjunction |${\mathcal {F}} \dashv U$|, of this map |$\mathsf {k} \colon \varPsi \rightarrow \varTheta = U(\varTheta , a)$|, yields a map of Eilenberg–Moore algebras:
In the above setting, the following three statements are equivalent.
- The distributive law |$\lambda \colon AT \Rightarrow TA$| commutes with the two composed steps |$\rho \circledcirc U(\varepsilon )$| and |$U(\varepsilon ) \circledcirc \rho $|, as in
(27)$$\ $$ There is a natural transformation |$\mathfrak {e} \colon \widehat {{\mathcal {F}}} \overline {A} \Rightarrow \overline {B} \widehat {{\mathcal {F}}}$| satisfying |$\mathfrak {e} J = \rho _2$| in
The functor |$\widehat {{\mathcal {F}}} \colon {\mathcal {K}}{\kern -.4ex}\ell (T) \rightarrow {\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)$| is the extension corresponding to |$U(\varepsilon )$|, according to Theorem 2.3; it is often called the ‘comparison’ functor and then written as |$K$|.
The equivalence of points (1) and (2) is an instance of Lemma 7.8, where it should be noted that we are instantiating |$ {\textbf {D}} $| with |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}(T)^{\textrm {op}}$|, which causes the two natural transformations in the above diagram to be in opposite direction.
We show the equivalence of (1) and (3). Using Lemma 2.7, it is straightforward to check, via Theorem 2.3, that |$\big (\rho \circledcirc U(\varepsilon )\big )_{2} = \big (\rho _1 \mathrel {\circ } AU\varepsilon \big )_2 = \overline {B} \varepsilon \mathrel {\circ } \rho _2$| and |$U\varepsilon \mathrel {\circ } T\rho _1 \mathrel {\circ } \lambda = \rho _2 \mathrel {\circ } \varepsilon \mathrel {\circ } {\mathcal {F}}(\lambda )$|. As a consequence, commutativity of Diagram (27) is equivalent to commutativity of the following diagram:
Under the above equivalent conditions, we obtain the desired algebra morphism.
If the equivalent conditions in Proposition 7.12 hold, then the map |$\overline {\mathsf {k}}\colon T(\varPsi ) \rightarrow \varTheta $| obtained from (26), is a |$TA$|-algebra morphism between corecursive algebras |$\ell _{\textrm {kl}}$| and |$\ell _{\textrm {em}}^A = \ell _{\textrm {em}} \mathrel {\circ } U(\rho _2)$|, as on the left below.
Just like in the comparison between Kleisli and logic, the above result gives a sufficient condition for the Eilenberg–Moore trace semantics to factor through the Kleisli trace semantics. However, again we do not know of a reasonable condition to ensure that the map |$\overline {\mathsf {k}}$| is monic. Such a result is important for the comparison: it would ensure that two states are equivalent w.r.t. Kleisli traces iff they are equivalent w.r.t. Eilenberg–Moore traces (right now, we only have the implication from left to right). In [22], such a condition is also missing; monicity of |$\overline {\mathsf {k}}$| is only shown to hold in several concrete examples.
In [22, Section 6], the Kleisli approach to coalgebraic trace semantics is compared with the Eilenberg–Moore approach, making use of an ‘extension’ natural transformation |$\mathfrak {e}$| satisfying two requirements, namely,
8 Completely iterative algebras
Milius [37] introduced a notion of ‘complete iterativity’ of algebras that is stronger than corecursiveness and has the advantage of being preserved by various constructions. So, whenever we encounter a corecursive algebra, it is natural to ask whether it is in fact completely iterative. This section shows that all our corecursive algebras are completely iterative (Theorem 8.3), and that this yields trace maps in more general settings.
Let |$ {\textbf {C}} $| have binary coproducts. For an endofunctor |$H$| on |$ {\textbf {C}} $|, an |$H$|-algebra |$a \colon HA \to A$| is completely iterative when |$[\textrm{id} ,a]$| is a corecursive |$A + H$|-coalgebra. Explicitly: when for every |$c \colon X \to A+ HX$| there is a unique |$f \colon X \to A$| such that the following diagram commutes.
The following gives two useful ways of constructing such algebras.
If |$\zeta \colon A \to HA$| is a final |$H$|-coalgebra, then |$(A,\zeta ^{-1})$| is completely iterative.
Given a step as in Section 2, the functor |$G_{\rho }$| preserves complete iterativity.
Given a step as in Section 2 and a final coalgebra |$\zeta \colon A \to HA$|, the algebra |$G_{\rho }(A,\zeta ^{-1})$| is completely iterative.
if |$L$| has a final coalgebra |$(\varPsi ,\zeta )$|, then |$G_{\rho }(A,\zeta ^{-1})$| is completely iterative.
Each of our examples is similar to this one: the completely iterative algebra yields trace semantics for a generalized transition system in which the semantics may sometimes be given directly.
9 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 [27], 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 [29, 42]. 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 Kleisli/logic and Kleisli/Eilenberg–Moore comparisons (Section 7) are similar, but the Eilenberg–Moore/logic comparison seems different. So far we have been unable to derive a general perspective on such comparisons that covers all three.
A further direction of research is provided by the recent [10], where graded monads are used to define trace semantics in a general way, together with associated expressive logics. On the one hand it would be interesting to try and capture this within our steps-and-adjunctions framework; but this would require to capture graded semantics via some notion of finality or corecursiveness, which we are not currently aware of. On the other hand, as pointed out by one of the reviewers, the comparison results of Section 7 can be viewed as expressivity results of one semantics w.r.t. the other—this insight is interesting on its own, and might help in devising a more general method for making comparisons as in Section 7, also discussed above. Further, the expressiveness criteria in [10] may be useful to address the issues in the comparison of Kleisli semantics to Eilenberg–Moore and logical trace semantics. We leave these considerations for future work.
Funding
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.
Acknowledgements
We are grateful to the anonymous referees of both the conference version and this extended paper for various comments and suggestions.
Footnotes
This is a revised and extended version of a paper which appeared in the proceedings of CMCS 2018 [21].
Many-sorted signatures, in the guise of ‘interaction structures’, are used for a similar purpose in [14].
References
A Details for Section 2
We recall a (standard) lemma that relates a step |$\rho _1$| to its mate |$\rho _2$|.
For any step |$\rho \colon HG \Rightarrow GL$|, the following diagrams commute.
The above lemma is useful in the proofs of Theorem 2.3 and Lemma 2.7, presented next.
The correspondence between |$\rho _1, \rho _2, \rho _3$| and |$\rho _4$| follows from Theorem 2.2. For the second part of the statement, suppose |$H$| and |$L$| have monad structures |$(H,\eta ^H,\mu ^H)$| and |$(L,\eta ^L,\mu ^L)$|, respectively. The fact that |$\rho _1$| is an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law iff |$\rho _4$| is a monad map can be reconstructed from [44].
We show that if |$\rho _1$| is an |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-law then |$\rho _2$| is a Kleisli law—the converse follows analogously. To this end, for the compatibility of |$\rho _2$| with |$\mu $|, consider the following diagram.
Finally, the correspondence between |${\mathcal {E}}{\kern -.4ex}{\mathcal {M}}$|-laws and liftings was shown in [25] and the variant for Kleisli laws in [39].
First, note that |$\big (\theta \circledcirc \rho \big )_2 = \varepsilon MLF \mathrel {\circ } F\theta _1 LF \mathrel {\circ } FK\rho _1 F \mathrel {\circ } FKH\eta $|. It thus suffices to prove that the following diagram commutes.
B Steps and bimodules
For the example of partial traces for I/O given in Section 6, it is convenient to take a different view of our step-and-adjunction setting, using the following notion.
A family of sets |$( {\textbf {O}} (X,Y))_{X \in {\textbf {C}}, Y \in {\textbf {D}}}$|, where |$g \in {\textbf {O}} (X,Y)$| is called an |$ {\textbf {O}} $|-morphism |$g \colon X \to Y$|.
Each |$g \colon X \to Y$| can be composed with a |$ {\textbf {C}} $|-map |$f \colon X^{\prime} \to X$| or |$ {\textbf {D}} $|-map |$h \colon Y \to Y^{\prime}$|.
A map of bimodules
sends each |$ {\textbf {O}} $|-morphism |$g \colon X \to Y$| to an |$ {\textbf {O}} ^{\prime}$|-morphism |$R g \colon X \to Y$| with the following commuting:
More generally, a 2-cell
sends each |$ {\textbf {O}} $|-morphism |$g \colon X \to Y$| to an |$ {\textbf {O}} ^{\prime}$|-morphism |$R g \colon HX \to LY$| with the following commuting:
Let |$( {\textbf {O}} _j \colon {\textbf {C}} _j \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textbf {D}} _j)_{j \in J}$| be a family of bimodules. Then the bimodule |$\prod _{j \in J} {\textbf {O}} _j \colon \prod _{j \in J} {\textbf {C}} _j \to \hspace {-0.65em} \shortmid \hspace {0.5em} \prod _{j \in J} {\textbf {D}} _j$| is defined by saying that a morphism |$(X_j)_{j \in J} \to (Y_{j})_{j \in J}$| is a family |$(g_j \colon X_j \to Y_j)_{j \in J}$|, where |$g_j$| is an |$ {\textbf {O}} _j$|-morphism for all |$j \in J$| . Composition is defined componentwise.
Here are two ways of constructing a bimodule |$ {\textbf {C}} \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textbf {D}} $|.
A functor |$F \colon {\textbf {C}} \to {\textbf {D}} $| gives |${F}^{\mathsf {Left}} \colon {\textbf {C}} \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textbf {D}} $|, where |${F}^{\mathsf {Left}}(X,Y) \stackrel{\scriptsize{\rm def}}{=} {\textbf {D}} (FX,Y)$|.
A functor |$G \colon {\textbf {D}} \to {\textbf {C}} $| gives |${G}^{\mathsf {Right}} \colon {\textbf {C}} \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textbf {D}} $|, where |${G}^{\mathsf {Right}}(X,Y) \stackrel {\scriptsize{\rm def}}{=} {\textbf {C}} (X,GY)$|.
For a bimodule |$ {\textbf {O}} \colon {\textbf {C}} \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textbf {D}} $|,
a left representation consists of a functor |$F \colon {\textbf {C}} \to {\textbf {D}} $| and an isomorphism |$m: {\textbf {O}} \cong {F}^{\mathsf {Left}}$|
a right representation consists of a functor |$G \colon {\textbf {C}} \to {\textbf {D}} $| and an isomorphism |$n: {\textbf {O}} \cong {G}^{\mathsf {Right}}$|.
The natural transformations in Theorem 2.2 correspond to 2-cells of bimodules, as follows.
Suppose we have left representations |$m\colon {\textbf {O}} \cong {F}^{\mathsf {Left}}$| and |$m^{\prime}\colon {\textbf {O}} ^{\prime} \cong {F^{\prime}}^{\mathsf {Left}}$|. Then a 2-cell
Now we give a more refined account of steps. Suppose we have a bimodule, two endofunctors and a 2-cell:
A coalgebra morphism from an |$H$|-coalgebra |$c\colon X \rightarrow H(X)$| to an |$L$|-coalgebra |$d \colon \varTheta \rightarrow L(\varTheta )$| is an |$ {\textbf {O}} $|-morphism |$g \colon X \to \varTheta $| such that the following commutes:
This gives a bimodule |$ {\textrm {CoAlg}}(H) \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textrm {CoAlg}}(L)$|.
A coalgebra-to-algebra morphism from an |$H$|-coalgebra |$c\colon X \rightarrow H(X)$| to an |$L$|-algebra |$a \colon L(\varTheta ) \Rightarrow \varTheta $| is an |$ {\textbf {O}} $|-morphism |$g \colon X \to \varTheta $| such that the following commutes:
Equivalently: such a morphism is a fixpoint for the endofunction on the homset |$ {\textbf {C}} (X,\varTheta )$| sending |$f$| to the composite |$ X {\stackrel{c}\longrightarrow} H(X) \stackrel{R(f)}{\longrightarrow} L\ {(\theta)} \stackrel{a}{\longrightarrow} {\theta} $|. This gives a bimodule |$ {\textrm {CoAlg}}(H) \to \hspace {-0.65em} \shortmid \hspace {0.5em} {\textrm {Alg}}(L)$|.
A final coalgebra |$d \colon \varTheta \Rightarrow L(\varTheta )$| is said to extend across |$ {\textbf {O}} $| when from each |$H$|-coalgebra |$c \colon X \to H(X)$| there is a unique morphism to |$(\varTheta ,d)$|.
A corecursive algebra |$a \colon L(\varTheta ) \Rightarrow \varTheta $| is said to extend across |$ {\textbf {O}} $| when from each |$H$|-coalgebra |$c \colon X \to H(X)$| there is a unique morphism to |$(\varTheta ,a)$|.
Now let us decompose Proposition 2.5 into two parts.
Let |$ {\textbf {O}} $| have a left representation |$m\colon {\textbf {O}} \cong {F}^{\mathsf {Left}}$|. Then any corecursive |$L$|-algebra |$(\varTheta ,a)$| extends across |$ {\textbf {O}} $|. (And hence also any final |$L$|-algebra.) Explicitly, the map |$(X,c) \to (\varTheta ,a)$| is |$m^{-1}$| applied to the map |$F^{\rho }(X,c) \to (\varTheta ,a)$|.
Let |$ {\textbf {O}} $| have a right representation |$n \colon {\textbf {O}} \cong {G}^{\mathsf {Right}}$|. Then any corecursive |$L$|-algebra |$(\varTheta ,a)$| extending across |$ {\textbf {O}} $| is sent by |$G_{\rho }$| to a corecursive |$H$|-algebra. Explicitly, the map |$(X,c) \to G_{\rho } (\varTheta ,a)$| is |$n$| applied to the map |$(X,c) \to (\varTheta ,a)$|.
Note that this story also appears, in contravariant form, in [35, Propositions 16–17].
