The Adjoint School 2023
The 2023 Adjoint School featured projects mentored by Priyaa Srinivasan, Barbara König, Chris Heunen, and Dan Marsden. It is organized by Ana Luiza da Conceição Tenorio, Nathan Haydon, Elena Di Lavore, and Angeline Aguinaldo. The research week was held at the University of Maryland, College Park, USA.
Research Projects
Message Passing Logic for Categorical Quantum Mechanics
Mentor: Priyaa Srinivasan
TA: Rose Kudzman-Blais
Students: Paige Frederick, Isaiah Hilsenrath, Fabian Wiesner, Brandon Baylor, Durgesh Kumar
Cockett and Pastro introduced two-tiered ‘Message Passing Logic’ in order to develop a type theory for concurrent programs with message passing as the communication primitive. The motivation was to allow one to guarantee certain formal properties of concurrent programs such as deadlock and livelock avoidance, which is not possible using the current programming technologies. Current programming languages lack such features because concurrency constructs are embedded in the sequential core without a formal underpinning. The categorical logic behind the machinery introduced by Cockett and Pastro is based on monoidal categories acting on linearly distributive categories with the proof theory given by multi categories acting on poly categories. A goal of this project is to develop models of this logic and to explore its possible connections to categorical quantum mechanics. Another goal of this project is to develop use cases in Computer Science on designing concurrent solutions using the Message Passing Logic.
Readings
- The logic of message-passing., Cockett, J. Robin B., and Craig Pastro Science of Computer Programming 74.8 (2009): 498-533.
- Weakly distributive categories., Cockett, J. Robin B., and Robert A.G. Journal of Pure and Applied Algebra 114.2 (1997): 133-173.
Behavioural Metrics, Quantitative Logics and Coalgebras
Mentor: Barbara König
TA: Paul Wild and Sebastian Gurke
Students: Keri D'Angelo, (Wojtek) Wojciech Rozowski, Matina Najafi, Johanna Maria Kirss, Avi Craimer
Behavioural equivalences are an important concept for the verification of concurrent systems. Two processes or system states are behaviourally equivalent if they are indistinguishable from the point of view of an external observer. For quantitative systems, the notion of behavioural equivalence is often not very robust and small deviations in quantitative information, such as probabilities, can cause two states that intuitively behave very much alike to be inequivalent in a formal sense. Hence a more suitable approach is to consider various forms of metrics for determining at what behavioural distance two states lie. Such metrics have often been studied in probabilistic settings, but this approach can be extended to measuring other forms of distances. Coalgebra offers a general categorical framework in which different kinds of (transition) systems, behavioural equivalences and in particular metrics can be modelled and studied. The branching type of the transition system (non-deterministic, probabilistic, weighted, etc.) is specified by a functor and a central ingredient of coalgebraic approaches to behavioural metrics is to define suitable functor liftings to metric spaces, generalizing the Kantorovich lifting from probability theory. Furthermore, coalgebraic modal logic can be transferred to this setting, resulting in a quantitative logic, generalizing the boolean case.
Readings
- Coalgebraic Behavioral Metrics, Paolo Baldan, Filippo Bonchi, Henning Kerstan, Barbara König Logical Methods in Computer Science (2018).
- Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions, Paul Wild, Lutz Schröder 31st International Conference on Concurrency Theory (CONCUR 2020).
Concurrency in monoidal categories
Mentor: Chris Heunen
TA: Carmen Constantin and Nesta van der Schaaf
Students: Ariadne Si Suo, Clémence Chanavat, Ariel Rosenfield, Luke Morris
Categories are all about processes happening one after the other. Monoidal categories are additionally about processes happening simultaneously. In any monoidal category we can cleanly separate these temporal and spatial aspects. There is a space 'in' which all the processes take place, and each process 'lives' only in some part of that space. You may therefore think monoidal categories are a perfect setting for concurrency. But something is missing: there is no way for a process to go from one part of the space to a disjoint part of the space. Instead, transfer of ownership requires additional structure. This project will find out what structure we can add to a monoidal category so that messages can be passed between different parts of its space.
Readings
- Sheaf representation of monoidal categories, R. Soares Barbosa, C. Heunen
- Concurrent Process Histories and Resource Transducers, C. Nester
Game Comonads and Finite Model Theory
Mentor: Dan Marsden
TA: Nihil Shah
Students: Tyler Hanks, Zhixuan Yang, Richie Yeung, Elena Dimitriadis Bermejo
Finite model theory has connections to many parts of computer science and logic, including database theory, descriptive complexity, algorithmic meta-theorems and combinatorics. Typical problems addressed using the techniques from this area focus on the Power of computation, for example efficiency of algorithms, or logical descriptions of complexity classes. By comparison, the tools used in the semantics of computation and logic have addressed different questions about the Structure of computation - for example what is the right model for dependent types, or programs with effects? Model comparison games are a key tool in finite model theory for establishing equivalence between models in a particular logic. In recent work of Abramsky, Dawar and Wang, and subsequently by Abramsky and Shah, introduced the novel idea of game comonads. These categorical structures encapsulate model comparison games, providing a direct mathematical connection between the Power of finite model theory, and the insights into Structure provided by the tools of modern semantics. Subsequent progress in this area has included incorporating many different logics, addressing Rossman's homomorphism preservation theorems, Lovasz homomorphism counting results, van Benthem-Rosen type theorems, composition methods in logic, algorithmic meta-theorems such as Courcelle's theorem, and categorical axiomatics. This project will introduce students to the required finite model theory, and the game comonads framework, and to engage with the current state of the art in this area. This will provide an opportunity to develop knowledge spanning two traditionally disparate areas of theoretical computer science and mathematics. Beyond the proposed readings, directions for further research, depending on the interests of the students, include studying additional logics of practical interest, investigating model theoretic questions, studying algorithmic meta-theorems, or investigating the underlying categorical structure, from the perspective of game comonads.
Readings
- Elements of Finite Model Theory Chapters 1-3 & 11, Leonid Libkin, 2012.
- Relating Structure and Power: Comonadic Semantics for Computational Resources, Samson Abramsky, Nihil Shah, 2018.