×

zbMATH — the first resource for mathematics

Completeness of the ZX-calculus. (English) Zbl 07215290
Summary: The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation for the so-called Clifford fragment of the language – a restriction that is not universal – by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T.
We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language – and an adapted system of back-and-forth translation – to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.
MSC:
03B70 Logic in computer science
68 Computer science
Software:
Quantomatic
PDF BibTeX XML Cite
Full Text: Link arXiv
References:
[1] Scott Aaronson and Daniel Gottesman. Improved simulation of stabilizer circuits.Phys. Rev. A, 70:052328, Nov 2004.
[2] Miriam Backens. The ZX-calculus is complete for stabilizer quantum mechanics. InNew Journal of Physics, volume 16, page 093021. IOP Publishing, Sep 2014.
[3] Miriam Backens. The ZX-calculus is complete for the single-qubit clifford+t group. In Bob Coecke, Ichiro Hasuo, and Prakash Panangaden, editors,Proceedings of the 11th workshop on Quantum Physics and Logic, Kyoto, Japan, 4-6th June 2014, volume 172 ofElectronic Proceedings in
[4] Miriam Backens and Ali Nabi Duman. A complete graphical calculus for Spekkens’ toy bit theory. Foundations of Physics, pages 1-34, 2014. · Zbl 1347.81019
[5] Miriam Backens, Simon Perdrix, and Quanlong Wang. A simplified stabilizer ZX-calculus. In Ross Duncan and Chris Heunen, editors,Proceedings 13th International Conference on Quantum Physics and Logic, Glasgow, Scotland, 6-10 June 2016, volume 236 ofElectronic Proceedings in
[6] Miriam Backens, Simon Perdrix, and Quanlong Wang. Towards a minimal stabilizer ZX-calculus. Sep 2017.
[7] Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and diagrammatics.New Journal of Physics, 13(4):043016, Apr 2011. · Zbl 1155.81316
[8] Bob Coecke and Aleks Kissinger. The compositional structure of multipartite quantum entanglement. InAutomata, Languages and Programming, pages 297-308. Springer Berlin Heidelberg, 2010. · Zbl 1288.81025
[9] Bob Coecke and Aleks Kissinger.Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. · Zbl 1405.81001
[10] Bob Coecke and Quanlong Wang. ZX-rules for 2-qubit Clifford+T quantum circuits, 2018. arXiv:1804.05356. · Zbl 06957262
[11] Niel de Beaudrap and Dominic Horsman. The ZX-calculus is a language for surface code lattice surgery.CoRR, abs/1704.08670, 2017.
[12] Ross Duncan and Kevin Dunne. Interacting Frobenius algebras are Hopf. InProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pages 535-544, · Zbl 1392.68297
[13] Ross Duncan and Liam Garvie. Verifying the smallest interesting colour code with quantomatic. In Bob Coecke and Aleks Kissinger, editors,Proceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017, volume 266 ofElectronic Proceedings in Theoretical Computer Science, pages 147-163, 2018.
[14] Ross Duncan and Maxime Lucas. Verifying the Steane code with Quantomatic. In Bob Coecke and Matty Hoban, editors,Proceedings of the 10th International Workshop on Quantum Physics
[15] Ross Duncan and Simon Perdrix. Rewriting measurement-based quantum computations with generalised flow.Lecture Notes in Computer Science, 6199:285-296, 2010. · Zbl 1288.68069
[16] Ross Duncan and Simon Perdrix. Pivoting makes the ZX-calculus complete for real stabilizers. In Bob Coecke and Matty Hoban, editors,Proceedings of the 10th International Workshop on · Zbl 1268.81046
[17] Ross Duncan. A graphical approach to measurement-based quantum computing. InQuantum Physics and Linguistics, pages 50-89. Oxford University Press, Feb 2013. · Zbl 1317.81059
[18] D. Gottesman. Quantum error correction and fault tolerance. InEncyclopedia of Mathematical Physics, pages 196-201. Elsevier, 2006.
[19] Brett Giles and Peter Selinger. Exact synthesis of multiqubit Clifford+T circuits.Phys. Rev. A, 87:032332, Mar 2013.
[20] Amar Hadzihasanovic. A diagrammatic axiomatisation for qubit entanglement. In2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 573-584, Jul 2015. · Zbl 1401.81012
[21] Amar Hadzihasanovic.The Algebra of Entanglement and the Geometry of Composition. PhD thesis, University of Oxford, 2017. · Zbl 1401.81012
[22] Amar Hadzihasanovic, Kang Feng Ng, and Quanlong Wang. Two complete axiomatisations of pure-state qubit quantum computing. InProceedings of the 33rd Annual ACM/IEEE Symposium
[23] Clare Horsman. Quantum picturalism for topological cluster-state computing.New Journal of Physics, 13(9):095011, Sep 2011.
[24] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 559-568, New York, NY, USA, 2018. ACM.
[25] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Diagrammatic reasoning beyond Clifford+T quantum mechanics. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 569-578, New York, NY, USA, 2018. ACM.
[26] Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart, and Quanlong Wang. ZX-calculus: Cyclotomic supplementarity and incompleteness for Clifford+T quantum mechanics. In Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin, editors,42nd International Symposium · Zbl 1447.81077
[27] Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In Amy P. Felty and Aart Middeldorp, editors,Automated Deduction - CADE-25, pages 326-336, Cham, 2015. Springer International Publishing. · Zbl 06515516
[28] Kang Feng Ng and Quanlong Wang. A universal completion of the ZX-calculus. arXiv:1706.09877, 2017.
[29] Simon Perdrix and Quanlong Wang. Supplementarity is necessary for quantum diagram reasoning. In41st International Symposium on Mathematical Foundations of Computer Science (MFCS · Zbl 1398.81015
[30] Robert Raussendorf, Daniel E. Browne, and Hans J. Briegel. Measurement-based quantum computation on cluster states.Physical Review A, 68(2), Aug 2003. · Zbl 1056.81020
[31] Steven Roman.Field Theory. Springer, 2006. · Zbl 1172.12001
[32] Christian Schr¨oder de Witt and Vladimir Zamdzhiev. The ZX-calculus is incomplete for quantum mechanics. In Bob Coecke, Ichiro Hasuo, and Prakash Panangaden, editors,Proceedings of the
[33] Peter Selinger. A survey of graphical languages for monoidal categories. InNew Structures for Physics, pages 289-355. Springer, 2010. · Zbl 1217.18002
[34] Yaoyun Shi. Both Toffoli and controlled-not need little help to do universal quantum computing. Quantum Information & Computation, 3(1):84-92, 2003. · Zbl 1152.81811
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.