This is the first paper in a series where we generalize the Categorical Quantum Mechanics program (due to Abramsky, Coecke, et al) to braided systems. In our view a uniform description of quantum information for braided systems has not yet emerged. The picture is complicated by a diversity of examples that lacks a unifying framework for proving theorems and discovering new protocols. We use category theory to construct a high-level language that abstracts the quantum mechanical properties of braided systems. We exploit this framework to propose an axiomatic description of braided quantum information intended for topological quantum computation. In this installment we first generalize the primordial Abramsky-Coecke "quantum information flow" paradigm from compact closed categories to right-rigid strict monoidal categories. We then study dagger structures for rigid and/or braided categories and formulate a graphical dagger calculus. We then propose two generalizations of strongly compact closed categories. Finally we study partial traces in the context of dagger categories.
This is the first paper in a series where we generalize the Categorical Quantum Mechanics program (due to Abramsky, Coecke, et al) to braided systems. In our view a uniform description of quantum information for braided systems has not yet emerged. The picture is complicated by a diversity of examples that lacks a unifying framework for proving theorems and discovering new protocols. We use category theory to construct a high-level language that abstracts the quantum mechanical properties of braided systems. We exploit this framework to propose an axiomatic description of braided quantum information intended for topological quantum computation. In this installment we first generalize the primordial Abramsky-Coecke "quantum information flow" paradigm from compact closed categories to right-rigid strict monoidal categories. We then study dagger structures for rigid and/or braided categories and formulate a graphical dagger calculus. We then propose two generalizations of strongly compact closed categories. Finally we study partial traces in the context of dagger categories.
This paper explores the application of category theory to provide a semantic framework for quantum vector spaces, which are fundamental to quantum mechanics and quantum information. We move beyond the traditional algebraic and analytical descriptions of Hilbert spaces to adopt a more abstract, compositional, and graphical approach rooted in monoidal categories. This categorical perspective allows for a unified understanding of quantum phenomena, including superposition, entanglement, and measurement, by representing quantum systems as objects and processes as morphisms. We delve into the concept of compact closed categories and dagger symmetric monoidal categories as the appropriate mathematical structures to capture the essential features of quantum theory, such as duality, adjoints, and the tensor product for composite systems. Furthermore, the paper discusses how graphical calculi, arising from these categorical structures, offer an intuitive and rigorous method for reasoning about quantum protocols and computations, facilitating the design and verification of quantum algorithms. By providing a high-level, axiomatic framework, categorical semantics clarifies the foundational principles of quantum mechanics and opens new avenues for developing quantum programming languages and understanding the interplay between quantum information and computation.
As shown by Abramsky and Coecke, quantum mechanics can be studied in terms of dagger compact closed categories with biproducts. Within this structure, many well-known quantum protocols can be described and their validity can be shown by establishing the commutativity of certain diagrams in that category. In this paper, we propose an explicit realisation of a category with enough structure to check the validity of a certain class of quantum protocols. In order to do this, we construct a category based on 1-dimensional cobordisms with attached elements of a certain group freely generated by a finite set. We use this category as a graphical language, and we show that it is dagger compact closed with biproducts. Then, relying on the coherence result for compact closed categories, proved by Kelly and Laplaza, we show the coherence result, which enables us to check the validity of quantum protocols just by drawing diagrams. In particular, we show the validity of quantum teleportation, entanglement swapping (as formulated in the work of Abramsky and Coecke) and superdense coding protocol.
Categorical quantum mechanics exploits the dagger compact closed structure of finite dimensional Hilbert spaces, and uses the graphical calculus of string diagrams to facilitate reasoning about finite dimensional processes. A significant portion of quantum physics, however, involves reasoning about infinite dimensional processes, and it is well-known that the category of all Hilbert spaces is not compact closed. Thus, a limitation of using dagger compact closed categories is that one cannot directly accommodate reasoning about infinite dimensional processes. A natural categorical generalization of compact closed categories, in which infinite dimensional spaces can be modelled, is *-autonomous categories and, more generally, linearly distributive categories. This article starts the development of this direction of generalizing categorical quantum mechanics. An important first step is to establish the behaviour of the dagger in these more general settings. Thus, these notes simultaneously develop the categorical semantics of multiplicative dagger linear logic. The notes end with the definition of a mixed unitary category. It is this structure which is subsequently used to extend the key features of categorical quantum mechanics.
Dagger compact closed categories were recently introduced by Abramsky and Coecke, under the name “strongly compact closed categories”, as an axiomatic framework for quantum mechanics. We present a graphical language for dagger compact closed categories, and sketch a proof of its completeness for equational reasoning. We give a general construction, the CPM construction, which associates to each dagger compact closed category its “category of completely positive maps”, and we show that the resulting category is again dagger compact closed. We apply these ideas to Abramsky and Coecke's interpretation of quantum protocols, and to D'Hondt and Panangaden's predicate transformer semantics.
This thesis is a study of the construction and representation of typed models of quantum mechanics for use in quantum computation. We introduce logical and graphical syntax for quantum mechanical processes and prove that these formal systems provide sound and complete representations of abstract quantum mechanics. In addition, we demonstrate how these representations may be used to reason about the behaviour of quantum computational processes. Quantum computation is presently mired in low-level formalisms, mostly derived directly from matrices over Hilbert spaces. These formalisms are an obstacle to the full understanding and exploitation of quantum effects in informatics since they obscure the essential structure of quantum states and processes. The aim of this work is to introduce higher level tools for quantum mechanics which will be better suited to computation than those presently employed in the field. Inessential details of Hilbert space representations are removed and the informatic structures are presented directly. Entangled states are particularly important in this treatment, as is appropriate, since entanglement is a fundamental driver of quantum computation. The benefits two-fold: as well as producing foundational tools for the study of quantum computation this work also connects quantum mechanics to mainstream areas of computer science such as categorical logic, type theory, program language semantics, and rewriting. We describe, following Abramsky and Coecke, how quantum mechanics may be carried out without reference to Hilbert space, in a strongly compact closed category. In particular we show how to freely construct a categorical model of abstract quantum mechanics from an arbitrary category. We introduceMultiplicative Categorical Quantum Logic (mCQL), a sequent calculus whose proof rules capture the structure of compact closed categories. This sequent calculus is interpreted in a freely generated compact closed category, and its semantics is sound with respect to cut elimination. We define an equivalent graphical syntax, similar to linear logic’s proof-nets, and prove that these proof-nets provide a full and faithful representation of any freely generated compact closed category. Further analysis of the structure of quantum states which correspond to mCQL proofs using multiplicative linear logic shows that the linear type system describes the quantum entanglement found in such states. We show that the entanglement present in these states is always of a particularly simple form: collections of entangled pairs. In order to tackle arbitrary entanglement, we generalise the work of Kelly and Laplaza to give a representation theorem for the free compact closed category by a polycategory. Such categories are shown to be equivalent to a generalised system of proof-nets whose axioms may have more than one premise
We establish a rigorous connection between Relational Quantum Dynamics (RQD) and Categorical Quantum Mechanics (CQM) by formally showing that the category Q of quantum processes in RQD can be endowed with the structure of a dagger compact category. In particular, we demonstrate that Q satisfies the axioms of a dagger symmetric monoidal category with compact closure, mirroring the standard categorical formalism for quantum theory. Within this framework, key physical features of quantum mechanics, such as the transfer of awareness (information) in interactions, the no-cloning theorem, and the quantum teleportation protocol, are naturally expressed and interpreted. We define the categorical structures and illustrate the concepts with examples from quantum computing and quantum information. These examples highlight how RQD’s relational worldview aligns with CQM’s diagrammatic and algebraic characterization of quantum processes, thus providing a robust unified description. The results underscore that the RQD category Q not only has the formal properties of a dagger compact category but also that this structure provides clear insight into quantum informational tasks and no-go theorems, while incorporating the notion of observer-dependent reality in RQD via a functional mapping of awareness.