Document Open Access Logo

Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions

Authors Gilles Barthe , Minbo Gao , Jam Kabeer Ali Khan , Matthijs Muis , Ivan Renison , Keiya Sakabe , Michael Walter , Yingte Xu , Tianshi Yu , Li Zhou

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.15.pdf
  • Filesize: 1.17 MB
  • 28 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Programming logic
  • Computer systems organization → Quantum computing
Keywords
  • relational program logics
  • infinite-dimensional quantum programs
  • classical-quantum programs
  • linear relations
  • quantum optimal transport

Metrics

Abstract

We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.

Cite As Get BibTex

Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Tianshi Yu, and Li Zhou. Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.15

Author Details

Gilles Barthe
  • Max-Planck Institute for Security and Privacy (MPI-SP), Bochum, Germany
  • IMDEA Software Institute, Madrid, Spain
Minbo Gao
  • Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China
  • Institute of Software, Chinese Academy of Sciences, Beijing, China
  • University of Chinese Academy of Sciences, Beijing, China
Jam Kabeer Ali Khan
  • Max-Planck Institute for Security and Privacy (MPI-SP), Bochum, Germany
Matthijs Muis
  • Max-Planck Institute for Security and Privacy (MPI-SP), Bochum, Germany
  • Eidgenössische Technische Hochschule (ETH) Zürich, Switzerland
Ivan Renison
  • Max-Planck Institute for Security and Privacy (MPI-SP), Bochum, Germany
Keiya Sakabe
  • Ludwig-Maximilians-Universität München, Germany
Michael Walter
  • Ludwig-Maximilians-Universität München, Germany
  • Munich Center for Quantum Science and Technology (MCQST), Germany
Yingte Xu
  • Max-Planck Institute for Security and Privacy (MPI-SP), Bochum, Germany
Tianshi Yu
  • Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China
  • Institute of Software, Chinese Academy of Sciences, Beijing, China
Li Zhou
  • Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China
  • Institute of Software, Chinese Academy of Sciences, Beijing, China

Funding

MG, TY, and LZ were supported by National Key Research and Development Program of China (Grant No. 2023YFA1009403). MW and KS acknowledge support by the European Research Council (ERC Grant 101040907), the German Research Foundation (556164098, EXC-2111 – 390814868, EXC-2092 - 390781972), and the German Federal Ministry of Research, Technology and Space (QuSol, 13N17173).

References

  1. Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434333.
  2. Charalambos D. Aliprantis and Kim C. Border. Infinite Dimensional Analysis. Springer-Verlag, Berlin/Heidelberg, 2006. URL: https://doi.org/10.1007/3-540-29587-9.
  3. Andris Ambainis, Eric Bach, Ashwin Nayak, Ashvin Vishwanath, and John Watrous. One-dimensional quantum walks. In Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing, pages 37-49, Hersonissos Greece, July 2001. ACM. URL: https://doi.org/10.1145/380752.380757.
  4. Richard Arens. Operational calculus of linear relations. Pacific J. Math., 11(4):9-23, 1961. Google Scholar
  5. Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire. A quantitative probabilistic relational Hoare logic. Proc. ACM Program. Lang., 9(POPL):1167-1195, 2025. URL: https://doi.org/10.1145/3704876.
  6. Ainesh Bakshi, Allen Liu, Ankur Moitra, and Ewin Tang. A Dobrushin condition for quantum Markov chains: Rapid mixing and conditional mutual information at high temperature, October 2025. Accepted by 58th Annual ACM Symposium on Theory of Computing (STOC 2026). URL: https://doi.org/10.48550/arXiv.2510.08542.
  7. Jialu Bao, Emanuele D'Osualdo, and Azadeh Farzan. Bluebell: An alliance of relational lifting and independence for probabilistic reasoning. Proc. ACM Program. Lang., 9(POPL):1719-1749, 2025. URL: https://doi.org/10.1145/3704894.
  8. Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, and Li Zhou. Easypqc: Verifying post-quantum cryptography. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS '21, pages 2564-2586, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3460120.3484567.
  9. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang., 2(POPL):57:1-57:29, 2018. URL: https://doi.org/10.1145/3158145.
  10. Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, and Li Zhou. Complete relational logic for infinite-dimensional quantum programs with unbounded assertions, 2025. The full version of this paper also includes references [Aliprantis and Border, 2006; Morgan et al., 1996; Reed and Simon, 1980; Rudin, 1987]. URL: https://doi.org/10.48550/arXiv.2510.07051.
  11. Gilles Barthe, Minbo Gao, Theo Wang, and Li Zhou. Complete Quantum Relational Hoare Logics from Optimal Transport Duality. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 884-925, Piscataway, NJ, USA, 2025. IEEE. URL: https://doi.org/10.1109/LICS65433.2025.00072.
  12. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. In Zhong Shao and Benjamin C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 90-101. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480894.
  13. Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. Relational proofs for quantum programs. Proc. ACM Program. Lang., 4(POPL), 2019. URL: https://doi.org/10.1145/3371089.
  14. Emily Beatty. Wasserstein distances on quantum structures: An overview. Reviews in Mathematical Physics, page 2630003, May 2026. URL: https://doi.org/10.1142/S0129055X26300037.
  15. Jussi Behrndt, Seppo Hassi, and Henk De Snoo. Boundary value problems, Weyl functions, and differential operators. Springer Nature, 2020. Google Scholar
  16. Jussi Behrndt, Seppo Hassi, Henk de Snoo, and Rudi Wietsma. Monotone convergence theorems for semi-bounded operators and forms with applications. Proceedings of the Royal Society of Edinburgh: Section A Mathematics, 140(5):927-951, 2010. URL: https://doi.org/10.1017/S030821050900078X.
  17. Dan Boneh, Özgür Dagdelen, Marc Fischlin, Anja Lehmann, Christian Schaffner, and Mark Zhandry. Random oracles in a quantum world. In Advances in Cryptology-ASIACRYPT 2011: 17th International Conference on the Theory and Application of Cryptology and Information Security, Seoul, South Korea, December 4-8, 2011. Proceedings 17, pages 41-69. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25385-0_3.
  18. Olivier Bousquet and André Elisseeff. Stability and generalization. Journal of Machine Learning Research, 2:499-526, 2002. URL: https://jmlr.org/papers/v2/bousquet02a.html.
  19. Gergely Bunth, József Pitrik, Tamás Titkos, and Dániel Virosztek. Wasserstein distances and divergences of order p by quantum channels, January 2025. URL: https://arxiv.org/abs/2501.08066.
  20. E. Caglioti, F. Golse, and T. Paul. Quantum Optimal Transport is Cheaper. Journal of Statistical Physics, 181(1):149-162, October 2020. URL: https://doi.org/10.1007/s10955-020-02571-7.
  21. Emanuele Caglioti, François Golse, and Thierry Paul. Towards optimal transport for quantum densities. Annali della Scuola Normale Superiore di Pisa, Classe di Scienze, 2022. Google Scholar
  22. Eric A. Carlen and Jan Maas. Gradient flow and entropy inequalities for quantum Markov semigroups with detailed balance. Journal of Functional Analysis, 273(5):1810-1869, September 2017. URL: https://doi.org/10.1016/j.jfa.2017.05.003.
  23. Eric A. Carlen and Jan Maas. Non-commutative Calculus, Optimal Transport and Functional Inequalities in Dissipative Quantum Systems. Journal of Statistical Physics, 178(2):319-378, January 2020. URL: https://doi.org/10.1007/s10955-019-02434-w.
  24. Matthias C. Caro, Hsin-Yuan Huang, M. Cerezo, Kunal Sharma, Andrew Sornborger, Lukasz Cincio, and Patrick J. Coles. Generalization in quantum machine learning from few training data. Nature Communications, 13(1):4919, August 2022. URL: https://doi.org/10.1038/s41467-022-32550-3.
  25. Shouvanik Chakrabarti, Huang Yiming, Tongyang Li, Soheil Feizi, and Xiaodi Wu. Quantum Wasserstein Generative Adversarial Networks. In H. Wallach, H. Larochelle, A. Beygelzimer, F. dAlché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019. Google Scholar
  26. Sam Cole, Michał Eckstein, Shmuel Friedland, and Karol Życzkowski. On Quantum Optimal Transport. Mathematical Physics, Analysis and Geometry, 26(2):14, June 2023. URL: https://doi.org/10.1007/s11040-023-09456-7.
  27. Ronald Cross. Multivalued linear operators, volume 213. CRC Press, 1998. Google Scholar
  28. Marco Cuturi and Gabriel Peyré. Computational optimal transport. Found. Trends Mach. Learn, 11(5-6):355-607, 2019. URL: https://doi.org/10.1561/2200000073.
  29. Giacomo De Palma, Tristan Klein, and Davide Pastorello. Classical shadows meet quantum optimal mass transport. Journal of Mathematical Physics, 65(9):092201, September 2024. URL: https://doi.org/10.1063/5.0178897.
  30. Giacomo De Palma, Milad Marvian, Dario Trevisan, and Seth Lloyd. The Quantum Wasserstein Distance of Order 1. IEEE Transactions on Information Theory, 67(10):6627-6643, October 2021. URL: https://doi.org/10.1109/TIT.2021.3076442.
  31. Giacomo De Palma and Davide Pastorello. Quantum Concentration Inequalities and Equivalence of the Thermodynamical Ensembles: An Optimal Mass Transport Approach. Journal of Statistical Physics, 192(6):87, June 2025. URL: https://doi.org/10.1007/s10955-025-03464-3.
  32. Giacomo De Palma and Dario Trevisan. Quantum Optimal Transport with Quantum Channels. Annales Henri Poincaré, 22(10):3199-3234, October 2021. URL: https://doi.org/10.1007/s00023-021-01042-3.
  33. Giacomo De Palma and Dario Trevisan. The Wasserstein Distance of Order 1 for Quantum Spin Systems on Infinite Lattices. Annales Henri Poincaré, 24(12):4237-4282, December 2023. URL: https://doi.org/10.1007/s00023-023-01340-y.
  34. Ellie D'Hondt and Prakash Panangaden. Quantum weakest preconditions. Mathematical Structures in Computer Science, 16(3):429-451, 2006. URL: https://doi.org/10.1017/S0960129506005251.
  35. Thierry Fack and Hideki Kosaki. Generalized s-numbers of τ-measurable operators. Pacific Journal of Mathematics, 123(2):269-300, 1986. Google Scholar
  36. Yuan Feng and Mingsheng Ying. Quantum Hoare Logic with Classical Variables. ACM Transactions on Quantum Computing, 2(4), 2021. URL: https://doi.org/10.1145/3456877.
  37. Shmuel Friedland, Michał Eckstein, Sam Cole, and Karol Życzkowski. Quantum Monge-Kantorovich Problem and Transport Distance between Density Matrices. Physical Review Letters, 129(11):110402, September 2022. URL: https://doi.org/10.1103/PhysRevLett.129.110402.
  38. Shmuel Friedland, Jingtong Ge, and Lihong Zhi. Quantum Strassen’s theorem. Infinite Dimensional Analysis, Quantum Probability and Related Topics, 23(03):2050020, 2020. URL: https://doi.org/10.1142/S0219025720500204.
  39. Kurt Friedrichs. Spektraltheorie halbbeschränkter operatoren und anwendung auf die spektralzerlegung von differentialoperatoren. Mathematische Annalen, 109(1):465-487, 1934. Google Scholar
  40. Elies Gil-Fuster, Jens Eisert, and Carlos Bravo-Prieto. Understanding quantum machine learning also requires rethinking generalization. Nature Communications, 15(1):2277, March 2024. URL: https://doi.org/10.1038/s41467-024-45882-z.
  41. François Golse, Clément Mouhot, and Thierry Paul. On the Mean Field and Classical Limits of Quantum Mechanics. Communications in Mathematical Physics, 343(1):165-205, April 2016. URL: https://doi.org/10.1007/s00220-015-2485-7.
  42. François Golse and Thierry Paul. The Schrödinger Equation in the Mean-Field and Semiclassical Regime. Archive for Rational Mechanics and Analysis, 223(1):57-94, January 2017. URL: https://doi.org/10.1007/s00205-016-1031-x.
  43. François Golse and Thierry Paul. Wave packets and the quadratic Monge-Kantorovich distance in quantum mechanics. Comptes Rendus. Mathématique, 356(2):177-197, January 2018. URL: https://doi.org/10.1016/j.crma.2017.12.007.
  44. François Golse and Thierry Paul. Optimal transport pseudometrics for quantum and classical densities. Journal of Functional Analysis, 282(9):109417, 2022. URL: https://doi.org/10.1016/j.jfa.2022.109417.
  45. Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. Asynchronous probabilistic couplings in higher-order separation logic. Proc. ACM Program. Lang., 8(POPL):753-784, 2024. URL: https://doi.org/10.1145/3632868.
  46. Uffe Haagerup et al. Lp-spaces associated with an arbitrary von Neumann algebra. In Algebres d’opérateurs et leurs applications en physique mathématique (Proc. Colloq., Marseille, 1977), volume 274, pages 175-184, 1979. Google Scholar
  47. Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. Approximate relational reasoning for higher-order probabilistic programs. Proc. ACM Program. Lang., 9(POPL):1196-1226, 2025. URL: https://doi.org/10.1145/3704877.
  48. Bettina Heim, Mathias Soeken, Sarah Marshall, Chris Granade, Martin Roetteler, Alan Geller, Matthias Troyer, and Krysta Svore. Quantum programming languages. Nature Reviews Physics, 2(12):709-722, 2020. Google Scholar
  49. Alexander S Holevo. Probabilistic and statistical aspects of quantum theory, volume 1. Springer Science & Business Media, Berlin, Heidelberg, 2011. Google Scholar
  50. Matt Hoogsteder-Riera, John Calsamiglia, and Andreas Winter. Approach to optimal quantum transport via states over time, April 2025. URL: https://arxiv.org/abs/2504.04856.
  51. Roger A. Horn and Fuzhen Zhang. The Schur Complement and Its Applications, chapter Basic Properties of the Schur Complement, pages 17-46. Springer US, Boston, MA, 2005. URL: https://doi.org/10.1007/0-387-24273-2_2.
  52. Wiktor Jurasz and Christian B. Mendl. Quantum Wasserstein GANs for State Preparation at Unseen Points of a Phase Diagram, September 2023. URL: https://doi.org/10.48550/arXiv.2309.09543.
  53. L.V. Kantorovich. On the translocation of masses. Dokl. Akad. Nauk SSSR, 37(7-8):227-229, 1942. English translation available in J. Math. Sci. (2006). Google Scholar
  54. Tosio Kato. Perturbation theory for linear operators, volume 132. Springer Science & Business Media, 2013. Google Scholar
  55. Julia Kempe. Quantum random walks: an introductory overview. Contemporary Physics, 44(4):307-327, 2003. Google Scholar
  56. Yangjia Li and Dominique Unruh. Quantum Relational Hoare Logic with Expectations. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198 of Leibniz International Proceedings in Informatics (LIPIcs), pages 136:1-136:20, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.136.
  57. Jan Maas, Simone Rademacher, Tamás Titkos, and Dániel Virosztek, editors. Optimal Transport on Quantum Structures. Number 29 in Bolyai Society Mathematical Studies. Springer Nature, Cham, Switzerland, 2024. Google Scholar
  58. Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325-353, May 1996. URL: https://doi.org/10.1145/229542.229547.
  59. S. T. Rachev and Ludger Rüschendorf. Mass Transportation Problems. Probability and Its Applications. Springer, New York, 1998. Google Scholar
  60. Michael Reed and Barry Simon. Methods of modern mathematical physics, 2. Fourier Analysis, Self-Adjointness. New York, London: Academic Press, 1972. Google Scholar
  61. Michael Reed and Barry Simon. Methods of modern mathematical physics: Functional analysis, volume 1. Gulf Professional Publishing, 1980. Google Scholar
  62. Walter Rudin. Real and complex analysis. McGraw-Hill, Inc., 1987. Google Scholar
  63. Mary Beth Ruskai. Inequalities for traces on von neumann algebras. Communications in Mathematical Physics, 26(4):280-289, 1972. Google Scholar
  64. Tetsuya Sato. Approximate relational Hoare logic for continuous random samplings. In Lars Birkedal, editor, The Thirty-second Conference on the Mathematical Foundations of Programming Semantics, MFPS 2016, Carnegie Mellon University, Pittsburgh, PA, USA, May 23-26, 2016, volume 325 of Electronic Notes in Theoretical Computer Science, pages 277-298. Elsevier, 2016. URL: https://doi.org/10.1016/J.ENTCS.2016.09.043.
  65. Konrad Schmüdgen. Unbounded self-adjoint operators on Hilbert space, volume 265. Springer Science & Business Media, 2012. Google Scholar
  66. Barry Simon. Lower semicontinuhy of positive quadratic forms. Proceedings of the Royal Society of Edinburgh: Section A Mathematics, 79(3–4):267-273, 1978. URL: https://doi.org/10.1017/S0308210500019776.
  67. Dominique Unruh. Quantum relational Hoare logic. Proc. ACM Program. Lang., 3(POPL), 2019. URL: https://doi.org/10.1145/3290346.
  68. Cédric Villani. Topics in Optimal Transportation. Number 58 in Graduate Studies in Mathematics. American Mathematical Society, Providence (R.I.), 2003. Google Scholar
  69. Cédric Villani. Optimal transport: Old and new. Springer, 2008. Google Scholar
  70. Melchior Wirth. A Noncommutative Transport Metric and Symmetric Quantum Markov Semigroups as Gradient Flows of the Entropy, August 2021. URL: https://arxiv.org/abs/1808.05419.
  71. Melchior Wirth. A Dual Formula for the Noncommutative Transport Distance. Journal of Statistical Physics, 187(2):19, May 2022. URL: https://doi.org/10.1007/s10955-022-02911-9.
  72. Melchior Wirth and Haonan Zhang. Complete Gradient Estimates of Quantum Markov Semigroups. Communications in Mathematical Physics, 387(2):761-791, October 2021. URL: https://doi.org/10.1007/s00220-021-04199-4.
  73. Jiaqi Yang, Wei Xie, and Xiaohua Xu. Stability and Generalization of Quantum Neural Networks, February 2025. URL: https://doi.org/10.48550/arXiv.2501.12737.
  74. Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(6):19:1-19:49, 2011. URL: https://doi.org/10.1145/2049706.2049708.
  75. Mingsheng Ying. Foundations of Quantum Programming. Morgan Kaufmann, Cambridge, MA, USA, second edition, 2024. Google Scholar
  76. Li Zhou, Nengkun Yu, Shenggang Ying, and Mingsheng Ying. Quantum earth mover’s distance, a no-go quantum Kantorovich-Rubinstein theorem, and quantum marginal problem. Journal of Mathematical Physics, 63(10):102201, October 2022. URL: https://doi.org/10.1063/5.0068344.
  77. Karol Zyczkowski and Wojeciech Slomczynski. The Monge distance between quantum states. Journal of Physics A: Mathematical and General, 31(45):9095-9104, November 1998. URL: https://doi.org/10.1088/0305-4470/31/45/009.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact