Dagger linear logic for categorical quantum mechanics

Whats in these talks? Linear logic, linearly distributive categories (LDCs) and properties, dagger LDCs, mixed unitary categories, linear duals, linear monoids, linear comonoids, linear bialgebras, dagger exponential LDCs.


These talks were presented as two-days tutorial at the 29th Foundational Methods in Computer Science Workshop held at Kananaskis, Canada in June 2022. 

FMCS2022-part1.pdf
FMCS2022-part2.pdf

Abstract: This talk was entirely based on my thesis.

(Part 1) 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 tutorial, I will describe a new non-compact 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.

(Part 2) One of the motivations to develop a non-compact framework is to accommodate arbitrary dimensional systems in CQM in a structurally seamless manner. 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. I will 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.