
The Calculus of Conjunctive Queries (CCQ) has foundational status in database
theory. A celebrated theorem of Chandra and Merlin states that CCQ query
inclusion is decidable. Its proof transforms logical formulas to graphs: each
query has a natural model  a kind of graph  and query inclusion reduces to
the existence of a graph homomorphism between natural models.
We introduce the diagrammatic language Graphical Conjunctive Queries (GCQ)
and show that it has the same expressivity as CCQ. GCQ terms are string
diagrams, and their algebraic structure allows us to derive a sound and
complete axiomatisation of query inclusion, which turns out to be exactly
Carboni and Walters' notion of cartesian bicategory of relations. Our
completeness proof exploits the combinatorial nature of string diagrams as
(certain cospans of) hypergraphs: Chandra and Merlin's insights inspire a
theorem that relates such cospans with spans. Completeness and decidability of
the (in)equational theory of GCQ follow as a corollary. Categorically speaking,
our contribution is a modeltheoretic completeness theorem of free cartesian
bicategories (on a relational signature) for the category of sets and
relations.

String diagrams are a powerful and intuitive graphical syntax for terms of
symmetric monoidal categories (SMCs). They find many applications in computer
science and are becoming increasingly relevant in other fields such as physics
and control theory.
An important role in many such approaches is played by equational theories of
diagrams, typically oriented and applied as rewrite rules. This paper lays a
comprehensive foundation of this form of rewriting. We interpret diagrams
combinatorially as typed hypergraphs and establish the precise correspondence
between diagram rewriting modulo the laws of SMCs on the one hand and double
pushout (DPO) rewriting of hypergraphs, subject to a soundness condition called
convexity, on the other. This result rests on a more general characterisation
theorem in which we show that typed hypergraph DPO rewriting amounts to diagram
rewriting modulo the laws of SMCs with a chosen special Frobenius structure.
We illustrate our approach with a proof of termination for the theory of
noncommutative bimonoids.

We introduce the theory IH of interacting Hopf algebras, parametrised over a
principal ideal domain R. The axioms of IH are derived using Lack's approach to
composing PROPs: they feature two Hopf algebra and two Frobenius algebra
structures on four different monoidcomonoid pairs. This construction is
instrumental in showing that IH is isomorphic to the PROP of linear relations
(i.e. subspaces) over the field of fractions of R.

A quite flourishing research thread in the recent literature on
componentbased systems is concerned with the algebraic properties of different
classes of connectors. In a recent paper, an algebra of stateless connectors
was presented that consists of five kinds of basic connectors, namely symmetry,
synchronization, mutual exclusion, hiding and inaction, plus their duals, and
it was shown how they can be freely composed in series and in parallel to model
sophisticated 'glues'. In this paper we explore the expressiveness of stateful
connectors obtained by adding oneplace buffers or unbounded buffers to the
stateless connectors. The main results are: i) we show how different classes of
connectors exactly correspond to suitable classes of Petri nets equipped with
compositional interfaces, called nets with boundaries; ii) we show that the
difference between strong and weak semantics in stateful connectors is
reflected in the semantics of nets with boundaries by moving from the classic
step semantics (strong case) to a novel banking semantics (weak case), where a
step can be executed by taking some 'debit' tokens to be given back during the
same step; iii) we show that the corresponding bisimilarities are congruences
(w.r.t. composition of connectors in series and in parallel); iv) we show that
suitable monoidality laws, like those arising when representing stateful
connectors in the tile model, can nicely capture concurrency (in the sense of
step semantics) aspects; and v) as a side result, we provide a basic algebra,
with a finite set of symbols, out of which we can compose all P/T nets with
boundaries, fulfilling a long standing quest.

In recent work, the author and others have studied compositional algebras of
Petri nets. Here we consider mathematical aspects of the pure linking algebras
that underly them. We characterise composition of nets without places as the
composition of spans over appropriate categories of relations, and study the
underlying algebraic structures.

In recent work, the second and third authors introduced a technique for
reachability checking in 1bounded Petri nets, based on wiring decompositions,
which are expressions in a fragment of the compositional algebra of nets with
boundaries. Here we extend the technique to the full algebra and introduce the
related structural property of decomposition width on directed hypergraphs.
Small decomposition width is necessary for the applicability of the
reachability checking algorithm. We give examples of families of nets with
constant decomposition width and develop the underlying theory of
decompositions.

Colimits that satisfy the Van Kampen condition have interesting exactness
properties. We show that the elementary presentation of the Van Kampen
condition is actually a characterisation of a universal property in the
associated bicategory of spans. The main theorem states that Van Kampen cocones
are precisely those diagrams in a category that induce bicolimit diagrams in
its associated bicategory of spans, provided that the category has pullbacks
and enough colimits.