Linearly distributive categories provide categorical description of multiplicative linear logic. Even though linear logic has been shown to have applications in many areas of computer science and quantum, applied category theorists have mostly stayed away from linearly distributive categories mostly because the foundational papers on these categories and their associated structures are highly technical in nature. The aim of this blog series is to provide an one-stop, accessible, intuitive introduction to linearly distributive categories, functors, transformations, other associated structures and applications by assimilating information spread across these multiple highly technical articles, and to encourage discussion in this topic.
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. 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, and is called a linear actegory. Chad Nester introduced resource transducers for concurrent process histories which is a toy model of linear actegories. This talk introduces Cockett and Pastro’s message passing logic and Nester’s resource transducers which is a toy model of this logic.
Dagger monoidal and dagger compact closed categories are the standard settings for Categorical Quantum Mechanics (CQM). These settings of CQM are categorical proof theories of compact dagger linear logic and are motivated by the interpretation of quantum systems in the category of finite dimensional Hilbert spaces. In this talk, I describe a new non-compact (infinite-dimensional) framework called Mixed Unitary Categories (MUCs) with examples built on linearly distributive and *-autonomous categories which are categorical proof theories of (non-compact) multiplicative linear logic. This talk is based on the first part of my thesis.
The notion of complimentary observables lies at the heart of quantum mechanics: two quantum observables A and B are complementary if measuring one increases the uncertainty regarding the value of the other. In this talk, I show that complementary observables and classical non-linearity are related by proving that every complementary pair of observables can be viewed as the exponential modalities - ! and ? - of linear logic "compacted" into the unitary core of the MUC, thereby exhibiting a complementary system as arising via the compaction of distinct systems of arbitrary dimensions. The machinery to arrive at this result involves linear monoids, linear comonoids, linear bialgebras and dagger-exponential modalities.
In physics, a resource theory is used to model physical systems for which certain transformations are considered to be "free of cost". For example, on a hot summer day, cooling down the water requires energy (used by a refrigerator), hence is not free. However, a glass of chilled water warming up to room temperature is a free transformation. Resources are states of such a system. Monotones assigns a real number to each resource based on their value or utility. A problem in physics is that, can monotones on one resource theory be extended to another in case the two theories are related.
Gour and Tomamichel studied the problem of extending monotones using set-theoretical framework when a resource theory embeds fully and faithfully into the larger theory. One can generalize the problem of computing monotone extensions to scenarios when there exists a functorial transformation of one resource theory to another instead of just a full and faithful inclusion. In this talk, I show that (point-wise) Kan extensions provide a precise categorical framework to describe and compute such extensions of monotones.
To set up monotone extensions using Kan extensions, we introduce partitioned categories (pCat) as a framework for resource theories and pCat functors to formalize relationship between resource theories. We describe monotones as pCat functors into ([0,∞],≤), and describe extending monotones along any pCat functor using Kan extensions. We show how our framework works by applying it to extend entanglement monotones for bipartite pure states to bipartite mixed states, to extend classical divergences to the quantum setting, and to extend a non-uniformity monotone from classical probabilistic theory to quantum theory.