February 19, 2018
Renaud Vilmart (LORIA)When it comes to reasoning on quantum evolutions, it is convenient to turn to quantum circuits, for they provide a graphical and compact visualisation of said evolutions. However two different circuits might represent the same evolution — or matrix: for instance two consecutive Hadamard gates or CNOT gates result in the identity, respectively on one and two qubits. One might then want to equip circuits with a set of transformation rules, that change the circuit, but not the corresponding matrix. The ZX-Calculus is another diagrammatic language well-fitted for quantum computation. Even though it is closely related to circuits, it is laxer, which simplifies the research for transformation rules. Indeed, here, some non-unitary operations are allowed, and the wires can be bent at will, which greatly changes our conception of the mathematical objects we handle, and that we call here diagrams. The ZX-Calculus can be used for reasoning on quantum circuits: these can easily be transformed into ZX-diagrams, and there exists a method that characterises “circuit-like” diagrams. ZX-Calculus can hence be used to simplify a circuit, or check if two circuits are equivalent. The applications of the language are not limited to circuitry. For instance the generators of the ZX-Calculus match exactly the operations of lattice surgery, a promising model designed for error correction. A restriction of the language — that we call fragment — is complete when two semantically equivalent diagrams of this fragment can be turned into one another using only the rules of the ZX-Calculus. Completeness guarantees that the language captures all the computational power of quantum computation. Some fragment were proven to be complete, but none of them was universal, and they can be efficiently simulated with a classical computer. We proposed the first complete axiomatisation of the ZX-Calculus for an approximately universal fragment, namely Clifford+T.