The Adjoint School 2024

The 2024 Adjoint School featured projects mentored by Dorette Pronk, Koko Muroya, Paolo Perrone, and Niccolò Veltri. It was organized by Ana Luiza da Conceição Tenorio, Nathan Haydon, Ari Rosenfield, and Elena Dimitriadis Bermejo. The research week was held at University of Oxford, UK.

Research Projects

Properties of Double Fibrations

Mentor: Dorette Pronk
TA: Luca Mesiti, Elena Caviglia
Students: C. B. Aberlé, Matt Kukla, Rubén Maldonado, Tanjona Ralaivaosaona

In this project we will study the properties of double fibrations between double categories. Fibrations play an important role in categorical logic and various kinds of type theory. Fibrations over a category C are closely related to pseudofunctors from C into Cat, the 2-category of categories, via the Grothendieck construction. Double categories are categories with two types of arrows (often called proarrows and arrows, where composition may be stricter in the arrow than the proarrow direction) and double cells between them, that have domains and codomains in both types of arrows. They have become prominent in recent research in applied category theory, in particular in terms of modelling open dynamical systems and in the study of decorated cospans. In recent work, Cruttwell, Lamberts, Szyld and the mentor for this research project have introduced double fibrations with a double Grothendieck construction. Patterson showed in a recent paper how decorated cospans form an example of a double fibration. In this project we want to further investigate this construction and the properties of double fibrations. There are a number of nice properties that ordinary Grothendieck fibrations enjoy for which we want to find double categorical generalizations and see what they mean for applications.

Readings

Applications of Skew Monoidal Categories

Mentor: Niccolò Veltri
TA: Cheng-Syuan Wan
Students: Pablo S. Ocal, Wilf Offord, Thea Li, Federica Pasqualone

Skew monoidal categories are a variant of monoidal categories where the structural morphisms of associativity and unitality are not required to be invertible, they are merely natural transformations in a particular direction, i.e. they are semi-associative and semi-unital variants of monoidal categories. The coherence problem for these categories cannot be solved using MacLane's coherence theorem for monoidal categories, since skew monoidal categories might contain pairs of unequal parallel structural morphisms. Solutions to the coherence problem exist and involve a concrete description of the free skew monoidal category, using combinatorial or proof-theoretic methodologies. Extensions of skew monoidal categories and their coherence problem have also been considered, e.g. a notion of skew braiding and symmetry, as well as a notion of skew internal hom.

Skew monoidal categories have been originally introduced by Szlachányi in his study of quantum structures and they appear prominently in the theory of relative monads. Their unit-free variant has connections to combinatorial structures such as the Tamari lattice and Stasheff associahedra. This project aims at discovering useful applications of skew monoidal categories and their variants in computer science, linguistics and combinatorics. For example, the free skew monoidal closed category can be presented as a skew variant of Lambek syntactic calculus, where resource manipulation and consumption follow a restricted "skew" discipline. Are there applications where this restriction is meaningful? Do semi-associativity and semi-unitality play a role in the study of natural languages? Theoretical questions also arise naturally: what is good notion of symmetric skew monoidal category with copy and discard?

Readings

Critical Pairs for String Diagram Rewriting

Mentor: Koko Muroya
TA: Diana Kessler, Juan Meleiro
Students: Anna Matsui, Innocent Obi, Guillaume Sabbagh, Leo Torres

Computer programs admit two kinds of rewriting: compile-time rewriting such as compiler optimisation, and runtime rewriting that yields the result of calculation. It is desirable to have a formal proof of their coherence, that is, compile-time rewriting does not change the overall behaviour of runtime rewriting. One approach to establish the coherence is to analyse if, and how, rules for compile-time rewriting interfere with rules for runtime rewriting. Such interference is summarised as the so-called "critical pairs."

String diagrams provide a graphical language for categories such as symmetric monoidal closed categories and cartesian closed categories. Functional programs can be represented graphically by string diagrams. The compile-time and runtime rewriting of programs can then be modelled by rule-based rewriting of string diagrams.

A goal of this project is to develop a method for enumerating critical pairs for rule-based string diagram rewriting. A motivating example is string diagram rewriting for the lambda-calculus, which use string diagrams for cartesian closed categories. The method could be seen as an instance of the maximum common subgraph problem in graph theory. We will try to figure out how it helps algorithmically to focus on string diagrams, which can be modelled by certain hypergraphs.

Readings

Modelling Uncertainty with Markov Categories

Mentor: Paolo Perrone
TA: Tomáš Gonda
Students: Utku Boduroglu, Laura Gonzalez Bravo, Drew Allen McNeely, Luis Lopez, Nico Wittrock

Probability theory is the most widely accepted mathematical framework to model uncertainty. However, there are situations in which the likelihood of an event cannot be assigned an exact numerical value or may not even be comparable with the likelihood of another one. Sometimes, a fuzzy version of logical deduction without the rules of classical probability is needed, such as with softmax layers in neural networks.

To this end, many alternative models of uncertainty have been developed over the years. These include imprecise probability measures, Dempster-Shafer belief functions, possibility and plausibility measures to name a few. Besides other uses, they can often express notions of independence and conditioning. Nevertheless, these approaches are often underdeveloped and lack a common unifying framework of models of uncertainty.

Markov categories have recently been very successful in both expressing the concepts and proving theorems of probability theory, by starting from an abstract version of a category of stochastic maps. Among the concepts are notions of determinism, independence, conditioning, sampling, almost sure equality, etc.

Some Markov categories are known, whose morphisms are not explicitly probabilistic processes, but which can still be interpreted as expressing uncertainty. One example comes from categories of relations, where many possible outcomes can happen, but neither is assigned a number expressing the likelihood of occurrence. However, the existing versions of theorems such as de Finetti's theorem, zero/one laws, and ergodic decomposition theorem in Markov categories are only known to apply to a handful of concrete Markov categories, which are generally of “probabilistic flavour”.

Can one model the aforementioned alternatives to and generalizations of probability theory within the framework of Markov categories? Do propagation of uncertainty, notions of independence and conditioning therein follow categorical laws? Can they harbour unbeknownst instances of the recently discovered theorems for Markov categories? These questions central to categorical probability are still wide open.

In this project, we will go through several of the alternative approaches to modelling uncertainty and we will check whether they constitute Markov categories. If yes, we will study their properties from the categorical point of view. If not, we will aim to understand why not and draw appropriate conclusions. In either case, we will achieve a deeper understanding both of probability theory broadly construed and of its categorical formalization.

Readings

  • Reasoning about uncertainty, J. Y. Halpern. Chapter 2, MIT Press, 2017.
  • Markov Categories and Entropy, Paolo Perrone , IEEE Transactions on Information Theory, 2023.

Sponsors