Distributive laws for monotone specifications
 225 Downloads
Abstract
Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that monotone specifications—that disallow negative premises—do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation.
1 Introduction
Structural operational semantics (SOS) is an expressive and popular framework for defining the operational semantics of programming languages and calculi. There is a wide variety of specification formats that syntactically restrict the full power of SOS, but guarantee certain desirable properties to hold [1]. A famous example is the socalled GSOS format [5]. Any GSOS specification induces a unique interpretation which is compositional with respect to (strong) bisimilarity.
In their seminal paper [30], Turi and Plotkin introduced an elegant mathematical approach to structural operational semantics, where the type of syntax is modeled by an endofunctor \(\varSigma \) and the type of behaviour is modeled by an endofunctor B. Operational semantics is then given by a distributive law of \(\varSigma \) over B. In this context, models are bialgebras, which consist of a \(\varSigma \)algebra and a Bcoalgebra over a common carrier. One major advantage of this framework over traditional approaches is that it is parametric in the type of behaviour. Indeed, by instantiating the theory to a particular functor B, one can obtain well behaved specification formats for probabilistic and stochastic systems, weighted transition systems, streams, and many more [4, 16, 17].
Both GSOS and coGSOS specifications induce distributive laws, and as a consequence they induce unique supported models on which behavioural equivalence is a congruence. The two formats are incomparable in terms of expressive power: GSOS specifications allow rules that involve complex terms in the conclusion, whereas coGSOS allows arbitrary lookahead in the arguments. It is straightforward to combine GSOS and coGSOS as a natural transformation of the form \(\varSigma B^\infty \Rightarrow B\varSigma ^*\), called a biGSOS specification, generalising both formats. However, such specifications are, in some sense, too expressive: they do not induce unique supported models, as already observed in [30]. For example, the rules (2) and (3) above (which are GSOS and coGSOS respectively) can be combined into a single biGSOS specification. Suppose this combined specification has a model. By the axiom for c, there is a transition \(c \xrightarrow {a} \sigma (c)\) in this model. However, is there a transition \(\sigma (c) \xrightarrow {a} \sigma (c)\)? If there is not, then by the rule for \(\sigma \), there is; but if there is such a transition, then it is not derivable, so it is not in the model! Thus, a supported model does not exist. In fact, it was recently shown that, for biGSOS, it is undecidable whether a (unique) supported model exists [19].
The use of negative premises in the above example (and in [19]) is crucial. In the present paper, we introduce the notion of monotonicity of biGSOS specifications, generalising monotone abstract GSOS [9]. In the case that B is a functor representing labelled transition systems, this corresponds to the absence of negative premises, but the format does allow lookahead in premises as well as complex terms in conclusions. Monotonicity requires an order on the functor B—technically, our definition of monotonicity is based on the similarity order [12] induced on the final coalgebra.
We show that if there is a pointed DCPO structure on the functor B, then any monotone biGSOS specification yields a least model as its operational interpretation. Indeed, monotone specifications do not necessarily have a unique model, but it is the least model which makes sense operationally, since this corresponds to the natural notion that every transition has a finite proof. Our main result is that if the functor B has a DCPO structure, then every monotone specification yields a canonical distributive law of the free monad for \(\varSigma \) over the cofree comonad for B. Its unique model coincides with the least supported model of the specification. As a consequence, behavioural equivalence on this model is a congruence.
However, the conditions of these results are a bit too restrictive: they rule out labelled transition systems, the main example. The problem is that the functors typically used to model transition systems either fail to have a cofree comonad (the powerset functor) or to have a DCPO structure (the finite or countable powerset functor). In the final section, we mitigate this problem using the theory of (countably) presentable categories and accessible functors. This allows us to relax the requirement of DCPO structure only to countable sets, given that the functor B is countably accessible (this is weaker than being finitary, a standard condition in the theory of coalgebras) and the syntax consists only of countably many operations each with finite arity. In particular, this applies to labelled transition systems (with countable branching) and certain kinds of weighted transition systems.
Related work The current paper is an extended version of a conference paper presented at EXPRESS/SOS 2017 [24]. The main new material is proofs of all results, most of which were missing in the conference version; more backgroud material, in particular on biGSOS rule formats; a result showing that the constructed distributive law extends a given biGSOS specification in the sense of [18].
The idea of studying distributive laws of monads over comonads that are not induced by GSOS or coGSOS specifications has been around for some time (e.g., [4]), but, according to a recent overview paper [17], general bialgebraic formats (other than GSOS or coGSOS) which induce such distributive laws have not been proposed so far. In fact, it is shown by Klin and Nachyła that the general problem of extending biGSOS specifications to distributive laws is undecidable [18, 19]. The current paper shows that one does obtain distributive laws from biGSOS specifications when monotonicity is assumed (negative premises are disallowed). A fundamentally different approach to positive formats with lookahead, not based on the framework of bialgebraic semantics but on labelled transition systems modeled very generally in a topos, was introduced in [29]. It is deeply rooted in labelled transition systems, and hence seems incomparable to our approach based on generic coalgebras for ordered functors. An abstract study of distributive laws of monads over comonads and possible morphisms between them is in [22], but it does not include characterisations in terms of simpler natural transformations.
Structure of the paper Section 2 contains preliminaries on (co)algebras, and Sect. 3 recalls (abstract) rule formats based on various kinds of distributive laws. In Sect. 4 the notion of similarity on coalgebras is recalled, which is then used in Sect. 5 to define monotone specifications and prove the existence of least supported models. Section 6 contains our main result: canonical distributive laws for monotone biGSOS specifications. In Sect. 7, this result is extended to countably accessible functors.
2 Preliminaries
We recall the necessary definitions on order theory, algebras, coalgebras, and distributive laws of monads over comonads. For an introduction to coalgebra see [14, 27]. All of the definitions and results below and most of the examples can be found in [17], which provides an overview of bialgebraic semantics. Unless mentioned otherwise, all functors considered are endofunctors on the category \(\mathsf {Set}\) of sets and functions.
Notation By \(\mathcal {P}\) we denote the (covariant) power set functor; \(\mathcal {P}_c\) is the countable power set functor and \(\mathcal {P}_f\) the finite power set functor. Given a relation \(R \subseteq X \times Y\), we write \(\pi _1 :R \rightarrow X\) and \(\pi _2 :R \rightarrow Y\) for its left and right projection, respectively. Given another relation \(S \subseteq Y \times Z\) we denote the composition of R and S by \(R \circ S\). We let \(R^\mathsf {op}= \{(y,x) \mid (x,y) \in R\}\). For a set X, we let \(\varDelta _X = \{(x,x) \mid x \in X\}\). The graph of a function \(f:X \rightarrow Y\) is \(\mathsf {Graph}(f) = \{(x,f(x)) \mid x \in X\}\). The image of a set \(S \subseteq X\) under f is denoted simply by \(f(S) = \{f(x) \mid x \in S\}\), and the inverse image of \(V \subseteq Y\) by \(f^{1}(V) = \{x \mid f(x) \in V\}\). The pairing of two functions f, g with a common domain is denoted by \(\langle f, g \rangle \) and the copairing (for functions f, g with a common codomain) by [f, g]. The set of functions from X to Y is denoted by \(Y^X\). Any relation \(R \subseteq Y \times Y\) can be lifted pointwise to a relation on \(Y^X\); in the sequel we will simply denote such a pointwise extension by the relation itself, i.e., for functions \(f, g :X \rightarrow Y\) we have \(f \, R \, g\) iff \(f(x) \, R \, g(x)\) for all \(x \in X\), or, equivalently, \((f \times g)(\varDelta _X) \subseteq R\). Composition of functors F, G (of the appropriate type) is denoted by \(F \circ G\) or simply by FG, and composition of natural transformations \(\alpha , \beta \) by \(\alpha \circ \beta \), given by \((\alpha \circ \beta )_X = \alpha _X \circ \beta _X\).
DCPOs We recall the basic ordertheoretic structures that we will use in fixed point constructions; see, e.g., [7] for details. Let \((P,\le )\) be a poset. Given a subset \(S \subseteq P\) we denote the least upper bound of S by \(\bigvee S\), if it exists. A subset \(S \subseteq P\) is called directed if S is nonempty, and every finite subset of S has an upper bound in S. A directed complete partial order (DCPO) is a poset in which every directed subset has a least upper bound (these are sometimes referred to as CPOs, but we prefer DCPO as it emphasises the directedness aspect). Further, a DCPO is called pointed if it has a least element \(\bot \). In this paper, every DCPO is assumed to be pointed, and thus will sometimes refer to a pointed DCPO simply as a DCPO. A map \(f :P \rightarrow Q\) between pointed DCPOs is called strict if \(f(\bot ) = \bot \), and continuous if, for every directed set \(S \subseteq P\), f(S) is again directed, and \(f(\bigvee S) = \bigvee f(S)\). We denote by \(\mathsf {DCPO}_\bot \) the category of pointed DCPOs and strict continuous maps.
2.1 Algebras and monads
An algebra for a functor \(\varSigma :\mathsf {Set}\rightarrow \mathsf {Set}\) consists of a set X and a function \(f :\varSigma X \rightarrow X\). An (algebra) homomorphism from \(f :\varSigma X \rightarrow X\) to \(g :\varSigma Y \rightarrow Y\) is a function \(h :X \rightarrow Y\) such that \(h \circ f = g \circ \varSigma h\). The category of algebras and their homomorphisms is denoted by \(\mathsf {alg}(\varSigma )\).
A monad is a triple \(\mathcal {T} = (T, \eta , \mu )\) where \(T :\mathsf {Set}\rightarrow \mathsf {Set}\) is a functor and \(\eta :\mathsf {Id}\Rightarrow T\) and \(\mu :TT \Rightarrow T\) are natural transformations such that \(\mu \circ T \eta = \mathsf {id}= \mu \circ \eta T\) and \(\mu \circ \mu T = \mu \circ T \mu \). An (EilenbergMoore, or EM)algebra for \(\mathcal {T}\) is a Talgebra \(f :TX \rightarrow X\) such that \(f \circ \eta _X = \mathsf {id}\) and \(f \circ \mu _X = f \circ Tf\). We denote the category of EMalgebras by \(\mathsf {Alg}(\mathcal {T})\).
2.2 Coalgebras and comonads
A coalgebra for the functor B consists of a set X and a function \(f :X \rightarrow BX\). A (coalgebra) homomorphism from \(f :X \rightarrow BX\) to \(g :Y \rightarrow BY\) is a function \(h :X \rightarrow Y\) such that \(Bh \circ f = g \circ h\). The category of Bcoalgebras and their homomorphisms is denoted by \(\mathsf {coalg}(B)\). The associated forgetful functor is denoted by \(U :\mathsf {coalg}(B) \rightarrow \mathsf {Set}\). An Fcoalgebra (Z, z) is called final if it is a final object in \(\mathsf {coalg}(B)\), i.e., if there exists a unique homomorphism from every Fcoalgebra into (Z, z).
A comonad is a triple \(\mathcal {D} = (D, \epsilon , \delta )\) consisting of a functor \(D :\mathsf {Set}\rightarrow \mathsf {Set}\) and natural transformations \(\epsilon :D \Rightarrow \mathsf {Id}\) and \(\delta :D \Rightarrow DD\) satisfying axioms dual to the monad axioms. The category of EilenbergMoore coalgebras for \(\mathcal {D}\), defined dually to EMalgebras, is denoted by \(\mathsf {CoAlg}(\mathcal {D})\).
Example 2.1
Consider the \(\mathsf {Set}\) functor \(BX = A \times X\) for a fixed set A. Coalgebras for B are called stream systems. There exists a final Bcoalgebra, whose carrier can be presented as the set \(A^\omega \) of all streams over A, i.e., \(A^\omega = \{\sigma \mid \sigma :\omega \rightarrow A \}\) where \(\omega \) is the set of natural numbers. For a set X, \(B^\infty X = (A \times X)^\omega \). Given \(f :X \rightarrow A \times X\), its coinductive extension \(f^\infty :X \rightarrow B^\infty X\) maps a state \(x \in X\) to its infinite unfolding. The final coalgebra of \(GX = A \times X + 1\) consists of finite and infinite streams over A, that is, elements of \(A^* \cup A^\omega \). For a set X, \(G^\infty X = (A \times X)^\omega \cup (A \times X)^* \times X\).
Example 2.2

