Coalgebraic Methods in Computer Science

Higher-order languages have been widely studied in functional programming, following the \(\lambda \)-calculus. In a higher-order calculus, variables may be instantiated with terms of the language. When multiple occurrences of the variable exist, this mechanism results in the possibility of copying the terms of the language.

We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs’ recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as “may” vs. “must”) are captured by Eilenberg-Moore algebras; (2) nested branching—like in games and in probabilistic systems with nondeterministic environments—is modularly modeled by a monad on the Eilenberg-Moore category of another.

Coalgebraic games have been recently introduced as a generalization of Conway games and other notions of games arising in different contexts. Using coalgebraic methods, games can be viewed as elements of a final coalgebra for a suitable functor, and operations on games can be analyzed in terms of (generalized) coiteration schemata. Coalgebraic games are sequential in nature, i.e. at each step either the Left (L) or the Right (R) player moves (global polarization), moreover only a single move can be performed at each step. Recently, in the context of Game Semantics, concurrent games have been introduced, where global polarization is abandoned, and multiple moves are allowed. In this paper, we introduce coalgebraic multigames, which are situated half-way between traditional sequential games and concurrent games: global polarization is still present, however multiple moves are possible at each step, i.e. a team of L/R players moves in parallel. Coalgebraic operations, such as sum and negation, can be naturally defined on multigames. Interestingly, sum on coalgebraic multigames turns out to be related to Conway’s selective sum on games, rather than the usual (sequential) disjoint sum. Selective sum has a parallel nature, in that at each step the current player performs a move in at least one component of the sum game, while on disjoint sum the current player performs a move in exactly one component at each step. A monoidal closed category of coalgebraic multigames in the vein of a Joyal category of Conway games is then built. The relationship between coalgebraic multigames and games is then formalized via an equivalence of the multigame category and a monoidal closed category of coalgebraic games where tensor is selective sum.

We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or \(\epsilon \)-transitions. Our approach employs monads with a parametrized fixpoint operator \(\dagger \) to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems.

In the first part of the paper we recall the coalgebraic approach to handling the so-called invisible transitions that appear in different state-based systems semantics. We claim that these transitions are always part of the unit of a certain monad. Hence, coalgebras with internal moves are exactly coalgebras over a monadic type. The rest of the paper is devoted to supporting our claim by studying two important behavioural equivalences for state-based systems with internal moves, namely: weak bisimulation and trace semantics. We continue our research on weak bisimulations for coalgebras over order enriched monads. The key notions used in this paper and proposed by us in our previous work are the notions of an order saturation monad and a saturator. A saturator operator can be intuitively understood as a reflexive, transitive closure operator. There are two approaches towards defining saturators for coalgebras with internal moves. Here, we give necessary conditions for them to yield the same notion of weak bisimulation. Finally, we propose a definition of trace semantics for coalgebras with silent moves via a uniform fixed point operator. We compare strong and weak bisimilation together with trace semantics for coalgebras with internal steps.

The literature on process theory and structural operational semantics abounds with various notions of behavioural equivalence and, more generally, simulation preorders. An important problem in this area from the point of view of logic is to find formulas that characterize states in finite transition systems with respect to these various relations. Recent work by Aceto et al. shows how such characterizing formulas in equational modal fixed point logics can be obtained for a wide variety of behavioural preorders using a single method. In this paper, we apply this basic insight from the work by Aceto et al. to Baltag’s “logics for coalgebraic simulation” to obtain a general result that yields characteristic formulas for a wide range of relations, including strong bisimilarity, simulation, as well as bisimulation and simulation on Markov chains and more. Hence this paper both generalizes the work of Aceto et al. and makes explicit the coalgebraic aspects of their work.

In a recent article Gorín and Schröder [3] study \(\lambda \)-simulations of coalgebras and relate them to preservation of positive formulae. Their main results assume that \(\lambda \) is a set of monotonic predicate liftings and their proofs are set-theoretical. We give a different definition of simulation, called strong simulation, which has several advantages:

Our notion agrees with that of [3] in the presence of monotonicity, but it has the advantage, that it allows diagrammatic reasoning, so several results from the mentioned paper can be obtained by simple diagram chases. We clarify the role of \(\lambda \)-monotonicity by showing the equivalence of We relate the notion to bisimulations and \(F\)-congruences - which are defined as pullbacks of homomorphisms. We show that

