Abstract In this paper, we extend diagrammatic reasoning in monoidal categories with algebraic operations and equations. We achieve this by considering monoidal categories that are enriched in the category of Eilenberg-Moore algebras for a monad. Under the condition that this monad is monoidal and there is an adjunction between the free algebra functor and the underlying category functor, we construct an adjunction between symmetric monoidal categories and symmetric monoidal categories enriched over algebras for the monad. This allows us to devise an extension, and its semantics, of the ZX-calculus with probabilistic choices by freely enriching over convex algebras, which are the algebras of the finite distribution monad. We show how this construction can be used for diagrammatic reasoning of noise in quantum systems.

Directed topology augments the concept of a topological space with a notion of directed paths. This leads to a category of directed spaces, in which the morphisms are continuous maps respecting directed paths. Directed topology thereby enables an accurate representation of computation paths in concurrent systems that usually cannot be reversed. Even though ideas from algebraic topology have analogues in directed topology, the directedness drastically changes how spaces can be characterised. For instance, while an important homotopy invariant of a topological space is its fundamental groupoid, for directed spaces this has to be replaced by the fundamental category because directed paths are not necessarily reversible. In this paper, we present a Lean 4 formalisation of directed spaces and of a Van Kampen theorem for them, which allows the fundamental category of a directed space to be computed in terms of the fundamental categories of subspaces. Part of this formalisation is also a significant theory of directed spaces, directed homotopy theory and path coverings, which can serve as basis for future formalisations of directed topology. The formalisation in Lean can also be used in computer-assisted reasoning about the behaviour of concurrent systems that have been represented as directed spaces.

Causality appears in various contexts as a property where present behaviour can only depend on past events, but not on future events. In this paper, we compare three different notions of causality that capture the idea of causality in the form of restrictions on morphisms between coinductively defined structures, such as final coalgebras and chains, in fairly general categories. We then focus on one presentation and show that it gives rise to a traced symmetric monoidal category of causal morphisms. This shows that causal morphisms are closed under sequential and parallel composition and, crucially, under recursion.

Compositional methods are central to the verification of software systems. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that channels in a program interact following a certain protocol—whether messages are exchanged in the intended order. In this article, we put on our coalgebraic spectacles to investigate session types , a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation enables us to derive a decidable type system with subtyping for the π-calculus, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective coincide with existing ones. We further apply to session coalgebras the coalgebraic approach to regular languages via the so-called rational fixed point, inspired by the trinity of automata, regular languages, and regular expressions with session coalgebras, rational fixed point, and session types, respectively. We establish a suitable restriction on session coalgebras that determines a similar trinity, and reveals the mismatch between usual session types and our syntax-free coalgebraic approach. Furthermore, we extend our coalgebraic approach to account for context-free session types, by equipping session coalgebras with a stack.

Abstract Compositional methods are central to the development and verification of software systems. They allow breaking down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that programs interact with channels according to a certain protocol, whether the intended messages are exchanged in a certain order. In this paper, we put on our coalgebraic spectacles to investigate session types, a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation makes it possible to elegantly derive a decidable type system with subtyping for $$\pi $$ π -calculus processes, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective agree with the existing ones.

Abstract In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen’s classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

International audience

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs ; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.

Abstract We define notions of well-definedness and observational equivalence for programs of mixed inductive and coinductive types. These notions are defined by means of tests formulas which combine structural congruence for inductive types and modal logic for coinductive types. Tests also correspond to certain evaluation contexts. We define a program to be well-defined if it is strongly normalizing under all tests, and two programs are observationally equivalent if they satisfy the same tests. We show that observational equivalence is sufficiently coarse to ensure that least and greatest fixed point types are initial algebras and final coalgebras, respectively. This yields inductive and coinductive proof principles for reasoning about program behaviour. On the other hand, we argue that observational equivalence does not identify too many terms, by showing that tests induce a topology that, on streams, coincides with usual topology induced by the prefix metric. As one would expect, observational equivalence is, in general, undecidable, but in order to develop some practically useful heuristics we provide coinductive techniques for establishing observational normalization and observational equivalence, along with up-to techniques for enhancing these methods.

We present a comparative study of four product operators on weighted languages: (i) the convolution, (ii) the shuffle, (iii) the infiltration and (iv) the Hadamard product. Exploiting the fact that the set of weighted languages is a final coalgebra, we use coinduction to prove that an operator of the classical difference calculus, the Newton transform, generalises from infinite sequences to weighted languages. We show that the Newton transform is an isomorphism of rings that transforms the Hadamard product of two weighted languages into their infiltration product, and we develop various representations for the Newton transform of a language, together with concrete calculation rules for computing them.

Distributive laws between functors are a fundamental tool in the theory of coalgebras. In the context of coinduction in complete lattices, they correspond to the so-called compatible functions, which enable enhancements of the coinductive proof technique. Amongst these, the greatest compatible function, called the companion, has recently been shown to satisfy many good properties. Categorically, the companion of a functor corresponds to the final object in a category of distributive laws. We show that every accessible functor on a locally presentable category has a companion. Central to this and other constructions in the paper is the presentation of distributive laws as coalgebras for a certain functor. This functor itself has again, what we call, a second-order companion. We show how this companion interacts with the various monoidal structures on functor categories. In particular, both the first- and second-order companion give rise to monads. We use these results to obtain an abstract GSOS-like extension result for specifications involving the second-order companion.

We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For example, all well-known basic types and type formers that are needed for using this type theory as a logic are definable: propositional connectives, like falsity, conjunction, disjunction, and function space, dependent function space, existential quantification, equality, natural numbers, vectors etc. The reduction relation on terms consists solely of a rule for recursion and a rule for corecursion. The reduction relations for well-known types arise from that. To further support the introduction of this new type theory, we also prove fundamental properties of its term calculus. Most importantly, we prove subject reduction and strong normalisation of the reduction relation, which gives computational meaning to the terms.