版权所有:内蒙古大学图书馆 技术提供:维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
作者机构:Graduate Program in Computer Science CalgaryAB Canada
出 版 物:《arXiv》 (arXiv)
年 卷 期:2023年
核心收录:
摘 要:This thesis develops the categorical proof theory for the non-compact multiplicative dagger (†) linear logic, and investigates its applications to Categorical Quantum Mechanics (CQM). The existing frameworks of CQM are categorical proof theories of compact †-linear logic, and are motivated by the interpretation of quantum systems in the category of finite dimensional Hilbert spaces. This thesis describes a new non-compact framework called Mixed Unitary Categories which can accommodate infinite dimensional systems, and develops models for the framework. To this end, it builds on linearly distributive categories, and ∗-autonomous categories which are categorical proof theories of (non-compact) multiplicative linear logic. The proof theory of non-compact †-linear logic is obtained from the basic setting of an LDC by adding a dagger functor satisfying appropriate coherences to give a †-LDC. From every (isomix) †-LDC one can extract a canonical unitary core which up to equivalence is the traditional CQM framework of †-monoidal categories. This leads to the framework of Mixed Unitary Categories (MUCs): every MUC contains a (compact) unitary core which is extended by a (non-compact) isomix †-LDC. Various models of MUCs based on Finiteness Spaces, Chu spaces, Hopf modules, etc., are developed in this thesis. This thesis also generalizes the key algebraic structures of CQM, such as observables, measurement, and complementarity, to MUC framework. Furthermore, using the MUC framework, this thesis establishes a connection between the complementary observables of quantum mechanics and the exponential modalities of linear logic. © 2023, CC BY.