if \(x \xrightarrow {a} x'\) then \(h(x) \xrightarrow {a} h(x')\), and

if \(h(x) \xrightarrow {a} y'\) then there is \(x'\) such that \(x \xrightarrow {a} x'\) and \(h(x') = y'\).
Example 2.3
A complete monoid is a (necessarily commutative) monoid M together with an infinitary sum operation consistent with the finite sum [8]. Define the functor \(\mathcal {M}:\mathsf {Set}\rightarrow \mathsf {Set}\) by \(\mathcal {M}(X) = \{\varphi \mid \varphi :X \rightarrow M\}\) and, for \(f :X \rightarrow Y\), \(\mathcal {M}(h)(\varphi ) = \lambda y. \sum _{x \in f^{1}(y)} \varphi (x)\). A weighted transition system over a set of labels A is a coalgebra \(f :X \rightarrow (\mathcal {M}X)^A\). Similar to the case of labelled transition systems, we obtain weighted transition systems whose branching is countable for each label as coalgebras for the functor \((\mathcal {M}_c )^A\), where \(\mathcal {M}_c\) is defined by \(\mathcal {M}_c(X) = \{\varphi :X \rightarrow M \mid \varphi (x) \ne 0 \text { for countably many }x \in X\}\). We note that this only requires a countable sum on M to be welldefined and, by further restricting to finite support, weighted transition systems are defined for any commutative monoid (see, e.g., [16]).
Labelled transition systems are retrieved by taking the monoid with two elements and logical disjunction as sum. Another example arises by taking the monoid \(M = \mathbb {R}^+ \cup \{\infty \}\) of nonnegative reals extended with a top element \(\infty \), with the supremum operation.
2.3 Distributive laws
In Sect. 3, we will use distributive laws as a common generalisation of several abstract rule formats. For now, we only recall a few basic definitions and properties.

