Book contents
- Frontmatter
- Contents
- Contributors
- Preface
- 1 No-Cloning in Categorical Quantum Mechanics
- 2 Classical and Quantum Structuralism
- 3 Generalized Proof-Nets for Compact Categories with Biproducts
- 4 Quantum Lambda Calculus
- 5 The Quantum IO Monad
- 6 Abstract Interpretation Techniques for Quantum Computation
- 7 Extended Measurement Calculus
- 8 Predicate Transformer Semantics of Quantum Programs
- 9 The Structure of Partial Isometries
- 10 Temporal Logics for Reasoning about Quantum Systems
- 11 Specification and Verification of Quantum Protocols
- Index
- References
3 - Generalized Proof-Nets for Compact Categories with Biproducts
Published online by Cambridge University Press: 05 July 2014
- Frontmatter
- Contents
- Contributors
- Preface
- 1 No-Cloning in Categorical Quantum Mechanics
- 2 Classical and Quantum Structuralism
- 3 Generalized Proof-Nets for Compact Categories with Biproducts
- 4 Quantum Lambda Calculus
- 5 The Quantum IO Monad
- 6 Abstract Interpretation Techniques for Quantum Computation
- 7 Extended Measurement Calculus
- 8 Predicate Transformer Semantics of Quantum Programs
- 9 The Structure of Partial Isometries
- 10 Temporal Logics for Reasoning about Quantum Systems
- 11 Specification and Verification of Quantum Protocols
- Index
- References
Summary
Abstract
Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic.We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets and show that the dynamic behavior of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut-elimination procedure is strongly normalizing: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as nonlogical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.
3.1 Introduction
3.1.1 Logic, Processes, and Categories
Birkhoff and von Neumann initiated the logical study of quantum mechanics in their well-known 1936 paper. They constructed a logic by assigning a proposition letter to each observable property of a given quantum system and studied negations, conjunctions, and disjunctions of these properties. The resulting lattice is nondistributive, and so the heart of what is called “quantum logic” is the study of various kinds of nondistributive lattices.
- Type
- Chapter
- Information
- Semantic Techniques in Quantum Computation , pp. 70 - 134Publisher: Cambridge University PressPrint publication year: 2009
References
- 3
- Cited by