Document Open Access Logo

Typed Compositional Quantum Computation with Lenses

Authors Jacques Garrigue , Takafumi Saikawa

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.15.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Jacques Garrigue
  • Nagoya University, Japan
Takafumi Saikawa
  • Nagoya University, Japan

Funding

This research was partially supported by JSPS KAKENHI grant No. JP22H00520 and MEXT Q-LEAP grant No. JPMXS0120319794.

Cite AsGet BibTex

Jacques Garrigue and Takafumi Saikawa. Typed Compositional Quantum Computation with Lenses. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.15

Abstract

We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows one to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Quantum computation theory
Keywords
  • quantum programming
  • semantics
  • lens
  • currying
  • Coq
  • MathComp

Metrics

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

Supplementary Materials

References

  1. F. Bancilhon and N. Spyratos. Update semantics of relational views. ACM Trans. Database Syst., 6(4):557-575, December 1981. URL: https://doi.org/10.1145/319628.319634.
  2. Davi M.J. Barbosa, Julien Cretin, Nate Foster, Michael Greenberg, and Benjamin C. Pierce. Matching lenses: alignment and view update. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pages 193-204, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1863543.1863572.
  3. 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, ESOP 2021, volume 12648 of Lecture Notes in Computer Science, pages 148-177, Cham, March 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-72019-3_6.
  4. Bob Coecke and Ross Duncan. Interacting quantum observables. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, pages 298-310, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-70583-3_25.
  5. Bob Coecke and Aleks Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. URL: https://doi.org/10.1017/9781316219317.
  6. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 34:1-34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.34.
  7. J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst., 29(3):17, 2007. URL: https://doi.org/10.1145/1232420.1232424.
  8. Jacques Garrigue and Hassan Aït-Kaci. The typed polymorphic label-selective λ-calculus. In Proc. ACM Symposium on Principles of Programming Languages, pages 35-47, 1994. URL: https://doi.org/10.1145/174675.174434.
  9. Jacques Garrigue and Takafumi Saikawa. QECC: Quantum Computation and Error-Correcting Codes. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:d4d158675180ee276e730bd7f67a9122a6472eb3;origin=https://github.com/t6s/qecc;visit=swh:1:snp:98c582f9ca38ec1ef707cc25a4ef8f23befe0386;anchor=swh:1:rev:afc45f0ce1b3258fbf0c9469085ff8749de14a2a (visited on 2024-08-21). URL: https://github.com/t6s/qecc.
  10. Daniel M. Greenberger, Michael A. Horne, and Anton Zeilinger. Going beyond bell’s theorem. In Menas Kafatos, editor, Bell’s Theorem, Quantum Theory and Conceptions of the Universe, pages 69-72. Springer Netherlands, Dordrecht, 1989. URL: https://doi.org/10.1007/978-94-017-0849-4_10.
  11. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434318.
  12. Adrian Lehmann, Ben Caldwell, and Robert Rand. VyZX : A vision for verifying the ZX calculus, 2022. URL: https://doi.org/10.48550/arXiv.2205.05781.
  13. Adrian Lehmann, Ben Caldwell, Bhakti Shah, and Robert Rand. VyZX: Formal verification of a graphical quantum language, 2023. URL: https://doi.org/10.48550/arXiv.2311.11571.
  14. Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. Formal verification of quantum programs: Theory, tools and challenges, 2022. URL: https://doi.org/10.1145/3624483.
  15. Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: A core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 846-858, 2017. URL: https://doi.org/10.1145/3009837.3009894.
  16. Qiskit contributors. Qiskit: An open-source framework for quantum computing, 2023. URL: https://doi.org/10.5281/zenodo.2573505.
  17. Peter W. Shor. Scheme for reducing decoherence in quantum computer memory. Phys. Rev. A, 52:R2493-R2496, October 1995. URL: https://doi.org/10.1103/PhysRevA.52.R2493.
  18. Dominique Unruh. Quantum and classical registers. CoRR, abs/2105.10914, 2021. URL: https://doi.org/10.48550/arXiv.2105.10914.
  19. Mingsheng Ying. Foundations of Quantum Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1st edition, 2016. URL: https://doi.org/10.1016/C2014-0-02660-3.
  20. Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. CoqQ: Foundational verification of quantum programs. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571222.
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