Drawing a ball from an urn filled with balls of different colours is one of the basic models in probability theory. The probability of drawing a ball of a particular colour is determined by the proportion / fraction of balls of that colour. This paper introduces a new stochastic model for such urns: draw a ball, recolour (repaint) it, and put it back into the urn. One can distinguish four modes of drawing-and-recolouring, namely whether done proportionally or uniformly (both for drawing and recolouring). These modes can be reformulated in financial terms as redistribution of wealth or in biological terms as evolutionary drift. The resulting four operations form a coalgebra for the distribution monad, on the set of multisets of a fixed size. In fact they form a Markov chain and even a hidden Markov model, in combination with the frequentist learning map as emission channel. This paper identifies fixed points, capturing stable situations, for these four modes of drawing-and-recolouring.
We introduce effectful Mealy machines - a general notion of Mealy machine with global effects - and give them semantics in terms of both bisimilarity and traces. Bisimilarity of effectful Mealy machines is characterized syntactically, via free uniform feedback. Their traces are given a novel semantic coinductive universe in terms of effectful streams. We prove that this framework generalizes standard causal processes and captures existing flavours of Mealy machine, bisimilarity, and trace. This is an extended abstract for the manuscript Effectful Mealy Machines: Bisimulation and Trace that will appear in the proceedings of LiCS 2025 [3]; an extended version with proofs is also available (arxiv.org/abs/2410.10627) [4]. We additionally characterise causal processes as lax-natural transformations.
We investigate a representation of computable functions as total functions over 2(infinity), the set of finite and infinite sequences over {0, 1}. In this model, infinite sequences are interpreted as non-terminating computations whilst finite sequences represent the sum of their digits. We introduce a new definition principle, function space corecursion, that simultaneously generalises minimisation and primitive recursion. This defines the class of computable corecursive functions that is closed under composition and function space corecursion. We prove computable corecursive functions represent all partial recursive functions, and show that all computable corecursive functions are indeed computable by translation into the untyped lambda-calculus.
We present a result that implies that an endofunctor on a category has a terminal coalgebra obtainable as a countable limit of its terminal-coalgebra sequence. It holds for finitary endofunctors preserving nonempty binary intersections on locally finitely presentable categories, assuming that the posets of strong quotients and subobjects of every finitely presentable object satisfy the descending chain condition. This allows one to adapt finiteness arguments that were originally advanced by Worrell concerning terminal coalgebras for finitary set functors. Examples include the categories of sets, posets, vector spaces, graphs, and nominal sets. A similar argument is presented for the category of metric spaces (although it is not locally finitely presentable).
We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra A of truth-degrees. More precisely, we work with coalgebraic modal logic via A-valued predicate liftings where A is an FLew-algebra, and interpret actions (abstracting programs and games) as F-coalgebras where the functor F represents some type of A-weighted system. We also allow combinations of crisp propositions with A-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for 2-valued iteration-free PDL with A-valued accessibility relations when A is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.
The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way.E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders the properties of the data structure precise, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.
Convex semilattices are algebras that are at the same time a convex algebra and a semilattice, together with a distributivity axiom. These algebras have attracted some attention in the last years as suitable algebras for probability and nondeterminism, in particular by being the Eilenberg-Moore algebras of the nonempty finitely-generated convex subsets of the distributions monad. A convex semilattice is cancellative if the underlying convex algebra is cancellative. Cancellative convex algebras have been characterized by M. H. Stone and by H. Kneser: A convex algebra is cancellative if and only if it is isomorphic to a convex subset of a vector space (with canonical convex algebra operations). We prove an analogous theorem for convex semilattices: A convex semilattice is cancellative if and only if it is isomorphic to a convex subset of a Riesz space, i.e., a lattice-ordered vector space (with canonical convex semilattice operations).
A Markov decision process (MDP) is a state-based dynamical system capable of describing probabilistic behaviour with rewards. In this paper, we view MDPs as coalgebras living in the category of analytic spaces, a very general class of measurable spaces. Note that analytic spaces were already studied in the literature on labelled Markov processes and bisimulation relations. Our results are twofold. First, we define bisimulation pseudometrics over such coalgebras using the framework of fibrations. Second, we develop a quantitative modal logic for such coalgebras and prove a quantitative form of Hennessy-Milner theorem in this new setting stating that the bisimulation pseudometric corresponds to the logical distance induced by modal formulae.
Tape diagrams provide a graphical representation for arrows of rig categories, namely categories equipped with two monoidal structures,. and., where. distributes over.. However, their applicability is limited to categories where. is a biproduct, i.e., both a categorical product and a coproduct. In this work, we extend tape diagrams to deal with Kleisli categories of symmetric monoidal monads, presented by algebraic theories.
Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose interpretation as a Set functor carries a monad structure. The category of containers is closed under container composition and is a monoidal category, whereas monadic containers do not in general compose. In this paper, we develop a characterisation of distributive laws of monadic containers. Distributive laws were introduced as a sufficient condition for the composition of the underlying functors of two monads to also carry a monad structure. Our development parallels Ahman and Uustalu's characterisation of distributive laws of directed containers, i.e. containers whose Set functor interpretation carries a comonad structure. Furthermore, by combining our work with theirs, we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the 'zoo' of container characterisations of (co)monads and their distributive laws. We have found these characterisations amenable to development of existence and uniqueness proofs of distributive laws, particularly in the mechanised setting of Cubical Agda, in which most of the theory of this paper has been formalised.
Moralisation and Triangulation are transformations allowing to switch between different ways of factoring a probability distribution into a graphical model. Moralisation allows to view a Bayesian network (a directed model) as a Markov network (an undirected model), whereas triangulation works in the opposite direction. We present a categorical framework where these transformations are modelled as functors between a category of Bayesian networks and one of Markov networks. The two kinds of network (the objects of these categories) are themselves represented as functors, from a `syntax' domain to a `semantics' codomain. Notably, moralisation and triangulation are definable inductively on such syntax, and operate as a form of functor pre-composition. This approach introduces a modular, algebraic perspective in the theory of probabilistic graphical models.
We introduce string diagrams for graded symmetric monoidal categories. Our approach includes a definition of graded monoidal theory and the corresponding freely generated syntactic category. Also, we show how an axiomatic presentation for the graded theory may be modularly obtained from one for the grading theory and one for the base category. The Para construction on monoidal actegories is a motivating example for our framework. As a case study, we show how to axiomatise a variant of the graded category ImP, recently introduced by Liell-Cock and Staton to model imprecise probability [34]. This culminates in a representation, as string diagrams with grading wires, of programs with primitives for nondeterministic and probabilistic choices and conditioning.
Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure. Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.
We present a higher-order extension of Turi and Plotkin’s abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe’s method is developed. It encompasses, for instance, Abramsky’s classical compositionality theorem for applicative similarity in the untyped λ -calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.
