The ZX Seminar
Initiated at University of Oxford, the weekly ZX seminar provides a virtual venue for researchers to share their work related to the ZX calculus.
It is chaired by John van de Wetering, co-organized by Alexander Koziell-Pipe and Sarah Meng Li.
Fall 2024 Schedule
Time: 8 - 9:30 am ET = 1 - 2:30 pm UK = 2 - 3:30 pm Netherlands
Abstract: In this special edition, leading minds from different aspects of ZX research will share the state of the art and discuss interesting open problems. We aim to provide a bird's eye view of different research directions and trigger interdisciplinary discussions.
Below are invited speakers, their discussion topics and slides, as well as the recordings. This is displayed according to the order of presentation.
Speakers | Topics | Recording | Slides | |||
---|---|---|---|---|---|---|
Education | ||||||
Measurement-Based Quantum Computing | ||||||
Quantum Compilation | Pending | |||||
ZX Completeness | ||||||
Machine Learning | ||||||
Quantum Error Correction |
Monday September 30th: Redefining Lexicographical Ordering: Optimizing Pauli String Decompositions for Quantum Compiling
Speaker: Qunsheng Huang (Technical University of Munich)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands/Germany
Abstract: In quantum computing, the efficient optimization of Pauli string decompositions is a crucial aspect for the compilation of quantum circuits for many applications, such as chemistry simulations and quantum machine learning. In this paper, we propose a novel algorithm for the synthesis of trotterized time-evolution operators that results in circuits with significantly fewer gates than previous solutions. Our synthesis procedure takes the qubit connectivity of a target quantum computer into account. As a result, the generated quantum circuit does not require routing, and no additional CNOT gates are needed to run the resulting circuit on a target device. We compare our algorithm against Paulihedral and TKET, and show a significant improvement for randomized circuits and different molecular ansatzes. We also investigate the Trotter error introduced by our ordering of the terms in the Hamiltonian versus default ordering and the ordering from the baseline methods and conclude that our method on average does not increase the Trotter error.
Joint-Work With: David Winderl, Arianne Meijer–van de Griend, Richie Yeung
Recording:
https://youtu.be/LlNTQqqwn4gMonday October 7th: Genons, Double Covers and Fault-tolerant Clifford Gates
Speaker: Simon Burton (Quantinuum)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: A great deal of work has been done developing quantum codes with varying overhead and connectivity constraints. However, given the such an abundance of codes, there is a surprising shortage of fault-tolerant logical gates supported therein. We define a construction, such that given an input \([[n, k, d]]\) code, yields a \([[2n, 2k, \geq d]]\) symplectic double code with naturally occurring fault-tolerant logical Clifford gates. As applied to 2-dimensional \(D(\mathbb{Z}_2)\)-topological codes with genons (twists) and domain walls, we find the symplectic double is genon free, and of possibly higher genus. Braiding of genons on the original code becomes Dehn twists on the symplectic double. Such topological operations are particularly suited for architectures with all-to-all connectivity, and we demonstrate this experimentally on Quantinuum’s H1-1 trapped-ion quantum computer.
Joint-Work With: Elijah Durso-Sabina and Natalie C. Brown
Recording:
https://youtu.be/mpdJdBFZNIAMonday October 14th: Minimal Complete ZW-Calculi for Qudit and Mixed Dimensional Systems
Speakers: Renaud Vilmart (Université Paris-Saclay)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands/France
Abstract: The ZW-calculus is a graphical language capable of representing 2-dimensional quantum systems (qubit) through its diagrams, and manipulating them through its equational theory. We extend the formalism to accommodate finite dimensional Hilbert spaces beyond qubit systems.
First we define a qu\(\mathbf{d}\)it version of the language, where all systems have the same arbitrary finite dimension d, and show that the provided equational theory is both complete – i.e. semantical equivalence is entirely captured by the equations – and minimal – i.e. none of the equations are consequences of the others. We then extend the graphical language further to allow for mixed-dimensional systems. We again show the completeness and minimality of the provided equational theory.
Joint-Work With: Marc de Visme
Recording:
https://youtu.be/-lUqneUsRYkMonday October 21st: Qubit-Count Optimization Using ZX-Calculus
Speaker: Vivien Vandaele (Eviden Quantum Lab and Université de Lorraine)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands/France
Abstract: We propose several methods for optimizing the number of qubits in a quantum circuit while preserving the number of non-Clifford gates. One of our approaches consists in reversing, as much as possible, the gadgetization of Hadamard gates, which is a procedure used by some T-count optimizers to circumvent Hadamard gates at the expense of additional qubits. We prove the NP-hardness of this problem and we present an algorithm for solving it. We also propose a more general approach to optimize the number of qubits by showing how it relates to the problem of finding a minimal-width path-decomposition of the graph associated with a given ZX-diagram. This approach can be used to optimize the number of qubits for any computational model that can natively be depicted in ZX-calculus, such as the Pauli Fusion computational model which can represent lattice surgery operations. We also show how this method can be used to efficiently optimize the number of qubits in a quantum circuit by using the ZX-calculus as an intermediate representation.
Recording:
https://youtu.be/7RkmBX_96ikMonday October 28th: Quantum Picturalism: Learning Quantum Theory in High School
Speaker: Lia Yeh (Quantinuum and University of Oxford)
Time: 10 - 11 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: Quantum theory is often regarded as challenging to learn and teach, with advanced mathematical prerequisites ranging from complex numbers and probability theory to matrix multiplication, vector space algebra and symbolic manipulation within the Hilbert space formalism. It is traditionally considered an advanced undergraduate or graduate-level subject. In this work, we challenge the conventional view by proposing “Quantum Picturalism” as a new approach to teaching the fundamental concepts of quantum theory and computation. We establish the foundations and methodology for an ongoing educational experiment to investigate the question “From what age can students learn quantum theory if taught using a diagrammatic approach?”. We anticipate that the primary benefit of leveraging such a diagrammatic approach, which is conceptually intuitive yet mathematically rigorous, will be eliminating some of the most daunting barriers to teaching and learning this subject while enabling young learners to reason proficiently about high-level problems. We posit that transitioning from symbolic presentations to pictorial ones will increase the appeal of STEM education, attracting more diverse audience.
Joint-Work With: Selma Dundar-Coecke, Caterina Puca, Sieglinde M.-L. Pfaendler, Muhammad Hamza Waseem, Thomas Cervoni, Aleks Kissinger, Stefano Gogioso, and Bob Coecke
Recording:
https://youtu.be/Je2I-Z74p7kMonday November 4th: Catalysing Completeness and Universality
Speaker: John van de Wetering (University of Amsterdam)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: A catalysis state is a quantum state that is used to make some desired operation possible or more efficient, while not being consumed in the process. Recent years have seen catalysis used in state-of-the-art protocols for implementing magic state distillation or small angle phase rotations. In this paper we will see that we can also use catalysis to prove that certain gate sets are computationally universal, and to extend completeness results of graphical languages to larger fragments. In particular, we give a simple proof of the computational universality of the CS+Hadamard gate set using the catalysis of a T gate using a CS gate, which sidesteps the more complicated analytic arguments of the original proof by Kitaev. This then also gives us a simple self-contained proof of the computational universality of Toffoli+Hadamard. Additionally, we show that the phase-free ZH-calculus can be extended to a larger complete fragment, just by using a single catalysis rule (and one scalar rule).
Joint-Work With: Aleks Kissinger and Neil J. Ross
Recording:
https://youtu.be/guZ5cVECJGIMonday November 11th: Towards Faster Quantum Circuit Simulation Using Graph Decompositions, GNNs and Reinforcement Learning
Speaker: Alexander Koziell-Pipe (University of Oxford)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: In this work, we train a graph neural network with reinforcement learning to more efficiently simulate quantum circuits using the ZX-calculus. Our experiments show a marked improvement in simulation efficiency using the trained model over existing methods that do not incorporate AI. In this way, we demonstrate a machine learning model that can reason effectively within a mathematical framework such that it enhances scientific research in the important domain of quantum computing.
Joint-Work With: Richie Yeung and Matthew Sutcliffe
Recording:
https://youtu.be/fTN_AiLbepgMonday November 18th: The XYZ Ruby Code: Making a Case for a Three-Colored Graphical Calculus for Quantum Error Correction in Spacetime
Speakers: Julio C. Magdalena de la Fuente (Freie Universität Berlin) and Josias Old (Forschungszentrum Jülich, RWTH Aachen University)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands/Germany
Abstract: Analyzing and developing new quantum error-correcting schemes is one of the most prominent tasks in quantum computing research. In such efforts, introducing time dynamics explicitly in both analysis and design of error-correcting protocols constitutes an important cornerstone. In this work, we present a graphical formalism based on tensor networks to capture the logical action and error-correcting capabilities of any Clifford circuit with Pauli measurements. We showcase the functioning of the formalism on new Floquet codes derived from topological subsystem codes, which we call XYZ ruby codes. Based on the projective symmetries of the building blocks of the tensor network we develop a framework of Pauli flows. Pauli flows allow for a graphical understanding of all quantities entering an error correction analysis of a circuit, including different types of QEC experiments, such as memory and stability experiments. We lay out how to derive a well-defined decoding problem from the tensor network representation of a protocol and its Pauli flows alone, independent of any stabilizer code or fixed circuit. Importantly, this framework applies to all Clifford protocols and encompasses both measurement-based and circuit-based approaches to fault tolerance. We apply our method to our new family of dynamical codes which are in the same topological phase as the \(2+1\)-dimensional color code, making them a promising candidate for low-overhead logical gates. In contrast to its static counterpart, the dynamical protocol applies a \(\mathbb{Z}_3\) automorphism to the logical Pauli group every three timesteps. We highlight some of its topological properties and comment on the anyon physics behind a planar layout. Lastly, we benchmark the performance of the XYZ ruby code on a torus by performing both memory and stability experiments and find competitive circuit-level noise thresholds of \(\approx 0.18%\), comparable with other Floquet codes and \(2+1\)-dimensional color codes.
Joint-Work With: Alex Townsend-Teague, Manuel Rispler, Jens Eisert, and Markus Müller
Recording:
https://youtu.be/JjcPwUOUpJkMonday November 25th: The Focked-up ZX Calculus: Picturing Continuous-Variable Quantum Computation
Speaker: Razin A. Shaikh (University of Oxford)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: While the ZX and ZW calculi have been effective as graphical reasoning tools for finite-dimensional quantum computation, the possibilities for continuous-variable quantum computation (CVQC) in infinite-dimensional Hilbert space are only beginning to be explored. In this work, we formulate a graphical language for CVQC. Each diagram is an undirected graph made of two types of spiders: the Z spider from the ZX calculus defined on the reals, and the newly introduced Fock spider defined on the natural numbers. The Z and X spiders represent functions in position and momentum space respectively, while the Fock spider represents functions in the discrete Fock basis. In addition to the Fourier transform between Z and X, and the Hermite transform between Z and Fock, we present exciting new graphical rules capturing heftier CVQC interactions.
We ensure this calculus is complete for all of Gaussian CVQC interpreted in infinite-dimensional Hilbert space, by translating the completeness in affine Lagrangian relations by Booth, Carette, and Comfort. Applying our calculus for quantum error correction, we derive graphical representations of the Gottesman-Kitaev-Preskill (GKP) code encoder, syndrome measurement, and magic state distillation of Hadamard eigenstates. Finally, we elucidate Gaussian boson sampling by providing a fully graphical proof that its circuit samples submatrix hafnians.
Joint-Work With: Lia Yeh and Stefano Gogioso
Recording:
https://youtu.be/12QCw7PJBU4Monday December 2nd: Scalable Spider Nests (...Or How to Graphically Grok Transversal Non-Clifford Gates)
Speaker: Aleks Kissinger (University of Oxford)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: This is the second in a series of "graphical grokking" papers in which we study how stabiliser codes can be understood using the ZX-calculus. In this paper we show that certain complex rules involving ZX-diagrams, called spider nest identities, can be captured succinctly using the scalable ZX-calculus, and all such identities can be proved inductively from a single new rule using the Clifford ZX-calculus. This can be combined with the ZX picture of CSS codes, developed in the first "grokking" paper, to give a simple characterisation of the set of all transversal diagonal gates at the third level of the Clifford hierarchy implementable in an arbitrary CSS code.
Joint-Work With: John van de Wetering
Recording:
https://youtu.be/l8U9pHzPHpwMonday December 9th: The Qudit ZH Calculus for Arbitrary Finite Fields: Universality and Application
Speaker: Dichuan (David) Gao (University of Oxford)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: We propose a generalization of the graphical ZH calculus to qudits of prime-power dimensions \(q = p^t\), implementing field arithmetic in arbitrary finite fields. This is an extension of a previous result [17] which implemented arithmetic of prime-sized fields; and an alternative to a result in [3] which extended the ZH to implement cyclic ring arithmetic in \(\mathbb{Z}/q\mathbb{Z}\) rather than field arithmetic in \(\mathbb{F}q\). We show this generalized ZH calculus to be universal over matrices \(\mathbb{C}^{q^n}\rightarrow \mathbb{C}^{q^m}\) with entries in the ring \(\mathbb{Z}[\omega]\) where \(\omega\) is a pth root of unity. As an illustration of the necessity of such an extension of ZH for field rather than cyclic ring arithmetic, we offer a graphical description and proof for a quantum algorithm for polynomial interpolation. This algorithm relies on the invertibility of multiplication, and therefore can only be described in a graphical language that implements field, rather than ring, multiplication.
[3] Simple ZX and ZH Calculi for Arbitrary Finite Dimensions, via Discrete Integrals.
[17] The Qudit ZH-Calculus: Generalised Toffoli+Hadamard and Universality.
Monday December 16th: A SAT Scalpel for Lattice Surgery: Representation and Synthesis of Subroutines for Surface-Code Fault-Tolerant Quantum Computing
Speaker: Daniel Bochen Tan (Google Quantum AI and University of California, Los Angeles)
Time: 9 - 10 am ET = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: Quantum error correction is necessary for largescale quantum computing. A promising quantum error correcting code is the surface code. For this code, fault-tolerant quantum computing (FTQC) can be performed via lattice surgery, i.e., splitting and merging patches of code. Given the frequent use of certain lattice-surgery subroutines (LaS), it becomes crucial to optimize their design in order to minimize the overall spacetime volume of FTQC. In this study, we define the variables to represent LaS and the constraints on these variables. Leveraging this formulation, we develop a synthesizer for LaS, LaSsynth, that encodes a LaS construction problem into a SAT instance, subsequently querying SAT solvers for a solution. Starting from a baseline design, we can gradually invoke the solver with shrinking spacetime volume to derive more compact designs. Due to our foundational formulation and the use of SAT solvers, LaSsynth can exhaustively explore the design space, yielding optimal designs in volume. For example, it achieves 8% and 18% volume reduction respectively over two states-of-the-art human designs for the 15-to-1 T-factory, a bottleneck in FTQC.
Joint-Work With: Murphy Yuezhen Niu and Craig Gidney
Spring 2024 Schedule
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: I will show an elementary proof that optimising T-count in quantum circuits is NP-hard. The same argument also applies to showing that optimising Toffoli count in classical reversible circuits, and optimising parametrised phase gates in a parametrised circuit is NP-hard. Then I will discuss in more detail the problem of optimising the number of parameters in a parametrised circuit and show that while it is hard in general, if we restrict to circuits where each parameter occurs on a unique gate, and the only allowed reductions are affine, then an existing strategy based on the ZX-calculus finds the optimal number. This talk is based on work with Matthew Amy (https://arxiv.org/abs/2310.05958) and Richie Yeung, Tuomas Laakkonen and Aleks Kissinger (https://arxiv.org/abs/2401.12877).
Recording: https://youtu.be/nhWeIdAXYyU
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: We give generators and relations for the hypergraph props of Gaussian relations and positive affine Lagrangian relations. The former extends Gaussian probabilistic processes by completely-uninformative priors, and the latter extends Gaussian quantum mechanics with infinitely-squeezed states. These presentations are given by adding a generator to the presentation of real affine relations and of real affine Lagrangian relations which freely codiscards effects, as well as certain rotations. The presentation of positive affine Lagrangian relations provides a rigorous justification for many common yet informal calculations in the quantum physics literature involving infinite-squeezing. Our presentation naturally extends Menicucci et al.’s graph-theoretic representation of Gaussian quantum states with a representation for Gaussian transformations. Using this graphical calculus, we also give a graphical proof of Braunstein and Kimble’s continuous-variable quantum teleportation protocol. We also interpret the LOv-calculus, a diagrammatic calculus for reasoning about passive linear-optical quantum circuits in our graphical calculus. Moreover, we show how our presentation allows for additional optical operations such as active squeezing.
Joint-Work With: Titouan Carette and Cole Comfort
Recording: https://youtu.be/Ar_H0ra-45w
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: In chaotic quantum systems, the entanglement of a region A can be described in terms of the surface tension of a spacetime membrane pinned to the boundary of A. Here, we interpret the tension of this entanglement membrane in terms of the rate at which information “flows” across it. For any orientation of the membrane, one can define (generically nonunitary) dynamics across the membrane; we explore this dynamics in various space-time translation-invariant (STTI) stabilizer circuits in one and two spatial dimensions. We find that the flux of information across the membrane in these STTI circuits reaches a steady state. In the cases where this dynamics is nonunitary and the steady state flux is nonzero, this occurs because the dynamics across the membrane is unitary in a subspace of extensive entropy. This generalized unitarity is present in a broad class of STTI stabilizer circuits, and is also present in some special non-stabilizer models. The existence of multiple unitary (or generalized unitary) directions forces the entanglement membrane tension to be a piecewise linear function of the orientation of the membrane; in this respect, the entanglement membrane behaves like an interface in a zero-temperature classical lattice model. We argue that entanglement membranes in random stabilizer circuits that produce volume-law entanglement are also effectively at zero temperature.
Joint-Work With: Sarang Gopalakrishnan, Michael J. Gullans, and David A. Huse
Recording: https://youtu.be/q2UvZS3OmRI
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: Clifford quantum circuits can be classically simulated very efficiently by reduction via the ZX-calculus. Classically simulating Clifford+T quantum circuits, on the other hand, is a notoriously inefficient task. Such circuits may be decomposed into sums of efficiently simulable Clifford diagrams, though the number of terms grows exponentially with the initial T-count. In a number of related tasks, such as weak simulation and computing marginal probabilities, this technique results in reductions over many similarly structured diagrams. In the first of two recent papers, we show how the work in reducing these similar diagrams can be shared via parameterisation of the diagrams and the rewriting rules of ZX-calculus, replacing complex reductions with simple GPU-parallelisable evaluations. With this approach, we are able, in many cases, to simulate Clifford+T quantum circuits upwards of 100x quicker. In the second paper, we offer a method - based on propagating weights from common local structures - that procedurally optimises a decomposition strategy to the specific circuit given, rather than relying on a “one-size-fits-all” strategy for all circuits. Applied to random structured circuits, we achieve a decomposition efficiency of 0.1≤ α ≤ 0.2, corresponding to an exponential improvement over the conventional approaches.
[1] Fast Classical Simulation of Quantum Circuits via Parametric Rewriting in the ZX-Calculus
[2] Procedurally Optimised ZX-Diagram Cutting for Efficient T-Decomposition in Classical Simulation
Joint-Work With: Aleks Kissinger
Recording: https://youtu.be/WP0ZVSOsOOM
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: Graph state verification protocols allow multiple parties to share a graph state while checking that the state is honestly prepared, even in the presence of malicious parties. Since graph states are the starting point of numerous quantum protocols, it is crucial to ensure that graph state verification protocols can safely be composed with other protocols, this property being known as composable security. Previous works conjectured that such a property could not be proven within the abstract cryptography framework: we disprove this conjecture by showing that all graph state verification protocols can be turned into a composably secure protocol with respect to the natural functionality for graph state preparation. Moreover, we show that any unchanged graph state verification protocols can also be considered as composably secure for a slightly different, yet useful, functionality. Finally, we show that these two results are optimal, in the sense that any such generic result, considering arbitrary black-box protocols, must either modify the protocol or consider a different functionality.
Along the way, we show a protocol to generalize entanglement swapping to arbitrary graph states that might be of independent interest.
Joint-Work With: Damian Markham and Raja Yehia
Recording: https://youtu.be/slZWkYTOKnI
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Germany/Netherlands
Abstract: Quantum circuit synthesis describes the process of converting arbitrary unitary operations into a gate sequence of a fixed universal gate set, usually defined by the operations native to a given hardware platform. Most current synthesis algorithms are designed to synthesize towards a set of single-qubit rotations and an additional entangling two-qubit gate, such as CX, CZ, or the Mølmer–Sørensen gate. However, with the emergence of neutral atom-based hardware and their native support for gates with more than two qubits, synthesis approaches tailored to these new gate sets become necessary. In this work, we present an approach to synthesize (multi-) controlled phase gates using ZX-calculus. By representing quantum circuits as graph-like ZX-diagrams, one can utilize the distinct graph structure of diagonal gates to identify multi-controlled phase gates inherently present in some quantum circuits even if none were explicitly defined in the original circuit. We evaluate the approach on a wide range of benchmark circuits and compare them to the standard Qiskit synthesis regarding its circuit execution time for neutral atom-based hardware with native support of multi-controlled gates. Our results show possible advantages for current state-of-the-art hardware and represent the first exact synthesis algorithm supporting arbitrary-sized multi-controlled phase gates.
Joint-Work With: Ludwig Schmid, Johannes Zeiher, Robert Wille, and Dieter Kranzlmüller
Recording: https://youtu.be/B1P6dcJrYfk
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm France/Netherlands
Abstract: Linear optical circuits can be used to manipulate the quantum states of photons as they pass through components including beam splitters and phase shifters. Those photonic states possess a particularly high level of expressiveness, as they reside within the bosonic Fock space, an infinite-dimensional Hilbert space. However, in the domain of linear optical quantum computation, these basic components may not be sufficient to efficiently perform all computations of interest. To address this limitation it is common to add auxiliary sources and detectors, which enable projections onto auxiliary photonic states and thus increase the versatility of the processes. In this paper, we introduce the \(LO_{fi}\)-calculus, a graphical language to reason on the infinite-dimensional bosonic Fock space with circuits composed of four core elements of linear optics: the phase shifter, the beam splitter, and auxiliary sources and detectors with bounded photon number. We present an equational theory that we prove to be complete: two \(LO_{fi}\)-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the \(LO_{fi}\)-calculus. We give a unique and compact universal form for such circuits.
Recording: https://youtu.be/_0l1KjI0nfA
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands = 5 - 6 pm Israel
Abstract: Measurement-based quantum computation (MBQC) is a universal platform to realize unitary gates, only using measurements which act on a pre-prepared entangled resource state. By deforming the measurement bases, as well as the geometry of the resource state, we show that MBQC circuits always transmit and act on the input state but generally realize nonunitary logical gates. In contrast to the stabilizer formalism which is often used for unitary gates, we find that ZX calculus is an ideal computation method of these nonunitary gates. As opposed to unitary gates, nonunitary gates can not be applied with certainty, due to the randomness of quantum measurements. We maximize the success probability of realizing nonunitary gates, and discuss applications including imaginary time evolution, which we demonstrate on a noisy intermediate scale quantum device.
Joint-Work With: Jonathan Ruhman and Eran Sela
Recording: https://youtu.be/-ccLsj4McpA
Tuesday June 25th: Constructing \(NP^{\#P}\)-Complete Problems and \(\#P\)-Hardness of Circuit Extraction in Phase-Free ZH
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: The ZH calculus is a graphical language for quantum computation reasoning. The phase-free variant offers a simple set of generators that guarantee universality. ZH calculus is effective in MBQC and analysis of quantum circuits constructed with the universal gate set Toffoli+H. While circuits naturally translate to ZH diagrams, finding an ancilla-free circuit equivalent to a given diagram is hard. Here, we show that circuit extraction for phase-free ZH calculus is #P-hard, extending the existing result for ZX calculus. Another problem believed to be hard is comparing whether two diagrams represent the same process. We show that two closely related problems are NP#P-complete. The first problem is: given two processes represented as diagrams, determine the existence of a computational basis state on which they equalize. The second problem is checking whether the matrix representation of a given diagram contains an entry equal to a given number. Our proof adapts the proof of Cook-Levin theorem to a reduction from a non-deterministic Turing Machine with access to #P oracle.
Recording: https://youtu.be/EuqikLkSHX8
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Germany/Netherlands
Abstract: We use Shor's algorithm for the computation of elliptic curve private keys as a case study for resource estimates in the silicon-photonics-inspired active-volume architecture. Here, a fault-tolerant surface-code quantum computer consists of modules with a logarithmic number of non-local inter-module connections, modifying the algorithmic cost function compared to 2D-local architectures. We find that the non-local connections reduce the cost per key by a factor of 300-700 depending on the operating regime. At 10% threshold, assuming a 10-μs code cycle and non-local connections, one key can be generated every 10 minutes using 6000 modules with 1152 physical qubits each. By contrast, a device with strict 2D-local connectivity requires more qubits and produces one key every 38 hours. We also find simple architecture-independent algorithmic modifications that reduce the Toffoli count per key by up to a factor of 5. These modifications involve reusing the stored state for multiple keys and spreading the cost of the modular division operation over multiple parallel instances of the algorithm.
Time: 10 - 11 am ET = 3 - 4 pm UK = 4 - 5 pm Germany/Netherlands
Abstract: Parameterized quantum circuits are attractive candidates for potential quantum advantage in the near term and beyond. At the same time, as quantum computing hardware not only continues to improve but also begins to incorporate new features such as mid-circuit measurement and adaptive control, opportunities arise for innovative algorithmic paradigms. In this work we focus on measurement-based quantum computing protocols for approximate optimization, in particular related to quantum alternating operator ans¨atze (QAOA), a popular quantum circuit model approach to combinatorial optimization. For the construction and analysis of our measurement-based protocols we demonstrate that diagrammatic approaches, specifically ZX-calculus and its extensions, are effective for adapting such algorithms to the measurement-based setting. In particular we derive measurement patterns for applying QAOA to the broad and important class of QUBO problems. We further outline how for constrained optimization, hard problem constraints may be directly incorporated into our protocol to guarantee the feasibility of the solution found and avoid the need for dealing with penalties. Finally we discuss the resource requirements and tradeoffs of our approach to that of more traditional quantum circuits.
Joint-Work With: Stuart Hadfield
Recording: https://youtu.be/dwLxBdhT0ZU
Winter 2024 Schedule
Time: 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Germany/Netherlands
Abstract: ZX-diagrams are a powerful graphical language for the description of quantum processes with applications in fundamental quantum mechanics, quantum circuit optimization, tensor network simulation, and many more. The utility of ZX-diagrams relies on a set of local transformation rules that can be applied to them without changing the underlying quantum process they describe. These rules can be exploited to optimize the structure of ZX diagrams for a range of applications. However, finding an optimal sequence of transformation rules is generally an open problem. In this work, we bring together ZX-diagrams with reinforcement learning, a machine learning technique designed to discover an optimal sequence of actions in a decision-making problem and show that a trained reinforcement learning agent can significantly outperform other optimization techniques like a greedy strategy or simulated annealing. The use of graph neural networks to encode the policy of the agent enables generalization to diagrams much bigger than seen during the training phase.
Recording: https://youtu.be/jVu-7MBImvs
Joint-Work With: Florian Marquardt
Time: 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Spain/Netherlands
Abstract: We propose a novel Reinforcement Learning (RL) method for optimizing quantum circuits using the graph-like representation of a ZX-diagram. The agent, trained using the Proximal Policy Optimization (PPO) algorithm, employs Graph Neural Networks to approximate the policy and value functions. We test our approach for two differentiated circuit size regimes of increasing relevance, and benchmark it against the best-performing ZX-calculus based algorithm of the PyZX library, a state-of-the-art tool for circuit optimization in the field. We demonstrate that the agent can generalize the strategies learned from 5-qubit circuits to 20-qubit circuits of up to 450 Clifford gates, with enhanced compressions with respect to its counterpart while remaining competitive in terms of computational performance.
Recording: https://youtu.be/PwqKvMNVzj0
Joint-Work With: Jordi Riu, Gerard Vilaplana, Artur Garcia-Saez, and Marta P. Estarellas
Time: 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: Blind quantum computation (BQC) protocols enable quantum algorithms to be executed on third-party quantum agents while keeping the data and algorithm confidential. The previous proposals for measurement-based BQC require preparing a highly entangled cluster state. In this paper, we show that such a requirement is not necessary. Our protocol only requires pre-shared Bell pairs between delegated quantum agents, and there is no requirement for any classical or quantum information exchange between agents during the execution. Our proposal requires fewer quantum resources than previous proposals by eliminating the need for a universal cluster state.
Recording: https://youtu.be/xFihqZ5cIZ0
Time: 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: In the one-way model of measurement-based quantum computation (MBQC), computation proceeds via measurements on a resource state. So-called flow conditions ensure that the overall computation is deterministic in a suitable sense, with Pauli flow being the most general of these. Computations, represented as measurement patterns, may be rewritten to optimise resource use and for other purposes. Such rewrites need to preserve the existence of flow to ensure the new pattern can still be implemented deterministically. The majority of existing work in this area has focused on rewrites that reduce the number of qubits, yet it can be beneficial to increase the number of qubits for certain kinds of optimisation, as well as for obfuscation.
In this work, we introduce several ZX-calculus rewrite rules that increase the number of qubits and preserve the existence of Pauli flow. These rules can be used to transform any measurement pattern into a pattern containing only (general or Pauli) measurements within the XY-plane. We also give the first flow-preserving rewrite rule that allows measurement angles to be changed arbitrarily, and use this to prove that the ‘neighbour unfusion’ rule of Staudacher et al. preserves the existence of Pauli flow. This implies it may be possible to reduce the runtime of their two-qubit-gate optimisation procedure by removing the need to regularly run the costly gflow-finding algorithm.
Recording: https://youtu.be/rKbtnOgzKZQ
Joint-Work With: Miriam Backens
Time: 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: We give complete presentations for the dagger-compact props of affine Lagrangian and coisotropic relations over an arbitrary field. This provides a unified family of graphical languages for both affinely constrained classical mechanical systems, as well as odd-prime-dimensional stabiliser quantum circuits. To this end, we present affine Lagrangian relations by a particular class of undirected coloured graphs. In order to reason about composite systems, we introduce a powerful scalable notation where the vertices of these graphs are themselves coloured by graphs. In the setting of stabiliser quantum mechanics, this scalable notation gives an extremely concise description of graph states, which can be composed via ``phased spider fusion.'' Likewise, in the classical mechanical setting of electrical circuits, we show that impedance matrices for reciprocal networks are presented in essentially the same way.
Recording: https://youtu.be/QJcEeZsL2S8
Joint-Work With: Titouan Carette and Cole Comfort
Time: 9 - 10 am CT = 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: Mathematical representations of graphs often resemble adjacency matrices or lists, representations that facilitate whiteboard reasoning and algorithm design. In the realm of proof assistants, inductive representations effectively define semantics for formal reasoning. This highlights a gap where algorithm design and proof assistants require a fundamentally different structure of graphs, particularly for process theories which represent programs using graphs. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category theory definitions. A key goal for VyZX is to Verify the ZX-calculus, a graphical language for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph’s semantic interpretation. We show how inductive graphs in VyZX are used to prove the correctness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. VyZX integrates easily with the proof engineer’s workflow through visualization and automation.
Recording: https://youtu.be/5cwd9u8jivo
Joint-Work With: Adrian Lehmann, Bhakti Shah, and Robert Rand
Time: 7 - 8 am PST = 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: Fault-tolerant complexes describe surface-code fault-tolerant protocols from a single geometric object. We first introduce fusion complexes that define a general family of fusion-based quantum computing (FBQC) fault tolerant quantum protocols based on surface codes. We show that any 3-dimensional cell complex where each edge has four incident faces gives a valid fusion complex. This construction enables an automated search for fault tolerance schemes, allowing us to identify 627 examples within a moderate search time. We implement this using the open-source software tool Gavrog and present threshold results for a variety of schemes, finding fusion networks with higher erasure and Pauli thresholds than those existing in the literature. We then define more general structures we call fault-tolerant complexes that provide a homological description of fault tolerance from a large family of low-level error models, which include circuit-based computation, floquet-based computation, and FBQC with multi-qubit measurements. This extends the applicability of homological descriptions of fault tolerance, and enables the generation of many new schemes which have not been previously identified. We also define families of fault-tolerant complexes for color codes and 3d single-shot subsystem codes, which enables similar constructive methods, and we present several new examples of each.
Recording: https://youtu.be/wCwkOX03hq8/a>
Joint-Work With: Hector Bombin, Chris Dawson, Terry Farrelly, Naomi Nickerson, Mihir Pant, Fernando Pastawski, and Sam Roberts
Time: 10 - 11 am EST = 3 - 4 pm UK = 4 - 5 pm Netherlands
Abstract: In this paper, we extend diagrammatic reasoning in monoidal categories with algebraic operations and equations. We achieve this by considering monoidal categories that are enriched in the category of Eilenberg-Moore algebras for a monad. Under the condition that this monad is monoidal and affine, we construct an adjunction between symmetric monoidal categories and symmetric monoidal categories enriched over algebras for the monad. This allows us to devise an extension, and its semantics, of the ZX-calculus with probabilistic choices by freely enriching over convex algebras, which are the algebras of the finite distribution monad. We show how this construction can be used for diagrammatic reasoning of noise in quantum systems.
Recording: https://youtu.be/yJCaEdw_Ots
Joint-Work With: Henning Basold and Alfons Laarman
Time: 10 - 11 am EST = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: Finite-dimensional quantum theory serves as the theoretical foundation for quantum information and computation based on 2-dimensional qubits, d-dimensional qudits, and their interactions. The qufinite ZX calculus has been used as a framework for mixed-dimensional quantum computing; however, it lacked the crucial property of completeness, which ensures that the calculus incorporates a set of rules rich enough to prove any equation. The ZXW calculus is a complete language for qudit quantum computing with applications previously unreachable solely with the ZX or ZW calculus. In this paper, we introduce the qufinite ZXW calculus, a unification of all qudit ZXW calculi in a single framework for mixed-dimensional quantum computing. We provide a set of rewrite rules and a unique normal form that make the calculus complete for finite-dimensional quantum theory. This work paves the way for the optimization of mixed dimensional circuits and tensor networks appearing in different areas of quantum computing including quantum chemistry, compilation, and quantum many-body systems.
Recording: https://youtu.be/AhEEOqpzADY
Joint-Work With: Quanlong Wang and Razin A. Shaikh
Time: 10 - 11 am EST = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: ZX calculus is a graphical language for reasoning about linear maps. Maps are represented as graphs, and reasoning amounts to graph rewrites. The main applications of ZX calculus are in quantum computation. We train small transformers to simplify ZX graphs, i.e. perform resource optimisation of quantum circuits. Preliminary experiments show that transformers can be trained to simplify CNOT and Clifford circuits with high accuracy. These are the simplest kinds of ZX graphs, in the sense that there exists an efficient rewrite strategy. We also show evidence that transformers learn to simplify the more complex Clifford + T graphs, for which in general there does not exist an efficient simplification algorithm.
Recording: https://youtu.be/gW_ZzRoIUMU
Joint-Work With: Konstantinos Meichanetzidis, Alexandre Krajenbrink, and François Charton
Time: 10 - 11 am EST = 2 - 3 pm UK = 3 - 4 pm France/Netherlands
Abstract: We introduce the first minimal and complete equational theory for quantum circuits. Hence, we show that any true equation on quantum circuits can be derived from simple rules, all of them being standard except a novel but intuitive one which states that a multi-control 2π rotation is nothing but the identity. Our work improves on the recent complete equational theories for quantum circuits, by getting rid of several rules including a fairly unpractical one. One of our main contributions is to prove the minimality of the equational theory, i.e. none of the rules can be derived from the other ones. More generally, we demonstrate that any complete equational theory on quantum circuits (when all gates are unitary) requires rules acting on an unbounded number of qubits. Finally, we also simplify the complete equational theories for quantum circuits with ancillary qubits and/or qubit discarding.
Recording: https://youtu.be/3q8eqihdtTs
Joint-Work With: Noé Delorme and Simon Perdrix
Fall 2023 Schedule
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: Floquet codes are a recently(-ish!) discovered type of quantum error correction code. Operationally, they work by repeatedly measuring multi-qubit Pauli operators, and thus can be thought of as generalising stabilizer codes. However, they have the defining property that representatives of logical Pauli operators in a Floquet code are dynamic - they change over time. In this talk, we will consider the following perspective, which unifies stabilizer and Floquet codes: every Clifford ZX-diagram is a quantum error correcting code. We will introduce tools needed to understand this view and discuss its applications.
Recording: https://www.youtube.com/watch?v=pP1DaKxlC_8
Joint-Work With: Julio Magdalena de la Fuente and Markus Kesselring
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: Recent advances in classical simulation of Clifford+T circuits make use of the ZX calculus to iteratively decompose and simplify magic states into stabiliser terms. We improve on this method by studying stabiliser decompositions of ZX diagrams involving the triangle operation. We show that this technique greatly speeds up the simulation of quantum circuits involving multi-controlled gates which can be naturally represented using triangles. We implement our approach in the QuiZX library and demonstrate a significant simulation speed-up (up to multiple orders of magnitude) for random circuits and a variation of previously used benchmarking circuits. Furthermore, we use our software to contract diagrams representing the gradient variance of parametrised quantum circuits, which yields a tool for the automatic numerical detection of the barren plateau phenomenon in ansätze used for quantum machine learning. Compared to traditional statistical approaches, our method yields exact values for gradient variances and only requires contracting a single diagram. The performance of this tool is competitive with tensor network approaches, as demonstrated with benchmarks against the quimb library.
Recording: https://youtu.be/8L6jqiNg9iM
Joint-Work With: Richie Yeung and Quanlong Wang
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Germany
Abstract: The synthesis of quantum circuits from so-called Pauli-Polynomials in the ZX Calculus facilitates quantum circuit optimization. In this work, we will develop three algorithms that can perform this task in an architecture-aware fashion. On top, we develop an architecture-aware synthesis method for synthesizing Clifford-Tableaus. Our results show an increase in the Reduction of CNOT-Gates for larger circuits for both Clifford circuits and circuits described by Pauli-Polynomials, which outlines the capabilities of architecture-aware synthesis in the circuit optimization realm.
Recording: https://youtu.be/V8dlZgSQYiU
Joint-Work With: Qunsheng Huang, Arianne Meijer-van de Griend, and Richie Yeung
Time: 9 - 10 am EDT = 1 - 2 pm UK = 2 - 3 pm Netherlands
Abstract: In this paper, we develop a graphical calculus to rewrite photonic circuits involving light-matter interactions and non-linear optical effects. We introduce the infinite ZW calculus, a graphical language for linear operators on the bosonic Fock space which captures both linear and non-linear photonic circuits. This calculus is obtained by combining the QPath calculus, a diagrammatic language for linear optics, and the recently developed qudit ZXW calculus, a complete axiomatisation of linear maps between qudits. It comes with a 'lifting' theorem allowing to prove equalities between infinite operators by rewriting in the ZXW calculus. We give a method for representing bosonic and fermionic Hamiltonians in the infinite ZW calculus. This allows us to derive their exponentials by diagrammatic reasoning. Examples include phase shifts and beam splitters, as well as non-linear Kerr media and Jaynes-Cummings light-matter interaction.
Recording: https://youtu.be/nOli0jB2hoY
Joint-Work With: Giovanni de Felice, Razin A. Shaikh, Lia Yeh, Quanlong Wang, and Bob Coecke
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Germany/Netherlands
Abstract: There are several models of quantum computation which exhibit shared fundamental fault-tolerance properties. This article makes commonalities explicit by presenting these different models in a unifying framework based on the ZX calculus. We focus on models of topological fault tolerance – specifically surface codes – including circuit-based, measurement-based and fusion-based quantum computation, as well as the recently introduced model of Floquet codes. We find that all of these models can be viewed as different flavors of the same underlying stabilizer fault-tolerance structure, and sustain this through a set of local equivalence transformations which allow mapping between flavors. We anticipate that this unifying perspective will pave the way to transferring progress among the different views of stabilizer fault-tolerance and help researchers familiar with one model easily understand others.
Joint-Work With: Hector Bombin, Daniel Litinski, Naomi Nickerson, and Sam Roberts
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: Optimising quantum circuits to reduce physical implementation resources is crucial, especially in the context of near term hardware, which is limited by quantum volume. This paper aims to minimise T-count and two-qubit gate count by building on ZX-calculus-based circuit optimisation strategies. By translating a circuit into a ZX-diagram it can be simplified before being extracted back into a circuit. We assert that simplifications preserve a graph-theoretic property called causal flow. This has the advantage that qubit lines are well defined throughout simplification, permitting a trivial extraction procedure and in turn enabling the calculation of an individual transformation's impact on the resulting circuit. A general algorithm for a decision strategy is introduced, inspired by the heuristic based method of Staudacher et. al. (2022). Also, both phase teleportation and the neighbour unfusion rule are generalised. In particular allowing unfusion of multiple neighbours is shown to lead to significant improvements in optimisation. When run on a set of benchmark circuits, the algorithm developed reduces the two qubit gate count by an average of 19.6%, beating both the previous best ZX-based strategy (14.2%) as well as the previous best non-ZX strategy (18.9%). This lays the foundation for improvements such as more advanced decision models.
Recording: https://youtu.be/9wO_-QcSAaM
Joint-Work With: Aleks Kissinger
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: ZXLive is a user-friendly, interactive tool designed for reasoning with the ZX calculus. It offers a simple interface to draw ZX diagrams or import them from various file formats. Once you have your diagram, switch to proof mode where you can easily apply the ZX rules and construct proofs. The tool supports exporting proofs to Tikzit for adding it into papers. These proofs can also be saved as lemmas, which can be used later as rewrite rules in other proofs. With support for custom rewrites, you can add new rules to ZXLive that are relevant for your current project. Beyond the vanilla ZX calculus, ZXLive supports the generators and rewrite rules of ZH, ZW, and ZXW calculi.
ZXLive is available as an open-source project on GitHub: https://github.com/Quantomatic/zxlive. Under the hood, it is powered by PyZX, which is an open-source python library for ZX. Along with being a useful tool for ZX practitioners, ZXLive is also a great educational tool for learning and experimenting with the ZX calculus.
Recording: https://youtu.be/J--c2q-KOc8
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: Quantum Error-Correcting Codes (QECCs) are vital for ensuring the reliability of quantum computing and quantum communication systems. Among QECCs, stabilizer codes, particularly graph codes, have attracted considerable attention due to their unique properties and potential applications. Concatenated codes, which combine multiple layers of quantum codes, offer a powerful technique for achieving high levels of error correction with a relatively low resource overhead. In this paper, we examine the concatenation of graph codes using the powerful and versatile graphical language of ZX-calculus. We establish a correspondence between the encoding map and ZX-diagrams, and provide a simple proof of the equivalence between encoding maps in the Pauli X basis and the graphic operation "generalized local complementation" (GLC) as previously demonstrated in [J. Math. Phys. 52, 022201]. Our analysis reveals that the resulting concatenated code remains a graph code only when the encoding qubits of the same inner code are not directly connected. When they are directly connected, additional Clifford operations are necessary to transform the concatenated code into a graphcode, thus generalizing the results in [J. Math. Phys. 52, 022201]. We further explore concatenated graph codesin different bases, including the examination of holographic codes as concatenated graph codes. Our findings showcase the potential of ZX-calculus in advancing the field of quantum error correction.
Recording: https://youtu.be/mbqx0OudY5c
Joint-Work With: Song Cheng and Bei Zeng
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: The ZX-calculus is a family of graphical languages used to reason about fragments of complex-valued matrices under the bilinear tensor product. However, by restricting oneself to the phase-free fragment of the ZX-calculus, one obtains a graphical calculus for reasoning about linear subspaces over the integers modulo p under the direct sum. In order to expose this correspondence, I will review the scalable notation and discuss how this allows one to perform basic constructions in linear algebra using the ZX-calculus. I will also discuss how one can capture more general notions of subspaces by adding more generators to the ZX-calculus. In particular, I will discuss how extending this correspondence between the phase-free ZX-calculus and linear subspaces over Z/pZ has can be applied to stabilizer codes as well as SAT solving. I will also discuss open problems which may be interesting to the ZX-calculus community.
Recording: https://youtu.be/80rx6LzWCWo
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Netherlands
Abstract: In this work, we present a generic approach to transform CSS codes by building upon their equivalence to phase-free ZX diagrams. Using the ZX calculus, we demonstrate diagrammatic transformations between encoding maps associated with different codes. As a motivating example, we give explicit transformations between the Steane code and the quantum Reed-Muller code, since by switching between these two codes, one can obtain a fault-tolerant universal gate set. To this end, we propose a bidirectional rewrite rule to find a (not necessarily transversal) physical implementation for any logical ZX diagram in any CSS code.
Then we focus on two code transformation techniques: code morphing, a procedure that transforms a code while retaining its fault-tolerant gates, and gauge fixing, where complimentary codes can be obtained from a common subsystem code (e.g., the Steane and the quantum Reed-Muller codes from the [[15,1,3,3]] code). We provide explicit graphical derivations for these techniques and show how ZX and graphical encoder maps relate several equivalent perspectives on these code-transforming operations.
Recording: https://youtu.be/ZhfQxdjodNs
Joint-Work With: Sarah Meng Li, Lia Yeh, Aleks Kissinger, Michele Mosca, and Michael Vasmer
Time: 9 - 10 am EDT = 2 - 3 pm UK = 3 - 4 pm Sweden
Abstract: Working from the internal type theory of compact closed symmetric monoidal categories, we extend the linear multiplicative typed λ-calculus with observable structures to obtain a programming language suitable for the categorical view of quantum computation. At the current stage of development, the phase groups and cocommutative comonoids of observable structures are embedded into the typing and structural rules of the language to provide basis-dependent non-linearity as well as a notion of rotational computing. We show that this language provides novel programming techniques and ways of constructing categorical quantum programs, notably in the ZX-calculus. The generality of the categorical definition of the language allows it to be instantiated in any model of compact closed symmetric monoidal categories with any number of observable structures, or internal cocommutative comonoids. We hope that this creates new avenues in which to explore what quantum programming might be, and which theories it might describe.
Recording: https://youtu.be/iUHEy3PZCso
Joint-Work With: Fabian Forslund