The Dijkstra monad has been introduced recently for capturing weakest precondition computations within the context of program verification, supported by a theorem prover. Here we give a more general description of such Dijkstra monads in a categorical setting. We first elaborate the recently developed view on program semantics in terms of a triangle of computations, state transformers, and predicate transformers. Instantiations of this triangle for different monads \(T\) show how to define the Dijkstra monad associated with \(T\), via the logic involved. Technically, we provide a morphism of monads from the state monad transformation applied to \(T\), to the Dijkstra monad associated with \(T\). This monad map is precisely the weakest precondition map in the triangle, given in categorical terms by substitution.

Abstract graph transformation approaches traditionally consider graph structures as algebras over signatures where all function symbols are unary.

Attributed graphs, with attributes taken from (term) algebras over arbitrary signatures do not fit directly into this kind of transformation approach, since algebras containing function symbols taking two or more arguments do not allow component-wise construction of pushouts. We show how shifting from the algebraic view to a coalgebraic view of graph structures opens up additional flexibility, and enables treating term algebras over arbitrary signatures in essentially the same way as unstructured label sets. We integrate substitution into our coalgebra homomorphisms by identifying a factoring over the term monad, and obtain a flexible framework for graphs with symbolic attributes. This allows us to prove that pushouts can be constructed for homomorphisms with unifiable substitution components.

We formalised the presented development in Agda, which crucially aided the exploration of the complex interaction of the different functors, and enables us to report all theorems as mechanically verified.

It is a well-known fact that a nondeterministic automaton can be transformed into an equivalent deterministic automaton via the powerset construction. From a categorical perspective this construction is the right adjoint to the inclusion functor from the category of deterministic automata to the category of nondeterministic automata. This is in fact an adjunction between two categories of coalgebras: deterministic automata are coalgebras over \(\mathbf {Set}\) and nondeterministic automata are coalgebras over \(\mathbf {Rel}\). We will argue that this adjunction between coalgebras originates from a canonical adjunction between \(\mathbf {Set}\) and \(\mathbf {Rel}\).

In this paper we describe how, in a quite generic setting, an adjunction can be lifted to coalgebras, and we compare some sufficient conditions. Then we illustrate this technique in length: we recover several constructions on automata as liftings of basic adjunctions including determinization of nondeterministic and join automata, codeterminization, and the dualization of linear weighted automata. Finally, we show how to use the lifted adjunction to check behavioral equivalence.

For each regular language \(L\) we describe a family of canonical nondeterministic acceptors (nfas). Their construction follows a uniform recipe: build the minimal dfa for \(L\) in a locally finite variety \(\mathcal {V}\), and apply an equivalence between the finite \(\mathcal {V}\)-algebras and a category of finite structured sets and relations. By instantiating this to different varieties we recover three well-studied canonical nfas (the átomaton, the jiromaton and the minimal xor automaton) and obtain a new canonical nfa called the distromaton. We prove that each of these nfas is minimal relative to a suitable measure, and give conditions for state-minimality. Our approach is coalgebraic, exhibiting additional structure and universal properties.

Temporal logics are an obvious high-level descriptive companion formalism to dynamical systems which model behavior as deterministic evolution of state over time. A wide variety of distinct temporal logics applicable to dynamical systems exists, and each candidate has its own pragmatic justification. Here, a systematic approach to the construction of temporal logics for dynamical systems is proposed: Firstly, it is noted that dynamical systems can be seen as coalgebras in various ways. Secondly, a straightforward standard construction of modal logics out of coalgebras, namely Moss’s coalgebraic logic, is applied. Lastly, the resulting systems are characterized with respect to the temporal properties they express.

We investigate the common recursive structure of history-dependent dynamic models in science and engineering. We give formal semantics in terms of a hybrid algebraic–coalgebraic scheme, namely course-of-value iteration. This theoretical approach yields categories of observationally equivalent model representations with precise semantic relationships. Along the initial–final axis of these categories, history dependence can appear both literally and transformed into instantaneous state. The framework can be connected to philosophical and epistemological discourse on one side, and to algorithmic considerations for computational modeling on the other.