We introduce the PBS-calculus to represent and reason on quantum computations involving coherent control of quantum operations. Coherent control, and in particular indefinite causal order, is known to enable multiple computational and communication advantages over classically ordered models like quantum circuits. The PBS-calculus is inspired by quantum optics, in particular the polarising beam splitter (PBS for short). We formalise the syntax and the semantics of the PBS-diagrams, and we equip the language with an equational theory, which is proved to be sound and complete: two diagrams are representing the same quantum evolution if and only if one can be transformed into the other using the rules of the PBS-calculus. Moreover, we show that the equational theory is minimal. Finally, we consider applications like the implementation of controlled permutations and the unrolling of loops.
We introduce a graphical language for coherent control of general quantum channels inspired by practical quantum optical setups involving polarising beam splitters (PBS). As standard completely positive trace preserving maps are known not to be appropriate to represent coherently controlled quantum channels, we propose to instead use purified channels, an extension of Stinespring's dilation. We characterise the observational equivalence of purified channels in various coherent-control contexts, paving the way towards a faithful representation of quantum channels under coherent control.
We introduce the LOv-calculus, a graphical language for reasoning about linear optical quantum circuits with so-called vacuum state auxiliary inputs. We present the axiomatics of the language and prove its soundness and completeness: two LOv-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the LOv-calculus. We give a confluent and terminating rewrite system to rewrite any polarisation-preserving LOv-circuit into a unique triangular normal form, inspired by the universal decomposition of Reck et al. (1994) for linear optical quan…
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 abstrac…
Different graphical calculi have been proposed to represent quantum computation. First the ZX- calculus [4], followed by the ZW-calculus [12] and then the ZH-calculus [1]. We can wonder if new Z*-calculi will continue to be proposed forever. This article answers negatively. All those language share a common core structure we call Z*-algebras. We classify Z*-algebras up to isomorphism in two dimensional Hilbert spaces and show that they are all variations of the aforementioned calculi. We do the same for linear relations and show that the calculus of [2] is essentially the unique one.
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 representati…
Graphical calculus is an intuitive visual notation for manipulating tensors and index contractions. Using graphical calculus leads to simple and memorable derivations, and with a bit of practice one can learn to prove complex identities even without the need for pen and paper. This manuscript is meant as a demonstration of the power and flexibility of graphical notation and we advocate exploring the use of graphical calculus in undergraduate courses. In the first part we define the following matrix products in graphical language: dot, tensor, Kronecker, Hadamard, Kathri-Rao and Tracy-Singh. We…
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 exploi…
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.
Graphical calculi such as the ZH-calculus are powerful tools in the study and analysis of quantum processes, with links to other models of quantum computation such as quantum circuits, measurement-based computing, etc. A somewhat compact but systematic way to describe a quantum process is through the use of quantum multiple-valued decision diagrams (QMDDs), which have already been used for the synthesis of quantum circuits as well as for verification. We show in this paper how to turn a QMDD into an equivalent ZH-diagram, and vice-versa, and show how reducing a QMDD translates in the ZH-Calcul…
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, th…
We describe a graphical calculus for completely positive maps and in doing so review the theory of open quantum systems and other fundamental primitives of quantum information theory using the language of tensor networks. In particular we demonstrate the construction of tensor networks to pictographically represent the Liouville-superoperator, Choi-matrix, process-matrix, Kraus, and system-environment representations for the evolution of quantum states, review how these representations interrelate, and illustrate how graphical manipulations of the tensor networks may be used to concisely trans…
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 scal…
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.
We give a complete presentation for the fragment, ZX&, of the ZX-calculus generated by the Z and X spiders (corresponding to copying and addition) along with the not gate and the and gate. To prove completeness, we freely add a unit and counit to the category TOF generated by the Toffoli gate and ancillary bits, showing that this yields the full subcategory of finite ordinals and functions with objects powers of two; and then perform a two way translation between this category and ZX&. A translation to some extension of TOF, as opposed to some fragment of the ZX-calculus, is a natural choice b…
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 exampl…
The ZX-calculus was introduced as a graphical language able to represent specific quantum primitives in an intuitive way. The recent completeness results have shown the theoretical possibility of a purely graphical description of quantum processes. However, in practice, such approaches are limited by the intrinsic low level nature of ZX calculus. The scalable notations have been proposed as an attempt to recover an higher level point of view while maintaining the topological rewriting rules of a graphical language. We demonstrate that the scalable ZX-calculus provides a formal, intuitive, and …
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…
The prop formalism allows representation of processes withstring diagrams and has been successfully applied in various areas such as quantum computing, electric circuits and control flow graphs. However, these graphical approaches suffer from scalability problems when it comes to writing large diagrams. A proposal to tackle this issue has been investigated for ZX-calculus using colored props. This paper extends the approach to any prop, making it a general tool for graphical languages manipulation.
We provide a unified graphical calculus for all Gaussian pure states, including graph transformation rules for all local and semi-local Gaussian unitary operations, as well as local quadrature measurements. We then use this graphical calculus to analyze continuous-variable (CV) cluster states, the essential resource for one-way quantum computing with CV systems. Current graphical approaches to CV cluster states are only valid in the unphysical limit of infinite squeezing, and the associated graph transformation rules only apply when the initial and final states are of this form. Our formalism …
In 2008 Coecke and Duncan proposed the graphical ZX-calculus rewrite system which came to formalize reasoning with quantum circuits, measurements and quantum states. The ZX-calculus is sound for qubit quantum mechanics. Hence, equality of diagrams under ZX-equivalent transformations lifts to an equality of corresponding equations over matrices. Conversely, in 2014 Backens proved completeness, establishing that any derivation done in stabilizer quantum mechanics with matrices can be derived graphically using the ZX-calculus. A graphical rewrite system that is both confluent and also terminates …
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 quan…
This paper is the first of a series where we study quantum channels from the random matrix point of view. We develop a graphical tool that allows us to compute the expected moments of the output of a random quantum channel. As an application, we study variations of random matrix models introduced by Hayden \cite{hayden}, and show that their eigenvalues converge almost surely. In particular we obtain for some models sharp improvements on the value of the largest eigenvalue, and this is shown in a further work to have new applications to minimal output entropy inequalities.
We provide a graphical calculus for computing averages of tensor network diagrams with respect to the distribution of random vectors containing independent uniform complex phases. Our method exploits the order structure of the partially ordered set of uniform block permutations. A similar calculus is developed for random vectors consisting of independent uniform signs, based on the combinatorics of the partially ordered set of even partitions. We employ our method to extend some of the results by Johnston and MacLean on the family of local diagonal unitary invariant matrices. Furthermore, our …
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 rel…
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 Fourie…
Categorical Quantum Mechanics, and graphical calculi in particular, has proven to be an intuitive and powerful way to reason about quantum computing. This work continues the exploration of graphical calculi, inside and outside of the quantum computing setting, by investigating the algebraic structures with which we label diagrams. The initial aim for this was Conjecture Synthesis; the algorithmic process of creating theorems. To this process we introduce a generalisation step, which itself requires the ability to infer and then verify parameterised families of theorems. This thesis introduces …
ZX-calculus is a graphical language for quantum computing which is complete in the sense that calculation in matrices can be done in a purely diagrammatic way. However, all previous universally complete axiomatisations of ZX-calculus have included at least one rule involving trigonometric functions such as sin and cos which makes it difficult for application purpose. In this paper we give an algebraic complete axiomatisation of ZX-calculus instead such that there are only ring operations involved for phases. With this algebraic axiomatisation of ZX-calculus, we are able to establish for the fi…
Graphical languages, like quantum circuits or ZX-calculus, have been successfully designed to represent (memoryless) quantum computations acting on a finite number of qubits. Meanwhile, delayed traces have been used as a graphical way to represent finite-memory computations on streams, in a classical setting (cartesian data types). We merge those two approaches and describe a general construction that extends any graphical language, equipped with a notion of discarding, to a graphical language of finite memory computations. In order to handle cases like the ZX-calculus, which is complete for p…
We introduce a graphical framework for Bayesian inference that is sufficiently general to accommodate not just the standard case but also recent proposals for a theory of quantum Bayesian inference wherein one considers density operators rather than probability distributions as representative of degrees of belief. The diagrammatic framework is stated in the graphical language of symmetric monoidal categories and of compact structures and Frobenius structures therein, in which Bayesian inversion boils down to transposition with respect to an appropriate compact structure. We characterize classi…
Symplectic vector spaces are the phase spaces of linear mechanical systems. The symplectic form describes, for example, the relation between position and momentum as well as current and voltage. The category of linear Lagrangian relations between symplectic vector spaces is a symmetric monoidal subcategory of relations which gives a semantics for the evolution -- and more generally linear constraints on the evolution -- of various physical systems. We give a new presentation of the category of Lagrangian relations over an arbitrary field as a `doubled' category of linear relations. More precis…
ZX-calculus is graphical language for quantum computing which usually focuses on qubits. In this paper, we generalise qubit ZX-calculus to qudit ZX-calculus in any finite dimension by introducing suitable generators, especially a carefully chosen triangle node. As a consequence we obtain a set of rewriting rules which can be seen as a direct generalisation of qubit rules, and a normal form for any qudit vectors. Based on the qudit ZX-calculi, we propose a graphical formalism called qufinite ZX-calculus as a unified framework for all qudit ZX-calculi, which is universal for finite quantum theor…
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 axiomati…
The ZX-calculus is a graphical language for reasoning about quantum computation that has recently seen an increased usage in a variety of areas such as quantum circuit optimisation, surface codes and lattice surgery, measurement-based quantum computation, and quantum foundations. The first half of this review gives a gentle introduction to the ZX-calculus suitable for those familiar with the basics of quantum computing. The aim here is to make the reader comfortable enough with the ZX-calculus that they could use it in their daily work for small computations on quantum circuits and states. The…
The ZH-calculus is a complete graphical calculus for linear maps between qubits that admits a straightforward encoding of hypergraph states and circuits arising from the Toffoli+Hadamard gate set. In this paper, we establish a correspondence between the ZH-calculus and the path-sum formalism, a technique recently introduced by Amy to verify quantum circuits. In particular, we find a bijection between certain canonical forms of ZH-diagrams and path-sum expressions. We then introduce and prove several new simplification rules for the ZH-calculus, which are in direct correspondence to the simplif…
Optimizing quantum circuits is a key challenge for quantum computing. The PyZX compiler broke new ground by optimizing circuits via the ZX calculus, a powerful graphical alternative to the quantum circuit model. Still, it carries no guarantee of its correctness. To address this, we developed VyZX, a verified ZX-calculus in the Coq proof assistant. VyZX provides two distinct representations of ZX diagrams for ease of programming and proof: A graph-based representation for writing high-level functions on diagrams and a block-based representation for proving ZX diagrams equivalent. Through these …
