We present a both simple and comprehensive graphical calculus for quantum computing. In particular, we axiomatize the notion of an environment, which together with the earlier introduced axiomatic notion of classical structure enables us to define classical channels, quantum measurements and classical control. If we moreover adjoin the earlier introduced axiomatic notion of complementarity, we obtain sufficient structural power for constructive representation and correctness derivation of typical quantum informatic protocols.
We present a both simple and comprehensive graphical calculus for quantum computing. In particular, we axiomatize the notion of an environment, which together with the earlier introduced axiomatic notion of classical structure enables us to define classical channels, quantum measurements and classical control. If we moreover adjoin the earlier introduced axiomatic notion of complementarity, we obtain sufficient structural power for constructive representation and correctness derivation of typical quantum informatic protocols.
In recent work, several researchers including the authors have developed a categorical formalization of quantum mechanics in terms of symmetric monoidal dagger categories. In this framework, classical data turned out to be represented by an algebraic structure, that of special commutative dagger Frobenius algebras. This structure captures the distinct capabilities that apply to classical data – that they can be copied and deleted. In the present paper, we provide categorical semantics and diagrammatic representations of deterministic, nondeterministic, and probabilistic operations over classical data represented in this way. Moreover, a combination of some fundamental categorical constructions (the Kleisli construction of the category of free algebras and the Grothendieck construction of the total category of an indexed category) with the specific categorical presentations of pure and mixed quantum states provides a resource-sensitive categorical account of classical control of quantum data and of classical data resulting from quantum measurements, as well as of the classical data processing that may happen in between measurements and controls. Along the way we also discover some apparently novel quantum typing structures. One of the salient features of categorical quantum mechanics is still its graphic calculus, which allows succinct presentations of diverse quantum protocols. The elements of an abstract stochastic calculus are beginning to emerge from it, pointing toward convenient refinements of resource-sensitive logics that are hoped to capture the probabilistic content and limited observability of quantum data.
This paper has two tightly intertwined aims: (i) to introduce an intuitive and universal graphical calculus for multi-qubit systems, the ZX -calculus, which greatly simplifies derivations in the area of quantum computation and information. (ii) To axiomatize complementarity of quantum observables within a general framework for physical theories in terms of dagger symmetric monoidal categories. We also axiomatize phase shifts within this framework. Using the well-studied canonical correspondence between graphical calculi and dagger symmetric monoidal categories, our results provide a purely graphical formalisation of complementarity for quantum observables. Each individual observable, represented by a commutative special dagger Frobenius algebra, gives rise to an Abelian group of phase shifts, which we call the phase group. We also identify a strong form of complementarity, satisfied by the Z - and X -spin observables, which yields a scaled variant of a bialgebra.
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
Categorical quantum mechanics is a way of formalising the structural features of quantum theory using category theory. It uses compound systems as the primitive notion, which is formalised by using symmetric monoidal categories. This leads to an elegant formalism for describing quantum protocols such as quantum teleportation. In particular, categorical quantum mechanics provides a graphical calculus that exposes the information flow of such protocols in an intuitive way. However, the graphical calculus also reveals surprising features of these protocols; for example, in the quantum teleportation protocol, information appears to flow `backwards-in-time'. This leads to question of how causal structure can be described within categorical quantum mechanics, and how this might lead to insight regarding the structural compatibility between quantum theory and relativity. This thesis is concerned with the project of formalising causal structure in categorical quantum mechanics. We begin by studying an abstract view of Bell-type experiments, as described by `no-signalling boxes', and we show that under time-reversal no-signalling boxes generically become signalling. This conflicts with the underlying symmetry of relativistic causal structure. This leads us to consider the framework of categorical quantum mechanics from the perspective of relativistic causal structure. We derive the properties that a symmetric monoidal category must satisfy in order to describe systems in such a background causal structure. We use these properties to define a new type of category, and this provides a formal framework for describing protocols in spacetime. We explore this new structure, showing how it leads to an understanding of the counter-intuitive information flow of protocols in categorical quantum mechanics. We then find that the formal properties of our new structure are naturally related to axioms for reconstructing quantum theory, and we show how a reconstruction scheme based on purification can be formalised using the structures of categorical quantum mechanics. Finally, we discuss the philosophical aspects of using category theory to describe fundamental physics. We consider a recent argument that category-theoretic formulations of physics, such as categorical quantum mechanics, can be used to support a variant of structural realism. We argue against this claim. The work of this thesis suggests instead that the philosophy of categorical quantum mechanics is subtler than either operationalism or realism.
Categorical quantum mechanics is a way of formalising the structural features of quantum theory using category theory. It uses compound systems as the primitive notion, which is formalised by using symmetric monoidal categories. This leads to an elegant formalism for describing quantum protocols such as quantum teleportation. In particular, categorical quantum mechanics provides a graphical calculus that exposes the information flow of such protocols in an intuitive way.
However, the graphical calculus also reveals surprising features of these protocols; for example, in the quantum teleportation protocol, information appears to flow `backwards-in-time'. This leads to question of how causal structure can be described within categorical quantum mechanics, and how this might lead to insight regarding the structural compatibility between quantum theory and relativity.
This thesis is concerned with the project of formalising causal structure in categorical quantum mechanics.
We begin by studying an abstract view of Bell-type experiments, as described by `no-signalling boxes', and we show that under time-reversal no-signalling boxes generically become signalling. This conflicts with the underlying symmetry of relativistic causal structure.
This leads us to consider the framework of categorical quantum mechanics from the perspective of relativistic causal structure. We derive the properties that a symmetric monoidal category must satisfy in order to describe systems in such a background causal structure.
We use these properties to define a new type of category, and this provides a formal framework for describing protocols in spacetime. We explore this new structure, showing how it leads to an understanding of the counter-intuitive information flow of protocols in categorical quantum mechanics. We then find that the formal properties of our new structure are naturally related to axioms for reconstructing quantum theory, and we show how a reconstruction scheme based on purification can be formalised using the structures of categorical quantum mechanics. Finally, we discuss the philosophical aspects of using category theory to describe fundamental physics. We consider a recent argument that category-theoretic formulations of physics, such as categorical quantum mechanics, can be used to support a variant of structural realism. We argue against this claim. The work of this thesis suggests instead that the philosophy of categorical quantum mechanics is subtler than either operationalism or realism.
We propose a higher semantics for the description of quantum protocols, which deals with quantum and classical information in a unified way. Central to our approach is the modelling of classical data by information transfer to the environment, and the use of 2-category theory to formalize the resulting framework. This 2-categorical semantics has a graphical calculus, the diagrams of which correspond exactly to physically-implementable quantum procedures. Quantum teleportation in its most general sense is reformulated as the ability to remove correlations between a quantum system and its environment, and is represented by an elegant graphical identity. We use this new formalism to describe two new families of quantum protocols.