arXiv subjects

Hector Miller-Bakewell

Publications and source records attributed to Hector Miller-Bakewell.

5 recordsLinked to original sources

arXiv2023

Completeness of the ZH-calculus

There are various gate sets used for describing quantum computation. A particularly popular one consists of Clifford gates and arbitrary single-qubit phase gates. Computations in this gate set can be elegantly described by the ZX-calculus, a graphical language for a class of string diagrams describing linear maps between qubits. The ZX-calculus has proven useful in a variety of areas of quantum information, but is less suitable for reasoning about operations outside its natural gate set such as multi-linear Boolean operations like the Toffoli gate. In this paper we study the ZH-calculus, an alternative graphical language of string diagrams that does allow straightforward encoding of Toffoli gates and other more complicated Boolean logic circuits. We find a set of simple rewrite rules for this calculus and show it is complete with respect to matrices over $\mathbb{Z}[\frac12]$, which correspond to the approximately universal Toffoli+Hadamard gateset. Furthermore, we construct an extended version of the ZH-calculus that is complete with respect to matrices over any ring $R$ where $1+1$ is not a zero-divisor.

quant-ph↗

arXiv2021

There and back again: A circuit extraction tale

Translations between the quantum circuit model and the measurement-based one-way model are useful for verification and optimisation of quantum computations. They make crucial use of a property known as gflow. While gflow is defined for one-way computations allowing measurements in three different planes of the Bloch sphere, most research so far has focused on computations containing only measurements in the XY-plane. Here, we give the first circuit-extraction algorithm to work for one-way computations containing measurements in all three planes and having gflow. The algorithm is efficient and the resulting circuits do not contain ancillae. One-way computations are represented using the ZX-calculus, hence the algorithm also represents the most general known procedure for extracting circuits from ZX-diagrams. In developing this algorithm, we generalise several concepts and results previously known for computations containing only XY-plane measurements. We bring together several known rewrite rules for measurement patterns and formalise them in a unified notation using the ZX-calculus. These rules are used to simplify measurement patterns by reducing the number of qubits while preserving both the semantics and the existence of gflow. The results can be applied to circuit optimisation by translating circuits to patterns and back again.

quant-ph↗

arXiv2020

Graphical Calculi and their Conjecture Synthesis

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 such inference and verification frameworks, in doing so forging novel links between graphical calculi and fields such as Algebraic Geometry and Galois Theory. These frameworks inspired further research into the design of graphical calculi, and we introduce two important new calculi here. First is the calculus RING, which is initial among ring-based qubit graphical calculi, and in turn inspired the introduction and classification of phase homomorphism pairs also presented here. The second is the calculus ZQ, an edge-decorated calculus which naturally expresses arbitrary qubit rotations, eliminating the need for non-linear rules such as (EU) of ZX. It is expected that these results will be of use to those creating optimisation schemes and intermediate representations for quantum computing, to those creating new graphical calculi, and for those performing conjecture synthesis.

quant-ph↗

arXiv2020

Finite Verification of Infinite Families of Diagram Equations

The ZX, ZW and ZH calculi are all graphical calculi for reasoning about pure state qubit quantum mechanics. All of these languages use certain diagrammatic decorations, called !-boxes and phase variables, to indicate not just one diagram but an infinite family of diagrams. These decorations are powerful enough to allow complete rulesets for these calculi to be expressed in around fifteen rules. Historically rules involving !-boxes have not been verifiable by computer. We present the first algorithm for reducing infinite families of equations involving !-boxes into finite verifying subsets. The only requirement for this method is a mild property on the connectivity of the !-boxes. Previous results had focussed on finite case analysis of phase variables in ZX, a result we also extend for ZW and ZH, as well as providing a general framework for further languages. The results presented here allow proof assistants to reduce infinite families of problems (involving combinations of phase variables and !-boxes) down to undecorated, case-by-case verification, in a way not previously possible. In particular we note the removal of the need to reason directly with !-boxes in verification tasks as something entirely new. This forms part of larger work in automated verification of quantum circuitry, conjecture synthesis, and diagrammatic languages in general. The methods described here extend to any diagrammatic languages that meet certain simple conditions.

quant-ph↗

arXiv2020

Entanglement and Quaternions: The graphical calculus ZQ

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

quant-ph↗