\(\overline{T}\) is a lifting of T;

\(U\overline{\eta } = \eta U\) and \(U \overline{\mu }= \mu U\).
The map h is a coalgebra for the comonad D. If D is the cofree comonad \(B^\infty \) of a functor B, then h corresponds to a Bcoalgebra; we refer to the latter as the operational model of \(\lambda \).
3 Abstract rule formats: GSOS, coGSOS and biGSOS
In this section we recall the abstract rule formats originally introduced in [30], and their combination, called biGSOS in [18].
3.1 GSOS
Example 3.1
A stream GSOS specification is a collection of stream GSOS rules over a common signature such that, for every operator \(\sigma \) (of arity n) and every sequence \((a_1, \ldots , a_n) \in \mathbb {R}^n\), there is exactly one rule with premises \(x_1 \xrightarrow {a_1} x_1'\), ..., \(x_n \xrightarrow {a_n} x_n'\).
Example 3.2
A GSOS specification is a collection of rules satisfying an imagefiniteness condition. As first observed in [30], and proved in detail in [4], specifications in the GSOS format are generalised by abstract GSOS specifications, where \(\varSigma \) models the signature and \(BX = (\mathcal {P}_fX)^A\).
The uniqueness of the supported model follows from the theory of distributive laws, using that every abstract GSOS specification \(\rho \) induces a distributive law \(\lambda :\varSigma ^* B^\infty \Rightarrow B^\infty \varSigma ^*\) of the free monad over the cofree comonad [17, 20].
It also follows from this correspondence that behavioural equivalence on the supported model of \(\rho \) is a congruence.
3.2 coGSOS
Example 3.3
In case of streams (i.e., \(BX = \mathbb {R}\times X\)), coGSOS specifications can be presented concretely as a rule format which allows lookahead in premises, but where the term t, the righthand side of the conclusion, can only be a single operation, or a variable.
The notion of (supported) model of a coGSOS specification is defined similarly (dually) to that of a GSOS specification; we will see a more definition that generalises both in the context of the biGSOS format, introduced next. Just like the GSOS case, coGSOS specifications have unique supported models, on which behavioural equivalence is a congruence [17].
3.3 biGSOS
The abstract GSOS and coGSOS formats have a straightforward common generalisation, called biGSOS in [18]. This notion, as well as the associated notion of model which we define later, subsumes both abstract GSOS and coGSOS.
Definition 3.4
Example 3.5
For streams (i.e., \(BX = \mathbb {R}\times X\)), a concrete presentation of the biGSOS format is very similar to the (coGSOS) format given in Example 3.3; however, the term t on the righthand side of the conclusion of a rule is now allowed to be an arbitrary term over the variables introduced in the premises, rather than just a single operator or variable.
Example 3.6
As stated in [30], every ntree specification (a collection of ntree rules with a certain imagefiniteness condition) induces a biGSOS specification where \(\varSigma \) models the signature and \(BX = (\mathcal {P}_fX)^A\). Safe ntree rules induce coGSOS specifications. The construction of a biGSOS specification \(\rho \) from an ntree specification is sketched in [30]. Here, we fill in some of the details. Note that it is not known whether there is a converse, i.e., whether every biGSOS specification is derived from an ntree specification [17].
 1.
\(h(x_i) = b_i\), and
 2.
if \(x \xrightarrow {a} x'\) (in the rooted tree induced by the premises) then \(h(x) \xrightarrow {a} h(x')\), and
 3.
if \(x /\!\!\!\!\!\xrightarrow {a}\) (an explicit negative premise in the rule) then \(h(x) /\!\!\!\!\!\xrightarrow {a}\) (no atransition from h(x)).
Contrary to the case of GSOS and coGSOS, in general there is no (unique) supported model. This is witnessed, for instance, by the example specification in the introduction. In Example 3.7, we shall see that biGSOS specifications may also have multiple supported models, and that behavioural equivalence is not even a congruence, in general.
Example 3.7
In fact, one can easily construct a model in which the behaviour of \(\sigma (\tau (c))\) is different from that of \(\sigma (\tau (d))\)—for example, a model where \(\sigma (\tau (c))\) does not make any transitions, whereas \(\sigma (\tau (d)) \xrightarrow {a} t\) for some t. Then behavioural equivalence is not a congruence; c is bisimilar to d, but \(\sigma (\tau (c))\) is not bisimilar to \(\sigma (\tau (d))\).
The above example features a specification that has many different interpretations as a supported model, on the set of closed terms. We are interested in the least model, since that only features finite proofs. It is sensible to speak about the least model of this specification, since it does not contain any negative premises. More generally, absence of negative premises can be defined based on an ordered functor and the induced similarity order, as we will see in the next sections.
The current paper takes a different approach, by disallowing negative premises—which are crucial in the proof of Klin and Nachyła. Further, we will construct a canonical distributive law that extends a given biGSOS specification (satisfying a monotonicity condition generalising absence of negative premises), but we make no claims about uniqueness.
4 Similarity on cofree coalgebras
In this section, we recall the notion of simulation of coalgebras from [12], and prove a few basic results concerning the similarity preorder on final coalgebras. This similarity preorder will be used in Sect. 5 to formulate what it means for a biGSOS specification to be monotone.
Lemma 4.1
 1.
\(\mathsf {Rel}(F)(\varDelta _X) = \varDelta _{FX}\).
 2.
For any \(R' \subseteq X \times X'\): if \(R \subseteq R'\) then \(\mathsf {Rel}(F)(R) \subseteq \mathsf {Rel}(F)(R')\).
 3.
For any \(f :X \rightarrow Y\), \(g :X' \rightarrow Y'\): \((F f \times F g) (\mathsf {Rel}(F)(R)) \subseteq \mathsf {Rel}(F)((f \times g)(R))\).
 4.
\(\mathsf {Rel}(F)(R)^\mathsf {op}= \mathsf {Rel}(F)(R^\mathsf {op})\).
 5.
If F preserves weak pullbacks, then for any \(f :X \rightarrow Y\): \(\mathsf {Rel}(F)(\mathsf {Graph}(f)) = \mathsf {Graph}(Ff)\) .
 6.
For any \(f :X \rightarrow Y\), \(g :X' \rightarrow Y'\): if \(f \mathrel {S} g\) then \(F(f) \mathrel {\mathsf {Rel}(F)(S)} F(g)\),
Proof
The first five properties are standard (see, e.g., [13]). For (6), by assumption we have \((f \times g)(\varDelta _X) \subseteq {S}\). By (2) this implies \(\mathsf {Rel}(F)((f \times g)(\varDelta _X)) \subseteq \mathsf {Rel}(F)(S)\). Further, by (1) and (3), we have \((F f \times F g)(\varDelta _{F X}) = (F f \times F g)(\mathsf {Rel}(F)(\varDelta _X)) \subseteq \mathsf {Rel}(F)((f \times g)(\varDelta _X))\). Thus \((F f \times F g)(\varDelta _{F X}) \subseteq \mathsf {Rel}(F)(S)\) as desired. \(\square \)

