A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914081543290880 |
|---|---|
| author | Barthe, Gilles Gao, Minbo Khan, Jam Kabeer Ali Muis, Matthijs Renison, Ivan Sakabe, Keiya Walter, Michael Xu, Yingte Zhou, Li |
| author_facet | Barthe, Gilles Gao, Minbo Khan, Jam Kabeer Ali Muis, Matthijs Renison, Ivan Sakabe, Keiya Walter, Michael Xu, Yingte Zhou, Li |
| contents | Duality theorems play a fundamental role in convex optimization. Recently, it was shown how duality theorems for countable probability distributions and finite-dimensional quantum states can be leveraged for building relatively complete relational program logics for probabilistic and quantum programs, respectively. However, complete relational logics for classical-quantum programs, which combine classical and quantum computations and operate over classical as well as quantum variables, have remained out of reach. The main gap is that while prior duality theorems could readily be derived using optimal transport and semidefinite programming methods, respectively, the combined setting falls out of the scope of these methods and requires new ideas. In this paper, we overcome this gap and establish the desired duality theorem for classical-quantum states. Our argument relies critically on a novel dimension-independent analysis of the convex optimization problem underlying the finite-dimensional quantum setting, which, in particular, allows us to take the limit where the classical state space becomes infinite. Using the resulting duality theorem, we establish soundness and completeness of a new relational program logic, called $\mathsf{cqOTL}$, for classical-quantum programs. In addition, we lift prior restrictions on the completeness of two existing program logics: $\mathsf{eRHL}$ for probabilistic programs (Avanzini et al., POPL 2025) and $\mathsf{qOTL}$ for quantum programs (Barthe et al., LICS 2025). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_07051 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics Barthe, Gilles Gao, Minbo Khan, Jam Kabeer Ali Muis, Matthijs Renison, Ivan Sakabe, Keiya Walter, Michael Xu, Yingte Zhou, Li Quantum Physics Logic in Computer Science Programming Languages Duality theorems play a fundamental role in convex optimization. Recently, it was shown how duality theorems for countable probability distributions and finite-dimensional quantum states can be leveraged for building relatively complete relational program logics for probabilistic and quantum programs, respectively. However, complete relational logics for classical-quantum programs, which combine classical and quantum computations and operate over classical as well as quantum variables, have remained out of reach. The main gap is that while prior duality theorems could readily be derived using optimal transport and semidefinite programming methods, respectively, the combined setting falls out of the scope of these methods and requires new ideas. In this paper, we overcome this gap and establish the desired duality theorem for classical-quantum states. Our argument relies critically on a novel dimension-independent analysis of the convex optimization problem underlying the finite-dimensional quantum setting, which, in particular, allows us to take the limit where the classical state space becomes infinite. Using the resulting duality theorem, we establish soundness and completeness of a new relational program logic, called $\mathsf{cqOTL}$, for classical-quantum programs. In addition, we lift prior restrictions on the completeness of two existing program logics: $\mathsf{eRHL}$ for probabilistic programs (Avanzini et al., POPL 2025) and $\mathsf{qOTL}$ for quantum programs (Barthe et al., LICS 2025). |
| title | A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics |
| topic | Quantum Physics Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2510.07051 |