# Poster Titles and Abstracts

## 1. A Characterization of Integral, Real, and Gaussian Clifford+T operators

Matthew Amy (University of Waterloo), Andrew M. Glaudell (University of Maryland), Neil J. Ross (Dalhousie University)

In 2012, Giles and Selinger showed that Clifford+T operators correspond to matrices of the form U=(1/\sqrt{2})^{k}M where k is a nonnegative integer and M is a matrix over the ring Z[omega]. Here, we consider the operators that arise when one restricts M to be a matrix over a subring of Z[omega]. We focus on the subrings Z, Z[\sqrt{2}], and Z[i], which define the integral, real, and Gaussian Clifford+T operators, respectively. We prove that these restricted Clifford+T operators correspond to circuits over well-known universal sets of quantum gates. Explicitly, we show that the integral Clifford+T operators are generated by the gate set {X, CX, CCX, H}, from which the real and Gaussian operators are obtained by adding the CS and CH gate, respectively.

## 2. Structured cospans and the ZX-calculus

Daniel Cicala (UC Riverside)

Structured cospans are a syntactic device used to reason about compositional systems. In this talk, we introduce a rewriting theory to structured cospans and illustrate this with the ZX-calculus. As a result, we obtain a symmetric monoidal double category and a bicategory of relations that encode the ZX-calculus.

## 3. ZX-Rules for 2-qubit Clifford+T Quantum Circuits, and beyond

Bob Coecke (University of Oxford), Quanlong Wang (University of Oxford)

We give the ZX-rules that enable one to derive all equations between 2-qubit Clifford+T circuits. Our rule set only extends stabilizer ZX-calculus with a single new rule, and hence is substantially less than those needed for the recently achieved universal completeness. In particular, these ZX-rules are much simpler than the complete of set Clifford+T circuit equations due to Selinger and Bian. The underlying reason is that ZX-calculus is not constrained by a fixed unitary gate set for performing intermediate computations.

Moreover, recently it was shown by Renaud Vilmart that our new rule suffices for universal completeness of ZX-calculus, the only difference between 2-qubit Clifford+T circuit rules and universal ZX-diagram rules being the variables to be used within the rule: in the case of universal completeness all explicit phase values are needed, while in the 2-qubit case one never needs to consider explicit phases, only relationships between these.

We also conjecture that while in that sense ZX-rules scale with increasing number of qubits, circuit rules don’t, and propose a pathway to a prove thereof.

## 4. Circuit Relations for Real Stabilizers: Towards TOF+H

Cole Comfort (University of Calgary)

The real stabilizer fragment of quantum mechanics was shown to have a complete axiomatization in terms of the angle-free fragment of the ZX-calculus. This fragment of the ZX-calculus—although abstractly elegant—is stated in terms of identities, such as spider fusion which generally do not have interpretations as circuit transformations.

We complete the category CNOT generated by the controlled not gate and the computational ancillary bits, presented by circuit relations, to the real stabilizer fragment of quantum mechanics. This is performed first, by adding the Hadamard gate and the scalar sqrt 2 as generators. We then construct translations to and from the angle-free fragment of the ZX-calculus, showing that they are inverses. We remove the generator sqrt 2 and then prove that the axioms are still complete for the remaining generators. This yields a category which is not compact closed, where the yanking identities hold up to a non-invertible, non-zero scalar.

We then discuss how this could potentially lead to a complete axiomatization, in terms of circuit relations, for the approximately universal fragment of quantum mechanics generated by the Toffoli gate, Hadamard gate and computational ancillary bits.

## 5. A ZX re-writing system for surface code lattice surgery

Richard East (University of Grenoble), Dominic Horsman (University of Grenoble)

Surface codes with lattice surgery are currently the leading proposal for the large-scale quantum error correction needed for fault tolerant quantum computing. Whereas quantum computation is usually based on the application of unitary operators (or gates) alongside measurement, lattice surgery uses logical fusion and splitting operations that are inherently non-unitary. The fusion (merge) operation in particular takes two logical qubits as input, and outputs one logical qubit. This operation clearly involves an inherent loss of (quantum) information. Such operations are not primitives in the usual circuit representation of quantum gates, making the design and verification of lattice surgery patterns a hard task in the absence of better representational tools. Previous work has shown that the operations of lattice surgery map to collections of generators of the ZX calculus, leading to the idea that ZX should become the language of choice for lattice surgery procedures. In this work we give the formal semantics and re-write system for such collections of ZX diagrams that correspond to lattice surgery procedures. This has been achieved by first considering the spectrum of an operator, defined as a set of density operators or CPTP maps. Re-writes are then defined both individually between elements in a spectrum, and as spectra of the re-writes themselves. We finish by giving the conditions under which these rewrites are complete. The move towards a complete language for lattice surgery offers a coherent mechanism to reason about about surface codes. It also forms part of a new model of quantum computing based on probabilistic operations and the ZX calculus, termed Pauli Fusion. These results will broaden the tool-set available to all those working on the algorithms and foundations of computation as performed using quantum systems.

