Simple Complete Equational Theories for Quantum Circuits with Ancillae or Partial Trace

Alexandre Clément (1, 2) , Noé Delorme (1, 2) , Simon Perdrix (1, 2) , Renaud Vilmart (3, 4)

1 MOCQUA - Designing the Future of Computational Models
2 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 QuaCS - Quantum Computation Structures
4 LMF - Laboratoire Méthodes Formelles

Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory. Our contribution is twofold: (i) We simplify this equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) We extend the complete equational theory to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings. The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

Mots clés: Completeness; Graphical Language; Quantum Circuits

Domaines: Logique en informatique [cs.LO]; Physique Quantique [quant-ph]

Alexandre Clément, Noé Delorme, Simon Perdrix, Renaud Vilmart. Simple Complete Equational Theories for Quantum Circuits with Ancillae or Partial Trace. 2023. ⟨hal-04016498v1⟩