For any set X, there is a preorder \({\sqsubseteq _{BX}} \subseteq BX \times BX\);

For any map \(f :X \rightarrow Y\), Bf is monotone, i.e., \(b \sqsubseteq _{BX} c\) implies \(Bf(b) \sqsubseteq _{BY} Bf(c)\).
Lemma 4.2
Proof
Example 4.3

\(\epsilon _X(p) = \epsilon _X(q)\), and

if \(p \xrightarrow {a} p'\) then there is \(q'\) such that \(q \xrightarrow {a} q'\) and \((p',q') \in R\).
Example 4.4
For any \(G :\mathsf {Set}\rightarrow \mathsf {Set}\), the functor \(B = G + 1\), where \(1 = \{\bot \}\), can be ordered as follows: \(x \le y\) iff \(x = \bot \) or \(x=y\), for all \(x,y \in BX\). If \(G = A \times \mathsf {Id}\) then \(B^\infty X\) consists of finite and infinite sequences of the form \(x_0 \xrightarrow {a_0} x_1 \xrightarrow {a_1} x_2 \xrightarrow {a_2} \ldots \) with \(x_i \in X\) and \(a_i \in A\) for each i (cf. Example 2.1). For \(\sigma ,\tau \in B^\infty X\) we have \(\sigma \lesssim _{B^\infty X} \tau \) if \(\tau \) does not terminate before \(\sigma \) does, and \(\sigma \) and \(\tau \) agree on labels in X and A on each position where \(\sigma \) is defined.
In the remainder of this section we state a few technical properties concerning similarity on cofree comonads, which will be necessary in the following sections.
Lemma 4.5
Coalgebra homomorphisms h, k preserve similarity: if \(x \lesssim y\) then \(h(x) \lesssim k(y)\).
Proof
Let \(h :X \rightarrow X'\) be a coalgebra homomorphism from (X, f) to \((X',f')\), and \(k :Y \rightarrow Y'\) a coalgebra homomorphism from (Y, g) to \((Y',g')\). In [12], it is shown that \(x \lesssim y\) iff \(h(x) \lesssim k(y)\) under the assumption of a stable order (meaning that \(\mathsf {Rel}_{\sqsubseteq }(B)\) is a fibred functor); but this is not necessary for the implication from left to right. In fact, the desired implication follows from the abstract theory of bifibrations, see, e.g., [23, Proposition 3.3.7].

\((h \times k) (f \times g)^{1} \subseteq (f' \times g')^{1} (Bh \times Bk)\) (pointwise inclusion). This is a straightforward computation: let \(S \subseteq BX \times BY\), and suppose \((f(x), g(y)) \in S\); we need to prove that \((h(x),h(y)) \in (f' \times g')^{1} (Bh \times Bk)(S)\). Indeed, we have \(((Bh)(f(x)),(Bk)(g(y))) \in (Bh \times Bk)(S)\), so we have \((f'(h(x)), k'(g(y))) \in (Bh \times Bk)(S)\) (since h and k are homomorphisms), as desired.

\((Bh \times Bk) (\mathsf {Rel}_{\sqsubseteq }(B)(R)) \subseteq \mathsf {Rel}_{\sqsubseteq }(B)((h \times k)(R))\) is shown concretely in [12, Lemma 4.2].
Pointwise inequality of coalgebras implies pointwise similarity of coinductive extensions:
Lemma 4.6
Let \((B, \sqsubseteq )\) be an ordered functor, and let f and g be Bcoalgebras on a common carrier X. If \(f \mathrel {\sqsubseteq _{BX}} g\) then \(f^\infty \mathrel {\lesssim _{B^\infty X}} g^\infty \).
Proof
Suppose \(f \mathrel {\sqsubseteq _{BX}} g\). This is equivalent to \((f \times g)(\varDelta _X) \subseteq {\sqsubseteq _{BX}}\). Since \(\sqsubseteq _{BX}\) is reflexive, we have \(\sqsubseteq _{BX} \subseteq {(\sqsubseteq _{BX} \circ \varDelta _{BX} \circ \sqsubseteq _{BX})}\). Further \(\varDelta _{BX} = \mathsf {Rel}(B)(\varDelta _X)\) by Lemma 4.1 (1), so that \(\sqsubseteq _{BX} \subseteq {(\sqsubseteq _{BX} \circ \mathsf {Rel}(B)(\varDelta _X) \circ \sqsubseteq _{BX})} = \mathsf {Rel}_{\sqsubseteq }(B)(\varDelta _X)\). Combined with the assumption, this yields \((f \times g)(\varDelta _X) \subseteq \mathsf {Rel}_{\sqsubseteq }(B)(\varDelta _X)\), so \(\varDelta _X\) is a simulation between f and g. By Lemma 4.2 this implies that \(x \lesssim x\) for any \(x \in X\), where \(\lesssim \) is the similarity order between \((X, \langle f, \mathsf {id}\rangle )\) and \((X, \langle g, \mathsf {id}\rangle )\) induced by \((B \times X, {\widetilde{\sqsubseteq }})\). Notice that \(f^\infty \) and \(g^\infty \) are coalgebra homomorphisms from \(\langle f, \mathsf {id}\rangle \) and \(\langle g, \mathsf {id}\rangle \) respectively into the cofree coalgebra \((B^\infty X, \langle \theta , \epsilon \rangle )\), so by Lemma 4.5 we have \((f^\infty \times g^\infty )(\varDelta _X) \subseteq {\lesssim _{B^\infty X}}\). \(\square \)
Recall from Sect. 2 that any Bhomomorphism yields a \(B^\infty \)homomorphism between coinductive extensions. A similar fact holds for inequalities.
Lemma 4.7
 1.
If \(Bh \circ f \sqsubseteq _{BY} g \circ h\) then \(B^\infty h \circ f^\infty \lesssim _{B^\infty Y} g^\infty \circ h\).
 2.
If \(Bh \circ f \sqsupseteq _{BY} g \circ h\) then \(B^\infty h \circ f^\infty \gtrsim _{B^\infty Y} g^\infty \circ h\).
Proof
The assumption in item 1. is equivalent to: \((f(x),g(h(x)) \in (\mathsf {Graph}(Bh) \circ {\sqsubseteq _{BY}})\) for all \(x \in X\). Thus \((f(x), g(h(x)) \in ({\sqsubseteq _{BX}} \circ \mathsf {Graph}(Bh) \circ {\sqsubseteq _{BY}})\) since \(\sqsubseteq _{BX}\) is reflexive. We have \(\mathsf {Graph}(Bh) = \mathsf {Rel}(B)(\mathsf {Graph}(h))\) by Lemma 4.1 (5) and the assumption that B preserves weak pullbacks, so by the above, \(\mathsf {Graph}(h)\) is a simulation between f and g. By Lemma 4.2 it follows that \(x \lesssim h(x)\), where \(\lesssim \) is the similarity order between \(\langle f, h \rangle :X \rightarrow BX \times Y\) and \(\langle g, \mathsf {id}\rangle :Y \rightarrow BY \times Y\) induced by \((B \times Y, {\widetilde{\sqsubseteq }})\).
5 Monotone biGSOS specifications
Definition 5.1
A biGSOS specification \(\rho :\varSigma B^\infty \Rightarrow B \varSigma ^*\) is monotone if the restriction of \(\rho _X \times \rho _X\) to \(\mathsf {Rel}(\varSigma )(\lesssim _{B^\infty X})\) corestricts to \(\sqsubseteq _{B\varSigma ^*X}\), for any set X.
Example 5.2
In the case of an ntree specification for labelled transition systems, if there are no negative premises then the induced biGSOS specification (Example 3.6) is monotone.
To see this, suppose that for all i, we have \(x_i \models _h b_i\) (notation of Example 3.6), and \(b_i \lesssim _{B^\infty X} c_i\). By definition of \(\lesssim _{B^\infty X}\) (cf. Example 4.3) and \(\models _h\), and the absence of negative premises, it follows that there is a map \(k :V \rightarrow B^\infty X\) from the set of variables occuring in the premises of the rules (notation of Example 3.6), such that \(\epsilon _X \circ k = \epsilon _X \circ h\) (i.e., they agree on node labels), and for all i: \(x_i \models _k c_i\). It follows that \(\rho _X(\sigma (b_1, \ldots , b_n)) \sqsubseteq _{B \varSigma ^* X} \rho _X(\sigma (c_1, \ldots , c_n))\), as needed.
Notice that the example specification in the introduction consisting of rules (2) and (3), which does not have a model, is not monotone. This is no coincidence: every monotone biGSOS specification has a model, if \(B\varSigma ^*\emptyset \) is a pointed DCPO, as we will see next. In fact, the proper canonical choice is the least model, corresponding to behaviour obtained in finitely many proof steps.
5.1 Models of monotone specifications
Let \(\rho \) be a monotone biGSOS specification. Suppose \(B\varSigma ^*\emptyset \) is a pointed DCPO. Then the set of coalgebras \(\mathsf {coalg}(B)_{\varSigma ^*\emptyset } = \{f \mid f :\varSigma ^*\emptyset \rightarrow B\varSigma ^*\emptyset \}\), ordered pointwise, is a pointed DCPO as well.
Lemma 5.3
The function \(\varphi \) is monotone.
Proof
Corollary 5.4
If \(B\varSigma ^*\emptyset \) is a pointed DCPO and \(\rho \) is a monotone biGSOS specification, then \(\rho \) has a least supported model.
The condition of the Corollary is satisfied if B is of the form \(B = G + 1\) (c.f. Example 4.4), that is, \(B = G + 1\) for some functor G (where the element in the singleton 1 is interpreted as the least element of the pointed DCPO). Consider, as an example, the functor \(BX = A \times X + 1\) of finite and infinite streams over A. Any specification that does not mention termination (i.e., a specification for the functor \(GX = A \times X\)) yields a monotone specification for B.
Example 5.5
The case of labelled transition systems is a bit more subtle. The problem is that \((\mathcal {P}_f\varSigma ^* \emptyset )^A\) and \((\mathcal {P}_c\varSigma ^* \emptyset )^A\) are not DCPOs, in general, whereas the functor \((\mathcal {P})^A\) does not have a cofree comonad. However, if the set of closed terms \(\varSigma ^* \emptyset \) is countable, then \((\mathcal {P}_c\varSigma ^* \emptyset )^A\) is a pointed DCPO, and thus Corollary 5.4 applies. The specification in Example 3.7 can be viewed as a specification for the functor \((\mathcal {P}_c)^A\), and it has a countable set of terms. Therefore it has, by the Corollary, a least supported model. In this model, the behaviour of \(\sigma (t)\) is empty, for any \(t \in \varSigma ^* \emptyset \).
6 Distributive laws for biGSOS specifications
In the previous section we have seen how to construct a least supported model of a monotone biGSOS specification, as the least fixed point of a certain monotone function. In the present section we show that, given a monotone biGSOS specification, the construction of a least model generalises to a lifting of the free monad \(\varSigma ^*\) to the category of Bcoalgebras. It then immediately follows that there exists a canonical distributive law of the monad \(\varSigma ^*\) over the comonad \(B^\infty \), and that the (unique) operational model of this distributive law corresponds to the least supported model as constructed above.
In order to proceed we define a \(\mathsf {DCPO}_\bot \)ordered functor as an ordered functor (Sect. 4) where \(\mathsf {PreOrd}\) is replaced by \(\mathsf {DCPO}_\bot \). Below we assume that \((B, \sqsubseteq )\) is \(\mathsf {DCPO}_\bot \)ordered, and \(\varSigma \) and B are as before (having a free monad and cofree comonad respectively). Throughout this section we assume a monotone biGSOS specification \(\rho :\varSigma B^\infty \Rightarrow B\varSigma ^*\).
Example 6.1
A general class of functors that are \(\mathsf {DCPO}_\bot \)ordered are those of the form \(B + 1\), where the singleton 1 is interpreted as the least element and all other distinct elements are incomparable (see Example 4.4). Another example is the functor \((\mathcal {P})^A\) of labelled transition systems with arbitrary branching, but this example can not be treated here because there exists no cofree comonad for it. The case of labelled transition systems is treated in Sect. 7.
Lemma 6.2
For any \(c :X \rightarrow BX\), the function \(\varphi _c\) is monotone.
For the lifting of \(\varSigma ^*\), we need to show that the above construction preserves coalgebra morphisms.
Theorem 6.3
Proof
Let (X, c) and (Y, d) be \(B\varSigma ^*\)coalgebras. We need to prove that, if \(h :X \rightarrow Y\) is a coalgebra homomorphism from c to d, then \(\varSigma ^*h\) is a homomorphism from \(\overline{c}\) to \(\overline{d}\).
The proof is by transfinite induction on the iterative construction of \(\overline{c}\) and \(\overline{d}\) as limits of the ordinalindexed initial chains of \(\varphi _c\) and \(\varphi _d\) respectively. For the limit (and base) case, given a (possibly empty) directed family of coalgebras \(f_i :\varSigma ^* X \rightarrow B\varSigma ^*X\) and another directed family \(g_i :\varSigma ^* Y \rightarrow B\varSigma ^*Y\), such that \(B \varSigma ^* h \circ f_i = g_i \circ \varSigma ^* h\) for all i, we have \(B\varSigma ^* h \circ \bigvee _i f_i = \bigvee _i (B\varSigma ^* h \circ f_i) = \bigvee _i (g_i \circ \varSigma ^* h) = (\bigvee _i g_i) \circ \varSigma ^* h\) by continuity of \(B\varSigma ^* h\) and assumption.
We show that the (free) monad\((\varSigma ^*,\eta ,\mu )\) lifts to \(\mathsf {coalg}(B)\). This is the heart of the matter. The main proof obligation is to show that \(\mu _X\) is a coalgebra homomorphism from \(\overline{\varSigma ^*}(\overline{\varSigma ^*}(X,c))\) to \(\overline{\varSigma ^*}(X,c)\), for any Bcoalgebra (X, c).
Theorem 6.4
If B preserves weak pullbacks, then the functor \(\overline{\varSigma ^*}\) extends to a monad \((\overline{\varSigma ^*},\eta ,\mu )\) on \(\mathsf {coalg}(B)\), which is a lifting of the free monad \((\varSigma ^*,\eta ,\mu )\).
Proof
For the other inequality, i.e., \(B\mu _X \circ \overline{\overline{c}} \sqsupseteq _{B\varSigma ^*X} \overline{c} \circ \mu _X\), one proves again by transfinite induction that \(B\mu _X \circ \overline{\overline{c}} \sqsupseteq _{B\varSigma ^*X} f \circ \mu _X\) for any \(f :\varSigma ^*X \rightarrow B\varSigma ^*X\) in the chain approximating \(\overline{c}\). The limit case is straightforward. For the successor step, assume \(B\mu _X \circ \overline{\overline{c}} \sqsupseteq _{B\varSigma ^*X} f \circ \mu _X\); we must prove that \(B\mu _X \circ \overline{\overline{c}} \sqsupseteq _{B\varSigma ^*X} \varphi _c(f) \circ \mu _X\).
The lifting gives rise to a distributive law of monad over comonad.
Theorem 6.5
Let \(\rho :\varSigma B^\infty \Rightarrow B \varSigma ^*\) be a monotone biGSOS specification, where B is \(\mathsf {DCPO}_\bot \)ordered and preserves weak pullbacks. There exists a distributive law \(\lambda :\varSigma ^* B^\infty \Rightarrow B^\infty \varSigma ^*\) of the free monad \(\varSigma ^*\) over the cofree comonad \(B^\infty \) such that the operational model of \(\lambda \) is the least supported model of \(\rho \).
Proof
By Theorem 6.4, we obtain a lifting of \((\varSigma ^*,\eta ,\mu )\) to \(\mathsf {coalg}(B)\). As explained in Sect. 2.3, such a lifting corresponds uniquely to a distributive law of the desired type. The operational model of \(\lambda \) can be obtained by applying the lifting to the unique coalgebra \(! :\emptyset \rightarrow B\emptyset \). But that coincides, by definition of the lifting, with the least supported model as defined in Sect. 5. \(\square \)
It follows from the general theory of bialgebras that the unique coalgebra morphism from the least supported model to the final coalgebra is an algebra homomorphism, i.e., behavioural equivalence on the least supported model of a monotone biGSOS specification is a congruence.
At the end of Sect. 3, we recalled that in general it is undecidable whether a given biGSOS specification extends uniquely to a distributive law. Above, we have shown how to construct a distributive law for a monotone biGSOS specification, in terms of a lifting. We next show that the constructed distributive law indeed extends the original biGSOS specification.
Theorem 6.6
The distributive law \(\lambda \) constructed in Theorem 6.5 extends the original monotone biGSOS specification \(\rho \).
Proof
Labelled transition systems The results above do not apply to labelled transition systems. The problem is that the cofree comonad for the functor \((\mathcal {P})^A\) does not exist. A first attempt would be to restrict to the finitely branching transition systems, i.e., coalgebras for the functor \((\mathcal {P}_f)^A\). But this functor is not \(\mathsf {DCPO}_\bot \)ordered, and indeed, contrary to the case of GSOS and coGSOS, even with a finite biGSOS specification one can easily generate a least model with infinite branching, so that a lifting as in the previous section can not exist.
Example 6.7
The model in the above example has countable branching. One might ask whether it can be adapted to generate uncountable branching, i.e., that we can construct a biGSOS specification for the functor \((\mathcal {P}_c)^A\), such that the model of this specification would feature uncountable branching. However, as it turns out, this is not the case, at least if we assume \(\varSigma \) to be a polynomial functor (a countable coproduct of finite products, modelling a signature with countably many operations each of finite arity), and the set of labels A to be countable. This is shown more generally in the next section.
7 Liftings for countably accessible functors
In the previous section, we have seen that one of the most important instances—the case of labelled transition systems—does not meet the necessary assumptions for our construction of a distributive law, because of size issues: the functors in question either do not have a cofree comonad, or are not DCPOordered. In the current section, we solve this problem by showing that, if both functors \(B, \varSigma \) are reasonably wellbehaved, then it suffices to have a DCPOordering of B only on countable sets. The general approach is to first construct a lifting of the free monad to the category of coalgebras with a countable carrier, and subsequently extend it to a lifting to the category of all coalgebras.
Example 7.1
The functor \((\mathcal {P}_c)^A\) coincides with the \(\mathsf {DCPO}_\bot \)ordered functor \((\mathcal {P})^A\) when restricted to countable sets, hence it satisfies the above assumption. Notice that \((\mathcal {P}_c)^A\) is not \(\mathsf {DCPO}_\bot \)ordered. The functor \((\mathcal {P}_f)^A\) does not satisfy the above assumption.
The functor \((\mathcal {M})^A\), for the complete monoid \(\mathbb {R}^+ \cup \{\infty \}\) (Example 2.3), is ordered as a complete lattice [25], so also \(\mathsf {DCPO}_\bot \)ordered. Similar to the above, the functor \((\mathcal {M}_c )^A\) is \(\mathsf {DCPO}_\bot \)ordered when restricted to countable sets, i.e., satisfies the above assumption.
We define \(\mathsf {coalg}_c(B)\) to be the full subcategory of Bcoalgebras whose carrier is a countable set, with inclusion \(\overline{I} :\mathsf {coalg}_c(B) \rightarrow \mathsf {coalg}(B)\). The associated forgetful functor is denoted by \(U :\mathsf {coalg}_c(B) \rightarrow \mathsf {cSet}\).
The pointed DCPO structure on each BX, for X countable, suffices to carry out the fixed point constructions from the previous sections for coalgebras over countable sets, if we assume that \(\varSigma ^*\) preserves countable sets. Notice that the (partial) order on the functor B is still necessary to define the simulation order on \(B^\infty X\), and hence speak about monotonicity of biGSOS specifications. The proof of the following theorem is essentially the same as in the previous section.
Theorem 7.2
Suppose \(\varSigma ^*\) preserves countable sets, and B is an ordered functor which preserves weak pullbacks and whose restriction to \(\mathsf {cSet}\) is \(\mathsf {DCPO}_\bot \)ordered. Let \((\varSigma ^*_c,\eta ^c,\mu ^c)\) be the restriction of \((\varSigma ^*,\eta ,\mu )\) to \(\mathsf {cSet}\). Any monotone biGSOS specification \(\rho :\varSigma B^\infty \Rightarrow B\varSigma ^*\) gives rise to a lifting \((\overline{\varSigma ^*}_c, \overline{\eta }^c, \overline{\mu }^c)\) of the monad \((\varSigma ^*_c,\eta ^c,\mu ^c)\) to \(\mathsf {coalg}_c(B)\).
The main result of this section is that, under certain additional conditions on B and \(\varSigma ^*\), the above lifting extends to a lifting of the monad \(\varSigma ^*\) from \(\mathsf {Set}\) to \(\mathsf {coalg}(B)\), and hence a distributive law of the monad \(\varSigma ^*\) over the cofree comonad \(B^\infty \) (Theorem 7.5). It relies on the fact that, under certain conditions, we can present every coalgebra as a (filtered) colimit of coalgebras over countable sets.
We use the theory of locally (countably, i.e., \(\omega _1\)) presentable categories and (countably) accessible categories. For now, we only recall a concrete characterisation of when a functor on \(\mathsf {Set}\) is countably accessible, since this will be assumed both for B and \(\varSigma ^*\) later on. For details, see [3] and the appendix; the latter also contains the proofs of the results below.
On \(\mathsf {Set}\), a functor \(B :\mathsf {Set}\rightarrow \mathsf {Set}\) is countably accessible if for every set X and element \(x \in BX\), there is an injective function \(i :Y \rightarrow X\) from a finite set Y and an element \(y \in BY\) such that \(Bi(y) = x\). Intuitively, such functors are determined by how they operate on countable sets.
Example 7.3
Any finitary functor is countably accessible. Further, the functors \((\mathcal {P}_c)^A\) and \((\mathcal {M}_c )^A\) (c.f. Example 7.1) are countably accessible if A is countable.
A functor is called strongly countably accessible if it is countably accessible and additionally preserves countable sets, i.e., it restricts to a functor \(\mathsf {cSet}\rightarrow \mathsf {cSet}\). We will assume this for our “syntax” functor \(\varSigma ^*\). If \(\varSigma \) correponds to a signature with countably many operations each of finite arity (so is a countable coproduct of finite products) then \(\varSigma ^*\) is strongly countably accessible.
The central idea of obtaining a lifting to \(\mathsf {coalg}(B)\) from a lifting to \(\mathsf {coalg}_c(B)\) is to extend the monad on \(\mathsf {coalg}_c(B)\) along the inclusion \(\overline{I} :\mathsf {coalg}_c(B) \rightarrow \mathsf {coalg}(B)\). Concretely, a functor \(T :\mathsf {Set}\rightarrow \mathsf {Set}\) extends \(T_c :\mathsf {cSet}\rightarrow \mathsf {cSet}\) if there is a natural isomorphism \(\alpha :IT_c {\mathop {\Rightarrow }\limits ^{\cong }} TI\). A monad \((T,\eta ,\mu )\) on \(\mathsf {Set}\) extends a monad \((T_c, \eta _c, \mu _c)\) on \(\mathsf {cSet}\) if \(T_c\) extends T with some isomorphism \(\alpha \) such that \(\alpha \circ I\eta _c = \eta I\) and \(\alpha \circ I \mu _c= \mu I \circ T\alpha \circ \alpha T_c\). This notion of extension is generalised naturally to arbitrary locally countably presentable categories. Monads on the subcategory of countably presentable objects^{1} can always be extended (Lemma B.2).
Since B is countably accessible, \(\mathsf {coalg}(B)\) is locally countably presentable and \(\mathsf {coalg}_c(B)\) is the associated category of countably presentable objects [2]. This means every Bcoalgebra can be presented as a filtered colimit of Bcoalgebras with countable carriers. The above lemma applies, so we can extend the monad on \(\mathsf {coalg}_c(B)\) of Theorem 7.2 to a monad on \(\mathsf {coalg}(B)\), resulting in Theorem 7.5 below. The latter relies on Theorem 7.4, which ensures that, doing so, we will get a lifting of the monad on \(\mathsf {Set}\) that we started with.
In the remainder of this section, we will consider a slightly relaxed version of functor liftings, up to isomorphism, similar to extensions defined before. This is harmless—those still correspond to distributive laws—but since the monad on \(\mathsf {coalg}(B)\) is constructed only up to isomorphism, it is more natural to work with in this setting. We say \((\overline{T}, \overline{\eta }, \overline{\mu })\) lifts \((T,\eta ,\mu )\) (up to isomorphism) if there is a natural isomorphism \(\alpha :U\overline{T} \Rightarrow TU\) such that \(\alpha \circ U\overline{\eta } = \eta U\) and \(\alpha \circ U \overline{\mu }= \mu U \circ T\alpha \circ \alpha \overline{T}\).
Theorem 7.4
 1.
\((T_c,\eta ^c,\mu ^c)\) extends to \((T,\eta ,\mu )\) along \(I :\mathsf {cSet}\rightarrow \mathsf {Set}\),
 2.
\((\overline{T}_c, \overline{\eta }^c, \overline{\mu }^c)\) extends to \((\overline{T}, \overline{\eta }, \overline{\mu })\) along \(\overline{I} :\mathsf {coalg}_c(B) \rightarrow \mathsf {coalg}(B)\),
 3.
\((\overline{T}, \overline{\eta }, \overline{\mu })\) is a lifting (up to isomorphism) of \((T,\eta ,\mu )\).
Theorem 7.5
Let \(\rho :\varSigma B^\infty \Rightarrow B \varSigma ^*\) be a monotone biGSOS specification, where B is an ordered functor whose restriction to countable sets is \(\mathsf {DCPO}_\bot \)ordered, B is countably accessible, B preserves weak pullbacks, and \(\varSigma ^*\) is strongly countably accessible. There exists a distributive law \(\lambda :\varSigma ^* B^\infty \Rightarrow B^\infty \varSigma ^*\) of the free monad \(\varSigma ^*\) over the cofree comonad \(B^\infty \) such that the operational model of \(\lambda \) is the least supported model of \(\rho \).
As explained in Examples 7.1 and 7.3, if B is either \((\mathcal {P}_c )^A\) or \((\mathcal {M}_c )^A\) (weighted in the nonnegative real numbers) with A countable, then it satisfies the above hypotheses (that \(\mathcal {M}_c\) preserves weak pullbacks follows essentially from [10]). So the above theorem applies to labelled transition systems and weighted transition systems (of the above type) over a countable set of labels, as long as the syntax is composed of countably many operations each with finite arity. Hence, behavioural equivalence on the operational model of any biGSOS specification for such systems is a congruence.
8 Future work
In this paper we provided a bialgebraic foundation of positive specification formats over ordered functors, involving rules that feature lookahead in the premises as well as complex terms in conclusions. From a practical point of view, it would be interesting to find more concrete rules formats corresponding to the abstract format of the present paper. In particular, concrete GSOS formats for weighted transition systems exist [16]; they could be a good starting point.
It is currently unclear to us whether the assumption of weak pullback preservation in the main results is necessary. This assumption is used in our proof of Lemma 4.7, which in turn is used in the proof that the free monad lifts to the category of coalgebras (Theorem 6.4). Further, in the current paper we focused on monotone biGSOS specifications \(\rho :\varSigma B^\infty \Rightarrow B\varSigma ^*\). It could be interesting to study stronger ordertheoretic conditions; for instance, continuous biGSOS specifications. This would require extending the DCPOorder on B to a DCPOorder on the cofree comonad \(B^\infty \), for which the techniques of [12] may be of use. The potential advantage of continuous specifications is that they could prohibit rules which use the infinite behaviour of premises, an operationally questionable feature of coGSOS and biGSOS. We leave an investigation of continuous specifications, both at the abstract level of biGSOS and more concrete syntactic formats, for future work.
Footnotes
 1.
On \(\mathsf {Set}\), the countably presentable objects are precisely the countable sets.
Notes
Acknowledgements
The author is grateful to Henning Basold, Marcello Bonsangue, Bartek Klin and Beata Nachyła for inspiring discussions and suggestions.
References
 1.Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 197–292. Elsevier, Amsterdam (2001). https://doi.org/10.1016/B9780444828309/500217 CrossRefGoogle Scholar
 2.Adámek, J., Porst, H.E.: On tree coalgebras and coalgebra presentations. Theor. Comput. Sci. 311(1–3), 257–283 (2004). https://doi.org/10.1016/S03043975(03)003785 MathSciNetCrossRefzbMATHGoogle Scholar
 3.Adámek, J., Rosický, J.: Locally Presentable and Accessible Categories. Cambridge Tracts in Mathematics. Cambridge University Press, Cambridge (1994). https://doi.org/10.1017/CBO9780511600579 CrossRefzbMATHGoogle Scholar
 4.Bartels, F.: On generalised coinduction and probabilistic specification formats. Ph.D. thesis, CWI, Amsterdam (2004)Google Scholar
 5.Bloom, B., Istrail, S., Meyer, A.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995). https://doi.org/10.1145/200836.200876 MathSciNetCrossRefzbMATHGoogle Scholar
 6.Bonchi, F., Petrisan, D., Pous, D., Rot, J.: A general account of coinduction upto. Acta Inf. 54(2), 127–190 (2017). https://doi.org/10.1007/s0023601602714 MathSciNetCrossRefzbMATHGoogle Scholar
 7.Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)CrossRefGoogle Scholar
 8.Droste, M., Kuich, W.: Semirings and formal power series. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, pp. 3–28. Springer, Berlin (2009). 10/bj2xgmCrossRefGoogle Scholar
 9.Fiore, M., Staton, S.: Positive structural operational semantics and monotone distributive laws. In: CMCS Short Contributions, p. 8 (2010)Google Scholar
 10.Gumm, H.P., Schröder, T.: Monoidlabeled transition systems. Electr. Notes Theor. Comput. Sci. 44(1), 185–204 (2001). https://doi.org/10.1016/S15710661(04)809083 CrossRefzbMATHGoogle Scholar
 11.Hansen, H.H., Kupke, C., Rutten, J.: Stream differential equations: specification formats and solution methods. Log. Methods Comput. Sci. 13(1), (2017). https://doi.org/10.23638/LMCS13(1:3)2017
 12.Hughes, J., Jacobs, B.: Simulations in coalgebra. Theor. Comput. Sci. 327(1–2), 71–108 (2004). https://doi.org/10.1016/j.tcs.2004.07.022 MathSciNetCrossRefzbMATHGoogle Scholar
 13.Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press, Cambridge (2016). https://doi.org/10.1017/CBO9781316823187 CrossRefzbMATHGoogle Scholar
 14.Jacobs, B., Rutten, J.: An introduction to (co)algebras and (co)induction. In: JJMM, Rutten, Sangiorgi, D. (eds.) Advanced Topics in Bisimulation and Coinduction, pp. 38–99. Cambridge University Press, Cambridge (2011). https://doi.org/10.1017/CBO9780511792588.003 CrossRefGoogle Scholar
 15.Johnstone, P.T.: Adjoint lifting theorems for categories of algebras. Bull. Lond. Math. Soc. 7(3), 294–297 (1975). https://doi.org/10.1112/blms/7.3.294 MathSciNetCrossRefzbMATHGoogle Scholar
 16.Klin, B.: Structural operational semantics for weighted transition systems. In: Palsberg, J. (ed.) Semantics and Algebraic Specification. LNCS, vol. 5700, pp. 121–139. Springer, Berlin (2009). 10/cxqzcfCrossRefGoogle Scholar
 17.Klin, B.: Bialgebras for structural operational semantics: an introduction. TCS 412(38), 5043–5069 (2011). https://doi.org/10.1016/j.tcs.2011.03.023 MathSciNetCrossRefzbMATHGoogle Scholar
 18.Klin, B., Nachyła, B.: Distributive laws and decidable properties of SOS specifications. In: J. Borgström, S. Crafa (eds.) Proceedings of EXPRESS/SOS 2014. EPTCS, vol. 160, pp. 79–93 (2014). https://doi.org/10.4204/EPTCS.160.8 MathSciNetCrossRefGoogle Scholar
 19.Klin, B., Nachyła, B.: Some undecidable properties of SOS specifications. J. Log. Algebr. Meth. Program. 87, 94–109 (2017). https://doi.org/10.1016/j.jlamp.2016.08.005 MathSciNetCrossRefzbMATHGoogle Scholar
 20.Lenisa, M., Power, J., Watanabe, H.: Distributivity for endofunctors, pointed and copointed endofunctors, monads and comonads. Electr. Notes Theor. Comput. Sci. 33, 230–260 (2000). https://doi.org/10.1016/S15710661(05)803500 MathSciNetCrossRefzbMATHGoogle Scholar
 21.Makkai, M., Paré, R.: Accessible Categories: The Foundations of Categorical Model Theory. Contemporary mathematics—American Mathematical Society, vol. 104. American Mathematical Society, Providence (1989). https://doi.org/10.1090/conm/104 CrossRefzbMATHGoogle Scholar
 22.Power, J., Watanabe, H.: Combining a monad and a comonad. Theor. Comput. Sci. 280(1–2), 137–162 (2002). https://doi.org/10.1016/S03043975(01)00024X MathSciNetCrossRefzbMATHGoogle Scholar
 23.Rot, J.: Enhanced coinduction. Ph.D. thesis, Leiden University (2015)Google Scholar
 24.Rot, J.: Distributive laws for monotone specifications. In: Peters, K., Tini, S. (eds.) Proceedings of EXPRESS/SOS 2017. EPTCS, vol. 255, pp. 83–97 (2017). https://doi.org/10.4204/EPTCS.255.6 MathSciNetCrossRefGoogle Scholar
 25.Rot, J., Bonsangue, M.M.: Structural congruence for bialgebraic semantics. J. Log. Algebr. Methods Program. 85(6), 1268–1291 (2016). https://doi.org/10.1016/j.jlamp.2016.08.001 MathSciNetCrossRefzbMATHGoogle Scholar
 26.Rutten, J.: Behavioural differential equations: a coinductive calculus of streams, automata, and power series. TCS 308(1–3), 1–53 (2003)MathSciNetCrossRefGoogle Scholar
 27.Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. TCS 249(1), 3–80 (2000)MathSciNetCrossRefGoogle Scholar
 28.Rutten, J.J.M.M.: Elements of stream calculus (an extensive exercise in coinduction). Electr. Notes Theor. Comput. Sci. 45, 358–423 (2001). https://doi.org/10.1016/S15710661(04)809721 CrossRefzbMATHGoogle Scholar
 29.Staton, S.: General structural operational semantics through categorical logic. In: LICS, pp. 166–177. IEEE Computer Society (2008). https://doi.org/10.1109/LICS.2008.43
 30.Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: LICS, pp. 280–291. IEEE Computer Society (1997). https://doi.org/10.1109/LICS.1997.614955
Copyright information
OpenAccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.