ZX-calculus publications

2020

• There and back again: A circuit extraction tale, Miriam Backens, Hector Miller-Bakewell, Giovanni de Felice, Leo Lobski and John van de Wetering, arXiv preprint arXiv:2003.01664 (2020).
  Keywords: ZX-Calculus, circuit-extraction, One-way computation, gflow, circuit optimisation. Abstract   Bibdata
  We give the first circuit-extraction algorithm to work for one-way computations containing measurements in all three planes and having gflow. The algorithm is efficient and the resulting circuits do not contain ancillae. One-way computations are represented using the ZX-calculus, hence the algorithm also represents the most general known procedure for extracting circuits from ZX-diagrams. In developing this algorithm, we generalise several concepts and results previously known for computations containing only XY-plane measurements. We bring together several known rewrite rules for measurement patterns and formalise them in a unified notation using the ZX-calculus. These rules are used to simplify measurement patterns by reducing the number of qubits while preserving both the semantics and the existence of gflow. The results can be applied to circuit optimisation by translating circuits to patterns and back again.

  @article{hobbit2020,
      author = {Backens, Miriam  and  Miller-Bakewell, Hector and  de Felice, Giovanni and Lobski, Leo and van de Wetering, John},
      title = {There and back again: A circuit extraction tale},
      year = {2020},
      journal = {arXiv preprint arXiv:2003.01664},
      link = {https://arxiv.org/abs/2003.01664},
      keywords = {ZX-Calculus,circuit-extraction, One-way computation,gflow,circuit optimisation },
      abstract = {We give the first circuit-extraction algorithm to work for
  one-way computations containing measurements in all three planes and having
  gflow. The algorithm is efficient and the resulting circuits do not contain
  ancillae. One-way computations are represented using the ZX-calculus, hence the
  algorithm also represents the most general known procedure for extracting
  circuits from ZX-diagrams. In developing this algorithm, we generalise several
  concepts and results previously known for computations containing only XY-plane
  measurements. We bring together several known rewrite rules for measurement
  patterns and formalise them in a unified notation using the ZX-calculus. These
  rules are used to simplify measurement patterns by reducing the number of
  qubits while preserving both the semantics and the existence of gflow. The
  results can be applied to circuit optimisation by translating circuits to
  patterns and back again.}
  }
  
  

• The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford, Renaud Vilmart, arXiv preprint arXiv:2003.05678 (2020).
  Keywords: ZH-Calculus, Clifford, Sum-Over-Paths. Abstract   Bibdata
  We show that the formalism of "Sum-Over-Path" (SOP), used for symbolically representing linear maps or quantum operators, together with a proper rewrite system, has a structure of dagger-compact PROP. Several consequences arise from this observation: 1) Morphisms of SOP are very close to the diagrams of the graphical calculus called ZH-Calculus, so we give a system of interpretation between the two; 2) A construction, called the discard construction, can be applied to enrich the formalism so that, in particular, it can represent the quantum measurement. We also enrich the rewrite system so as to get the completeness of the Clifford fragments of both the initial formalism and its enriched version.

  @article{pathsRenaud,
      author = {Renaud Vilmart},
      title = {The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford},
      year = {2020},
      journal = {arXiv preprint arXiv:2003.05678},
      link = {https://arxiv.org/abs/2003.05678},
      keywords = {ZH-Calculus,Clifford,Sum-Over-Paths },
      abstract = {We show that the formalism of "Sum-Over-Path" (SOP), used for symbolically representing linear maps or quantum operators, together with a proper rewrite system, has a structure of dagger-compact PROP. Several consequences arise from this observation: 1) Morphisms of SOP are very close to the diagrams of the graphical calculus called ZH-Calculus, so we give a system of interpretation between the two; 2) A construction, called the discard construction, can be applied to enrich the formalism so that, in particular, it can represent the quantum measurement. We also enrich the rewrite system so as to get the completeness of the Clifford fragments of both the initial formalism and its enriched version.}
  }
  
  

• Entanglement and Quaternions: The graphical calculus ZQ, Hector Miller-Bakewell, arXiv preprint arXiv:2003.09999 (2020).
  Keywords: ZQ-Calculus, Quaternions. Abstract   Bibdata
  Graphical calculi are vital tools for representing and reasoning about quantum circuits and processes. Some are not only graphically intuitive but also logically complete. The best known of these is the ZX-calculus, which is an industry candidate for an Intermediate Representation; a language that sits between the algorithm designer's intent and the quantum hardware's gate instructions. The ZX calculus, built from generalised Z and X rotations, has difficulty reasoning about arbitrary rotations. This contrasts with the cross-hardware compiler TriQ which uses these arbitrary rotations to exploit hardware efficiencies. In this paper we introduce the graphical calculus ZQ, which uses quaternions to represent these arbitrary rotations, similar to TriQ, and the phase-free Z spider to represent entanglement, similar to ZX. We show that this calculus is sound and complete for qubit quantum computing, while also showing that a fully spider-based representation would have been impossible. This new calculus extends the zoo of qubit graphical calculi, each with different strengths, and we hope it will provide a common language for the optimisation procedures of both ZX and TriQ.

  @article{ZQHector,
      author = {Hector Miller-Bakewell},
      title = {Entanglement and Quaternions: The graphical calculus ZQ},
      year = {2020},
      journal = {arXiv preprint arXiv:2003.09999},
      link = {https://arxiv.org/abs/2003.09999},
      keywords = {ZQ-Calculus,Quaternions },
      abstract = {Graphical calculi are vital tools for representing and reasoning about quantum circuits and processes. Some are not only graphically intuitive but also logically complete. The best known of these is the ZX-calculus, which is an industry candidate for an Intermediate Representation; a language that sits between the algorithm designer's intent and the quantum hardware's gate instructions. The ZX calculus, built from generalised Z and X rotations, has difficulty reasoning about arbitrary rotations. This contrasts with the cross-hardware compiler TriQ which uses these arbitrary rotations to exploit hardware efficiencies. In this paper we introduce the graphical calculus ZQ, which uses quaternions to represent these arbitrary rotations, similar to TriQ, and the phase-free Z spider to represent entanglement, similar to ZX. We show that this calculus is sound and complete for qubit quantum computing, while also showing that a fully spider-based representation would have been impossible. This new calculus extends the zoo of qubit graphical calculi, each with different strengths, and we hope it will provide a common language for the optimisation procedures of both ZX and TriQ. }
  }
  
  

2019

• ZX-calculus over arbitrary commutative rings and semirings, Quanlong Wang, arXiv preprint arXiv:1912.01003 (2019).
  Keywords: rings, semirings, ZX-calculus. Abstract   Bibdata
  In this extended abstract we give an axiomatisation of ZX-calculus over arbi-trary commutative rings and semirings respectively. By a normal form inspiredfrom matrix elementary operations such as row addition and row multiplication,we can obtain that these versions of ZX-calculus are still universal and complete.

  @article{ringZX,
      author = { Wang, Quanlong},
      title = {ZX-calculus over arbitrary commutative rings and semirings},
      year = {2019},
      journal = {arXiv preprint arXiv:1912.01003},
      link = {https://arxiv.org/abs/1912.01003},
      keywords = {rings,semirings, ZX-calculus},
      abstract = {In this extended abstract we give an axiomatisation of ZX-calculus over arbi-trary commutative rings and semirings respectively. By a normal form inspiredfrom matrix elementary operations such as row addition and row multiplication,we can obtain that these versions of ZX-calculus are still universal and complete.  }
  }
  
  

• Efficient compression of quantum braided circuits, Michael Hanks, Marta P. Estarellas, William J. Munro and Kae Nemoto, arXiv preprint arXiv:1912.11503 (2019).
  Keywords: braiding, circuites, ZX-calculus. Abstract   Bibdata
  Mapping a quantum algorithm to any practical large-scale quantum computer will require a sequence of compilations and optimizations. At the level of fault-tolerant encoding, one likely requirement of this process is the translation into a topological circuit, for which braided circuits represent one candidate model. Given the large overhead associated with encoded circuits, it is paramount to reduce their size in terms of computation time and qubit number through circuit compression. While these optimizations have typically been performed in the language of 3-dimensional diagrams, such a representation does not allow an efficient, general and scalable approach to reduction or verification. We propose the use of the ZX-calculus as an intermediate language for braided circuit compression, demonstrating advantage by comparing results using this approach with those previously obtained for the compression of |A⟩ and |Y⟩ state distillation circuits. We then provide a rough benchmark of our method against a small set of Clifford+T circuits, yielding compression percentages of ∼77%. Our results suggest that the overheads of braided, defect-based circuits are comparable to those of their lattice-surgery counterparts, restoring the potential of this model for surface code quantum computation.

  @article{braidedCircuits,
      author = {Hanks,Michael and P. Estarellas,Marta and   Munro,William J. and  Nemoto, Kae},
      title = {Efficient compression of quantum braided circuits},
      year = {2019},
      journal = {arXiv preprint arXiv:1912.11503},
      link = {https://arxiv.org/abs/1912.11503},
      keywords = {braiding, circuites, ZX-calculus},
      abstract = {Mapping a quantum algorithm to any practical large-scale quantum computer will require a sequence of compilations and optimizations. At the level of fault-tolerant encoding, one likely requirement of this process is the translation into a topological circuit, for which braided circuits represent one candidate model. Given the large overhead associated with encoded circuits, it is paramount to reduce their size in terms of computation time and qubit number through circuit compression. While these optimizations have typically been performed in the language of 3-dimensional diagrams, such a representation does not allow an efficient, general and scalable approach to reduction or verification. We propose the use of the ZX-calculus as an intermediate language for braided circuit compression, demonstrating advantage by comparing results using this approach with those previously obtained for the compression of |A⟩ and |Y⟩ state distillation circuits. We then provide a rough benchmark of our method against a small set of Clifford+T circuits, yielding compression percentages of ∼77\%. Our results suggest that the overheads of braided, defect-based circuits are comparable to those of their lattice-surgery counterparts, restoring the potential of this model for surface code quantum computation.   }
  }
  
  

• An algebraic axiomatisation of ZX-calculus, Quanlong Wang, arXiv preprint arXiv:1911.06752 (2019).
  Keywords: axiomatisation, ZX-calculus, ZH-calculus. Abstract   Bibdata
  In this paper we give an algebraic complete axiomatisation of ZX-calculus in the sense that there are only ring operations involved for phases, without any need of trigonometry functions such as sin and cos, in contrast to previous universally complete axiomatisations of ZX-calculus. With this algebraic axiomatisation of ZX-calculus, we are able to establish an invertible translation from ZH-calculus to ZX-calculus and to derive all the ZX-translated rules of ZH-calculus. As a consequence, we have a great benefit that all techniques obtained in ZH-calculus can be transplanted to ZX-calculus.

  @article{algebraicZX,
      author = {Wang, Quanlong},
      title = {An algebraic axiomatisation of ZX-calculus},
      year = {2019},
      journal = {arXiv preprint arXiv:1911.06752},
      link = {https://arxiv.org/abs/1911.06752},
      keywords = {axiomatisation, ZX-calculus, ZH-calculus},
      abstract = {In this paper we give an algebraic complete axiomatisation of ZX-calculus in the sense that there are only ring operations involved for phases, without any need of trigonometry functions such as sin and cos, in contrast to previous universally complete axiomatisations of ZX-calculus. With this algebraic axiomatisation of ZX-calculus, we are able to establish an invertible translation from ZH-calculus to ZX-calculus and to derive all the ZX-translated rules of ZH-calculus. As a consequence, we have a great benefit that all techniques obtained in ZH-calculus can be transplanted to ZX-calculus. }
  }
  
  

• Techniques to reduce π/4-parity phase circuits, motivated by the ZX calculus, Niel de Beaudrap, Xiaoning Bian and Quanlong Wang, arXiv preprint arXiv:1911.09039 (2019).
  Keywords: phase circuits, ZX-calculus. Abstract   Bibdata
  To approximate arbitrary unitary transformations on one or more qubits, one must perform transformations which are outside of the Clifford group. The gate most commonly considered for this purpose is the T=diag(1,exp(iπ/4)) gate. As T gates are computationally expensive to perform fault-tolerantly in the most promising error-correction technologies, minimising the "T-count" (the number of T gates) required to realise a given unitary in a Clifford+T circuit is of great interest. We describe techniques to find circuits with reduced T-count in unitary circuits, which develop on the ideas of Heyfron and Campbell [arXiv:1712.01557] with the help of the ZX calculus. Following [arXiv:1712.01557], we reduce the problem to that of minimising the T count of a CNOT+T circuit. The ZX calculus motivates a further reduction to simplifying a product of commuting "π/4-parity-phase" operations: diagonal unitary transformations which induce a relative phase of exp(iπ/4) depending on the outcome of a parity computation on the standard basis (which motivated Kissinger and van de Wetering [1903.10477] to introduce "phase gadgets"). For a number of standard benchmark circuits, we show that these techniques --- in some cases supplemented by the TODD subroutine of Heyfron and Campbell [arXiv:1712.01557] --- yield T-counts comparable to or better than the best previously known results.

  @article{pi4parity,
      author = {de Beaudrap, Niel and Bian, Xiaoning and Wang, Quanlong},
      title = {Techniques to reduce \pi/4-parity phase circuits, motivated by the ZX calculus},
      year = {2019},
      journal = {arXiv preprint arXiv:1911.09039},
      link = {https://arxiv.org/abs/1911.09039},
      keywords = {phase circuits, ZX-calculus},
      abstract = {To approximate arbitrary unitary transformations on one or more qubits, one must perform transformations which are outside of the Clifford group. The gate most commonly considered for this purpose is the T=diag(1,exp(i\pi/4)) gate. As T gates are computationally expensive to perform fault-tolerantly in the most promising error-correction technologies, minimising the "T-count" (the number of T gates) required to realise a given unitary in a Clifford+T circuit is of great interest. We describe techniques to find circuits with reduced T-count in unitary circuits, which develop on the ideas of Heyfron and Campbell [arXiv:1712.01557] with the help of the ZX calculus. Following [arXiv:1712.01557], we reduce the problem to that of minimising the T count of a CNOT+T circuit. The ZX calculus motivates a further reduction to simplifying a product of commuting "\pi/4-parity-phase" operations: diagonal unitary transformations which induce a relative phase of exp(i\pi/4) depending on the outcome of a parity computation on the standard basis (which motivated Kissinger and van de Wetering [1903.10477] to introduce "phase gadgets"). For a number of standard benchmark circuits, we show that these techniques --- in some cases supplemented by the TODD subroutine of Heyfron and Campbell [arXiv:1712.01557] --- yield T-counts comparable to or better than the best previously known results.  }
  }
  
  

• A note on AND-gates in ZX-calculus: QBC-completeness and phase gadgets, Anthony Munson, Bob Coecke and Quanlong Wang, arXiv preprint arXiv:1910.06818 (2019).
  Keywords: Phase Gadget, QBC-completeness, ZX-calculus, AND-gates. Abstract   Bibdata
  In this note we exploit the utility of the triangle symbol in ZX-calculus, and its role within the ZX-representation of AND-gates in particular. First, we derive a decomposition theorem for large phase gadgets, something that is of key importance to recent developments in quantum circuit optimisation and T-count reduction in particular. Then, using the same rule set, we prove a completeness theorem for quantum Boolean circuits (QBCs), which adds to the plethora of complete reasoning systems under the umbrella of ZX-calculus.

  @article{noteOnAndGates,
      author = {Munson, Anthony and Coecke, Bob and Wang, Quanlong},
      title = {A note on AND-gates in ZX-calculus: QBC-completeness and phase gadgets},
      year = {2019},
      journal = {arXiv preprint arXiv:1910.06818},
      link = {https://arxiv.org/abs/1910.06818},
      keywords = {Phase Gadget, QBC-completeness, ZX-calculus,AND-gates},
      abstract = {In this note we exploit the utility of the triangle symbol in ZX-calculus, and its role within the ZX-representation of AND-gates in particular. First, we derive a decomposition theorem for large phase gadgets, something that is of key importance to recent developments in quantum circuit optimisation and T-count reduction in particular. Then, using the same rule set, we prove a completeness theorem for quantum Boolean circuits (QBCs), which adds to the plethora of complete reasoning systems under the umbrella of ZX-calculus. }
  }
  
  

• Phase Gadget Synthesis for Shallow Circuits, Alexander Cowtan, Silas Dilkes, Ross Duncan, Will Simmons and Seyon Sivarajah, arXiv preprint arXiv:1906.01734 (2019).
  Keywords: Phase Gadget, Chemistry, ZX-calculus. Abstract   Bibdata
  We give an overview of the circuit optimisation methods used by tket, a compiler system for quantum software developed by Cambridge Quantum Computing Ltd. We focus on a novel technique based around phase gadgets, a family of multi-qubit quantum operations which occur naturally in a wide range of quantum circuits of practical interest. The phase gadgets have a simple presentation in the ZX-calculus, which makes it easy to reason about them. Taking advantage of this, we present an efficient method to translate the phase gadgets back to CNOT gates and single qubit operations suitable for execution on a quantum computer with significant reductions in gate count and circuit depth. We demonstrate the effectiveness of these methods on a quantum chemistry benchmarking set based on variational circuits for ground state estimation of small molecules.

  @article{phaseGadgetSynth,
      author = {Cowtan, Alexander and Dilkes, Silas and Duncan, Ross and Simmons, Will and Sivarajah, Seyon},
      title = {Phase Gadget Synthesis for Shallow Circuits},
      year = {2019},
      journal = {arXiv preprint arXiv:1906.01734},
      link = {https://arxiv.org/abs/1906.01734},
      keywords = {Phase Gadget, Chemistry, ZX-calculus},
      abstract = {We give an overview of the circuit optimisation methods used by tket, a compiler system for quantum software developed by Cambridge Quantum Computing Ltd. We focus on a novel technique based around phase gadgets, a family of multi-qubit quantum operations which occur naturally in a wide range of quantum circuits of practical interest. The phase gadgets have a simple presentation in the ZX-calculus, which makes it easy to reason about them. Taking advantage of this, we present an efficient method to translate the phase gadgets back to CNOT gates and single qubit operations suitable for execution on a quantum computer with significant reductions in gate count and circuit depth. We demonstrate the effectiveness of these methods on a quantum chemistry benchmarking set based on variational circuits for ground state estimation of small molecules.}
  }
  
  

• SZX-calculus: Scalable Graphical Quantum Reasoning, Titouan Carette, Dominic Horsman and Simon Perdrix, arXiv preprint arXiv:1905.00041 (2019).
  Keywords: ZX-calculus, Scalable ZX. Abstract   Bibdata
  We introduce the Scalable ZX-calculus (SZX-calculus for short), a formal and compact graphical language for the design and verification of quantum computations. The SZX-calculus is an extension of the ZX-calculus, a powerful framework that captures graphically the fundamental properties of quantum mechanics through its complete set of rewrite rules. The ZX-calculus is, however, a low level language, with each wire representing a single qubit. This limits its ability to handle large and elaborate quantum evolutions. We extend the ZX-calculus to registers of qubits and allow compact representation of sub-diagrams via binary matrices. We show soundness and completeness of the SZX-calculus and provide two examples of applications, for graph states and error correcting codes.

  @article{SZXCalculus,
      author = {Carette, Titouan and Horsman, Dominic and Perdrix, Simon},
      title = {SZX-calculus: Scalable Graphical Quantum Reasoning},
      year = {2019},
      journal = {arXiv preprint arXiv:1905.00041},
      link = {https://arxiv.org/abs/1905.00041},
      keywords = {ZX-calculus, Scalable ZX},
      abstract = {We introduce the Scalable ZX-calculus (SZX-calculus for short), a formal and compact graphical language for the design and verification of quantum computations. The SZX-calculus is an extension of the ZX-calculus, a powerful framework that captures graphically the fundamental properties of quantum mechanics through its complete set of rewrite rules. The ZX-calculus is, however, a low level language, with each wire representing a single qubit. This limits its ability to handle large and elaborate quantum evolutions. We extend the ZX-calculus to registers of qubits and allow compact representation of sub-diagrams via binary matrices. We show soundness and completeness of the SZX-calculus and provide two examples of applications, for graph states and error correcting codes.}
  }
  
  

• Hopf-Frobenius algebras and a new Drinfeld double, Joseph Collins and Ross Duncan, arXiv preprint arXiv:1905.00797 (2019).
  Keywords: Frobenius algebras, Category Theory. Abstract   Bibdata
  The zx-calculus and related theories are based on so-called interacting Frobenius algebras, where a pair of \(\dagger\)-special commutative Frobenius algebras jointly form a pair of Hopf algebras. In this setting we introduce a generalisation of this structure, Hopf-Frobenius algebras, starting from a single Hopf algebra which is not necessarily commutative or cocommutative. We provide the necessary and sufficient condition for a Hopf algebra to be a Hopf-Frobenius algebra, and show that every Hopf algebra in \(\textbfFVect_\textk\) is a Hopf-Frobenius algebra. Hopf-Frobenius algebras provide a notion of duality, and give us a "dual" Hopf algebra that is isomorphic to the usual dual Hopf algebra in a compact closed category. We use this isomorphism to construct a Hopf algebra isomorphic to the Drinfeld double that is defined on \(Høtimes H\) rather than \(Høtimes H^*\).

  @article{HopfFrobenius,
      author = {Collins, Joseph and Duncan, Ross},
      title = {Hopf-Frobenius algebras and a new Drinfeld double},
      year = {2019},
      journal = {arXiv preprint arXiv:1905.00797},
      link = {https://arxiv.org/abs/1905.00797},
      keywords = {Frobenius algebras, Category Theory},
      abstract = {The zx-calculus and related theories are based on so-called interacting Frobenius algebras, where a pair of $\dagger$-special commutative Frobenius algebras jointly form a pair of Hopf algebras. In this setting we introduce a generalisation of this structure, Hopf-Frobenius algebras, starting from a single Hopf algebra which is not necessarily commutative or cocommutative. We provide the necessary and sufficient condition for a Hopf algebra to be a Hopf-Frobenius algebra, and show that every Hopf algebra in $\textbf{FVect}_\text{k}$ is a Hopf-Frobenius algebra. Hopf-Frobenius algebras provide a notion of duality, and give us a "dual" Hopf algebra that is isomorphic to the usual dual Hopf algebra in a compact closed category. We use this isomorphism to construct a Hopf algebra isomorphic to the Drinfeld double that is defined on $H\otimes H$ rather than $H\otimes H^*$.}
  }
  
  

• Flexible layout of surface code computations using AutoCCZ states, Craig Gidney and Austin G. Fowler, arXiv preprint arXiv:1905.08916 (2019).
  Keywords: CCZ, Surface codes, ZX-calculus. Abstract   Bibdata
  We construct a self-correcting CCZ state (the "AutoCCZ") with embedded delayed choice CZs for completing gate teleportations. Using the AutoCCZ state we create efficient surface code spacetime layouts for both a depth-limited circuit (a ripply-carry addition) and a Clifford-limited circuit (a QROM read). Our layouts account for distillation and routing, are based on plausible physical assumptions for a large-scale superconducting qubit platform, and suggest that circuit-level Toffoli parallelism (e.g. using a carry-lookahead adder instead of a ripple-carry adder) will not reduce the execution time of computations involving fewer than five million physical qubits. We reduce the spacetime volume of delayed choice CZs by a factor of 4 compared to techniques from previous work (Fowler 2012), and make several improvements to the CCZ magic state factory from (Gidney 2019).

  @article{autoCCZ,
      author = {  Gidney,Craig and   Fowler, Austin G.},
      title = {Flexible layout of surface code computations using AutoCCZ states},
      year = {2019},
      journal = {arXiv preprint arXiv:1905.08916},
      link = {https://arxiv.org/abs/1905.08916},
      keywords = {CCZ, Surface codes, ZX-calculus},
      abstract = {We construct a self-correcting CCZ state (the "AutoCCZ") with embedded delayed choice CZs for completing gate teleportations. Using the AutoCCZ state we create efficient surface code spacetime layouts for both a depth-limited circuit (a ripply-carry addition) and a Clifford-limited circuit (a QROM read). Our layouts account for distillation and routing, are based on plausible physical assumptions for a large-scale superconducting qubit platform, and suggest that circuit-level Toffoli parallelism (e.g. using a carry-lookahead adder instead of a ripple-carry adder) will not reduce the execution time of computations involving fewer than five million physical qubits. We reduce the spacetime volume of delayed choice CZs by a factor of 4 compared to techniques from previous work (Fowler 2012), and make several improvements to the CCZ magic state factory from (Gidney 2019).  }
  }
  
  

• PyZX: Large Scale Automated Diagrammatic Reasoning, Aleks Kissinger and John van de Wetering, arXiv preprint arXiv:1904.04735 (2019).
  Keywords: ZX-Calculus, Circuit Optimisation, PyZX, Automation. Abstract   Bibdata
  The ZX-calculus is a graphical language for reasoning about ZX-diagrams, a tensor network-like language that can represent arbitrary linear maps between qubits. Using the ZX-calculus, we can intuitively reason about quantum mechanics, and optimise and validate quantum circuits. In this paper we introduce PyZX, an open source library for automated reasoning with large ZX-diagrams. We give a brief introduction to the ZX-calculus, then show how PyZX implements methods for circuit optimisation, equality validation, and visualisation and how it can be used in tandem with other software. We end with a set of challenges that when solved would expand the power of automated diagrammatic reasoning.

  @article{kissinger2019Pyzx,
      author = {Kissinger, Aleks and van de Wetering, John},
      title = {PyZX: Large Scale Automated Diagrammatic Reasoning},
      year = {2019},
      journal = {arXiv preprint arXiv:1904.04735},
      link = {https://arxiv.org/abs/1904.04735},
      keywords = {ZX-Calculus, Circuit Optimisation, PyZX, Automation},
      abstract = {The ZX-calculus is a graphical language for reasoning about ZX-diagrams, a tensor network-like language that can represent arbitrary linear maps between qubits. Using the ZX-calculus, we can intuitively reason about quantum mechanics, and optimise and validate quantum circuits. In this paper we introduce PyZX, an open source library for automated reasoning with large ZX-diagrams. We give a brief introduction to the ZX-calculus, then show how PyZX implements methods for circuit optimisation, equality validation, and visualisation and how it can be used in tandem with other software. We end with a set of challenges that when solved would expand the power of automated diagrammatic reasoning.}
  }
  
  

• Completeness of the Phase-free ZH-calculus, John van de Wetering and Sal Wolffs, arXiv preprint arXiv:1904.07545 (2019).
  Keywords: ZH-Calculus, Completeness. Abstract   Bibdata
  The ZH-calculus is a graphical calculus for linear maps between qubits that allows a natural representation of the Toffoli+Hadamard gate set. The original version of the calculus, which allows every generator to be labelled by an arbitrary complex number, was shown to be complete by Backens and Kissinger. Even though the calculus is complete, this does not mean it allows one to easily reason in restricted settings such as is the case in quantum computing. In this paper we study the fragment of the ZH-calculus that is phase-free, and thus is closer aligned to physically implementable maps. We present a modified rule-set for the phase-free ZH-calculus and show that it is complete. We further discuss the minimality of this rule-set and we give an intuitive interpretation of the rules. Our completeness result follows by reducing to Vilmart's rule-set for the phase-free \(Δ\)ZX-calculus.

  @article{PhasefreeZH2019,
      author = {van de Wetering, John and Wolffs, Sal},
      title = {Completeness of the Phase-free ZH-calculus},
      year = {2019},
      journal = {arXiv preprint arXiv:1904.07545},
      link = {https://arxiv.org/abs/1904.07545},
      keywords = {ZH-Calculus, Completeness},
      abstract = {The ZH-calculus is a graphical calculus for linear maps between qubits that allows a natural representation of the Toffoli+Hadamard gate set. The original version of the calculus, which allows every generator to be labelled by an arbitrary complex number, was shown to be complete by Backens and Kissinger. Even though the calculus is complete, this does not mean it allows one to easily reason in restricted settings such as is the case in quantum computing. In this paper we study the fragment of the ZH-calculus that is phase-free, and thus is closer aligned to physically implementable maps. We present a modified rule-set for the phase-free ZH-calculus and show that it is complete. We further discuss the minimality of this rule-set and we give an intuitive interpretation of the rules. Our completeness result follows by reducing to Vilmart's rule-set for the phase-free $\Delta$ZX-calculus. }
  }
  
  

• Graphical Fourier Theory and the Cost of Quantum Addition, Stach Kuijpers, John van de Wetering and Aleks Kissinger, arXiv preprint arXiv:1904.07551 (2019).
  Keywords: ZH-Calculus, ZX-Calculus, Fourier. Abstract   Bibdata
  The ZX-calculus is a convenient formalism for expressing and reasoning about quantum circuits at a low level, whereas the recently-proposed ZH-calculus yields convenient expressions of mid-level quantum gates such as Toffoli and CCZ. In this paper, we will show that the two calculi are linked by Fourier transform. In particular, we will derive new Fourier expansion rules using the ZH-calculus, and show that we can straightforwardly pass between ZH- and ZX-diagrams using them. Furthermore, we demonstrate that the graphical Fourier expansion of a ZH normal-form corresponds to the standard Fourier transform of a semi-Boolean function. As an illustration of the calculational power of this technique, we then show that several tricks for reducing the T-gate cost of Toffoli circuits, which include for instance quantum adders, can be derived using graphical Fourier theory and straightforwardly generalized to more qubits.

  @article{GraphicalFourier2019,
      author = {Kuijpers, Stach and van de Wetering, John and  Kissinger, Aleks},
      title = {Graphical Fourier Theory and the Cost of Quantum Addition},
      year = {2019},
      journal = {arXiv preprint arXiv:1904.07551},
      link = {https://arxiv.org/abs/1904.07551},
      keywords = {ZH-Calculus, ZX-Calculus, Fourier},
      abstract = {The ZX-calculus is a convenient formalism for expressing and reasoning about quantum circuits at a low level, whereas the recently-proposed ZH-calculus yields convenient expressions of mid-level quantum gates such as Toffoli and CCZ. In this paper, we will show that the two calculi are linked by Fourier transform. In particular, we will derive new Fourier expansion rules using the ZH-calculus, and show that we can straightforwardly pass between ZH- and ZX-diagrams using them. Furthermore, we demonstrate that the graphical Fourier expansion of a ZH normal-form corresponds to the standard Fourier transform of a semi-Boolean function. As an illustration of the calculational power of this technique, we then show that several tricks for reducing the T-gate cost of Toffoli circuits, which include for instance quantum adders, can be derived using graphical Fourier theory and straightforwardly generalized to more qubits.}
  }
  
  

• CNOT circuit extraction for topologically-constrained quantum memories, Aleks Kissinger and Arianne Meijer-van de Griend, arXiv preprint arXiv:1904.00633 (2019).
  Keywords: ZX Adjacent, CNOT, Circuit extraction, Quantum memories. Abstract   Bibdata
  Many physical implementations of quantum computers impose stringent memory constraints in which 2-qubit operations can only be performed between qubits which are nearest neighbours in a lattice or graph structure. Hence, before a computation can be run on such a device, it must be mapped onto the physical architecture. That is, logical qubits must be assigned physical locations in the quantum memory, and the circuit must be replaced by an equivalent one containing only operations between nearest neighbours. In this paper, we give a new technique for quantum circuit mapping (a.k.a. routing), based on Gaussian elimination constrained to certain optimal spanning trees called Steiner trees. We give a reference implementation of the technique for CNOT circuits and show that it significantly out-performs general-purpose routines on CNOT circuits. We then comment on how the technique can be extended straightforwardly to the synthesis of CNOT+Rz circuits and as a modification to a recently-proposed circuit simplification/extraction procedure for generic circuits based on the ZX-calculus.

  @article{CNOTKuijpers2019,
      author = { Kissinger, Aleks and  Meijer-van de Griend, Arianne },
      title = {CNOT circuit extraction for topologically-constrained quantum memories},
      year = {2019},
      journal = {arXiv preprint arXiv:1904.00633},
      link = {https://arxiv.org/abs/1904.00633},
      keywords = {ZX Adjacent, CNOT, Circuit extraction, Quantum memories},
      abstract = {Many physical implementations of quantum computers impose stringent memory constraints in which 2-qubit operations can only be performed between qubits which are nearest neighbours in a lattice or graph structure. Hence, before a computation can be run on such a device, it must be mapped onto the physical architecture. That is, logical qubits must be assigned physical locations in the quantum memory, and the circuit must be replaced by an equivalent one containing only operations between nearest neighbours. In this paper, we give a new technique for quantum circuit mapping (a.k.a. routing), based on Gaussian elimination constrained to certain optimal spanning trees called Steiner trees. We give a reference implementation of the technique for CNOT circuits and show that it significantly out-performs general-purpose routines on CNOT circuits. We then comment on how the technique can be extended straightforwardly to the synthesis of CNOT+Rz circuits and as a modification to a recently-proposed circuit simplification/extraction procedure for generic circuits based on the ZX-calculus. }
  }
  
  

• Pauli Fusion: a computational model to realise quantum transformations from ZX terms, Niel de Beaudrap, Ross Duncan, Dominic Horsman and Simon Perdrix, arXiv preprint arXiv:1904.12817 (2019).
  Keywords: ZX-calculus, Lattice Surgery, Pauli Fusion. Abstract   Bibdata
  We present an abstract model of quantum computation, the Pauli Fusion model, whose primitive operations correspond closely to generators of the ZX calculus (a formal graphical language for quantum computing). The fundamental operations of Pauli Fusion are also straightforward abstractions of basic processes in some leading proposed quantum technologies. These operations have non-deterministic heralded effects, similarly to measurement-based quantum computation. We describe sufficient conditions for Pauli Fusion procedures to be deterministically realisable, so that it performs a given transformation independently of its non-deterministic outcomes. This provides an operational model to realise ZX terms beyond the circuit model.

  @article{PauliFusion,
      author = {de Beaudrap, Niel and Duncan, Ross and Horsman, Dominic and Perdrix, Simon},
      title = {Pauli Fusion: a computational model to realise quantum transformations from ZX terms},
      year = {2019},
      journal = {arXiv preprint arXiv:1904.12817},
      link = {https://arxiv.org/abs/1904.12817},
      keywords = {ZX-calculus, Lattice Surgery, Pauli Fusion},
      abstract = {We present an abstract model of quantum computation, the Pauli Fusion model, whose primitive operations correspond closely to generators of the ZX calculus (a formal graphical language for quantum computing). The fundamental operations of Pauli Fusion are also straightforward abstractions of basic processes in some leading proposed quantum technologies. These operations have non-deterministic heralded effects, similarly to measurement-based quantum computation. We describe sufficient conditions for Pauli Fusion procedures to be deterministically realisable, so that it performs a given transformation independently of its non-deterministic outcomes. This provides an operational model to realise ZX terms beyond the circuit model.}
  }
  
  

• Finite Verification for Infinite Families of Diagram Equations, Hector Miller-Bakewell, arXiv preprint arXiv:1904.00706 (2019).
  Keywords: ZX-calculus, Bang-Boxes, ZH-calculus, ZW-calculus, Automation. Abstract   Bibdata
  The ZX, ZW and ZH calculi are all complete graphical calculi for reasoning about pure state qubit quantum mechanics. All of these languages use certain diagrammatic decorations, called !-boxes and phase variables, to indicate not just one diagram but an infinite family of diagrams. In this same manner one can express infinite families of equations between diagrams, and these decorations are powerful enough to allow for complete rulesets expressing any equivalence in pure state qubit quantum mechanics. We present here results that show that equations between separable infinite families of diagrams are finitely verifiable; that is to say that to verify these infinite families of equations it suffices to check a finite subset of that family, provided a condition we call separability is met. The results we present in this paper not only construct such a verifying subfamily directly, but also generalise to any diagrammatic calculus that satisfies certain simple conditions.

  @article{Hector2019,
      author = {Miller-Bakewell, Hector},
      title = {Finite Verification for Infinite Families of Diagram Equations},
      year = {2019},
      journal = {arXiv preprint arXiv:1904.00706},
      link = {https://arxiv.org/abs/1904.00706},
      keywords = {ZX-calculus, Bang-Boxes, ZH-calculus, ZW-calculus, Automation},
      abstract = {The ZX, ZW and ZH calculi are all complete graphical calculi for reasoning about pure state qubit quantum mechanics. All of these languages use certain diagrammatic decorations, called !-boxes and phase variables, to indicate not just one diagram but an infinite family of diagrams. In this same manner one can express infinite families of equations between diagrams, and these decorations are powerful enough to allow for complete rulesets expressing any equivalence in pure state qubit quantum mechanics. We present here results that show that equations between separable infinite families of diagrams are finitely verifiable; that is to say that to verify these infinite families of equations it suffices to check a finite subset of that family, provided a condition we call separability is met. The results we present in this paper not only construct such a verifying subfamily directly, but also generalise to any diagrammatic calculus that satisfies certain simple conditions.}
  }
  
  

• Completeness of the ZX-Calculus, Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart, arXiv preprint arXiv:1903.06035 (2019).
  Keywords: ZX-Calculus, Completeness, Triangle, Clifford+T, Universal Fragment. Abstract   Bibdata
  The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation or the so-called Clifford fragment of the language - a restriction that is not universal - by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T. We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language - and an adapted system of back-and-forth translation - to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.

  @article{jeandel2019completeness,
      author = {Jeandel, Emmanuel and Perdrix, Simon and Vilmart, Renaud},
      title = {Completeness of the ZX-Calculus},
      year = {2019},
      journal = {arXiv preprint arXiv:1903.06035},
      link = {https://arxiv.org/abs/1903.06035},
      keywords = {ZX-Calculus, Completeness, Triangle, Clifford+T, Universal Fragment},
      abstract = {The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation or the so-called Clifford fragment of the language - a restriction that is not universal - by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T. We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language - and an adapted system of back-and-forth translation - to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.}
  }
  
  

• Reducing T-count with the ZX-calculus, Aleks Kissinger and John van de Wetering, arXiv preprint arXiv:1903.10477 (2019).
  Keywords: ZX-Calculus, Clifford+T, Circuit Optimisation. Abstract   Bibdata
  Reducing the number of non-Clifford quantum gates present in a circuit is an important task for efficiently implementing quantum computations, especially in the fault-tolerant regime. We present a new method for reducing the number of T-gates in a quantum circuit based on the ZX-calculus, which matches or beats previous approaches to T-count reduction on the majority of our benchmark circuits in the ancilla-free case, in some cases yielding up to 50% improvement. Our method begins by representing the quantum circuit as a ZX-diagram, a tensor network-like structure that can be transformed and simplified according to the rules of the ZX-calculus. We then show that a recently-proposed simplification strategy can be extended to reduce T-count using a new technique called phase teleportation. This technique allows non-Clifford phases to combine and cancel by propagating non-locally through a generic quantum circuit. Phase teleportation does not change the number or location of non-phase gates and the method also applies to arbitrary non-Clifford phase gates as well as gates with unknown phase parameters in parametrised circuits. Furthermore, the simplification strategy we use is powerful enough to validate equality of many circuits. In particular, we use it to show that our optimised circuits are indeed equal to the original ones. We have implemented the routines of this paper in the open-source library PyZX.

  @article{kissinger2019tcount,
      author = {Kissinger, Aleks and van de Wetering, John},
      title = {{Reducing T-count with the ZX-calculus}},
      year = {2019},
      journal = {arXiv preprint arXiv:1903.10477},
      link = {https://arxiv.org/abs/1903.10477},
      keywords = {ZX-Calculus, Clifford+T, Circuit Optimisation},
      abstract = {Reducing the number of non-Clifford quantum gates present in a circuit is an important task for efficiently implementing quantum computations, especially in the fault-tolerant regime. We present a new method for reducing the number of T-gates in a quantum circuit based on the ZX-calculus, which matches or beats previous approaches to T-count reduction on the majority of our benchmark circuits in the ancilla-free case, in some cases yielding up to 50\% improvement. Our method begins by representing the quantum circuit as a ZX-diagram, a tensor network-like structure that can be transformed and simplified according to the rules of the ZX-calculus. We then show that a recently-proposed simplification strategy can be extended to reduce T-count using a new technique called phase teleportation. This technique allows non-Clifford phases to combine and cancel by propagating non-locally through a generic quantum circuit. Phase teleportation does not change the number or location of non-phase gates and the method also applies to arbitrary non-Clifford phase gates as well as gates with unknown phase parameters in parametrised circuits. Furthermore, the simplification strategy we use is powerful enough to validate equality of many circuits. In particular, we use it to show that our optimised circuits are indeed equal to the original ones. We have implemented the routines of this paper in the open-source library PyZX.}
  }
  
  

• Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus, Ross Duncan, Aleks Kissinger, Simon Pedrix and John van de Wetering, arXiv preprint arXiv:1902.03178 (2019).
  Keywords: ZX-Calculus, Circuit optimisation. Abstract   Bibdata
  We present the theoretical foundations for a new quantum circuit optimisation technique based on an equational theory called the ZX-calculus. We first interpret quantum circuits as ZX-diagrams, which provide a flexible, lower-level language for describing quantum computations graphically. Then, using the rules of the ZX-calculus, we derive a terminating simplification procedure for ZX-diagrams based on the two graph transformations of local complementation and pivoting. While little is known about extracting an equivalent quantum circuit from an arbitrary ZX-diagram, we show that our simplification procedure preserves a graph property called focused gFlow, and use this property to derive a deterministic strategy for circuit re-extraction. Hence, this approach enables us to temporarily break the rigid quantum circuit structure and 'see around' obstructions (namely non-Clifford quantum gates) to produce significant reductions, while still maintaining enough data to extract a reduced quantum circuit at the end.

  @article{duncan2019graph,
      author = {Duncan, Ross and Kissinger, Aleks and Pedrix, Simon and van de Wetering, John},
      title = {Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus},
      year = {2019},
      journal = {arXiv preprint arXiv:1902.03178},
      link = {https://arxiv.org/abs/1902.03178},
      keywords = {ZX-Calculus, Circuit optimisation},
      abstract = {We present the theoretical foundations for a new quantum circuit optimisation technique based on an equational theory called the ZX-calculus. We first interpret quantum circuits as ZX-diagrams, which provide a flexible, lower-level language for describing quantum computations graphically. Then, using the rules of the ZX-calculus, we derive a terminating simplification procedure for ZX-diagrams based on the two graph transformations of local complementation and pivoting. While little is known about extracting an equivalent quantum circuit from an arbitrary ZX-diagram, we show that our simplification procedure preserves a graph property called focused gFlow, and use this property to derive a deterministic strategy for circuit re-extraction. Hence, this approach enables us to temporarily break the rigid quantum circuit structure and 'see around' obstructions (namely non-Clifford quantum gates) to produce significant reductions, while still maintaining enough data to extract a reduced quantum circuit at the end.}
  }
  
  

• Completeness of Graphical Languages for Mixed States Quantum Mechanics, Titouan Carette, Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart, arXiv:1902.07143 [quant-ph] (2019).
  Keywords: Completeness, Category Theory, Mixed States. Abstract   Bibdata
  There exist several graphical languages for quantum information processing, like quantum circuits, ZX-Calculus, ZW-Calculus, etc. Each of these languages forms a dagger-symmetric monoidal category (dagger-SMC) and comes with an interpretation functor to the dagger-SMC of (finite dimension) Hilbert spaces. In the recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of the extension of these languages beyond pure quantum mechanics, in order to reason on mixed states and general quantum operations, i.e. completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map which allows one to get rid of a quantum system, operation which is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction, which transforms any dagger-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However this construction fails for some fringe cases like the Clifford+T quantum mechanics, as the category does not have enough isometries.

  @article{carette_completeness_2019,
      author = {Carette, Titouan and Jeandel, Emmanuel and Perdrix, Simon and Vilmart, Renaud},
      title = {Completeness of Graphical Languages for Mixed States Quantum Mechanics},
      year = {2019},
      journal = {arXiv:1902.07143 [quant-ph]},
      link = {http://arxiv.org/abs/1902.07143},
      keywords = {Completeness, Category Theory, Mixed States},
      abstract = {There exist several graphical languages for quantum information processing, like quantum circuits, ZX-Calculus, ZW-Calculus, etc. Each of these languages forms a dagger-symmetric monoidal category (dagger-SMC) and comes with an interpretation functor to the dagger-SMC of (finite dimension) Hilbert spaces. In the recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of the extension of these languages beyond pure quantum mechanics, in order to reason on mixed states and general quantum operations, i.e. completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map which allows one to get rid of a quantum system, operation which is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction, which transforms any dagger-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However this construction fails for some fringe cases like the Clifford+T quantum mechanics, as the category does not have enough isometries.},
      month = {feb},
      urldate = {2019-02-20}
  }
  
  

• Optimising Clifford Circuits with Quantomatic, Andrew Fagan and Ross Duncan, Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL) (2019).
  Keywords: ZX-Calculus, Quantomatic, Clifford Fragment, Circuit optimisation, Automation. Abstract   Bibdata
  We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.

  @inproceedings{FaganDuncan,
      author = {Fagan, Andrew and Duncan, Ross},
      title = {Optimising Clifford Circuits with Quantomatic},
      year = {2019},
      booktitle = {Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL)},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {287},
      pages = {85-105},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.287.5},
      link = {https://arxiv.org/abs/1901.10114},
      keywords = {ZX-Calculus, Quantomatic, Clifford Fragment, Circuit optimisation, Automation},
      abstract = {We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.}
  }
  
  

2018

• A Near-Optimal Axiomatisation of ZX-Calculus for Pure Qubit Quantum Mechanics, Renaud Vilmart, arXiv preprint arXiv:1812.09114 (2018).
  Keywords: ZX-Calculus, Completeness, Universal Fragment. Abstract   Bibdata
  Recent developments in the ZX-Calculus have resulted in complete axiomatisations first for an approximately universal restriction of the language, and then for the whole language. The main drawbacks were that the axioms that were added to achieve completeness were numerous, tedious to manipulate and lacked a physical interpretation. We present in this paper two complete axiomatisations for the general ZX-Calculus, that we believe are optimal, in that all their equations are necessary and moreover have a nice physical interpretation.

  @article{vilmarteulercompleteness,
      author = {Renaud Vilmart},
      title = {{A Near-Optimal Axiomatisation of ZX-Calculus for Pure Qubit Quantum Mechanics}},
      year = {2018},
      journal = {arXiv preprint arXiv:1812.09114},
      link = {https://arxiv.org/abs/1812.09114},
      keywords = {ZX-Calculus, Completeness, Universal Fragment},
      abstract = {Recent developments in the ZX-Calculus have resulted in complete axiomatisations first for an approximately universal restriction of the language, and then for the whole language. The main drawbacks were that the axioms that were added to achieve completeness were numerous, tedious to manipulate and lacked a physical interpretation. We present in this paper two complete axiomatisations for the general ZX-Calculus, that we believe are optimal, in that all their equations are necessary and moreover have a nice physical interpretation.}
  }
  
  

• Efficient magic state factories with a catalyzed |CCZ> to 2|T> transformations, Craig Gidney and Austin G. Fowler, arXiv preprint arXiv:1812.01238 (2018).
  Keywords: magic, magic states, ZX-calculus. Abstract   Bibdata
  We present magic state factory constructions for producing |CCZ⟩ states and |T⟩ states. For the |CCZ⟩ factory we apply the surface code lattice surgery construction techniques described by Fowler et al. to the fault-tolerant Toffoli. The resulting factory has a footprint of 12d×6d (where d is the code distance) and produces one |CCZ⟩ every 5.5d surface code cycles. Our |T⟩ state factory uses the |CCZ⟩ factory's output and a catalyst |T⟩ state to exactly transform one |CCZ⟩ state into two |T⟩ states. It has a footprint 25% smaller than the factory of Fowler et al. but outputs |T⟩ states twice as quickly. We show how to generalize the catalyzed transformation to arbitrary phase angles, and note that the case \(θ=22.5^a\) produces a particularly efficient circuit for producing |T−−√⟩ states. Compared to using the 12d×8d×6.5d |T⟩ factory of Fowler et al., our |CCZ⟩ factory can quintuple the speed of algorithms that are dominated by the cost of applying Toffoli gates, including Shor's algorithm and the chemistry algorithm of Babbush et al.. Assuming a physical gate error rate of 10−3, our CCZ factory can produce ∼1010 states on average before an error occurs. This is sufficient for classically intractable instantiations of the chemistry algorithm, but for more demanding algorithms such as Shor's algorithm the mean number of states until failure can be increased to ∼1012 by increasing the factory footprint ~20%

  @article{magicFactories,
      author = {  Gidney,Craig and   Fowler, Austin G.},
      title = {Efficient magic state factories with a catalyzed |CCZ> to 2|T> transformations},
      year = {2018},
      journal = {arXiv preprint arXiv:1812.01238},
      link = {https://arxiv.org/abs/1812.01238},
      keywords = {magic, magic states, ZX-calculus},
      abstract = {We present magic state factory constructions for producing |CCZ⟩ states and |T⟩ states. For the |CCZ⟩ factory we apply the surface code lattice surgery construction techniques described by Fowler et al. to the fault-tolerant Toffoli. The resulting factory has a footprint of 12d×6d (where d is the code distance) and produces one |CCZ⟩ every 5.5d surface code cycles. Our |T⟩ state factory uses the |CCZ⟩ factory's output and a catalyst |T⟩ state to exactly transform one |CCZ⟩ state into two |T⟩ states. It has a footprint 25\% smaller than the factory of Fowler et al. but outputs |T⟩ states twice as quickly. We show how to generalize the catalyzed transformation to arbitrary phase angles, and note that the case $θ=22.5^a$ produces a particularly efficient circuit for producing |T−−√⟩ states. Compared to using the 12d×8d×6.5d |T⟩ factory of Fowler et al., our |CCZ⟩ factory can quintuple the speed of algorithms that are dominated by the cost of applying Toffoli gates, including Shor's algorithm and the chemistry algorithm of Babbush et al.. Assuming a physical gate error rate of 10−3, our CCZ factory can produce ∼1010 states on average before an error occurs. This is sufficient for classically intractable instantiations of the chemistry algorithm, but for more demanding algorithms such as Shor's algorithm the mean number of states until failure can be increased to ∼1012 by increasing the factory footprint ~20\%  }
  }
  
  

• The rational fragment of the ZX-calculus, Emmanuel Jeandel, arXiv:1810.05377 [quant-ph] (2018).
  Keywords: ZX-Calculus, Rational Fragment, Completeness. Abstract   Bibdata
  We introduce here a new axiomatisation of the rational fragment of the ZX-calculus, a diagrammatic language for quantum mechanics. Compared to the previous axiomatisation introduced in [8], our axiomatisation does not use any metarule , but relies instead on a more natural rule, called the cyclotomic supplementarity rule, that was introduced previously in the literature. Our axiomatisation is only complete for diagrams using rational angles , and is not complete in the general case. Using results on diophantine geometry, we characterize precisely which diagram equality involving arbitrary angles are provable in our framework without any new axioms, and we show that our axiomatisation is continuous, in the sense that a diagram equality involving arbitrary angles is provable iff it is a limit of diagram equalities involving rational angles. We use this result to give a complete characterization of all Euler equations that are provable in this axiomatisation.

  @article{jeandel_rational_2018,
      author = {Jeandel, Emmanuel},
      title = {The rational fragment of the ZX-calculus},
      year = {2018},
      journal = {arXiv:1810.05377 [quant-ph]},
      link = {http://arxiv.org/abs/1810.05377},
      keywords = {ZX-Calculus, Rational Fragment, Completeness},
      abstract = {We introduce here a new axiomatisation of the rational fragment of the ZX-calculus, a diagrammatic language for quantum mechanics. Compared to the previous axiomatisation introduced in [8], our axiomatisation does not use any metarule , but relies instead on a more natural rule, called the cyclotomic supplementarity rule, that was introduced previously in the literature. Our axiomatisation is only complete for diagrams using rational angles , and is not complete in the general case. Using results on diophantine geometry, we characterize precisely which diagram equality involving arbitrary angles are provable in our framework without any new axioms, and we show that our axiomatisation is continuous, in the sense that a diagram equality involving arbitrary angles is provable iff it is a limit of diagram equalities involving rational angles. We use this result to give a complete characterization of all Euler equations that are provable in this axiomatisation.},
      month = {oct},
      note = {arXiv: 1810.05377},
      urldate = {2018-10-15}
  }
  
  

• A Generic Normal Form for ZX-Diagrams and Application to the Rational Angle Completeness, Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart, arXiv preprint arXiv:1805.05296 (2018).
  Keywords: ZX-Calculus, Normal-form, Rational Fragment. Abstract   Bibdata
  Recent completeness results on the ZX-Calculus used a third-party language, namely the ZW-Calculus. As a consequence, these proofs are elegant, but sadly non-constructive. We address this issue in the following. To do so, we first describe a generic normal form for ZX-diagrams in any fragment that contains Clifford+T quantum mechanics. We give sufficient conditions for an axiomatisation to be complete, and an algorithm to reach the normal form. Finally, we apply these results to the Clifford+T fragment and the general ZX-Calculus -- for which we already know the completeness--, but also for any fragment of rational angles: we show that the axiomatisation for Clifford+T is also complete for any fragment of dyadic angles, and that a simple new rule (called cancellation) is necessary and sufficient otherwise.

  @article{ZXNormalForm,
      author = {Jeandel, Emmanuel and Perdrix, Simon and Vilmart, Renaud},
      title = {A Generic Normal Form for ZX-Diagrams and Application to the Rational Angle Completeness},
      year = {2018},
      journal = {arXiv preprint arXiv:1805.05296},
      link = {https://arxiv.org/abs/1805.05296},
      keywords = {ZX-Calculus, Normal-form, Rational Fragment},
      abstract = {Recent completeness results on the ZX-Calculus used a third-party language, namely the ZW-Calculus. As a consequence, these proofs are elegant, but sadly non-constructive. We address this issue in the following. To do so, we first describe a generic normal form for ZX-diagrams in any fragment that contains Clifford+T quantum mechanics. We give sufficient conditions for an axiomatisation to be complete, and an algorithm to reach the normal form. Finally, we apply these results to the Clifford+T fragment and the general ZX-Calculus -- for which we already know the completeness--, but also for any fragment of rational angles: we show that the axiomatisation for Clifford+T is also complete for any fragment of dyadic angles, and that a simple new rule (called cancellation) is necessary and sufficient otherwise.}
  }
  
  

• ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity, Miriam Backens and Aleks Kissinger, Proceedings of the 15th International Conference on Quantum Physics and Logic, Halifax, Canada, 3-7th June 2018 (2019).
  Keywords: ZH-calculus, Completeness. Abstract   Bibdata
  We present a new graphical calculus that is sound and complete for a universal family of quantum circuits, which can be seen as the natural string-diagrammatic extension of the approximately (real-valued) universal family of Hadamard+CCZ circuits. The diagrammatic language is generated by two kinds of nodes: the so-called 'spider' associated with the computational basis, as well as a new arity-N generalisation of the Hadamard gate, which satisfies a variation of the spider fusion law. Unlike previous graphical calculi, this admits compact encodings of non-linear classical functions. For example, the AND gate can be depicted as a diagram of just 2 generators, compared to ~25 in the ZX-calculus. Consequently, N-controlled gates, hypergraph states, Hadamard+Toffoli circuits, and diagonal circuits at arbitrary levels of the Clifford hierarchy also enjoy encodings with low constant overhead. This suggests that this calculus will be significantly more convenient for reasoning about the interplay between classical non-linear behaviour (e.g. in an oracle) and purely quantum operations. After presenting the calculus, we will prove it is sound and complete for universal quantum computation by demonstrating the reduction of any diagram to an easily describable normal form.

  @inproceedings{EPTCS287.2,
      author = {Backens, Miriam and Kissinger, Aleks},
      title = {ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity},
      year = {2019},
      booktitle = {Proceedings of the 15th International Conference on
  Quantum Physics and Logic,
  Halifax, Canada, 3-7th June 2018},
      editor = {Selinger, Peter and Chiribella, Giulio},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {287},
      pages = {23-42},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.287.2},
      link = {https://arxiv.org/abs/1805.02175},
      keywords = {ZH-calculus, Completeness},
      abstract = {We present a new graphical calculus that is sound and complete for a universal family of quantum circuits, which can be seen as the natural string-diagrammatic extension of the approximately (real-valued) universal family of Hadamard+CCZ circuits. The diagrammatic language is generated by two kinds of nodes: the so-called 'spider' associated with the computational basis, as well as a new arity-N generalisation of the Hadamard gate, which satisfies a variation of the spider fusion law. Unlike previous graphical calculi, this admits compact encodings of non-linear classical functions. For example, the AND gate can be depicted as a diagram of just 2 generators, compared to ~25 in the ZX-calculus. Consequently, N-controlled gates, hypergraph states, Hadamard+Toffoli circuits, and diagonal circuits at arbitrary levels of the Clifford hierarchy also enjoy encodings with low constant overhead. This suggests that this calculus will be significantly more convenient for reasoning about the interplay between classical non-linear behaviour (e.g. in an oracle) and purely quantum operations. After presenting the calculus, we will prove it is sound and complete for universal quantum computation by demonstrating the reduction of any diagram to an easily describable normal form.}
  }
  
  

• ZX-rules for 2-qubit Clifford+ T quantum circuits, Bob Coecke and Quanlong Wang, International Conference on Reversible Computation (2018).
  Keywords: ZX-Calculus, Completeness, Clifford+T. Abstract   Bibdata
  ZX-calculus is a high-level graphical formalism for qubit computation. In this paper we give the ZX-rules that enable one to derive all equations between 2-qubit Clifford+T quantum circuits. Our rule set is only a small extension of the rules of stabilizer ZX-calculus, and substantially less than those needed for the recently achieved universal completeness. One of our rules is new, and we expect it to also have other utilities. These ZX-rules are much simpler than the complete of set Clifford+T circuit equations due to Selinger and Bian, which indicates that ZX-calculus provides a more convenient arena for quantum circuit rewriting than restricting oneself to circuit equations. The reason for this is that ZX-calculus is not constrained by a fixed unitary gate set for performing intermediate computations.

  @inproceedings{coecke2018zx,
      author = {Coecke, Bob and Wang, Quanlong},
      title = {ZX-rules for 2-qubit Clifford+ T quantum circuits},
      year = {2018},
      booktitle = {International Conference on Reversible Computation},
      pages = {144--161},
      link = {https://arxiv.org/abs/1804.05356},
      keywords = {ZX-Calculus, Completeness, Clifford+T},
      abstract = {ZX-calculus is a high-level graphical formalism for qubit computation. In this paper we give the ZX-rules that enable one to derive all equations between 2-qubit Clifford+T quantum circuits. Our rule set is only a small extension of the rules of stabilizer ZX-calculus, and substantially less than those needed for the recently achieved universal completeness. One of our rules is new, and we expect it to also have other utilities. 
  These ZX-rules are much simpler than the complete of set Clifford+T circuit equations due to Selinger and Bian, which indicates that ZX-calculus provides a more convenient arena for quantum circuit rewriting than restricting oneself to circuit equations. The reason for this is that ZX-calculus is not constrained by a fixed unitary gate set for performing intermediate computations.},
      organization = {Springer}
  }
  
  

• A ZX-Calculus with Triangles for Toffoli-Hadamard, Clifford+T, and Beyond, Renaud Vilmart, Proceedings of the 15th International Conference on Quantum Physics and Logic, Halifax, Canada, 3-7th June 2018 (2019).
  Keywords: ZX-Calculus, Completeness, Triangle. Abstract   Bibdata
  We consider a ZX-calculus augmented with triangle nodes which is well-suited to reason on the so-called Toffoli-Hadamard fragment of quantum mechanics. We precisely show the form of the matrices it represents, and we provide an axiomatisation which makes the language complete for the Toffoli-Hadamard quantum mechanics. We extend the language with arbitrary angles and show that any true equation involving linear diagrams which constant angles are multiple of Pi are derivable. We show that a single axiom is then necessary and sufficient to make the language equivalent to the ZX-calculus which is known to be complete for Clifford+T quantum mechanics. As a by-product, it leads to a new and simple complete axiomatisation for Clifford+T quantum mechanics.

  @inproceedings{EPTCS287.18,
      author = {Vilmart, Renaud},
      title = {A ZX-Calculus with Triangles for Toffoli-Hadamard, Clifford+T, and Beyond},
      year = {2019},
      booktitle = {Proceedings of the 15th International Conference on
  Quantum Physics and Logic,
  Halifax, Canada, 3-7th June 2018},
      editor = {Selinger, Peter and Chiribella, Giulio},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {287},
      pages = {313-344},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.287.18},
      link = {https://arxiv.org/abs/1804.03084},
      keywords = {ZX-Calculus, Completeness, Triangle},
      abstract = {We consider a ZX-calculus augmented with triangle nodes which is well-suited to reason on the so-called Toffoli-Hadamard fragment of quantum mechanics. We precisely show the form of the matrices it represents, and we provide an axiomatisation which makes the language complete for the Toffoli-Hadamard quantum mechanics. We extend the language with arbitrary angles and show that any true equation involving linear diagrams which constant angles are multiple of Pi are derivable. We show that a single axiom is then necessary and sufficient to make the language equivalent to the ZX-calculus which is known to be complete for Clifford+T quantum mechanics. As a by-product, it leads to a new and simple complete axiomatisation for Clifford+T quantum mechanics.}
  }
  
  

• Qutrit ZX-calculus is Complete for Stabilizer Quantum Mechanics, Quanlong Wang, Proceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017 (2018).
  Keywords: ZX-Calculus, Qutrits, Clifford Fragment. Abstract   Bibdata
  In this paper, we show that a qutrit version of ZX-calculus, with rules significantly different from that of the qubit version, is complete for pure qutrit stabilizer quantum mechanics, where state preparations and measurements are based on the three dimensional computational basis, and unitary operations are required to be in the generalized Clifford group. This means that any equation of diagrams that holds true under the standard interpretation in Hilbert spaces can be derived diagrammatically. In contrast to the qubit case, the situation here is more complicated due to the richer structure of this qutrit ZX-calculus.

  @inproceedings{EPTCS266.3,
      author = {Wang, Quanlong},
      title = {Qutrit ZX-calculus is Complete for Stabilizer Quantum Mechanics},
      year = {2018},
      booktitle = {Proceedings 14th International Conference on
  Quantum Physics and Logic,
  Nijmegen, The Netherlands, 3-7 July 2017},
      editor = {Coecke, Bob and Kissinger, Aleks},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {266},
      pages = {58-70},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.266.3},
      link = {https://arxiv.org/abs/1803.00696},
      keywords = {ZX-Calculus, Qutrits, Clifford Fragment},
      abstract = {In this paper, we show that a qutrit version of ZX-calculus, with rules significantly different from that of the qubit version, is complete for pure qutrit stabilizer quantum mechanics, where state preparations and measurements are based on the three dimensional computational basis, and unitary operations are required to be in the generalized Clifford group. This means that any equation of diagrams that holds true under the standard interpretation in Hilbert spaces can be derived diagrammatically. In contrast to the qubit case, the situation here is more complicated due to the richer structure of this qutrit ZX-calculus.}
  }
  
  

• Diagrammatic Reasoning Beyond Clifford+T Quantum Mechanics, Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018).
  Keywords: ZX-Calculus, Completeness, Universal Fragment. Abstract   Bibdata
  The ZX-Calculus is a graphical language for quantum mechanics. An axiomatisation has recently been proven to be complete for an approximatively universal fragment of quantum mechanics, the so-called Clifford+T fragment. We focus here on the expressive power of this axiomatisation beyond Clifford+T Quantum mechanics. We consider the full pure qubit quantum mechanics, and mainly prove two results: (i) First, the axiomatisation for Clifford+T quantum mechanics is also complete for all equations involving some kind of linear diagrams. The linearity of the diagrams reflects the phase group structure, an essential feature of the ZX-calculus. In particular all the axioms of the ZX-calculus are involving linear diagrams. (ii) We also show that the axiomatisation for Clifford+T is not complete in general but can be completed by adding a single (non linear) axiom, providing a simpler axiomatisation of the ZX-calculus for pure quantum mechanics than the one recently introduced by Ng&Wang.

  @inproceedings{JPV-universal,
      author = {Jeandel, Emmanuel and Perdrix, Simon and Vilmart, Renaud},
      title = {{Diagrammatic Reasoning Beyond Clifford+T Quantum Mechanics}},
      year = {2018},
      booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
      series = {LICS '18},
      pages = {569--578},
      publisher = {ACM},
      doi = {10.1145/3209108.3209139},
      link = {https://arxiv.org/abs/1801.10142},
      keywords = {ZX-Calculus, Completeness, Universal Fragment},
      abstract = {The ZX-Calculus is a graphical language for quantum mechanics. An axiomatisation has recently been proven to be complete for an approximatively universal fragment of quantum mechanics, the so-called Clifford+T fragment. We focus here on the expressive power of this axiomatisation beyond Clifford+T Quantum mechanics. We consider the full pure qubit quantum mechanics, and mainly prove two results: (i) First, the axiomatisation for Clifford+T quantum mechanics is also complete for all equations involving some kind of linear diagrams. The linearity of the diagrams reflects the phase group structure, an essential feature of the ZX-calculus. In particular all the axioms of the ZX-calculus are involving linear diagrams. (ii) We also show that the axiomatisation for Clifford+T is not complete in general but can be completed by adding a single (non linear) axiom, providing a simpler axiomatisation of the ZX-calculus for pure quantum mechanics than the one recently introduced by Ng&Wang.},
      acmid = {3209139},
      address = {New York, NY, USA},
      isbn = {978-1-4503-5583-4},
      location = {Oxford, United Kingdom},
      numpages = {10}
  }
  
  

• A diagrammatic calculus of fermionic quantum circuits, Amar Hadzihasanovic, Giovanni de Felice and Kang Feng Ng, Logical Methods in Computer Science (2019).
  Keywords: ZW-Calculus, Completeness, Fermionic quantum computing. Abstract   Bibdata
  We introduce the fermionic ZW calculus, a string-diagrammatic language for fermionic quantum computing (FQC). After defining a fermionic circuit model, we present the basic components of the calculus, together with their interpretation, and show how the main physical gates of interest in FQC can be represented in our language. We then list our axioms, and derive some additional equations. We prove that the axioms provide a complete equational axiomatisation of the monoidal category whose objects are systems of finitely many local fermionic modes (LFMs), with maps that preserve or reverse the parity of states, and the tensor product as monoidal product. We achieve this through a procedure that rewrites any diagram in a normal form. As an example, we show how the statistics of a fermionic Mach-Zehnder interferometer can be calculated in the diagrammatic language. We conclude by giving a diagrammatic treatment of the dual-rail encoding, a standard method in optical quantum computing used to perform universal quantum computation.

  @article{hadzihasanovic2018diagrammatic,
      author = {Hadzihasanovic, Amar and de Felice, Giovanni and Ng, Kang Feng},
      title = {A diagrammatic calculus of fermionic quantum circuits},
      year = {2019},
      journal = {Logical Methods in Computer Science},
      volume = {15},
      publisher = {Episciences. org},
      link = {https://arxiv.org/abs/1801.01231},
      keywords = {ZW-Calculus, Completeness, Fermionic quantum computing},
      abstract = {We introduce the fermionic ZW calculus, a string-diagrammatic language for fermionic quantum computing (FQC). After defining a fermionic circuit model, we present the basic components of the calculus, together with their interpretation, and show how the main physical gates of interest in FQC can be represented in our language. We then list our axioms, and derive some additional equations. We prove that the axioms provide a complete equational axiomatisation of the monoidal category whose objects are systems of finitely many local fermionic modes (LFMs), with maps that preserve or reverse the parity of states, and the tensor product as monoidal product. We achieve this through a procedure that rewrites any diagram in a normal form. As an example, we show how the statistics of a fermionic Mach-Zehnder interferometer can be calculated in the diagrammatic language. We conclude by giving a diagrammatic treatment of the dual-rail encoding, a standard method in optical quantum computing used to perform universal quantum computation.}
  }
  
  

• Completeness of the ZX-calculus for Pure Qubit Clifford+T Quantum Mechanics, Kang Feng Ng and Quanlong Wang, arXiv:1801.07993 [quant-ph] (2018).
  Keywords: ZX-Calculus, Completeness, Clifford+T. Abstract   Bibdata
  Recently, we gave a complete axiomatisation of the ZX-calculus for the overall pure qubit quantum mechanics. Based on this result, here we also obtain a complete axiomatisation of the ZX-calculus for the Clifford+T quantum mechanics by restricting the ring of complex numbers to its subring corresponding to the Clifford+T fragment resting on the completeness theorem of the ZW-calculus for arbitrary commutative ring. In contrast to the first complete axiomatisation of the ZX-calculus for the Clifford+T fragment, we have two new generators as features rather than novelties: the triangle can be employed as an essential component to construct a Toffoli gate in a very simple form, while the lambda box can be slightly extended to a generalised phase so that the generalised supplementarity (cyclotomic supplementarity ) is naturally seen as a special case of the generalised spider rule.

  @article{ng_completeness_2018,
      author = {Ng, Kang Feng and Wang, Quanlong},
      title = {Completeness of the ZX-calculus for Pure Qubit Clifford+T Quantum Mechanics},
      year = {2018},
      journal = {arXiv:1801.07993 [quant-ph]},
      link = {http://arxiv.org/abs/1801.07993},
      keywords = {ZX-Calculus, Completeness, Clifford+T},
      abstract = {Recently, we gave a complete axiomatisation of the ZX-calculus for the overall pure qubit quantum mechanics. Based on this result, here we also obtain a complete axiomatisation of the ZX-calculus for the Clifford+T quantum mechanics by restricting the ring of complex numbers to its subring corresponding to the Clifford+T fragment resting on the completeness theorem of the ZW-calculus for arbitrary commutative ring. In contrast to the first complete axiomatisation of the ZX-calculus for the Clifford+T fragment, we have two new generators as features rather than novelties: the triangle can be employed as an essential component to construct a Toffoli gate in a very simple form, while the lambda box can be slightly extended to a generalised phase so that the generalised supplementarity (cyclotomic supplementarity ) is naturally seen as a special case of the generalised spider rule.},
      month = {jan},
      urldate = {2018-02-16}
  }
  
  

• Two Complete Axiomatisations of Pure-state Qubit Quantum Computing, Amar Hadzihasanovic, Kang Feng Ng and Quanlong Wang, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018).
  Keywords: ZW-Calculus, Completeness, Universal Fragment, Normal-form. Abstract   Bibdata
  Categorical quantum mechanics places finite-dimensional quantum theory in the context of compact closed categories, with an emphasis on diagrammatic reasoning. In this framework, two equational diagrammatic calculi have been proposed for pure-state qubit quantum computing: the ZW calculus, developed by Coecke, Kissinger and the first author for the purpose of qubit entanglement classification, and the ZX calculus, introduced by Coecke and Duncan to give an abstract description of complementary observables. Neither calculus, however, provided a complete axiomatisation of their model. In this paper, we present extended versions of ZW and ZX, and show their completeness for pure-state qubit theory, thus solving two major open problems in categorical quantum mechanics. First, we extend the original ZW calculus to represent states and linear maps with coefficients in an arbitrary commutative ring, and prove completeness by a strategy that rewrites all diagrams into a normal form. We then extend the language and axioms of the original ZX calculus, and show their completeness for pure-state qubit theory through a translation between ZX and ZW specialised to the field of complex numbers. This translation expands the one used by Jeandel, Perdrix, and Vilmart to derive an axiomatisation of the approximately universal Clifford+T fragment; restricting the field of complex numbers to a suitable subring, we obtain an alternative axiomatisation of the same theory.

  @inproceedings{HarnyAmarCompleteness,
      author = {Hadzihasanovic, Amar and Ng, Kang Feng and Wang, Quanlong},
      title = {Two Complete Axiomatisations of Pure-state Qubit Quantum Computing},
      year = {2018},
      booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
      series = {LICS '18},
      pages = {502--511},
      publisher = {ACM},
      doi = {10.1145/3209108.3209128},
      link = {https://dl.acm.org/citation.cfm?id=3209128},
      keywords = {ZW-Calculus, Completeness, Universal Fragment, Normal-form},
      abstract = {Categorical quantum mechanics places finite-dimensional quantum theory in the context of compact closed categories, with an emphasis on diagrammatic reasoning. In this framework, two equational diagrammatic calculi have been proposed for pure-state qubit quantum computing: the ZW calculus, developed by Coecke, Kissinger and the first author for the purpose of qubit entanglement classification, and the ZX calculus, introduced by Coecke and Duncan to give an abstract description of complementary observables. Neither calculus, however, provided a complete axiomatisation of their model.
  
  In this paper, we present extended versions of ZW and ZX, and show their completeness for pure-state qubit theory, thus solving two major open problems in categorical quantum mechanics. First, we extend the original ZW calculus to represent states and linear maps with coefficients in an arbitrary commutative ring, and prove completeness by a strategy that rewrites all diagrams into a normal form. We then extend the language and axioms of the original ZX calculus, and show their completeness for pure-state qubit theory through a translation between ZX and ZW specialised to the field of complex numbers. This translation expands the one used by Jeandel, Perdrix, and Vilmart to derive an axiomatisation of the approximately universal Clifford+T fragment; restricting the field of complex numbers to a suitable subring, we obtain an alternative axiomatisation of the same theory.},
      acmid = {3209128},
      address = {New York, NY, USA},
      isbn = {978-1-4503-5583-4},
      location = {Oxford, United Kingdom},
      numpages = {10}
  }
  
  

• Completeness of the ZX-calculus, Quanlong Wang, PhD Thesis (2018).
  Keywords: ZX-Calculus, Completeness, PhD Thesis. Abstract   Bibdata
  The ZX-calculus is an intuitive but also mathematically strict graphical language for quantum computing, which is especially powerful for the framework of quantum circuits. Completeness of the ZX-calculus means any equality of matrices with size powers of n can be derived purely diagrammatically. In this thesis, we give the first complete axiomatisation the ZX-calculus for the overall pure qubit quantum mechanics, via a translation from the completeness result of another graphical language for quantum computing– the ZW-calculus. This paves the way for automated pictorial quantum computing, with the aid of some software like Quantomatic. Based on this universal completeness, we directly obtain a complete axiomatisation of the ZX-calculus for the Clifford+T quantum mechanics, which is approximatively universal for quantum computing, by restricting the ring of complex numbers to its subring corresponding to the Clifford+T fragment resting on the completeness theorem of the ZW-calculus for arbitrary commutative ring. Furthermore, we prove the completeness of the ZX-calculus (with just 9 rules) for 2-qubit Clifford+T circuits by verifying the complete set of 17 circuit relations in diagrammatic rewriting. This is an important step towards efficient simplification of general n-qubit Clifford+T circuits, considering that we now have all the necessary rules for diagrammatical quantum reasoning and a very simple construction of Toffoli gate within our axiomatisation framework, which is approximately universal for quantum computation together with the Hadamard gate. In addition to completeness results within the qubit related formalism, we extend the completeness of the ZX-calculus for qubit stabilizer quantum mechanics to the qutrit stabilizer system. Finally, we show with some examples the application of the ZX-calculus to the proof of generalised supplementarity, the representation of entanglement classification and Toffoli gate, as well as equivalence-checking for the UMA gate.

  @phdthesis{wang_completeness_2018,
      author = {Wang, Quanlong},
      title = {Completeness of the ZX-calculus},
      year = {2018},
      link = {http://www.cs.ox.ac.uk/people/bob.coecke/Harny.pdf},
      keywords = {ZX-Calculus, Completeness, PhD Thesis},
      abstract = {The ZX-calculus is an intuitive but also mathematically strict graphical language for quantum computing, which is especially powerful for the framework of quantum circuits. Completeness of the ZX-calculus means any equality of matrices with size powers of n can be derived purely diagrammatically. In this thesis, we give the first complete axiomatisation the ZX-calculus for the overall pure qubit quantum mechanics, via a translation from the completeness result of another graphical language for quantum computing– the ZW-calculus. This paves the way for automated pictorial quantum computing, with the aid of some software like Quantomatic.
  
  Based on this universal completeness, we directly obtain a complete axiomatisation of the ZX-calculus for the Clifford+T quantum mechanics, which is approximatively universal for quantum computing, by restricting the ring of complex numbers to its subring corresponding to the Clifford+T fragment resting on the completeness theorem of the ZW-calculus for arbitrary commutative ring.
  
  Furthermore, we prove the completeness of the ZX-calculus (with just 9 rules) for 2-qubit Clifford+T circuits by verifying the complete set of 17 circuit relations in diagrammatic rewriting. This is an important step towards efficient simplification of general n-qubit Clifford+T circuits, considering that we now have all the necessary rules for diagrammatical quantum reasoning and a very simple construction of Toffoli gate within our axiomatisation framework, which is approximately universal for quantum computation together with the Hadamard gate.
  
  In addition to completeness results within the qubit related formalism, we extend the completeness of the ZX-calculus for qubit stabilizer quantum mechanics to the qutrit stabilizer system.
  
  Finally, we show with some examples the application of the ZX-calculus to the proof of generalised supplementarity, the representation of entanglement classification and Toffoli gate, as well as equivalence-checking for the UMA gate.},
      note = {PhD Thesis},
      school = {University of Oxford},
      type = {PhD thesis},
      urldate = {2019-02-26}
  }
  
  

• Towards Minimality of Clifford+T ZX-Calculus, Borun Shi, University of Oxford Master thesis (2018).
  Keywords: ZX-Calculus, Minimality, Master Thesis. Abstract   Bibdata
  ZX-calculus is a high-level graphical language used for quantum computation. A complete set of axioms for ZX-calculus has been found very recently. This thesis works towards minimizing axioms of ZX-calculus for Clifford+T quantum mechanics, a fragment consisting of an approximately universal gate set. Similar work has been done for the smaller fragment, stabilizer quantum mechanics, which motivates many of our proofs. We derive some singleton axioms and instances of axiom schemes. We establish the necessity and some weaker independence results of several axioms, by considering a variety of models. As a further step towards simplification we also consider alternative presentations of axioms that are equivalent and discuss their uses.

  @unpublished{Borun,
      author = {Shi, Borun},
      title = {Towards Minimality of Clifford+T ZX-Calculus},
      year = {2018},
      link = {http://www.cs.ox.ac.uk/people/bob.coecke/Borun},
      keywords = {ZX-Calculus, Minimality, Master Thesis},
      abstract = {ZX-calculus is a high-level graphical language used for quantum computation.  A complete set of axioms for ZX-calculus has been found very recently. This thesis works towards minimizing axioms of ZX-calculus for Clifford+T quantum  mechanics,  a  fragment  consisting  of  an  approximately  universal gate  set. Similar work  has  been  done  for  the  smaller  fragment,  stabilizer quantum mechanics, which motivates many of our proofs.  We derive some singleton axioms and instances of axiom schemes.  We establish the necessity and some weaker independence results of several axioms, by considering a variety of models.  As a further step towards simplification we also consider alternative  presentations  of  axioms  that  are  equivalent  and  discuss  their uses.},
      note = {University of Oxford Master thesis}
  }
  
  

2017

• The algebra of entanglement and the geometry of composition, Amar Hadzihasanovic, PhD Thesis (2017).
  Keywords: ZW-Calculus, Completeness, PhD Thesis. Abstract   Bibdata
  String diagrams turn algebraic equations into topological moves that have recurring shapes, involving the sliding of one diagram past another. We individuate, at the root of this fact, the dual nature of polygraphs as presentations of higher algebraic theories, and as combinatorial descriptions of "directed spaces". Operations of polygraphs modelled on operations of topological spaces are used as the foundation of a compositional universal algebra, where sliding moves arise from tensor products of polygraphs. We reconstruct several higher algebraic theories in this framework. In this regard, the standard formalism of polygraphs has some technical problems. We propose a notion of regular polygraph, barring cell boundaries that are not homeomorphic to a disk of the appropriate dimension. We define a category of non-degenerate shapes, and show how to calculate their tensor products. Then, we introduce a notion of weak unit to recover weakly degenerate boundaries in low dimensions, and prove that the existence of weak units is equivalent to a representability property. We then turn to applications of diagrammatic algebra to quantum theory. We re-evaluate the category of Hilbert spaces from the perspective of categorical universal algebra, which leads to a bicategorical refinement. Then, we focus on the axiomatics of fragments of quantum theory, and present the ZW calculus, the first complete diagrammatic axiomatisation of the theory of qubits. The ZW calculus has several advantages over ZX calculi, including a computationally meaningful normal form, and a fragment whose diagrams can be read as setups of fermionic oscillators. Moreover, its generators reflect an operational classification of entangled states of 3 qubits. We conclude with generalisations of the ZW calculus to higher-dimensional systems, including the definition of a universal set of generators in each dimension.

  @article{hadzihasanovic2017algebra,
      author = {Hadzihasanovic, Amar},
      title = {The algebra of entanglement and the geometry of composition},
      year = {2017},
      link = {https://arxiv.org/abs/1709.08086},
      keywords = {ZW-Calculus, Completeness, PhD Thesis},
      abstract = {String diagrams turn algebraic equations into topological moves that have recurring shapes, involving the sliding of one diagram past another. We individuate, at the root of this fact, the dual nature of polygraphs as presentations of higher algebraic theories, and as combinatorial descriptions of "directed spaces". Operations of polygraphs modelled on operations of topological spaces are used as the foundation of a compositional universal algebra, where sliding moves arise from tensor products of polygraphs. We reconstruct several higher algebraic theories in this framework. 
  In this regard, the standard formalism of polygraphs has some technical problems. We propose a notion of regular polygraph, barring cell boundaries that are not homeomorphic to a disk of the appropriate dimension. We define a category of non-degenerate shapes, and show how to calculate their tensor products. Then, we introduce a notion of weak unit to recover weakly degenerate boundaries in low dimensions, and prove that the existence of weak units is equivalent to a representability property. 
  We then turn to applications of diagrammatic algebra to quantum theory. We re-evaluate the category of Hilbert spaces from the perspective of categorical universal algebra, which leads to a bicategorical refinement. Then, we focus on the axiomatics of fragments of quantum theory, and present the ZW calculus, the first complete diagrammatic axiomatisation of the theory of qubits. 
  The ZW calculus has several advantages over ZX calculi, including a computationally meaningful normal form, and a fragment whose diagrams can be read as setups of fermionic oscillators. Moreover, its generators reflect an operational classification of entangled states of 3 qubits. We conclude with generalisations of the ZW calculus to higher-dimensional systems, including the definition of a universal set of generators in each dimension.},
      note = {PhD Thesis}
  }
  
  

• A universal completion of the ZX-calculus, Kang Feng Ng and Quanlong Wang, arXiv preprint arXiv:1706.09877 (2017).
  Keywords: ZX-Calculus, Completeness, Universal Fragment. Abstract   Bibdata
  In this paper, we give a universal completion of the ZX-calculus for the whole of pure qubit quantum mechanics. This proof is based on the completeness of another graphical language: the ZW-calculus, with direct translations between these two graphical systems.

  @article{ng2017universal,
      author = {Ng, Kang Feng and Wang, Quanlong},
      title = {A universal completion of the ZX-calculus},
      year = {2017},
      journal = {arXiv preprint arXiv:1706.09877},
      link = {https://arxiv.org/abs/1706.09877},
      keywords = {ZX-Calculus, Completeness, Universal Fragment},
      abstract = {In this paper, we give a universal completion of the ZX-calculus for the whole of pure qubit quantum mechanics. This proof is based on the completeness of another graphical language: the ZW-calculus, with direct translations between these two graphical systems.}
  }
  
  

• Verifying the Smallest Interesting Colour Code with Quantomatic, Liam Garvie and Ross Duncan, Proceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017 (2018).
  Keywords: ZX-Calculus, Quantomatic, Error correcting codes. Abstract   Bibdata
  In this paper we present a Quantomatic case study, verifying the basic properties of the Smallest Interesting Colour Code error detecting code.

  @inproceedings{EPTCS266.10,
      author = {Garvie, Liam and Duncan, Ross},
      title = {Verifying the Smallest Interesting Colour Code with Quantomatic},
      year = {2018},
      booktitle = {Proceedings 14th International Conference on
  Quantum Physics and Logic,
  Nijmegen, The Netherlands, 3-7 July 2017},
      editor = {Coecke, Bob and Kissinger, Aleks},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {266},
      pages = {147-163},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.266.10},
      link = {https://arxiv.org/abs/1706.02717},
      keywords = {ZX-Calculus, Quantomatic, Error correcting codes},
      abstract = {In this paper we present a Quantomatic case study, verifying the basic properties of the Smallest Interesting Colour Code error detecting code.}
  }
  
  

• A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics, Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018).
  Keywords: Clifford+T, Completeness, ZX-Calculus. Abstract   Bibdata
  We introduce the first complete and approximatively universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding four new axioms to the language. The completeness of the ZX-Calculus for Clifford+T quantum mechanics was one of the main open questions in categorical quantum mechanics. We prove the completeness of the Clifford+T fragment of the ZX-Calculus using the recently studied ZW-Calculus, a calculus dealing with integer matrices. We also prove that the Clifford+T fragment of the ZX-Calculus represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals.

  @inproceedings{SimonCompleteness,
      author = {Jeandel, Emmanuel and Perdrix, Simon and Vilmart, Renaud},
      title = {{A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics}},
      year = {2018},
      booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
      series = {LICS '18},
      pages = {559--568},
      publisher = {ACM},
      doi = {10.1145/3209108.3209131},
      link = {https://arxiv.org/abs/1705.11151},
      keywords = {Clifford+T, Completeness, ZX-Calculus},
      abstract = {We introduce the first complete and approximatively universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding four new axioms to the language. The completeness of the ZX-Calculus for Clifford+T quantum mechanics was one of the main open questions in categorical quantum mechanics. We prove the completeness of the Clifford+T fragment of the ZX-Calculus using the recently studied ZW-Calculus, a calculus dealing with integer matrices. We also prove that the Clifford+T fragment of the ZX-Calculus represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals.},
      acmid = {3209131},
      address = {New York, NY, USA},
      isbn = {978-1-4503-5583-4},
      location = {Oxford, United Kingdom},
      numpages = {10}
  }
  
  

• Universal MBQC with generalised parity-phase interactions and Pauli measurements, Aleks Kissinger and John van de Wetering, Quantum (2019).
  Keywords: ZX-Calculus, Clifford+T, MBQC. Abstract   Bibdata
  We introduce a new family of models for measurement-based quantum computation which are deterministic and approximately universal. The resource states which play the role of graph states are prepared via 2-qubit gates of the form \(\exp(−iπ 2nZøtimes Z)\). When \(n=2\), these are equivalent, up to local Clifford unitaries, to graph states. However, when \(n>2\), their behaviour diverges in two important ways. First, multiple applications of the entangling gate to a single pair of qubits produces non-trivial entanglement, and hence multiple parallel edges between nodes play an important role in these generalised graph states. Second, such a state can be used to realise deterministic, approximately universal computation using only Pauli Z and X measurements and feed-forward. Even though, for \(n>2\), the relevant resource states are no longer stabiliser states, they admit a straightforward, graphical representation using the ZX-calculus. Using this representation, we are able to provide a simple, graphical proof of universality. We furthermore show that for every \(n>2\) this family is capable of producing all Clifford gates and all diagonal gates in the \(n\)-th level of the Clifford hierarchy.

  @article{kissinger2017MBQC,
      author = {Kissinger, Aleks and van de Wetering, John},
      title = {{Universal MBQC with generalised parity-phase interactions and Pauli measurements}},
      year = {2019},
      journal = {Quantum},
      volume = {3},
      link = {https://arxiv.org/abs/1704.06504},
      keywords = {ZX-Calculus, Clifford+T, MBQC},
      abstract = {We introduce a new family of models for measurement-based quantum computation which are deterministic and approximately universal. The resource states which play the role of graph states are prepared via 2-qubit gates of the form $\exp(−i\pi 2nZ\otimes Z)$. When $n=2$, these are equivalent, up to local Clifford unitaries, to graph states. However, when $n>2$, their behaviour diverges in two important ways. First, multiple applications of the entangling gate to a single pair of qubits produces non-trivial entanglement, and hence multiple parallel edges between nodes play an important role in these generalised graph states. Second, such a state can be used to realise deterministic, approximately universal computation using only Pauli Z and X measurements and feed-forward. Even though, for $n>2$, the relevant resource states are no longer stabiliser states, they admit a straightforward, graphical representation using the ZX-calculus. Using this representation, we are able to provide a simple, graphical proof of universality. We furthermore show that for every $n>2$ this family is capable of producing all Clifford gates and all diagonal gates in the $n$-th level of the Clifford hierarchy.},
      issue = {134}
  }
  
  

• Equivalence of Local Complementation and Euler Decomposition in the Qutrit ZX-calculus, Xiaoyan Gong and Quanlong Wang, arXiv:1704.05955 [quant-ph] (2017).
  Keywords: ZX-Calculus, Qutrits, Local Complementation. Abstract   Bibdata
  In this paper, we give a modified version of the qutrit ZX-calculus, by which we represent qutrit graph states as diagrams and prove that the qutrit version of local complementation property is true if and only if the qutrit Hadamard gate H has an Euler decomposition into \(4π/3\)-green and red rotations. This paves the way for studying the completeness of qutrit ZX-calculus for qutrit stabilizer quantum mechanics.

  @article{gong_equivalence_2017,
      author = {Gong, Xiaoyan and Wang, Quanlong},
      title = {Equivalence of Local Complementation and Euler Decomposition in the Qutrit ZX-calculus},
      year = {2017},
      journal = {arXiv:1704.05955 [quant-ph]},
      link = {http://arxiv.org/abs/1704.05955},
      keywords = {ZX-Calculus, Qutrits, Local Complementation},
      abstract = {In this paper, we give a modified version of the qutrit ZX-calculus, by which we represent qutrit graph states as diagrams and prove that the qutrit version of local complementation property is true if and only if the qutrit Hadamard gate H has an Euler decomposition into $4\pi/3$-green and red rotations. This paves the way for studying the completeness of qutrit ZX-calculus for qutrit stabilizer quantum mechanics.},
      month = {apr},
      note = {arXiv: 1704.05955},
      urldate = {2017-04-21}
  }
  
  

• Categorifying the ZX-calculus, Daniel Cicala, Proceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017 (2018).
  Keywords: ZX-Calculus, Category Theory. Abstract   Bibdata
  We build a symmetric monoidal and compact closed bicategory by combining spans and cospans inside a topos. This can be used as a framework in which to study open networks and diagrammatic languages. We illustrate this framework with Coecke and Duncan's zx-calculus by constructing a bicategory with the natural numbers for 0-cells, the zx-calculus diagrams for 1-cells, and rewrite rules for 2-cells.

  @inproceedings{cicala_categorifying_2018,
      author = {Cicala, Daniel},
      title = {Categorifying the {ZX-calculus}},
      year = {2018},
      booktitle = {{\rm Proceedings 14th International Conference on}
  Quantum Physics and Logic,
  {\rm Nijmegen, The Netherlands, 3-7 July 2017}},
      editor = {Coecke, Bob and Kissinger, Aleks},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {266},
      pages = {294-314},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.266.19},
      link = {http://arxiv.org/abs/1704.07034},
      keywords = {ZX-Calculus, Category Theory},
      abstract = {We build a symmetric monoidal and compact closed bicategory by combining spans and cospans inside a topos. This can be used as a framework in which to study open networks and diagrammatic languages. We illustrate this framework with Coecke and Duncan's zx-calculus by constructing a bicategory with the natural numbers for 0-cells, the zx-calculus diagrams for 1-cells, and rewrite rules for 2-cells.}
  }
  
  

• The ZX calculus is a language for surface code lattice surgery, Niel de Beaudrap and Dominic Horsman, Quantum (2020).
  Keywords: ZX-Calculus, Lattice Surgery, Topological Quantum Computing. Abstract   Bibdata
  Quantum computing is moving rapidly to the point of deployment of technology. Functional quantum devices will require the ability to correct error in order to be scalable and effective. A leading choice of error correction, in particular for modular or distributed architectures, is the surface code with logical two-qubit operations realised via "lattice surgery". These operations consist of "merges" and "splits" acting non-unitarily on the logical states and are not easily captured by standard circuit notation. This raises the question of how best to reason about lattice surgery in order efficiently to use quantum states and operations in architectures with complex resource management issues. In this paper we demonstrate that the operations of the ZX calculus, a form of quantum diagrammatic reasoning designed using category theory, match exactly the operations of lattice surgery. Red and green "spider" nodes match rough and smooth merges and splits, and follow the axioms of a dagger special associative Frobenius algebra. Some lattice surgery operations can require non-trivial correction operations, which are captured natively in the use of the ZX calculus in the form of ensembles of diagrams. We give a first taste of the power of the calculus as a language for surgery by considering two operations (magic state use and producing a CNOT) and show how ZX diagram re-write rules give lattice surgery procedures for these operations that are novel, efficient, and highly configurable.

  @article{horsman2017surgery,
      author = {de Beaudrap, Niel and Horsman, Dominic},
      title = {The ZX calculus is a language for surface code lattice surgery},
      year = {2020},
      journal = {Quantum},
      volume = {4},
      doi = {https://doi.org/10.22331/q-2020-01-09-218},
      link = {https://arxiv.org/abs/1704.08670},
      keywords = {ZX-Calculus, Lattice Surgery, Topological Quantum Computing},
      abstract = {Quantum computing is moving rapidly to the point of deployment of technology. Functional quantum devices will require the ability to correct error in order to be scalable and effective. A leading choice of error correction, in particular for modular or distributed architectures, is the surface code with logical two-qubit operations realised via "lattice surgery". These operations consist of "merges" and "splits" acting non-unitarily on the logical states and are not easily captured by standard circuit notation. This raises the question of how best to reason about lattice surgery in order efficiently to use quantum states and operations in architectures with complex resource management issues. In this paper we demonstrate that the operations of the ZX calculus, a form of quantum diagrammatic reasoning designed using category theory, match exactly the operations of lattice surgery. Red and green "spider" nodes match rough and smooth merges and splits, and follow the axioms of a dagger special associative Frobenius algebra. Some lattice surgery operations can require non-trivial correction operations, which are captured natively in the use of the ZX calculus in the form of ensembles of diagrams. We give a first taste of the power of the calculus as a language for surgery by considering two operations (magic state use and producing a CNOT) and show how ZX diagram re-write rules give lattice surgery procedures for these operations that are novel, efficient, and highly configurable.}
  }
  
  

• ZX-Calculus: Cyclotomic Supplementarity and Incompleteness for Clifford+T Quantum Mechanics, Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart and Quanlong Wang, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017) (2017).
  Keywords: ZX-Calculus, Completeness, Rational Fragment. Abstract   Bibdata
  The ZX-Calculus is a powerful graphical language for quantum mechanics and quantum information processing. The completeness of the language -- i.e. the ability to derive any true equation -- is a crucial question. In the quest of a complete ZX-calculus, supplementarity has been recently proved to be necessary for quantum diagram reasoning (MFCS 2016). Roughly speaking, supplementarity consists in merging two subdiagrams when they are parameterized by antipodal angles. We introduce a generalised supplementarity -- called cyclotomic supplementarity -- which consists in merging n subdiagrams at once, when the n angles divide the circle into equal parts. We show that when n is an odd prime number, the cyclotomic supplementarity cannot be derived, leading to a countable family of new axioms for diagrammatic quantum reasoning.We exhibit another new simple axiom that cannot be derived from the existing rules of the ZX-Calculus, implying in particular the incompleteness of the language for the so-called Clifford+T quantum mechanics. We end up with a new axiomatisation of an extended ZX-Calculus, including an axiom schema for the cyclotomic supplementarity.

  @inproceedings{cyclo,
      author = {Emmanuel Jeandel and Simon Perdrix and Renaud Vilmart and Quanlong Wang},
      title = {{ZX-Calculus: Cyclotomic Supplementarity and Incompleteness for Clifford+T Quantum Mechanics}},
      year = {2017},
      booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
      editor = {Kim G. Larsen and Hans L. Bodlaender and Jean-Francois Raskin},
      series = {Leibniz International Proceedings in Informatics (LIPIcs)},
      volume = {83},
      pages = {11:1--11:13},
      publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
      doi = {10.4230/LIPIcs.MFCS.2017.11},
      link = {https://arxiv.org/abs/1702.01945},
      keywords = {ZX-Calculus, Completeness, Rational Fragment},
      abstract = {The ZX-Calculus is a powerful graphical language for quantum mechanics and quantum information processing. The completeness of the language -- i.e. the ability to derive any true equation -- is a crucial question. In the quest of a complete ZX-calculus, supplementarity has been recently proved to be necessary for quantum diagram reasoning (MFCS 2016). Roughly speaking, supplementarity consists in merging two subdiagrams when they are parameterized by antipodal angles. We introduce a generalised supplementarity -- called cyclotomic supplementarity -- which consists in merging n subdiagrams at once, when the n angles divide the circle into equal parts. We show that when n is an odd prime number, the cyclotomic supplementarity cannot be derived, leading to a countable family of new axioms for diagrammatic quantum reasoning.We exhibit another new simple axiom that cannot be derived from the existing rules of the ZX-Calculus, implying in particular the incompleteness of the language for the so-called Clifford+T quantum mechanics. We end up with a new axiomatisation of an extended ZX-Calculus, including an axiom schema for the cyclotomic supplementarity.},
      address = {Dagstuhl, Germany},
      isbn = {978-3-95977-046-0},
      issn = {1868-8969}
  }
  
  

• Y-Calculus: A Language for Real Matrices Derived from the ZX-Calculus, Emmanuel Jeandel, Simon Perdrix and Renaud Vilmart, Proceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017 (2018).
  Keywords: Y-Calculus, Completeness, Real Fragment. Abstract   Bibdata
  We introduce a ZX-like diagrammatic language devoted to manipulating real matrices - and rebits -, with its own set of axioms. We prove the necessity of some non trivial axioms of these. We show that some restriction of the language is complete. We exhibit two interpretations to and from the ZX-Calculus, thus showing the consistency between the two languages. Finally, we derive from our work a way to extract the real or imaginary part of a ZX-diagram, and prove that a restriction of our language is complete if the equivalent restriction of the ZX-calculus is complete.

  @inproceedings{EPTCS266.2,
      author = {Jeandel, Emmanuel and Perdrix, Simon and Vilmart, Renaud},
      title = {Y-Calculus: A Language for Real Matrices Derived from the ZX-Calculus},
      year = {2018},
      booktitle = {Proceedings 14th International Conference on
  Quantum Physics and Logic,
  Nijmegen, The Netherlands, 3-7 July 2017},
      editor = {Coecke, Bob and Kissinger, Aleks},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {266},
      pages = {23-57},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.266.2},
      link = {https://arxiv.org/abs/1702.00934},
      keywords = {Y-Calculus, Completeness, Real Fragment},
      abstract = {We introduce a ZX-like diagrammatic language devoted to manipulating real matrices - and rebits -, with its own set of axioms. We prove the necessity of some non trivial axioms of these. We show that some restriction of the language is complete. We exhibit two interpretations to and from the ZX-Calculus, thus showing the consistency between the two languages. Finally, we derive from our work a way to extract the real or imaginary part of a ZX-diagram, and prove that a restriction of our language is complete if the equivalent restriction of the ZX-calculus is complete.}
  }
  
  

• Picturing Quantum Processes, Bob Coecke and Aleks Kissinger, Cambridge University Press (2017).
  Keywords: . Abstract   Bibdata
  The unique features of the quantum world are explained in this book through the language of diagrams, setting out an innovative visual method for presenting complex theories. Requiring only basic mathematical literacy, this book employs a unique formalism that builds an intuitive understanding of quantum features while eliminating the need for complex calculations. This entirely diagrammatic presentation of quantum theory represents the culmination of ten years of research, uniting classical techniques in linear algebra and Hilbert spaces with cutting-edge developments in quantum computation and foundations. Written in an entertaining and user-friendly style and including more than one hundred exercises, this book is an ideal first course in quantum theory, foundations, and computation for students from undergraduate to PhD level, as well as an opportunity for researchers from a broad range of fields, from physics to biology, linguistics, and cognitive science, to discover a new set of tools for studying processes and interaction.

  @book{CKbook,
      author = {Coecke, Bob and Kissinger, Aleks},
      title = {Picturing Quantum Processes},
      year = {2017},
      journal = {Cambridge University Press},
      publisher = {Cambridge University Press},
      link = {https://www.amazon.com/Picturing-Quantum-Processes-Diagrammatic-Reasoning/dp/110710422X},
      abstract = {The unique features of the quantum world are explained in this book through the language of diagrams, setting out an innovative visual method for presenting complex theories. Requiring only basic mathematical literacy, this book employs a unique formalism that builds an intuitive understanding of quantum features while eliminating the need for complex calculations. This entirely diagrammatic presentation of quantum theory represents the culmination of ten years of research, uniting classical techniques in linear algebra and Hilbert spaces with cutting-edge developments in quantum computation and foundations. Written in an entertaining and user-friendly style and including more than one hundred exercises, this book is an ideal first course in quantum theory, foundations, and computation for students from undergraduate to PhD level, as well as an opportunity for researchers from a broad range of fields, from physics to biology, linguistics, and cognitive science, to discover a new set of tools for studying processes and interaction.}
  }
  
  

2016

• Graphical Structures for Design and Verification of Quantum Error Correction, Nicholas Chancellor, Aleks Kissinger, Joschka Roffe, Stefan Zohren and Dominic Horsman, arXiv preprint arXiv:1611.08012 (2016).
  Keywords: ZX-Calculus, Quantomatic, Error correcting codes. Abstract   Bibdata
  We introduce a high-level graphical framework for the design, analysis, and verification of quantum error correcting codes. The coherent parity check construction for stabilizer codes allows us to construct a broad range of quantum codes based on classical codes, and gives a framework in which large classes of such codes can be both analytically and numerically discovered. Using graphical tools based on the \zx calculus, we explicitly construct small distance 3 and 5 codes with high code rates using this framework. We also show how this framework can be used to represent CSS codes and conversely how to compute stabilisers for a CPC code. We give a construction turns (almost) any pair of classical [n,k,3] codes into a [[2n - k + 2, k, 3]] CPC code, and give a straightforward technique for machine search which yields thousands of potential codes, and demonstrate its operation for distance 3 and 5 codes. Finally we use the graphical tools we introduce to demonstrate how Clifford computation can be performed within CPC codes.

  @article{chancellor2016coherent,
      author = {Chancellor, Nicholas and Kissinger, Aleks and Roffe, Joschka and Zohren, Stefan and Horsman, Dominic},
      title = {Graphical Structures for Design and Verification of Quantum Error Correction},
      year = {2016},
      journal = {arXiv preprint arXiv:1611.08012},
      link = {https://arxiv.org/abs/1611.08012},
      keywords = {ZX-Calculus, Quantomatic, Error correcting codes},
      abstract = {We introduce a high-level graphical framework for the design, analysis, and verification of quantum error correcting codes. The coherent parity check construction for stabilizer codes allows us to construct a broad range of quantum codes based on classical codes, and gives a framework in which large classes of such codes can be both analytically and numerically discovered. Using graphical tools based on the \zx calculus, we explicitly construct small distance 3 and 5 codes with high code rates using this framework. We also show how this framework can be used to represent CSS codes and conversely how to compute stabilisers for a CPC code. We give a construction turns (almost) any pair of classical [n,k,3] codes into a [[2n - k + 2, k, 3]] CPC code, and give a straightforward technique for machine search which yields thousands of potential codes, and demonstrate its operation for distance 3 and 5 codes. Finally we use the graphical tools we introduce to demonstrate how Clifford computation can be performed within CPC codes.}
  }
  
  

• A Simplified Stabilizer ZX-calculus, Miriam Backens, Simon Perdrix and Quanlong Wang, Proceedings 13th International Conference on Quantum Physics and Logic, Glasgow, Scotland, 6-10 June 2016 (2017).
  Keywords: ZX-Calculus, Completeness, Clifford Fragment. Abstract   Bibdata
  The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics.The language is sound and complete: a stabilizer ZX-diagram can be transformed into another one if and only if these two diagrams represent the same quantum evolution or quantum state. We show that the stabilizer ZX-calculus can be simplified, removing unnecessary equations while keeping only the essential axioms which potentially capture fundamental structures of quantum mechanics. We thus give a significantly smaller set of axioms and prove that meta-rules like 'colour symmetry' and 'upside-down symmetry', which were considered as axioms in previous versions of the language, can in fact be derived. In particular, we show that the additional symbol and one of the rules which had been recently introduced to keep track of scalars (diagrams with no inputs or outputs) are not necessary.

  @inproceedings{BackensSimplified,
      author = {Backens, Miriam and Perdrix, Simon and Wang, Quanlong},
      title = {A Simplified Stabilizer ZX-calculus},
      year = {2017},
      booktitle = {Proceedings 13th International Conference on Quantum Physics and Logic, Glasgow, Scotland, 6-10 June 2016},
      editor = {Duncan, Ross and Heunen, Chris},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {236},
      pages = {1-20},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.236.1},
      link = {https://arxiv.org/abs/1602.04744},
      keywords = {ZX-Calculus, Completeness, Clifford Fragment},
      abstract = {The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics.The language is sound and complete: a stabilizer ZX-diagram can be transformed into another one if and only if these two diagrams represent the same quantum evolution or quantum state. We show that the stabilizer ZX-calculus can be simplified, removing unnecessary equations while keeping only the essential axioms which potentially capture fundamental structures of quantum mechanics. We thus give a significantly smaller set of axioms and prove that meta-rules like 'colour symmetry' and 'upside-down symmetry', which were considered as axioms in previous versions of the language, can in fact be derived. In particular, we show that the additional symbol and one of the rules which had been recently introduced to keep track of scalars (diagrams with no inputs or outputs) are not necessary.}
  }
  
  

• Completeness and the ZX-calculus, Miriam Backens, PhD Thesis (2016).
  Keywords: ZX-Calculus, Completeness, PhD Thesis. Abstract   Bibdata
  Graphical languages offer intuitive and rigorous formalisms for quantum physics. They can be used to simplify expressions, derive equalities, and do computations. Yet in order to replace conventional formalisms, rigour alone is not sufficient: the new formalisms also need to have equivalent deductive power. This requirement is captured by the property of completeness, which means that any equality that can be derived using some standard formalism can also be derived graphically. In this thesis, I consider the ZX-calculus, a graphical language for pure state qubit quantum mechanics. I show that it is complete for pure state stabilizer quantum mechanics, so any problem within this fragment of quantum theory can be fully analysed using graphical methods. This includes questions of central importance in areas such as error-correcting codes or measurement-based quantum computation. Furthermore, I show that the ZX-calculus is complete for the single-qubit Clifford+T group, which is approximately universal: any single-qubit unitary can be approximated to arbitrary accuracy using only Clifford gates and the T-gate. Lastly, I extend the use of rigorous graphical languages outside quantum theory to Spekkens' toy theory, a local hidden variable model that nevertheless exhibits some features commonly associated with quantum mechanics. I develop a graphical calculus similar to the ZX-calculus that fully describes Spekkens' toy theory, and show that it is complete. Hence, stabilizer quantum mechanics and Spekkens' toy theory can be fully analysed and compared using graphical formalisms. Intuitive graphical languages can replace conventional formalisms for the analysis of many questions in quantum computation and foundations without loss of mathematical rigour or deductive power.

  @phdthesis{backens_completeness_2016,
      author = {Backens, Miriam},
      title = {Completeness and the ZX-calculus},
      year = {2016},
      link = {http://arxiv.org/abs/1602.08954},
      keywords = {ZX-Calculus, Completeness, PhD Thesis},
      abstract = {Graphical languages offer intuitive and rigorous formalisms for quantum physics. They can be used to simplify expressions, derive equalities, and do computations. Yet in order to replace conventional formalisms, rigour alone is not sufficient: the new formalisms also need to have equivalent deductive power. This requirement is captured by the property of completeness, which means that any equality that can be derived using some standard formalism can also be derived graphically. In this thesis, I consider the ZX-calculus, a graphical language for pure state qubit quantum mechanics. I show that it is complete for pure state stabilizer quantum mechanics, so any problem within this fragment of quantum theory can be fully analysed using graphical methods. This includes questions of central importance in areas such as error-correcting codes or measurement-based quantum computation. Furthermore, I show that the ZX-calculus is complete for the single-qubit Clifford+T group, which is approximately universal: any single-qubit unitary can be approximated to arbitrary accuracy using only Clifford gates and the T-gate. Lastly, I extend the use of rigorous graphical languages outside quantum theory to Spekkens' toy theory, a local hidden variable model that nevertheless exhibits some features commonly associated with quantum mechanics. I develop a graphical calculus similar to the ZX-calculus that fully describes Spekkens' toy theory, and show that it is complete. Hence, stabilizer quantum mechanics and Spekkens' toy theory can be fully analysed and compared using graphical formalisms. Intuitive graphical languages can replace conventional formalisms for the analysis of many questions in quantum computation and foundations without loss of mathematical rigour or deductive power.},
      address = {Oxford},
      language = {English},
      month = {feb},
      note = {PhD Thesis},
      school = {University of Oxford},
      type = {PhD Thesis},
      urldate = {2016-03-01}
  }
  
  

2015

• Making the stabilizer ZX-calculus complete for scalars, Miriam Backens, Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL 2015) (2015).
  Keywords: ZX-Calculus, Completeness, Scalars. Abstract   Bibdata
  The ZX-calculus is a graphical language for quantum processes with built-in rewrite rules. The rewrite rules allow equalities to be derived entirely graphically, leading to the question of completeness: can any equality that is derivable using matrices also be derived graphically? The ZX-calculus is known to be complete for scalar-free pure qubit stabilizer quantum mechanics, meaning any equality between two pure stabilizer operators that is true up to a non-zero scalar factor can be derived using the graphical rewrite rules. Here, we replace those scalar-free rewrite rules with correctly scaled ones and show that, by adding one new diagram element and a new rewrite rule, the calculus can be made complete for pure qubit stabilizer quantum mechanics with scalars. This completeness property allows amplitudes and probabilities to be calculated entirely graphically. We also explicitly consider stabilizer zero diagrams, i.e. diagrams that represent a zero matrix, and show that two new rewrite rules suffice to make the calculus complete for those.

  @inproceedings{Backens:2015aa,
      author = {Miriam Backens},
      title = {Making the stabilizer ZX-calculus complete for scalars},
      year = {2015},
      booktitle = {Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL 2015)},
      editor = {Chris Heunen and Peter Selinger and Jamie Vicary},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {195},
      pages = {17--32},
      doi = {10.4204/EPTCS.195.2},
      link = {https://arxiv.org/abs/1507.03854},
      keywords = {ZX-Calculus, Completeness, Scalars},
      abstract = {The ZX-calculus is a graphical language for quantum processes with built-in rewrite rules. The rewrite rules allow equalities to be derived entirely graphically, leading to the question of completeness: can any equality that is derivable using matrices also be derived graphically? The ZX-calculus is known to be complete for scalar-free pure qubit stabilizer quantum mechanics, meaning any equality between two pure stabilizer operators that is true up to a non-zero scalar factor can be derived using the graphical rewrite rules. Here, we replace those scalar-free rewrite rules with correctly scaled ones and show that, by adding one new diagram element and a new rewrite rule, the calculus can be made complete for pure qubit stabilizer quantum mechanics with scalars. This completeness property allows amplitudes and probabilities to be calculated entirely graphically. We also explicitly consider stabilizer zero diagrams, i.e. diagrams that represent a zero matrix, and show that two new rewrite rules suffice to make the calculus complete for those.}
  }
  
  

• Supplementarity is Necessary for Quantum Diagram Reasoning, Simon Perdrix and Quanlong Wang, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016) (2016).
  Keywords: ZX-Calculus, Completeness, Clifford+T. Abstract   Bibdata
  The ZX-calculus is a powerful diagrammatic language for quantum mechanics and quantum information processing. We prove that its \(π/4\)-fragment is not complete, in other words the ZX-calculus is not complete for the so called "Clifford+T quantum mechanics". The completeness of this fragment was one of the main open problems in categorical quantum mechanics, a programme initiated by Abramsky and Coecke. The ZX-calculus was known to be incomplete for quantum mechanics. On the other hand, its \(π/2\)-fragment is known to be complete, i.e. the ZX-calculus is complete for the so called "stabilizer quantum mechanics". Deciding whether its \(π/4\)-fragment is complete is a crucial step in the development of the ZX-calculus since this fragment is approximately universal for quantum mechanics, contrary to the \(π/2\)-fragment. To establish our incompleteness result, we consider a fairly simple property of quantum states called supplementarity. We show that supplementarity can be derived in the ZX-calculus if and only if the angles involved in this equation are multiples of \(π/2\). In particular, the impossibility to derive supplementarity for \(π/4\) implies the incompleteness of the ZX-calculus for Clifford+T quantum mechanics. As a consequence, we propose to add the supplementarity to the set of rules of the ZX-calculus. We also show that if a ZX-diagram involves antiphase twins, they can be merged when the ZX-calculus is augmented with the supplementarity rule. Merging antiphase twins makes diagrammatic reasoning much easier and provides a purely graphical meaning to the supplementarity rule.

  @inproceedings{supplementarity,
      author = {Perdrix, Simon and Wang, Quanlong},
      title = {Supplementarity is Necessary for Quantum Diagram Reasoning},
      year = {2016},
      booktitle = {41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
      series = {Leibniz International Proceedings in Informatics (LIPIcs)},
      volume = {58},
      pages = {76:1--76:14},
      doi = {10.4230/LIPIcs.MFCS.2016.76},
      link = {https://arxiv.org/abs/1506.03055},
      keywords = {ZX-Calculus, Completeness, Clifford+T},
      abstract = {The ZX-calculus is a powerful diagrammatic language for quantum mechanics and quantum information processing. We prove that its $\pi/4$-fragment is not complete, in other words the ZX-calculus is not complete for the so called "Clifford+T quantum mechanics". The completeness of this fragment was one of the main open problems in categorical quantum mechanics, a programme initiated by Abramsky and Coecke. The ZX-calculus was known to be incomplete for quantum mechanics. On the other hand, its $\pi/2$-fragment is known to be complete, i.e. the ZX-calculus is complete for the so called "stabilizer quantum mechanics". Deciding whether its $\pi/4$-fragment is complete is a crucial step in the development of the ZX-calculus since this fragment is approximately universal for quantum mechanics, contrary to the $\pi/2$-fragment. To establish our incompleteness result, we consider a fairly simple property of quantum states called supplementarity. We show that supplementarity can be derived in the ZX-calculus if and only if the angles involved in this equation are multiples of $\pi/2$. In particular, the impossibility to derive supplementarity for $\pi/4$ implies the incompleteness of the ZX-calculus for Clifford+T quantum mechanics. As a consequence, we propose to add the supplementarity to the set of rules of the ZX-calculus. We also show that if a ZX-diagram involves antiphase twins, they can be merged when the ZX-calculus is augmented with the supplementarity rule. Merging antiphase twins makes diagrammatic reasoning much easier and provides a purely graphical meaning to the supplementarity rule.},
      address = {Krakow, Poland}
  }
  
  

• Quantomatic: A proof assistant for diagrammatic reasoning, Aleks Kissinger and Vladimir Zamdzhiev, International Conference on Automated Deduction (2015).
  Keywords: Quantomatic, Automation. Abstract   Bibdata
  Monoidal algebraic structures consist of operations that can have multiple outputs as well as multiple inputs, which have applications in many areas including categorical algebra, programming language semantics, representation theory, algebraic quantum information, and quantum groups. String diagrams provide a convenient graphical syntax for reasoning formally about such structures, while avoiding many of the technical challenges of a term-based approach. Quantomatic is a tool that supports the (semi-)automatic construction of equational proofs using string diagrams. We briefly outline the theoretical basis of Quantomatic's rewriting engine, then give an overview of the core features and architecture and give a simple example project that computes normal forms for commutative bialgebras.

  @inproceedings{kissinger2015quantomatic,
      author = {Kissinger, Aleks and Zamdzhiev, Vladimir},
      title = {Quantomatic: A proof assistant for diagrammatic reasoning},
      year = {2015},
      booktitle = {International Conference on Automated Deduction},
      pages = {326--336},
      link = {https://arxiv.org/abs/1503.01034},
      keywords = {Quantomatic, Automation},
      abstract = {Monoidal algebraic structures consist of operations that can have multiple outputs as well as multiple inputs, which have applications in many areas including categorical algebra, programming language semantics, representation theory, algebraic quantum information, and quantum groups. String diagrams provide a convenient graphical syntax for reasoning formally about such structures, while avoiding many of the technical challenges of a term-based approach. Quantomatic is a tool that supports the (semi-)automatic construction of equational proofs using string diagrams. We briefly outline the theoretical basis of Quantomatic's rewriting engine, then give an overview of the core features and architecture and give a simple example project that computes normal forms for commutative bialgebras.},
      organization = {Springer}
  }
  
  

• A diagrammatic axiomatisation for qubit entanglement, Amar Hadzihasanovic, 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (2015).
  Keywords: ZW-Calculus, Completeness. Abstract   Bibdata
  Diagrammatic techniques for reasoning about monoidal categories provide an intuitive understanding of the symmetries and connections of interacting computational processes. In the context of categorical quantum mechanics, Coecke and Kissinger suggested that two 3-qubit states, GHZ and W, may be used as the building blocks of a new graphical calculus, aimed at a diagrammatic classification of multipartite qubit entanglement that would highlight the communicational properties of quantum states, and their potential uses in cryptographic schemes. In this paper, we present a full graphical axiomatisation of the relations between GHZ and W: the ZW calculus. This refines a version of the preexisting ZX calculus, while keeping its most desirable characteristics: undirectedness, a large degree of symmetry, and an algebraic underpinning. We prove that the ZW calculus is complete for the category of free abelian groups on a power of two generators - "qubits with integer coefficients" - and provide an explicit normalisation procedure.

  @inproceedings{hadzihasanovic2015diagrammatic,
      author = {Hadzihasanovic, Amar},
      title = {A diagrammatic axiomatisation for qubit entanglement},
      year = {2015},
      booktitle = {2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science},
      pages = {573--584},
      link = {https://arxiv.org/abs/1501.07082},
      keywords = {ZW-Calculus, Completeness},
      abstract = {Diagrammatic techniques for reasoning about monoidal categories provide an intuitive understanding of the symmetries and connections of interacting computational processes. In the context of categorical quantum mechanics, Coecke and Kissinger suggested that two 3-qubit states, GHZ and W, may be used as the building blocks of a new graphical calculus, aimed at a diagrammatic classification of multipartite qubit entanglement that would highlight the communicational properties of quantum states, and their potential uses in cryptographic schemes. 
  In this paper, we present a full graphical axiomatisation of the relations between GHZ and W: the ZW calculus. This refines a version of the preexisting ZX calculus, while keeping its most desirable characteristics: undirectedness, a large degree of symmetry, and an algebraic underpinning. We prove that the ZW calculus is complete for the category of free abelian groups on a power of two generators - "qubits with integer coefficients" - and provide an explicit normalisation procedure.},
      organization = {IEEE}
  }
  
  

2014

• The ZX-calculus is complete for the single-qubit Clifford+T group, Miriam Backens, Proceedings of the 11th workshop on Quantum Physics and Logic, Kyoto, Japan, 4-6th June 2014 (2014).
  Keywords: ZX-Calculus, Clifford+T, Completeness. Abstract   Bibdata
  The ZX-calculus is a graphical calculus for reasoning about pure state qubit quantum mechanics. It is complete for pure qubit stabilizer quantum mechanics, meaning any equality involving only stabilizer operations that can be derived using matrices can also be derived pictorially. Stabilizer operations include the unitary Clifford group, as well as preparation of qubits in the state |0>, and measurements in the computational basis. For general pure state qubit quantum mechanics, the ZX-calculus is incomplete: there exist equalities involving non-stabilizer unitary operations on single qubits which cannot be derived from the current rule set for the ZX-calculus. Here, we show that the ZX-calculus for single qubits remains complete upon adding the operator T to the single-qubit stabilizer operations. This is particularly interesting as the resulting single-qubit Clifford+T group is approximately universal, i.e. any unitary single-qubit operator can be approximated to arbitrary accuracy using only Clifford operators and T.

  @inproceedings{backens2014zx,
      author = {Backens, Miriam},
      title = {The {ZX-calculus} is complete for the single-qubit {Clifford+T} group},
      year = {2014},
      booktitle = {{\rm Proceedings of the 11th workshop on}
  Quantum Physics and Logic,
  {\rm Kyoto, Japan, 4-6th June 2014}},
      editor = {Coecke, Bob and Hasuo, Ichiro and Panangaden, Prakash},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {172},
      pages = {293-303},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.172.21},
      link = {https://arxiv.org/abs/1412.8553},
      keywords = {ZX-Calculus, Clifford+T, Completeness},
      abstract = {The ZX-calculus is a graphical calculus for reasoning about pure state qubit quantum mechanics. It is complete for pure qubit stabilizer quantum mechanics, meaning any equality involving only stabilizer operations that can be derived using matrices can also be derived pictorially. Stabilizer operations include the unitary Clifford group, as well as preparation of qubits in the state |0>, and measurements in the computational basis. For general pure state qubit quantum mechanics, the ZX-calculus is incomplete: there exist equalities involving non-stabilizer unitary operations on single qubits which cannot be derived from the current rule set for the ZX-calculus. Here, we show that the ZX-calculus for single qubits remains complete upon adding the operator T to the single-qubit stabilizer operations. This is particularly interesting as the resulting single-qubit Clifford+T group is approximately universal, i.e. any unitary single-qubit operator can be approximated to arbitrary accuracy using only Clifford operators and T.}
  }
  
  

• A Complete Graphical Calculus for Spekkens’ Toy Bit Theory, Miriam Backens and Ali Nabi Duman, Foundations of Physics (2015).
  Keywords: ZX-Calculus, Spekkens Toy Model, Completeness. Abstract   Bibdata
  While quantum theory cannot be described by a local hidden variable model, it is nevertheless possible to construct such models that exhibit features commonly associated with quantum mechanics. These models are also used to explore the question of \(ψ\)-ontic versus \(ψ\)-epistemic theories for quantum mechanics. Spekkens’ toy theory is one such model. It arises from classical probabilistic mechanics via a limit on the knowledge an observer may have about the state of a system. The toy theory for the simplest possible underlying system closely resembles stabilizer quantum mechanics, a fragment of quantum theory which is efficiently classically simulable but also non-local. Further analysis of the similarities and differences between those two theories can thus yield new insights into what distinguishes quantum theory from classical theories, and \(ψ\)-ontic from \(ψ\)-epistemic theories. In this paper, we develop a graphical language for Spekkens’ toy theory. Graphical languages offer intuitive and rigorous formalisms for the analysis of quantum mechanics and similar theories. To compare quantum mechanics and a toy model, it is useful to have similar formalisms for both. We show that our language fully describes Spekkens’ toy theory and in particular, that it is complete: meaning any equality that can be derived using other formalisms can also be derived entirely graphically. Our language is inspired by a similar graphical language for quantum mechanics called the ZX-calculus. Thus Spekkens’ toy bit theory and stabilizer quantum mechanics can be analysed and compared using analogous graphical formalisms.

  @article{backens_complete_2015,
      author = {Backens, Miriam and Duman, Ali Nabi},
      title = {A Complete Graphical Calculus for Spekkens’ Toy Bit Theory},
      year = {2015},
      journal = {Foundations of Physics},
      volume = {46},
      pages = {70--103},
      doi = {10.1007/s10701-015-9957-7},
      link = {https://arxiv.org/abs/1411.1618},
      keywords = {ZX-Calculus, Spekkens Toy Model, Completeness},
      abstract = {While quantum theory cannot be described by a local hidden variable model, it is nevertheless possible to construct such models that exhibit features commonly associated with quantum mechanics. These models are also used to explore the question of $\psi$-ontic versus $\psi$-epistemic theories for quantum mechanics. Spekkens’ toy theory is one such model. It arises from classical probabilistic mechanics via a limit on the knowledge an observer may have about the state of a system. The toy theory for the simplest possible underlying system closely resembles stabilizer quantum mechanics, a fragment of quantum theory which is efficiently classically simulable but also non-local. Further analysis of the similarities and differences between those two theories can thus yield new insights into what distinguishes quantum theory from classical theories, and $\psi$-ontic from $\psi$-epistemic theories. In this paper, we develop a graphical language for Spekkens’ toy theory. Graphical languages offer intuitive and rigorous formalisms for the analysis of quantum mechanics and similar theories. To compare quantum mechanics and a toy model, it is useful to have similar formalisms for both. We show that our language fully describes Spekkens’ toy theory and in particular, that it is complete: meaning any equality that can be derived using other formalisms can also be derived entirely graphically. Our language is inspired by a similar graphical language for quantum mechanics called the ZX-calculus. Thus Spekkens’ toy bit theory and stabilizer quantum mechanics can be analysed and compared using analogous graphical formalisms.},
      issn = {0015-9018, 1572-9516},
      language = {en},
      month = {oct},
      number = {1},
      url = {http://link.springer.com/article/10.1007/s10701-015-9957-7},
      urldate = {2016-01-15}
  }
  
  

• Qutrit Dichromatic Calculus and Its Universality, Quanlong Wang and Xiaoning Bian, Electronic Proceedings in Theoretical Computer Science (2014).
  Keywords: ZX-Calculus, Qutrit, Qudit. Abstract   Bibdata
  We introduce a dichromatic calculus (RG) for qutrit systems. We show that the decomposition of the qutrit Hadamard gate is non-unique and not derivable from the dichromatic calculus. As an application of the dichromatic calculus, we depict a quantum algorithm with a single qutrit. Since it is not easy to decompose an arbitrary d ×d unitary matrix into Z and X phase gates when d > 2, the proof of the universality of qudit ZX calculus for quantum mechanics is far from trivial. We construct a counterexample to Ranchin’s universality proof, and give another proof by Lie theory that the qudit ZX calculus contains all single qudit unitary transformations, which implies that qudit ZX calculus, with qutrit dichromatic calculus as a special case, is universal for quantum mechanics.

  @article{Qtritdit,
      author = {  Wang , Quanlong and Bian,Xiaoning },
      title = {Qutrit Dichromatic Calculus and Its Universality},
      year = {2014},
      journal = {Electronic Proceedings in Theoretical Computer Science},
      link = {https://arxiv.org/abs/1406.3056},
      keywords = {ZX-Calculus, Qutrit, Qudit},
      abstract = {We introduce a dichromatic calculus (RG) for qutrit systems. We show that the decomposition of
  the qutrit Hadamard gate is non-unique and not derivable from the dichromatic calculus. As an
  application of the dichromatic calculus, we depict a quantum algorithm with a single qutrit. Since it
  is not easy to decompose an arbitrary d ×d unitary matrix into Z and X phase gates when d > 2, the
  proof of the universality of qudit ZX calculus for quantum mechanics is far from trivial. We construct
  a counterexample to Ranchin’s universality proof, and give another proof by Lie theory that the qudit
  ZX calculus contains all single qudit unitary transformations, which implies that qudit ZX calculus,
  with qutrit dichromatic calculus as a special case, is universal for quantum mechanics.}
  }
  
  

• The ZX-calculus is incomplete for quantum mechanics, Christian Schröder de Witt and Vladimir Zamdzhiev, Proceedings QPL 2014 (2014).
  Keywords: ZX-Calculus, Completeness. Abstract   Bibdata
  We prove that the ZX-calculus is incomplete for quantum mechanics. We suggest the addition of a new 'color-swap' rule, of which currently no analytical formulation is known and which we suspect may be necessary, but not sufficient to make the ZX-calculus complete.

  @inproceedings{Witt:2014aa,
      author = {Christian Schr{\"o}der de Witt and Vladimir Zamdzhiev},
      title = {The ZX-calculus is incomplete for quantum mechanics},
      year = {2014},
      booktitle = {Proceedings QPL 2014},
      series = {EPTCS},
      volume = {172},
      pages = {285-292},
      doi = {10.4204/EPTCS.172.20},
      link = {https://arxiv.org/abs/1404.3633},
      keywords = {ZX-Calculus, Completeness},
      abstract = {We prove that the ZX-calculus is incomplete for quantum mechanics. We suggest the addition of a new 'color-swap' rule, of which currently no analytical formulation is known and which we suspect may be necessary, but not sufficient to make the ZX-calculus complete.}
  }
  
  

• Depicting qudit quantum mechanics and mutually unbiased qudit theories, André Ranchin, Proceedings of the 11th workshop on Quantum Physics and Logic, Kyoto, Japan, 4-6th June 2014 (2014).
  Keywords: ZX-calculus, Qudits, Spekkens Toy Model. Abstract   Bibdata
  We generalize the ZX calculus to quantum systems of dimension higher than two. The resulting calculus is sound and universal for quantum mechanics. We define the notion of a mutually unbiased qudit theory and study two particular instances of these theories in detail: qudit stabilizer quantum mechanics and Spekkens-Schreiber toy theory for dits. The calculus allows us to analyze the structure of qudit stabilizer quantum mechanics and provides a geometrical picture of qudit stabilizer theory using D-toruses, which generalizes the Bloch sphere picture for qubit stabilizer quantum mechanics. We also use our framework to describe generalizations of Spekkens toy theory to higher dimensional systems. This gives a novel proof that qudit stabilizer quantum mechanics and Spekkens-Schreiber toy theory for dits are operationally equivalent in three dimensions. The qudit pictorial calculus is a useful tool to study quantum foundations, understand the relationship between qubit and qudit quantum mechanics, and provide a novel, high level description of quantum information protocols.

  @inproceedings{1404.1288,
      author = {Andr{\'e} Ranchin},
      title = {Depicting qudit quantum mechanics and mutually unbiased qudit theories},
      year = {2014},
      booktitle = { Proceedings of the 11th workshop on Quantum Physics and Logic, Kyoto, Japan, 4-6th June 2014},
      editor = {Coecke, Bob and Hasuo, Ichiro and Panangaden, Prakash},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {172},
      pages = {68-91},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.172.6},
      link = {https://arxiv.org/abs/1404.1288},
      keywords = {ZX-calculus, Qudits, Spekkens Toy Model},
      abstract = {We generalize the ZX calculus to quantum systems of dimension higher than two. The resulting
  calculus is sound and universal for quantum mechanics. We define the notion of a mutually unbiased
  qudit theory and study two particular instances of these theories in detail: qudit stabilizer quantum
  mechanics and Spekkens-Schreiber toy theory for dits. The calculus allows us to analyze the structure
  of qudit stabilizer quantum mechanics and provides a geometrical picture of qudit stabilizer theory
  using D-toruses, which generalizes the Bloch sphere picture for qubit stabilizer quantum mechanics.
  We also use our framework to describe generalizations of Spekkens toy theory to higher dimensional
  systems. This gives a novel proof that qudit stabilizer quantum mechanics and Spekkens-Schreiber
  toy theory for dits are operationally equivalent in three dimensions. The qudit pictorial calculus
  is a useful tool to study quantum foundations, understand the relationship between qubit and qudit
  quantum mechanics, and provide a novel, high level description of quantum information protocols.
  }
  }
  
  

2013

• Complete set of circuit equations for stabilizer quantum mechanics, André Ranchin and Bob Coecke, Physical Review A (2014).
  Keywords: ZX-Calculus, Completeness, Clifford Fragment. Abstract   Bibdata
  We find a sufficient set of equations between quantum circuits from which we can derive any other equation between stabilizer quantum circuits. To establish this result, we rely upon existing work on the completeness of the graphical ZX language for quantum processes, a two-coloured logical calculus for multi-qubit systems. The complexity of the circuit equations, as opposed to the very intuitive reading of the much smaller number of ZX equations, advocates the latter for performing computations with quantum circuits.

  @article{ranchin_complete_2014,
      author = {Ranchin, André and Coecke, Bob},
      title = {Complete set of circuit equations for stabilizer quantum mechanics},
      year = {2014},
      journal = {Physical Review A},
      volume = {90},
      doi = {10.1103/PhysRevA.90.012109},
      link = {https://arxiv.org/abs/1310.7932},
      keywords = {ZX-Calculus, Completeness, Clifford Fragment},
      abstract = {We find a sufficient set of equations between quantum circuits from which we can derive any other equation between stabilizer quantum circuits. To establish this result, we rely upon existing work on the completeness of the graphical ZX language for quantum processes, a two-coloured logical calculus for multi-qubit systems. The complexity of the circuit equations, as opposed to the very intuitive reading of the much smaller number of ZX equations, advocates the latter for performing computations with quantum circuits.},
      month = {jul},
      number = {1},
      url = {http://link.aps.org/doi/10.1103/PhysRevA.90.012109},
      urldate = {2014-11-05}
  }
  
  

• Pivoting makes the ZX-calculus complete for real stabilizers, Ross Duncan and Simon Perdrix, Proceedings of the 10th International Workshop on Quantum Physics and Logic (QPL) (2014).
  Keywords: ZX-Calculus, Clifford Fragment, Completeness. Abstract   Bibdata
  We show that pivoting property of graph states cannot be derived from the axioms of the ZX-calculus, and that pivoting does not imply local complementation of graph states. Therefore the ZX-calculus augmented with pivoting is strictly weaker than the calculus augmented with the Euler decomposition of the Hadamard gate. We derive an angle-free version of the ZX-calculus and show that it is complete for real stabilizer quantum mechanics.

  @inproceedings{DP3,
      author = {Duncan, Ross and Perdrix, Simon},
      title = {{Pivoting makes the ZX-calculus complete for real stabilizers}},
      year = {2014},
      booktitle = {Proceedings of the 10th International Workshop on Quantum Physics and Logic (QPL)},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {171},
      pages = {50-62},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.171.5},
      link = {https://arxiv.org/abs/1307.7048},
      keywords = {ZX-Calculus, Clifford Fragment, Completeness},
      abstract = {We show that pivoting property of graph states cannot be derived from the axioms of the ZX-calculus, and that pivoting does not imply local complementation of graph states. Therefore the ZX-calculus augmented with pivoting is strictly weaker than the calculus augmented with the Euler decomposition of the Hadamard gate. We derive an angle-free version of the ZX-calculus and show that it is complete for real stabilizer quantum mechanics.}
  }
  
  

• The ZX-calculus is complete for stabilizer quantum mechanics, Miriam Backens, New Journal of Physics (2014).
  Keywords: ZX-Calculus, Completeness, Clifford Fragment, Normal-form. Abstract   Bibdata
  The ZX-calculus is a graphical calculus for reasoning about quantum systems and processes. It is known to be universal for pure state qubit quantum mechanics, meaning any pure state, unitary operation and post-selected pure projective measurement can be expressed in the ZX-calculus. The calculus is also sound, i.e. any equality that can be derived graphically can also be derived using matrix mechanics. Here, we show that the ZX-calculus is complete for pure qubit stabilizer quantum mechanics, meaning any equality that can be derived using matrices can also be derived pictorially. The proof relies on bringing diagrams into a normal form based on graph states and local Clifford operations.

  @article{Backens1,
      author = {Backens, Miriam},
      title = {The ZX-calculus is complete for stabilizer quantum mechanics},
      year = {2014},
      journal = {New Journal of Physics},
      volume = {16},
      pages = {093021},
      publisher = {IOP Publishing},
      link = {https://arxiv.org/abs/1307.7025},
      keywords = {ZX-Calculus, Completeness, Clifford Fragment, Normal-form},
      abstract = {The ZX-calculus is a graphical calculus for reasoning about quantum systems and processes. It is known to be universal for pure state qubit quantum mechanics, meaning any pure state, unitary operation and post-selected pure projective measurement can be expressed in the ZX-calculus. The calculus is also sound, i.e. any equality that can be derived graphically can also be derived using matrix mechanics. Here, we show that the ZX-calculus is complete for pure qubit stabilizer quantum mechanics, meaning any equality that can be derived using matrices can also be derived pictorially. The proof relies on bringing diagrams into a normal form based on graph states and local Clifford operations.},
      number = {9}
  }
  
  

• Verifying the Steane code with Quantomatic, Ross Duncan and Maxime Lucas, Proceedings of the 10th International Workshop on Quantum Physics and Logic, Castelldefels (Barcelona), Spain, 17th to 19th July 2013 (2014).
  Keywords: ZX-Calculus, Quantomatic, Error correcting codes. Abstract   Bibdata
  In this paper we give a partially mechanized proof of the correctness of Steane's 7-qubit error correcting code, using the tool Quantomatic. To the best of our knowledge, this represents the largest and most complicated verification task yet carried out using Quantomatic.

  @inproceedings{duncan2013verifying,
      author = {Duncan, Ross and Lucas, Maxime},
      title = {Verifying the {Steane} code with {Quantomatic}},
      year = {2014},
      booktitle = {{\rm Proceedings of the 10th International Workshop on}
  Quantum Physics and Logic,
  {\rm Castelldefels (Barcelona), Spain, 17th to 19th July 2013}},
      editor = {Coecke, Bob and Hoban, Matty},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {171},
      pages = {33-49},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.171.4},
      link = {https://arxiv.org/abs/1306.4532},
      keywords = {ZX-Calculus, Quantomatic, Error correcting codes},
      abstract = {In this paper we give a partially mechanized proof of the correctness of Steane's 7-qubit error correcting code, using the tool Quantomatic. To the best of our knowledge, this represents the largest and most complicated verification task yet carried out using Quantomatic.}
  }
  
  

• The ZX calculus is incomplete for non-stabilizer quantum mechanics, Christian Schröder de Witt, University of Oxford Master thesis (2013).
  Keywords: ZX-Calculus, Completeness, Master Thesis. Abstract   Bibdata
  We prove that the ZX-calculus is incomplete for non-stabilizer quantum mechanics. We suggest additional rules to be integrated with the graphical calculus and possible further incompleteness sources. We express a simple quantum error correction circuit in Selinger's CPM construction in an attempt to obtain a graphical construction framework for general stabilizer error codes. We also provide a simple framework for the integration of gate approximation errors into the ZX-calculus, including a simple way of propagating upper approximation bounds through quantum circuits.

  @unpublished{ChristianMSC,
      author = {Schr{\"o}der de Witt, Christian },
      title = {The ZX calculus is incomplete for non-stabilizer quantum mechanics},
      year = {2013},
      link = {http://www.cs.ox.ac.uk/people/bob.coecke/Christian_thesis.pdf},
      keywords = {ZX-Calculus, Completeness, Master Thesis},
      abstract = {We prove that the ZX-calculus is incomplete for non-stabilizer quantum mechanics.   We suggest additional rules to be integrated with the graphical calculus and possible further incompleteness sources.  We express a simple quantum error correction circuit in Selinger's CPM construction in an attempt to obtain a graphical construction framework for general stabilizer error codes.  We also provide a simple framework for the integration of gate approximation errors into the ZX-calculus, including a simple way of propagating upper approximation bounds through quantum circuits.},
      note = {University of Oxford Master thesis}
  }
  
  

2012

• Superdense Coding with GHZ and Quantum Key Distribution with W in the ZX-calculus, Anne Hillebrand, Electronic Proceedings in Theoretical Computer Science (2012).
  Keywords: ZX-Calculus, Protocols. Abstract   Bibdata
  Quantum entanglement is a key resource in many quantum protocols, such as quantum teleportation and quantum cryptography. Yet entanglement makes protocols presented in Dirac notation difficult to verify. This is why Coecke and Duncan have introduced a diagrammatic language for quantum protocols, called the ZX-calculus. This diagrammatic notation is both intuitive and formally rigorous. It is a simple, graphical, high level language that emphasises the composition of systems and naturally captures the essentials of quantum mechanics. In the author's MSc thesis it has been shown for over 25 quantum protocols that the ZX-calculus provides a relatively easy and more intuitive presentation. Moreover, the author embarked on the task to apply categorical quantum mechanics on quantum security; earlier works did not touch anything but Bennett and Brassard's quantum key distribution protocol, BB84. Superdense coding with the Greenberger-Horne-Zeilinger state and quantum key distribution with the W-state are presented in the ZX-calculus in this paper.

  @article{hillebrand_superdense_2012,
      author = {Hillebrand, Anne},
      title = {Superdense Coding with GHZ and Quantum Key Distribution with W in the ZX-calculus},
      year = {2012},
      journal = {Electronic Proceedings in Theoretical Computer Science},
      volume = {95},
      pages = {103--121},
      doi = {10.4204/EPTCS.95.10},
      link = {http://arxiv.org/abs/1210.0650},
      keywords = {ZX-Calculus, Protocols},
      abstract = {Quantum entanglement is a key resource in many quantum protocols, such as quantum teleportation and quantum cryptography. Yet entanglement makes protocols presented in Dirac notation difficult to verify. This is why Coecke and Duncan have introduced a diagrammatic language for quantum protocols, called the ZX-calculus. This diagrammatic notation is both intuitive and formally rigorous. It is a simple, graphical, high level language that emphasises the composition of systems and naturally captures the essentials of quantum mechanics. In the author's MSc thesis it has been shown for over 25 quantum protocols that the ZX-calculus provides a relatively easy and more intuitive presentation. Moreover, the author embarked on the task to apply categorical quantum mechanics on quantum security; earlier works did not touch anything but Bennett and Brassard's quantum key distribution protocol, BB84. Superdense coding with the Greenberger-Horne-Zeilinger state and quantum key distribution with the W-state are presented in the ZX-calculus in this paper.},
      issn = {2075-2180},
      month = {oct},
      note = {arXiv: 1210.0650},
      urldate = {2015-01-29}
  }
  
  

• Strong complementarity and non-locality in categorical quantum mechanics, Bob Coecke, Ross Duncan, Aleks Kissinger and Quanlong Wang, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS) (2012).
  Keywords: Foundational, Category Theory. Abstract   Bibdata
  Categorical quantum mechanics studies quantum theory in the framework of dagger-compact closed categories. Using this framework, we establish a tight relationship between two key quantum theoretical notions: non-locality and complementarity. In particular, we establish a direct connection between Mermin-type non-locality scenarios, which we generalise to an arbitrary number of parties, using systems of arbitrary dimension, and performing arbitrary measurements, and a new stronger notion of complementarity which we introduce here. Our derivation of the fact that strong complementarity is a necessary condition for a Mermin scenario provides a crisp operational interpretation for strong complementarity. We also provide a complete classification of strongly complementary observables for quantum theory, something which has not yet been achieved for ordinary complementarity. Since our main results are expressed in the (diagrammatic) language of dagger-compact categories, they can be applied outside of quantum theory, in any setting which supports the purely algebraic notion of strongly complementary observables. We have therefore introduced a method for discussing non-locality in a wide variety of models in addition to quantum theory. The diagrammatic calculus substantially simplifies (and sometimes even trivialises) many of the derivations, and provides new insights. In particular, the diagrammatic computation of correlations clearly shows how local measurements interact to yield a global overall effect. In other words, we depict non-locality.

  @inproceedings{CDKZ,
      author = {Coecke, Bob and Duncan, Ross and Kissinger, Aleks and Wang, Quanlong},
      title = {Strong complementarity and non-locality in categorical quantum mechanics},
      year = {2012},
      booktitle = {Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS)},
      link = {https://arxiv.org/abs/1203.4988},
      keywords = {Foundational, Category Theory},
      abstract = {Categorical quantum mechanics studies quantum theory in the framework of dagger-compact closed categories. 
  Using this framework, we establish a tight relationship between two key quantum theoretical notions: non-locality and complementarity. In particular, we establish a direct connection between Mermin-type non-locality scenarios, which we generalise to an arbitrary number of parties, using systems of arbitrary dimension, and performing arbitrary measurements, and a new stronger notion of complementarity which we introduce here. 
  Our derivation of the fact that strong complementarity is a necessary condition for a Mermin scenario provides a crisp operational interpretation for strong complementarity. We also provide a complete classification of strongly complementary observables for quantum theory, something which has not yet been achieved for ordinary complementarity. 
  Since our main results are expressed in the (diagrammatic) language of dagger-compact categories, they can be applied outside of quantum theory, in any setting which supports the purely algebraic notion of strongly complementary observables. We have therefore introduced a method for discussing non-locality in a wide variety of models in addition to quantum theory. 
  The diagrammatic calculus substantially simplifies (and sometimes even trivialises) many of the derivations, and provides new insights. In particular, the diagrammatic computation of correlations clearly shows how local measurements interact to yield a global overall effect. In other words, we depict non-locality.},
      note = {arXiv:1203.4988}
  }
  
  

• A graphical approach to measurement-based quantum computing, Ross Duncan, arXiv preprint arXiv:1203.6242 (2013).
  Keywords: ZX-calculus, MBQC. Abstract   Bibdata
  Quantum computations are easily represented in the graphical notation known as the ZX-calculus, a.k.a. the red-green calculus. We demonstrate its use in reasoning about measurement-based quantum computing, where the graphical syntax directly captures the structure of the entangled states used to represent computations, and show that the notion of information flow within the entangled states gives rise to rewriting strategies for proving the correctness of quantum programs.

  @incollection{DuncanMBQC,
      author = {Duncan, Ross},
      title = {A graphical approach to measurement-based quantum computing},
      year = {2013},
      journal = {arXiv preprint arXiv:1203.6242},
      booktitle = {Quantum Physics and Linguistics: A Compositional, Diagrammatic Discourse},
      editor = {Chris Heunen, Mehrnoosh Sadrzadeh, and Edward Grefenstette},
      doi = {10.1093/acprof:oso/9780199646296.001.0001},
      link = {https://arxiv.org/abs/1203.6242},
      keywords = {ZX-calculus, MBQC},
      abstract = {Quantum computations are easily represented in the graphical notation known as the ZX-calculus, a.k.a. the red-green calculus. We demonstrate its use in reasoning about measurement-based quantum computing, where the graphical syntax directly captures the structure of the entangled states used to represent computations, and show that the notion of information flow within the entangled states gives rise to rewriting strategies for proving the correctness of quantum programs.},
      isbn = {9780199646296}
  }
  
  

2011

• Trichromatic Open Digraphs for Understanding Qubits, Alex Lang and Bob Coecke, Proceedings 8th International Workshop on Quantum Physics and Logic, Nijmegen, Netherlands, October 27-29, 2011 (2012).
  Keywords: ZX-Calculus. Abstract   Bibdata
  We introduce a trichromatic graphical calculus for quantum computing. The generators represent three complementary observables that are treated on equal footing, hence reflecting the symmetries of the Bloch sphere. We derive the Euler angle decomposition of the Hadamard gate within it as well as the so-called supplementary relationships, which are valid equations for qubits that were not derivable within Z/X-calculus of Coecke and Duncan. More specifically, we have: dichromatic Z/X-calculus + Euler angle decomposition of the Hadamard gate = trichromatic calculus.

  @inproceedings{EPTCS95.14,
      author = {Lang, Alex and Coecke, Bob},
      title = {Trichromatic Open Digraphs for Understanding Qubits},
      year = {2012},
      booktitle = {{\rm Proceedings 8th International Workshop on}
  Quantum Physics and Logic,
  {\rm Nijmegen, Netherlands, October 27-29, 2011}},
      editor = {Jacobs, Bart and Selinger, Peter and Spitters, Bas},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {95},
      pages = {193-209},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.95.14},
      link = {https://arxiv.org/abs/1110.2613},
      keywords = {ZX-Calculus},
      abstract = {We introduce a trichromatic graphical calculus for quantum computing. The generators represent three complementary observables that are treated on equal footing, hence reflecting the symmetries of the Bloch sphere. We derive the Euler angle decomposition of the Hadamard gate within it as well as the so-called supplementary relationships, which are valid equations for qubits that were not derivable within Z/X-calculus of Coecke and Duncan. More specifically, we have: dichromatic Z/X-calculus + Euler angle decomposition of the Hadamard gate = trichromatic calculus.}
  }
  
  

• Three qubit entanglement within graphical Z/X-calculus, Bob Coecke and Bill Edwards, Proceedings CSR 2010 Workshop on High Productivity Computations, Kazan, Russia, June 21-22, 2010 (2011).
  Keywords: ZX-Calculus, Entanglement, ZW-Calculus. Abstract   Bibdata
  The compositional techniques of categorical quantum mechanics are applied to analyse 3-qubit quantum entanglement. In particular the graphical calculus of complementary observables and corresponding phases due to Duncan and one of the authors is used to construct representative members of the two genuinely tripartite SLOCC classes of 3-qubit entangled states, GHZ and W. This nicely illustrates the respectively pairwise and global tripartite entanglement found in the W- and GHZ-class states. A new concept of supplementarity allows us to characterise inhabitants of the W class within the abstract diagrammatic calculus; these method extends to more general multipartite qubit states.

  @inproceedings{EPTCS52.3,
      author = {Coecke, Bob and Edwards, Bill},
      title = {Three qubit entanglement within graphical Z/X-calculus},
      year = {2011},
      booktitle = {Proceedings CSR 2010 Workshop on High Productivity Computations,
  Kazan, Russia, June 21-22, 2010},
      editor = {Ablayev, Farid and Coecke, Bob and Vasiliev, Alexander},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {52},
      pages = {22-33},
      publisher = {Open Publishing Association},
      doi = {10.4204/EPTCS.52.3},
      link = {https://arxiv.org/abs/1103.2811},
      keywords = {ZX-Calculus, Entanglement, ZW-Calculus},
      abstract = {The compositional techniques of categorical quantum mechanics are applied to analyse 3-qubit quantum entanglement. In particular the graphical calculus of complementary observables and corresponding phases due to Duncan and one of the authors is used to construct representative members of the two genuinely tripartite SLOCC classes of 3-qubit entangled states, GHZ and W. This nicely illustrates the respectively pairwise and global tripartite entanglement found in the W- and GHZ-class states. A new concept of supplementarity allows us to characterise inhabitants of the W class within the abstract diagrammatic calculus; these method extends to more general multipartite qubit states.}
  }
  
  

• The GHZ/W-calculus contains rational arithmetic, Bob Coecke, Aleks Kissinger, Alex Merry and Shibdas Roy, Electronic Proceedings in Theoretical Computer Science (2010).
  Keywords: ZW-Calculus, Foundational. Abstract   Bibdata
  Graphical calculi for representing interacting quantum systems serve a number of purposes: compositionally, intuitive graphical reasoning, and a logical underpinning for automation. The power of these calculi stems from the fact that they embody generalized symmetries of the structure of quantum operations, which, for example, stretch well beyond the Choi-Jamiolkowski isomorphism. One such calculus takes the GHZ and W states as its basic generators. Here we show that this language allows one to encode standard rational calculus, with the GHZ state as multiplication, the W state as addition, the Pauli X gate as multiplicative inversion, and the Pauli Z gate as additive inversion.

  @article{CKMR,
      author = {Coecke, Bob and Kissinger, Aleks and Merry, Alex and Roy, Shibdas},
      title = {The GHZ/W-calculus contains rational arithmetic},
      year = {2010},
      journal = {Electronic Proceedings in Theoretical Computer Science},
      volume = {52},
      pages = {34-48},
      link = {https://arxiv.org/abs/1103.2812},
      keywords = {ZW-Calculus, Foundational},
      abstract = {Graphical calculi for representing interacting quantum systems serve a number of purposes: compositionally, intuitive graphical reasoning, and a logical underpinning for automation. The power of these calculi stems from the fact that they embody generalized symmetries of the structure of quantum operations, which, for example, stretch well beyond the Choi-Jamiolkowski isomorphism. One such calculus takes the GHZ and W states as its basic generators. Here we show that this language allows one to encode standard rational calculus, with the GHZ state as multiplication, the W state as addition, the Pauli X gate as multiplicative inversion, and the Pauli Z gate as additive inversion.}
  }
  
  

• Quantum picturalism for topological cluster-state computing, Clare Horsman, New Journal of Physics (2011).
  Keywords: ZX-calculus, Topological Quantum Computing. Abstract   Bibdata
  Topological quantum computing is a way of allowing precise quantum computations to run on noisy and imperfect hardware. One implementation uses surface codes created by forming defects in a highly-entangled cluster state. Such a method of computing is a leading candidate for large-scale quantum computing. However, there has been a lack of sufficiently powerful high-level languages to describe computing in this form without resorting to single-qubit operations, which quickly become prohibitively complex as the system size increases. In this paper we apply the category-theoretic work of Abramsky and Coecke to the topological cluster-state model of quantum computing to give a high-level graphical language that enables direct translation between quantum processes and physical patterns of measurement in a computer - a "compiler language". We give the equivalence between the graphical and topological information flows, and show the applicable rewrite algebra for this computing model. We show that this gives us a native graphical language for the design and analysis of topological quantum algorithms, and finish by discussing the possibilities for automating this process on a large scale.

  @article{horsman2011quantum,
      author = {Horsman, Clare},
      title = {Quantum picturalism for topological cluster-state computing},
      year = {2011},
      journal = {New Journal of Physics},
      volume = {13},
      pages = {095011},
      publisher = {IOP Publishing},
      link = {https://arxiv.org/abs/1101.4722},
      keywords = {ZX-calculus, Topological Quantum Computing},
      abstract = {Topological quantum computing is a way of allowing precise quantum computations to run on noisy and imperfect hardware. One implementation uses surface codes created by forming defects in a highly-entangled cluster state. Such a method of computing is a leading candidate for large-scale quantum computing. However, there has been a lack of sufficiently powerful high-level languages to describe computing in this form without resorting to single-qubit operations, which quickly become prohibitively complex as the system size increases. In this paper we apply the category-theoretic work of Abramsky and Coecke to the topological cluster-state model of quantum computing to give a high-level graphical language that enables direct translation between quantum processes and physical patterns of measurement in a computer - a "compiler language". We give the equivalence between the graphical and topological information flows, and show the applicable rewrite algebra for this computing model. We show that this gives us a native graphical language for the design and analysis of topological quantum algorithms, and finish by discussing the possibilities for automating this process on a large scale.},
      number = {9}
  }
  
  

• Quantum Protocols involving Multiparticle Entanglement and their Representations in the ZX-calculus, Anne Hillebrand, University of Oxford Master thesis (2011).
  Keywords: ZX-Calculus, Protocols, Master Thesis. Abstract   Bibdata
  Quantum entanglement, described by Einstein as "spooky action at a distance", is a key resource in many quantum protocols, like quantum teleportation and quantum cryptography. Yet entanglement makes protocols presented in Dirac notation difficult to follow and check. This is why Coecke and Duncan have introduced a diagrammatic language for multi-qubit systems, called the red/green calculus or the ZX-calculus. This diagrammatic notation is both intuitive and formally rigorous. It is a simple, graphical, high level language that emphasises the composition of systems and naturally captures the essentials of quantum mechanics. One crucial feature that will be exploited here is the encoding of complementary observables and corresponding phase shifts. Reasoning is done by rewriting diagrams, i.e. locally replacing some part of a diagram. Diagrams are defined by their topology only; the number of inputs and outputs and the way they are connected. This exemplifies the 'flow' of information. For protocols involving multipartite entangled states, such as the GreenbergerHorne-Zeilinger and W-state, it will be shown that the zx-calculus provides a relatively easy and more intuitive presentation. Moreover, in this representation it is easier to check that protocols are correct. Protocols that will be discussed in detail are quantum teleportation, quantum cryptography, leader election, superdense coding and quantum direct communication with multipartite entangled states.

  @unpublished{Anne,
      author = {Hillebrand, Anne},
      title = {Quantum Protocols involving Multiparticle Entanglement and their Representations in the ZX-calculus},
      year = {2011},
      link = {http://www.cs.ox.ac.uk/people/bob.coecke/Anne.pdf},
      keywords = {ZX-Calculus, Protocols, Master Thesis},
      abstract = {Quantum entanglement, described by Einstein as "spooky action at a distance", is a key resource in many quantum protocols, like quantum teleportation and quantum cryptography. Yet entanglement makes protocols presented in Dirac notation difficult to follow and check. This is why Coecke and Duncan have introduced a diagrammatic language for multi-qubit systems, called the red/green calculus or the ZX-calculus. This diagrammatic notation is both intuitive and formally rigorous. It is a simple, graphical, high level language that emphasises the composition of systems and naturally captures the essentials of quantum mechanics. One crucial feature that will be exploited here is the encoding of complementary observables and corresponding phase shifts. Reasoning is done by rewriting diagrams, i.e. locally replacing some part of a diagram. Diagrams are defined by their topology only; the number of inputs and outputs and the way they are connected. This exemplifies the 'flow' of information. For protocols involving multipartite entangled states, such as the GreenbergerHorne-Zeilinger and W-state, it will be shown that the zx-calculus provides a relatively easy and more intuitive presentation. Moreover, in this representation it is easier to check that protocols are correct. Protocols that will be discussed in detail are quantum teleportation, quantum cryptography, leader election, superdense coding and quantum direct communication with multipartite entangled states.},
      note = {University of Oxford Master thesis}
  }
  
  

• Towards normal forms for GHZ/W calculus, Shibdas Roy, AIP Conference Proceedings (2011).
  Keywords: ZW-calculus, Normal-forms. Abstract   Bibdata
  Recently, a novel GHZ/W graphical calculus has been established to study and reason more intuitively about interacting quantum systems. The compositional structure of this calculus was shown to be well‐equipped to sufficiently express arbitrary mutlipartite quantum states equivalent under stochastic local operations and classical communication (SLOCC). However, it is still not clear how to explicitly identify which graphical properties lead to what states. This can be achieved if we have well‐behaved normal forms for arbitrary graphs within this calculus. This article lays down a first attempt at realizing such normal forms for a restricted class of such graphs, namely simple and regular graphs. These results should pave the way for the most general cases as part of future work.

  @inproceedings{roy2011towards,
      author = {Roy, Shibdas},
      title = {Towards normal forms for {GHZ/W} calculus},
      year = {2011},
      booktitle = {AIP Conference Proceedings},
      volume = {1384},
      pages = {112--119},
      doi = {10.1063/1.3635852},
      link = {https://aip.scitation.org/doi/abs/10.1063/1.3635852},
      keywords = {ZW-calculus, Normal-forms},
      abstract = {Recently, a novel GHZ/W graphical calculus has been established to study and reason more intuitively about interacting quantum systems. The compositional structure of this calculus was shown to be well‐equipped to sufficiently express arbitrary mutlipartite quantum states equivalent under stochastic local operations and classical communication (SLOCC). However, it is still not clear how to explicitly identify which graphical properties lead to what states. This can be achieved if we have well‐behaved normal forms for arbitrary graphs within this calculus. This article lays down a first attempt at realizing such normal forms for a restricted class of such graphs, namely simple and regular graphs. These results should pave the way for the most general cases as part of future work.},
      number = {1},
      organization = {AIP}
  }
  
  

2010

• Environment and classical channels in categorical quantum mechanics, Bob Coecke and Simon Perdrix, Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL) (2010).
  Keywords: ZX-Calculus, Foundational. Abstract   Bibdata
  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.

  @inproceedings{CPer,
      author = {Coecke, Bob and Perdrix, Simon},
      title = {Environment and classical channels in categorical quantum mechanics},
      year = {2010},
      booktitle = {Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL)},
      series = {Lecture Notes in Computer Science},
      volume = {6247},
      pages = {230-244},
      link = {https://arxiv.org/abs/1004.1598},
      keywords = {ZX-Calculus, Foundational},
      abstract = {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.},
      note = {Extended version: {a}rXiv:1004.1598}
  }
  
  

• Phase groups and the origin of non-locality for qubits, Bob Coecke, Bill Edwards and Rob Spekkens, Electronic Notes in Theoretical Computer Science (2011).
  Keywords: ZX-Calculus, Spekkens Toy Model. Abstract   Bibdata
  We describe a general framework in which we can precisely compare the structures of quantum-like theories which may initially be formulated in quite different mathematical terms. We then use this framework to compare two theories: quantum mechanics restricted to qubit stabiliser states and operations, and Spekkens's toy theory. We discover that viewed within our framework these theories are very similar, but differ in one key aspect - a four element group we term the phase group which emerges naturally within our framework. In the case of the stabiliser theory this group is Z4 while for Spekkens's toy theory the group is Z2 x Z2. We further show that the structure of this group is intimately involved in a key physical difference between the theories: whether or not they can be modelled by a local hidden variable theory. This is done by establishing a connection between the phase group, and an abstract notion of GHZ state correlations. We go on to formulate precisely how the stabiliser theory and toy theory are `similar' by defining a notion of `mutually unbiased qubit theory', noting that all such theories have four element phase groups. Since Z4 and Z2 x Z2 are the only such groups we conclude that the GHZ correlations in this type of theory can only take two forms, exactly those appearing in the stabiliser theory and in Spekkens's toy theory. The results point at a classification of local/non-local behaviours by finite Abelian groups, extending beyond qubits to finitary theories whose observables are all mutually unbiased.

  @article{CES,
      author = {Coecke, Bob and Edwards, Bill and Spekkens, Rob},
      title = {Phase groups and the origin of non-locality for qubits},
      year = {2011},
      journal = {Electronic Notes in Theoretical Computer Science},
      volume = {270},
      pages = {15-36},
      link = {https://arxiv.org/abs/1003.5005},
      keywords = {ZX-Calculus, Spekkens Toy Model},
      abstract = {We describe a general framework in which we can precisely compare the structures of quantum-like theories which may initially be formulated in quite different mathematical terms. We then use this framework to compare two theories: quantum mechanics restricted to qubit stabiliser states and operations, and Spekkens's toy theory. We discover that viewed within our framework these theories are very similar, but differ in one key aspect - a four element group we term the phase group which emerges naturally within our framework. In the case of the stabiliser theory this group is Z4 while for Spekkens's toy theory the group is Z2 x Z2. We further show that the structure of this group is intimately involved in a key physical difference between the theories: whether or not they can be modelled by a local hidden variable theory. This is done by establishing a connection between the phase group, and an abstract notion of GHZ state correlations. We go on to formulate precisely how the stabiliser theory and toy theory are `similar' by defining a notion of `mutually unbiased qubit theory', noting that all such theories have four element phase groups. Since Z4 and Z2 x Z2 are the only such groups we conclude that the GHZ correlations in this type of theory can only take two forms, exactly those appearing in the stabiliser theory and in Spekkens's toy theory. The results point at a classification of local/non-local behaviours by finite Abelian groups, extending beyond qubits to finitary theories whose observables are all mutually unbiased.},
      note = {{a}rXiv:1003.5005},
      number = {2}
  }
  
  

• The compositional structure of multipartite quantum entanglement, Bob Coecke and Aleks Kissinger, Automata, Languages and Programming (2010).
  Keywords: ZW-Calculus, Foundational. Abstract   Bibdata
  While multipartite quantum states constitute a (if not the) key resource for quantum computations and protocols, obtaining a high-level, structural understanding of entanglement involving arbitrarily many qubits is a long-standing open problem in quantum computer science. In this paper we expose the algebraic and graphical structure of the GHZ-state and the W-state, as well as a purely graphical distinction that characterises the behaviours of these states. In turn, this structure yields a compositional graphical model for expressing general multipartite states. We identify those states, named Frobenius states, which canonically induce an algebraic structure, namely the structure of a commutative Frobenius algebra (CFA). We show that all SLOCC-maximal tripartite qubit states are locally equivalent to Frobenius states. Those that are SLOCC-equivalent to the GHZ-state induce special commutative Frobenius algebras, while those that are SLOCC-equivalent to the W-state induce what we call anti-special commutative Frobenius algebras. From the SLOCC-classification of tripartite qubit states follows a representation theorem for two dimensional CFAs. Together, a GHZ and a W Frobenius state form the primitives of a graphical calculus. This calculus is expressive enough to generate and reason about arbitrary multipartite states, which are obtained by "composing" the GHZ- and W-states, giving rise to a rich graphical paradigm for general multipartite entanglement.

  @inproceedings{CK,
      author = {Coecke, Bob and Kissinger, Aleks},
      title = {The compositional structure of multipartite quantum entanglement},
      year = {2010},
      booktitle = {Automata, Languages and Programming},
      series = {Lecture Notes in Computer Science},
      pages = {297--308},
      publisher = {Springer},
      link = {http://arxiv.org/abs/1002.2540},
      keywords = {ZW-Calculus, Foundational},
      abstract = {While multipartite quantum states constitute a (if not the) key resource for quantum computations and protocols, obtaining a high-level, structural understanding of entanglement involving arbitrarily many qubits is a long-standing open problem in quantum computer science. In this paper we expose the algebraic and graphical structure of the GHZ-state and the W-state, as well as a purely graphical distinction that characterises the behaviours of these states. In turn, this structure yields a compositional graphical model for expressing general multipartite states. 
  We identify those states, named Frobenius states, which canonically induce an algebraic structure, namely the structure of a commutative Frobenius algebra (CFA). We show that all SLOCC-maximal tripartite qubit states are locally equivalent to Frobenius states. Those that are SLOCC-equivalent to the GHZ-state induce special commutative Frobenius algebras, while those that are SLOCC-equivalent to the W-state induce what we call anti-special commutative Frobenius algebras. From the SLOCC-classification of tripartite qubit states follows a representation theorem for two dimensional CFAs. 
  Together, a GHZ and a W Frobenius state form the primitives of a graphical calculus. This calculus is expressive enough to generate and reason about arbitrary multipartite states, which are obtained by "composing" the GHZ- and W-states, giving rise to a rich graphical paradigm for general multipartite entanglement.}
  }
  
  

• Rewriting measurement-based quantum computations with generalised flow, Ross Duncan and Simon Perdrix, International Colloquium on Automata, Languages, and Programming (2010).
  Keywords: ZX-Calculus, MBQC. Abstract   Bibdata
  We present a method for verifying measurement-based quantum computations, by producing a quantum circuit equivalent to a given deterministic measurement pattern. We define a diagrammatic presentation of the pattern, and produce a circuit via a rewriting strategy based on the generalised flow of the pattern. Unlike other methods for translating measurement patterns with generalised flow to circuits, this method uses neither ancilla qubits nor acausal loops.

  @inproceedings{duncan2010rewriting,
      author = {Duncan, Ross and Perdrix, Simon},
      title = {Rewriting measurement-based quantum computations with generalised flow},
      year = {2010},
      booktitle = {International Colloquium on Automata, Languages, and Programming},
      pages = {285--296},
      link = {http://personal.strath.ac.uk/ross.duncan/papers/gflow.pdf},
      keywords = {ZX-Calculus, MBQC},
      abstract = {We present a method for verifying measurement-based quantum computations, by producing a quantum circuit equivalent to a given deterministic measurement pattern. We define a diagrammatic presentation of the pattern, and produce a circuit via a rewriting strategy based on the generalised flow of the pattern. Unlike other methods for translating measurement patterns with generalised flow to circuits, this method uses neither ancilla qubits nor acausal loops.},
      organization = {Springer}
  }
  
  

• Models of Multipartite Entanglement, Michael Herrmann, University of Oxford Master thesis (2010).
  Keywords: ZW-Calculus, Entanglement, Master Thesis. Abstract   Bibdata
  While multipartite entanglement is a crucial resource for many quantum algorithms and protocols, the abstract, structural rules governing it are still not fully understood. In their recent paper, Coecke and Kissinger propose a new language called GHZ/W-calculus that aims to give a structural axiomatization of multipartite entanglement in terms of interacting ``special'' and ``anti-special'' commutative Frobenius algebras (S/A-CFAs). These algebraic structures correspond precisely to the two different types of genuine entanglement between three qubits, as given by inter-convertability by stochastic local (quantum) operations and classical communication (SLOCC). An important feature of the language is that it lives in the framework of categorical quantum mechanics and thus comes with a Penrose-Joyal-Street graphical calulus. This thesis explores the expressive power of the GHZ/W-calculus. We prove a new result that demonstrates the canonicity of the recent concept of antispeciality for CFAs and use it to give a new classification of Frobenius Algebras on \(ℂ^2\) in FdHilb, the category of finite-dimensional Hilbert spaces and bounded linear maps. Next, we look at the non-standard model of categorical quantum mechanics given by FRel, the category of finite sets and binary relations. We classify all special CFAs in this category, prove some properties of anti-special ones and identify precisely which SCFAs/ACFAs are captured by the GHZ/W-language. Finally, we define a quantum AND gate in the graphical language and prove (or disprove) some of its properties. We come to the conclusion that the GHZ/W-calculus is unlikely to be the final answer to the structural entanglement problem in dimensions \(D > 2\) and identify intermediate ranks \(1 < rank < D\) as the notion it fails to explain.

  @unpublished{HerrmannThesis,
      author = {Herrmann, Michael},
      title = {Models of Multipartite Entanglement},
      year = {2010},
      link = {http://www.cs.ox.ac.uk/people/bob.coecke/Michael.pdf},
      keywords = {ZW-Calculus, Entanglement, Master Thesis},
      abstract = {While multipartite entanglement is a crucial resource for many quantum algorithms and protocols, the abstract, structural rules governing it are still not fully understood. In their recent paper, Coecke and Kissinger propose a new language called GHZ/W-calculus that aims to give a structural axiomatization of multipartite entanglement in terms of interacting ``special'' and ``anti-special'' commutative Frobenius algebras (S/A-CFAs). These algebraic structures correspond precisely to the two different types of genuine entanglement between three qubits, as given by inter-convertability by stochastic local (quantum) operations and classical communication (SLOCC). An important feature of the language is that it lives in the framework of categorical quantum mechanics and thus comes with a Penrose-Joyal-Street graphical calulus. This thesis explores the expressive power of the GHZ/W-calculus. We prove a new result that demonstrates the canonicity of the recent concept of antispeciality for CFAs and use it to give a new classification of Frobenius Algebras on $\mathbb{C}^2$ in FdHilb, the category of finite-dimensional Hilbert spaces and bounded linear maps. Next, we look at the non-standard model of categorical quantum mechanics given by FRel, the category of finite sets and binary relations. We classify all special CFAs in this category, prove some properties of anti-special ones and identify precisely which SCFAs/ACFAs are captured by the GHZ/W-language. Finally, we define a quantum AND gate in the graphical language and prove (or disprove) some of its properties. We come to the conclusion that the GHZ/W-calculus is unlikely to be the final answer to the structural entanglement problem in dimensions $D > 2$ and identify intermediate ranks $1 < rank < D$ as the notion it fails to explain.},
      note = {University of Oxford Master thesis}
  }
  
  

2009

• Quantum picturalism, Bob Coecke, Contemporary Physics (2009).
  Keywords: ZX-Calculus, Foundational. Abstract   Bibdata
  The quantum mechanical formalism doesn't support our intuition, nor does it elucidate the key concepts that govern the behaviour of the entities that are subject to the laws of quantum physics. The arrays of complex numbers are kin to the arrays of 0s and 1s of the early days of computer programming practice. In this review we present steps towards a diagrammatic `high-level' alternative for the Hilbert space formalism, one which appeals to our intuition. It allows for intuitive reasoning about interacting quantum systems, and trivialises many otherwise involved and tedious computations. It clearly exposes limitations such as the no-cloning theorem, and phenomena such as quantum teleportation. As a logic, it supports `automation'. It allows for a wider variety of underlying theories, and can be easily modified, having the potential to provide the required step-stone towards a deeper conceptual understanding of quantum theory, as well as its unification with other physical theories. Specific applications discussed here are purely diagrammatic proofs of several quantum computational schemes, as well as an analysis of the structural origin of quantum non-locality. The underlying mathematical foundation of this high-level diagrammatic formalism relies on so-called monoidal categories, a product of a fairly recent development in mathematics. These monoidal categories do not only provide a natural foundation for physical theories, but also for proof theory, logic, programming languages, biology, cooking, ... The challenge is to discover the necessary additional pieces of structure that allow us to predict genuine quantum phenomena.

  @article{ContPhys,
      author = {Coecke, Bob},
      title = {Quantum picturalism},
      year = {2009},
      journal = {Contemporary Physics},
      volume = {51},
      pages = {59-83},
      link = {http://arxiv.org/abs/0908.1787},
      keywords = {ZX-Calculus, Foundational},
      abstract = {The quantum mechanical formalism doesn't support our intuition, nor does it elucidate the key concepts that govern the behaviour of the entities that are subject to the laws of quantum physics. The arrays of complex numbers are kin to the arrays of 0s and 1s of the early days of computer programming practice. In this review we present steps towards a diagrammatic `high-level' alternative for the Hilbert space formalism, one which appeals to our intuition. It allows for intuitive reasoning about interacting quantum systems, and trivialises many otherwise involved and tedious computations. It clearly exposes limitations such as the no-cloning theorem, and phenomena such as quantum teleportation. As a logic, it supports `automation'. It allows for a wider variety of underlying theories, and can be easily modified, having the potential to provide the required step-stone towards a deeper conceptual understanding of quantum theory, as well as its unification with other physical theories. Specific applications discussed here are purely diagrammatic proofs of several quantum computational schemes, as well as an analysis of the structural origin of quantum non-locality. The underlying mathematical foundation of this high-level diagrammatic formalism relies on so-called monoidal categories, a product of a fairly recent development in mathematics. These monoidal categories do not only provide a natural foundation for physical theories, but also for proof theory, logic, programming languages, biology, cooking, ... The challenge is to discover the necessary additional pieces of structure that allow us to predict genuine quantum phenomena.}
  }
  
  

• Interacting quantum observables: categorical algebra and diagrammatics, Bob Coecke and Ross Duncan, New Journal of Physics (2011).
  Keywords: ZX-Calculus, Foundational. Abstract   Bibdata
  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 axiomatise 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 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.

  @article{CD2,
      author = {Coecke, Bob and Duncan, Ross},
      title = {Interacting quantum observables: categorical algebra and diagrammatics},
      year = {2011},
      journal = {New Journal of Physics},
      volume = {13},
      pages = {043016},
      link = {https://arxiv.org/abs/0906.4725},
      keywords = {ZX-Calculus, Foundational},
      abstract = {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 axiomatise 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 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.}
  }
  
  

• Graph states and the necessity of Euler decomposition, Ross Duncan and Simon Perdrix, Conference on Computability in Europe (2009).
  Keywords: ZX-Calculus, Clifford Fragment, Graph-states, Foundational. Abstract   Bibdata
  Coecke and Duncan recently introduced a categorical formalisation of the interaction of complementary quantum observables. In this paper we use their diagrammatic language to study graph states, a computationally interesting class of quantum states. We give a graphical proof of the fixpoint property of graph states. We then introduce a new equation, for the Euler decomposition of the Hadamard gate, and demonstrate that Van den Nest's theorem--locally equivalent graphs represent the same entanglement--is equivalent to this new axiom. Finally we prove that the Euler decomposition equation is not derivable from the existing axioms.

  @inproceedings{DuncanPerdrixGraphStates,
      author = {Duncan, Ross and Perdrix, Simon},
      title = {Graph states and the necessity of {Euler} decomposition},
      year = {2009},
      booktitle = {Conference on Computability in Europe},
      pages = {167--177},
      link = {https://arxiv.org/abs/0902.0500},
      keywords = {ZX-Calculus, Clifford Fragment, Graph-states, Foundational},
      abstract = {Coecke and Duncan recently introduced a categorical formalisation of the interaction of complementary quantum observables. In this paper we use their diagrammatic language to study graph states, a computationally interesting class of quantum states. We give a graphical proof of the fixpoint property of graph states. We then introduce a new equation, for the Euler decomposition of the Hadamard gate, and demonstrate that Van den Nest's theorem--locally equivalent graphs represent the same entanglement--is equivalent to this new axiom. Finally we prove that the Euler decomposition equation is not derivable from the existing axioms.},
      organization = {Springer}
  }
  
  

2008

• Interacting quantum observables, Bob Coecke and Ross Duncan, Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP) (2008).
  Keywords: ZX-Calculus, Foundational. Abstract   Bibdata
  We formalise the constructive content of an essential feature of quantum mechanics: the interaction of complementary quantum observables, and information flow mediated by them. Using a general categorical formulation, we show that pairs of mutually unbiased quantum observables form bialgebra-like structures. We also provide an abstract account on the quantum data encoded in complex phases, and prove a normal form theorem for it. Together these enable us to describe all observables of finite dimensional Hilbert space quantum mechanics. The resulting equations suffice to perform computations with elementary quantum gates, translate between distinct quantum computational models, establish the equivalence of entangled quantum states, and simulate quantum algorithms such as the quantum Fourier transform. All these computations moreover happen within an intuitive diagrammatic calculus.

  @inproceedings{CD1,
      author = {Coecke, Bob and Duncan, Ross},
      title = {Interacting quantum observables},
      year = {2008},
      booktitle = {Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP)},
      series = {Lecture Notes in Computer Science},
      link = {https://ora.ox.ac.uk/objects/uuid:77175185-265b-4467-a81a-a9593ed329e7/download_file?file_format=pdf&safe_filename=Interacting%252520Quantum%252520Observables.pdf&type_of_work=Conference+item},
      keywords = {ZX-Calculus, Foundational},
      abstract = {We formalise the constructive content of an essential feature of quantum mechanics: the interaction of complementary quantum observables, and information flow mediated by them. Using a general categorical formulation, we show that pairs of mutually unbiased quantum observables form bialgebra-like structures. We also provide an abstract account on the quantum data encoded in complex phases, and prove a normal form theorem for it. Together these enable us to describe all observables of finite dimensional Hilbert space quantum mechanics. The resulting equations suffice to perform computations with elementary quantum gates, translate between distinct quantum computational models, establish the equivalence of entangled quantum states, and simulate quantum algorithms such as the quantum Fourier transform. All these computations moreover happen within an intuitive diagrammatic calculus.}
  }