## 6. Impossibility of Quantum Bit Commitment, a Categorical Perspective

Feifei He (Sun Yat-sen University), Xin Sun (Sun Yat-sen University), Quanlong Wang (University of Oxford), Xishun Zhao (Sun Yat-sen University)

Bit commitment is a cryptographic task in which Alice commits a bit to Bob such that she cannot change the value of the bit after her commitment and Bob cannot learn the value of the bit before Alice opens her commitment. According to the MLC no-go theorem, ideal bit commitment is impossible within quantum theory. In the information theoretic-reconstruction of quantum theory, the impossibility of quantum bit commitment is one of the three information-theoretic constrains that characterize quantum theory. In this paper, we first provide a very simple proof of the MLC no-go theorem. Then we formalize bit commitment in the theory of dagger monoidal categories. We show that in the setting of dagger monoidal categories, the impossibility of bit commitment is equivalent to the unitary equivalence of purification.

## 7. Categorical Equivalence between Orthocomplemented Quantales and Complete Orthomodular Lattices

Kohei Kishida (Dalhousie University), Soroush Rafiee Rad (University of Bayreuth), Joshua Sack (California State University Long Beach), Shengyang Zhong (Peking University)

This paper provides a categorical equivalence between two types of quantum structures.  One is a complete orthomodular lattice, which is used for reasoning about testable properties of a quantum system.  The other is an orthomodular dynamic algebra, which is a quantale used for reasoning about quantum actions. The result extends to more restrictive lattices than orthomodular lattices, and includes Hilbert lattices of closed subspaces of a Hilbert space.  These other lattice structures have connections to a wide range of different quantum structures; hence our equivalence establishes a categorical connection between quantales and a great variety of quantum structures.

## 8. Graphical Fourier Theory and the Cost of Quantum Addition

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.

## 9. Quantum simulation of partially distinguishable boson sampling

Alexandra Moylett (University of Bristol), Peter Turner (University of Bristol)

Boson Sampling is the problem of sampling from the same output probability distribution as a collection of indistinguishable single photons input into a linear interferometer. It has been shown that, subject to certain computational complexity conjectures, in general the problem is difficult to solve classically, motivating optical experiments aimed at demonstrating quantum computational “supremacy”. There are a number of challenges faced by such experiments, including the generation of indistinguishable single photons. We provide a quantum circuit that simulates bosonic sampling with arbitrarily distinguishable particles. This makes clear how distinguishabililty leads to decoherence in the standard quantum circuit model, allowing insight to be gained. At the heart of the circuit is the quantum Schur transform, which follows from a representation theoretic approach to the physics of distinguishable particles in first quantisation. The techniques are quite general and have application beyond boson sampling.

## 10. AND-gates in ZX-calculus: QBC-completeness and phase gadgets

Anthony Munson (Harvard University), Bob Coecke (University of Oxford), Quanlong Wang (University of Oxford)

In this paper 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.

## 11. Quantum computing, Seifert surfaces and singular fibers

Michel Planat (FEMTO-ST CNRS), Raymond Aschheim (Quantum Gravity Research), Marcelo Amaral (Quantum Gravity Research), Klee Irwin (Quantum Gravity Research)

The fundamental group $\pi_1(L)$ of a knot or link $L$ may be used to generate magic states appropriate for performing universal quantum computation and simultaneously for retrieving complete information about the processed quantum states. In this paper, one defines braids whose closure is the $L$ of such a quantum computer model and computes their Seifert surfaces and the corresponding Alexander polynomial.

In particular, some $d$-fold coverings of the trefoil knot, with $d=3$, $4$, $6$ or $12$, define appropriate links $L$ and the latter two cases connect to the Dynkin diagrams of $E_6$ and $D_4$, respectively. In this new context, one finds that this correspondence continues with the Kodaira’s classification of elliptic singular fibers. The Seifert fibered toroidal manifold $\Sigma’$, at the boundary of the singular fiber $\tilde {E_8}$, allows possible models of quantum computing.

## 12. Mathematical methods for resource-based type theories

Aarthi Sundaram (University of Maryland), Brad Lackey (Microsoft)

With the wide range of quantum programming languages on offer now, efficient program verification and type checking for these languages presents a challenge — especially when classical debugging techniques may affect the states in a quantum program. In this work, we make progress towards a program verification approach using the formalism of operational quantum mechanics and resource theories. We present a logical framework that captures two mathematical approaches to resource theory based on monoids (algebraic) and monoidal categories (categorical). We develop the syntax of this framework as an intuitionistic sequent calculus, and prove soundness and completeness of an algebraic and categorical semantics that recover these approaches. We also provide a cut-elimination theorem, normal form, and analogue of Lambek’s lifting theorem for polynomial systems over the logics. Using these approaches along with the Curry-Howard-Lambek correspondence for programs, proofs and categories, this work lays the mathematical groundwork for a type checker for some resource theory based frameworks, with the possibility of extending it other quantum programming languages.

## 13. Completeness of the Phase-free ZH-calculus

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.