Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation

Author Renaud Vilmart



PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.36.pdf
  • Filesize: 0.8 MB
  • 17 pages

Document Identifiers

Author Details

Renaud Vilmart
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, LMF, 91190, Gif-sur-Yvette, France

Cite As Get BibTex

Renaud Vilmart. Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.36

Abstract

The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear maps that describe quantum systems, and is a tool that is used in formal verification of such systems.
We give here a new set of rewrite rules for the formalism, and show that it is complete for "Toffoli-Hadamard", the simplest approximately universal fragment of quantum mechanics. We show that the rewriting is terminating, but not confluent (which is expected from the universality of the fragment). We do so using the connection between Sum-over-Paths and graphical language ZH-Calculus, and also show how the axiomatisation translates into the latter.
Finally, we show how to enrich the rewrite system to reach completeness for the dyadic fragments of quantum computation - obtained by adding phase gates with dyadic multiples of π to the Toffoli-Hadamard gate-set - used in particular in the Quantum Fourier Transform.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantum computation theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • Quantum Computation
  • Verification
  • Sum-Over-Paths
  • Rewrite Strategy
  • Toffoli-Hadamard
  • Completeness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Scott Aaronson and Daniel Gottesman. Improved simulation of stabilizer circuits. Phys. Rev. A, 70:052328, November 2004. URL: https://doi.org/10.1103/PhysRevA.70.052328.
  2. Dorit Aharonov. A simple proof that Toffoli and Hadamard are quantum universal. eprint arXiv, January 2003. URL: http://arxiv.org/abs/quant-ph/0301040.
  3. Matthew Amy. Towards large-scale functional verification of universal quantum circuits. In Peter Selinger and Giulio Chiribella, editors, rm Proceedings of the 15th International Conference on Quantum Physics and Logic, rm Halifax, Canada, 3-7th June 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 1-21, 2019. URL: https://doi.org/10.4204/EPTCS.287.1.
  4. Miriam Backens and Aleks Kissinger. ZH: A complete graphical calculus for quantum computations involving classical non-linearity. In Peter Selinger and Giulio Chiribella, editors, rm Proceedings of the 15th International Conference on Quantum Physics and Logic, rm Halifax, Canada, 3-7th June 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 23-42, 2019. URL: https://doi.org/10.4204/EPTCS.287.2.
  5. Miriam Backens, Aleks Kissinger, Hector Miller-Bakewell, John van de Wetering, and Sal Wolffs. Completeness of the ZH-calculus, 2021. Google Scholar
  6. Adam D. Bookatz. QMA-complete problems. Quantum Information and Computation, 14(5&6):361-383, May 2014. URL: https://doi.org/10.26421/qic14.5-6-1.
  7. Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. An automated deductive verification framework for circuit-building quantum programs. In Nobuko Yoshida, editor, Programming Languages and Systems, pages 148-177, Cham, 2021. Springer International Publishing. Google Scholar
  8. Christophe Chareton, Sébastien Bardin, Dongho Lee, Benoît Valiron, Renaud Vilmart, and Zhaowei Xu. Formal methods for quantum programs: A survey, 2021. URL: https://doi.org/10.48550/arXiv.2109.06493.
  9. Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and diagrammatics. New Journal of Physics, 13(4):043016, April 2011. URL: https://doi.org/10.1088/1367-2630/13/4/043016.
  10. Bob Coecke and Aleks Kissinger. The compositional structure of multipartite quantum entanglement. In Automata, Languages and Programming, pages 297-308. Springer Berlin Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_25.
  11. Niel de Beaudrap, Xiaoning Bian, and Quanlong Wang. Fast and Effective Techniques for T-Count Reduction via Spider Nest Identities. In Steven T. Flammia, editor, 15th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2020), volume 158 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:23, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TQC.2020.11.
  12. Amar Hadzihasanovic. A diagrammatic axiomatisation for qubit entanglement. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 573-584, July 2015. URL: https://doi.org/10.1109/LICS.2015.59.
  13. Mohammad Haidar, Marko J. Rančić, Thomas Ayral, Yvon Maday, and Jean-Philip Piquemal. Open source variational quantum eigensolver extension of the quantum learning machine (qlm) for quantum chemistry, 2022. URL: https://doi.org/10.48550/arXiv.2206.08798.
  14. Dominik Janzing, Pawel Wocjan, and Thomas Beth. Non-identity check is qma-complete. International Journal of Quantum Information, 03(03):463-473, September 2005. URL: https://doi.org/10.1142/s0219749905001067.
  15. Aleks Kissinger and John van de Wetering. Reducing the number of non-Clifford gates in quantum circuits. Phys. Rev. A, 102:022406, August 2020. URL: https://doi.org/10.1103/PhysRevA.102.022406.
  16. Stephen Lack. Composing PROPs. In Theory and Applications of Categories, volume 13, pages 147-163, 2004. URL: http://www.tac.mta.ca/tac/volumes/13/9/13-09abs.html.
  17. Louis Lemonnier. Relating high-level frameworks for quantum circuits. Master’s thesis, Radbound University, 2019. URL: https://www.cs.ox.ac.uk/people/aleks.kissinger/papers/lemonnier-high-level.pdf.
  18. Louis Lemonnier, John van de Wetering, and Aleks Kissinger. Hypergraph simplification: Linking the path-sum approach to the ZH-calculus. In Benoît Valiron, Shane Mansfield, Pablo Arrighi, and Prakash Panangaden, editors, Proceedings 17th International Conference on Quantum Physics and Logic, Paris, France, June 2 - 6, 2020, volume 340 of Electronic Proceedings in Theoretical Computer Science, pages 188-212. Open Publishing Association, 2021. URL: https://doi.org/10.4204/EPTCS.340.10.
  19. Saunders Mac Lane. Categories for the Working Mathematician, volume 5. Springer Science & Business Media, 2013. Google Scholar
  20. Yosuke Sato, Shutaro Inoue, Akira Suzuki, Katsusuke Nabeshima, and Ko Sakai. Boolean gröbner bases. J. Symb. Comput., 46(5):622-632, May 2011. URL: https://doi.org/10.1016/j.jsc.2010.10.011.
  21. Peter Selinger. A survey of graphical languages for monoidal categories. In New Structures for Physics, pages 289-355. Springer, 2010. Google Scholar
  22. Yaoyun Shi. Both Toffoli and controlled-not need little help to do universal quantum computing. Quantum Information & Computation, 3(1):84-92, 2003. URL: http://portal.acm.org/citation.cfm?id=2011515.
  23. John van de Wetering and Sal Wolffs. Completeness of the Phase-free ZH-calculus, April 2019. URL: http://arxiv.org/abs/1904.07545.
  24. Renaud Vilmart. A ZX-calculus with triangles for Toffoli-Hadamard, Clifford+T, and beyond. In Peter Selinger and Giulio Chiribella, editors, rm Proceedings of the 15th International Conference on Quantum Physics and Logic, rm Halifax, Canada, 3-7th June 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 313-344, 2019. URL: https://doi.org/10.4204/EPTCS.287.18.
  25. Renaud Vilmart. The structure of sum-over-paths, its consequences, and completeness for clifford. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, pages 531-550, Cham, 2021. Springer International Publishing. Google Scholar
  26. Fabio Zanasi. Interacting Hopf Algebras - the theory of linear systems. PhD thesis, Université de Lyon, 2015. URL: http://www.zanasi.com/fabio/files/thesis2015.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail