Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Lecture notes in computer science

Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation

Lucas Dixon, Ross Duncan

Published Jul 26, 2008• 8 citations
Publisher
DOI
10.1007/978-3-540-85110-3_8

Related papers

Graphical reasoning in compact closed categories for quantum computation

Lucas Dixon, Ross Duncan

arXiv:0902.0514•Annals of Mathematics and Artificial Intelligence•May 1, 2009•43 citations

Types for Quantum Computing

Duncan, Ross

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

•Jan 1, 2006•34 citations

Compact Representations for the Design of Quantum Logic

Philipp Niemann, Robert Wille

SpringerBriefs in physics•Jan 1, 2017•3 citations

Projective representations of quantum logics

Stanley Gudder

International Journal of Theoretical Physics•Apr 1, 1970•7 citations

Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing

Aleks Kissinger

This work is about diagrammatic languages, how they can be represented, and what they in turn can be used to represent. More specifically, it focuses on representations and applications of string diagrams. String diagrams are used to represent a collection of processes, depicted as "boxes" with multiple (typed) inputs and outputs, depicted as "wires". If we allow plugging input and output wires together, we can intuitively represent complex compositions of processes, formalised as morphisms in a monoidal category. [...] The first major contribution of this dissertation is the introduction of a discretised version of a string diagram called a string graph. String graphs form a partial adhesive category, so they can be manipulated using double-pushout graph rewriting. Furthermore, we show how string graphs modulo a rewrite system can be used to construct free symmetric traced and compact closed categories on a monoidal signature. The second contribution is in the application of graphical languages to quantum information theory. We use a mixture of diagrammatic and algebraic techniques to prove a new classification result for strongly complementary observables. [...] We also introduce a graphical language for multipartite entanglement and illustrate a simple graphical axiom that distinguishes the two maximally-entangled tripartite qubit states: GHZ and W. [...] The third contribution is a description of two software tools developed in part by the author to implement much of the theoretical content described here. The first tool is Quantomatic, a desktop application for building string graphs and graphical theories, as well as performing automated graph rewriting visually. The second is QuantoCoSy, which performs fully automated, model-driven theory creation using a procedure called conjecture synthesis.

arXiv:1203.0202•Mar 1, 2012•44 citations

Dagger Compact Closed Categories and Completely Positive Maps

Peter Selinger

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.

Electronic Notes in Theoretical Computer Science•Mar 1, 2007•391 citations
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
This work is about diagrammatic languages, how they can be represented, and what they in turn can be used to represent. More specifically, it focuses on representations and applications of string diagrams. String diagrams are used to represent a collection of processes, depicted as "boxes" with multiple (typed) inputs and outputs, depicted as "wires". If we allow plugging input and output wires together, we can intuitively represent complex compositions of processes, formalised as morphisms in a monoidal category. [...] The first major contribution of this dissertation is the introduction of a discretised version of a string diagram called a string graph. String graphs form a partial adhesive category, so they can be manipulated using double-pushout graph rewriting. Furthermore, we show how string graphs modulo a rewrite system can be used to construct free symmetric traced and compact closed categories on a monoidal signature. The second contribution is in the application of graphical languages to quantum information theory. We use a mixture of diagrammatic and algebraic techniques to prove a new classification result for strongly complementary observables. [...] We also introduce a graphical language for multipartite entanglement and illustrate a simple graphical axiom that distinguishes the two maximally-entangled tripartite qubit states: GHZ and W. [...] The third contribution is a description of two software tools developed in part by the author to implement much of the theoretical content described here. The first tool is Quantomatic, a desktop application for building string graphs and graphical theories, as well as performing automated graph rewriting visually. The second is QuantoCoSy, which performs fully automated, model-driven theory creation using a procedure called conjecture synthesis.
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.