Document Open Access Logo

Concrete Categorical Model of a Quantum Circuit Description Language with Measurement

Authors Dongho Lee, Valentin Perrelle, Benoît Valiron, Zhaowei Xu

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.51.pdf
  • Filesize: 2.1 MB
  • 20 pages

Document Identifiers

Author Details

Dongho Lee
  • Université Paris-Saclay, CentraleSupélec, LMF, France & CEA, List, France
Valentin Perrelle
  • Université Paris-Saclay, CEA, List, France
Benoît Valiron
  • Université Paris-Saclay, CentraleSupélec, LMF, France
Zhaowei Xu
  • Université Paris-Saclay, LMF, France

Funding

This work was supported in part by the French National Research Agency (ANR) under the research projects SoftQPRO ANR-17-CE25-0009-02 and PPS ANR-19-CE48-0014, by the DGE of the French Ministry of Industry under the research project PIA-GDN/QuantEx P163746-484124, and by STICAMSUD 21-SITC-20 Qapla'.

Acknowledgements

The authors want to thank Christophe Chareton and Sébastien Bardin for enlightening discussions.

Cite AsGet BibTex

Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 51:1-51:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.51

Abstract

In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data - qubits - into classical data - booleans -. We propose a type system and an operational semantics for the language and we state safety properties. Next, we introduce a concrete categorical semantics for the proposed language, basing our approach on a recent model from Rios&Selinger for Proto-Quipper-M. Our approach is to construct on top of a concrete category of circuits with measurements a Kleisli category, capturing as a side effect the action of retrieving classical content out of a quantum memory. We then show a soundness result for this semantics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • Categorical semantics
  • Operational semantics
  • Quantum circuit description language

Metrics

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

References

  1. Linda Anticoli, Carla Piazza, Leonardo Taglialegne, and Paolo Zuliani. Towards quantum programs verification: from Quipper circuits to qpmc. In International Conference on Reversible Computation, pages 213-219. Springer, 2016. Google Scholar
  2. P Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic, pages 121-135. Springer, 1994. Google Scholar
  3. Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin T. Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 286-300. ACM, 2020. URL: https://doi.org/10.1145/3385412.3386007.
  4. Qingxiuxiong Dong, Marco Túlio Quintino, Akihito Soeda, and Mio Murao. Success-or-draw: A strategy allowing repeat-until-success in quantum computation. Phys. Rev. Lett., 126:150504, April 2021. URL: https://doi.org/10.1103/PhysRevLett.126.150504.
  5. Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 440-453, 2020. Google Scholar
  6. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. Google Scholar
  7. Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A scalable quantum programming language. In Hans-Juergen Boehm and Cormac Flanagan, editors, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'13, pages 333-342. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462177.
  8. Emmanuel Knill. Conventions for quantum pseudocode. Technical report, Los Alamos National Lab., NM (United States), 1996. Google Scholar
  9. Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. Enriching a linear/non-linear lambda calculus: A programming language for string diagrams. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 659-668. ACM, 2018. Google Scholar
  10. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. Google Scholar
  11. Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: a core language for quantum circuits. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL'17, pages 846-858. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009894.
  12. Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE practice: Formal verification of quantum circuits in coq. In Bob Coecke and Aleks Kissinger, editors, Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, volume 266 of Electronic Proceedings in Theoretical Computer Science, pages 119-132, 2017. URL: https://doi.org/10.4204/EPTCS.266.8.
  13. Mathys Rennela and Sam Staton. Classical control, quantum circuits and linear logic in enriched category theory. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:30)2020.
  14. Francisco Rios and Peter Selinger. A categorical model for a quantum circuit description language. In Bob Coecke and Aleks Kissinger, editors, Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, volume 266 of Electronic Proceedings in Theoretical Computer Science, pages 164-178, 2018. URL: https://doi.org/10.4204/EPTCS.266.11.
  15. Neil J. Ross. Algebraic and logical methods in quantum computation. PhD thesis, Dalhousie University, 2015. Google Scholar
  16. Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010. Google Scholar
  17. Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16(3):527-552, 2006. Google Scholar
  18. Robert S. Smith, Michael J. Curtis, and William J. Zeng. A practical quantum instruction set architecture. arXiv preprint, 2016. URL: http://arxiv.org/abs/1608.03355.
  19. Sam Staton. Algebraic effects, linearity, and quantum programming languages. SIGPLAN Not., 50(1):395-406, January 2015. URL: https://doi.org/10.1145/2775051.2676999.
  20. Krysta M. Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. Q#: Enabling scalable quantum computing and development with a high-level domain-specific language. arXiv preprint, 2018. URL: http://arxiv.org/abs/1803.00652.
  21. Benoît Valiron. Semantics for a higher order functional programming language for quantum computation. PhD thesis, University of Ottawa, 2008. Google Scholar
  22. Dave Wecker and Krysta M. Svore. LIQUi∣⟩: A software design architecture and domain-specific language for quantum computing. arXiv preprint, 2014. URL: http://arxiv.org/abs/1402.4467.
  23. William K. Wootters and Wojciech H. Zurek. A single quantum cannot be cloned. Nature, 299:802-803, October 1982. URL: https://doi.org/10.1038/299802a0.
  24. Bernhard Ömer. Structured quantum programming. PhD thesis, Technical University of Vienna, 2003. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact