Complete Quantum Relational Hoare Logics from Optimal Transport Duality

Gilles Barthe; Li Zhou; Minbo Gao; Theo Wang

REVIEW 2 major objections 4 minor 1 cited by

Complete Quantum Relational Hoare Logics from Optimal Transport Duality

T0 review · 2 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Quantum relational Hoare logic is now sound and complete

desk verdict Completeness for coupling-based quantum relational Hoare logics is here; the SDP-duality worry is a presentation gap, not a flaw. read the letter →

arxiv 2501.15238 v1 pith:MIOIGZZG submitted 2025-01-25 cs.LO quant-ph

Gilles Barthe , Minbo Gao , Theo Wang , Li Zhou This is my paper · ORCID

classification cs.LOquant-ph MSC 68Q6068Q1281P68

keywords quantumrelationalHoarelogicoptimaltransportdualitycouplingsStrassentheoremalmost-surelyterminatingprogramsinfinite-valuedpredicatesprogramequivalencedifferentialprivacy

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper introduces qOTL, a relational Hoare logic for pairs of quantum while-programs, and proves that the logic is sound and complete for almost surely terminating programs with bounded quantitative postconditions. Validity is coupling-based: a judgment {P} S1 ~ S2 {Q} holds when the expected value of P on the input bounds the expected value of Q on some quantum coupling of the two outputs. The completeness proof sidesteps the hard problem of constructing couplings directly and instead uses a quantum version of optimal-transport duality to reduce any bounded postcondition to a split postcondition, for which ordinary compositional rules are already complete. A secondary contribution is an infinitary extension of positive semidefinite predicates that lets projective, subspace-based assertions be embedded completely into the quantitative logic. If correct, the paper turns relational verification of quantum programs from a search for witnesses into a proof-theoretic guarantee: every true bounded judgment has a derivation.

What carries the argument

The load-bearing mechanism is the quantum Strassen theorem with defects (Theorem III.3), a duality for quantum couplings proved by semidefinite programming. It characterizes the existence of a coupling with bounded cost through a universal dual inequality over positive semidefinite witnesses; the paper generalizes it from subspace liftings to arbitrary PSD costs and infinite-valued defects, and then to partial couplings so that non-trace-preserving programs are covered. On top of that sits the duality rule, which converts a judgment with an arbitrary bounded postcondition Q into universally quantified judgments with split postconditions Q1⊗I + I⊗Q2, and the one-sided weakest-precondition lemmas that prove split judgments by structural induction. Infinite-valued predicates in Pos∞ act as a separate mechanism: a predicate X|A = A + ∞·X⊥ enforces a projective precondition X inside the quantitative logic, which is what makes the complete embedding of projective assertions possible.

What would settle it

Numerically solve the primal SDP for the quantum Strassen theorem—minimizing tr(Xρ) over couplings of two equal-trace states—and its dual for a two-qubit cost operator X such as the projector onto the singlet state with a small defect ε; a primal value strictly below the dual value would show strong duality fails and would invalidate the duality rule. A companion check is to test Theorem IV.4 on a pair of one-qubit AST programs where Q is a bounded non-split postcondition: if all the universal split judgments are derivable but the original judgment is not, completeness fails.

Watch

Extended reading notes

Core claim

On its own terms, the central claim is that a minimal set of Hoare rules—one-sided rules for initialization, unitaries, conditionals and loops, two-sided rules for skip and sequence, and a rule of consequence—becomes complete when augmented with a single duality rule. The duality rule is powered by a quantum Strassen theorem with defects: for equal-trace states, a coupling with tr(Xρ) ≤ ε exists exactly when every pair of positive semidefinite operators Y1, Y2 with X ⊒ Y1⊗I − I⊗Y2 satisfies tr(Y1ρ1) ≤ tr(Y2ρ2) + ε. Lifting this from states to quantum operations gives Theorem IV.4, which says that a pair of programs is monotone with respect to a cost Q if and only if it is monotone with respect to all split costs Y1⊗I + I⊗(nI − Y2) below Q. Hence any valid judgment with a bounded postcondition Q can be derived by proving universally quantified split-postcondition judgments, and those are handled by one-sided weakest preconditions. The result is Theorem VI.7: for almost surely terminating programs and bounded Q, validity implies derivability.

Load-bearing premise

The load-bearing premise is that the semidefinite duality in the quantum Strassen theorem with defects is exact: existence of a coupling with cost at most ε is equivalent to the dual inequality over all positive-semidefinite witness pairs, with strong duality surviving arbitrary PSD costs and infinite-valued defects.

Editorial extensions

If this is right

Any valid relational judgment about almost surely terminating quantum programs with a bounded PSD postcondition has a formal proof in qOTL, so relational verification is complete in principle.
The duality rule is the only structural rule needed; the standard one-sided rules for initialization, unitaries, conditionals and loops are already complete for split postconditions.
Infinite-valued predicates give a complete bridge between subspace-based projective predicates and quantitative PSD predicates, so the two styles of quantum Hoare logic can be used interchangeably.
Program equivalence, trace distance and diamond norm bounds, Wasserstein semi-distance, non-interference, and quantum differential privacy all receive complete characterizations as derivable judgments for AST programs.
By the same route, the probabilistic relational Hoare logic eRHL is complete for bounded postconditions and almost surely terminating programs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Because completeness is reduced to SDP duality, proof search could in principle be driven by solving the primal and dual semidefinite programs that define a postcondition's split witnesses; the paper does not develop such an algorithm.
The finiteness restriction on postconditions in the duality theorem suggests that completeness for genuinely infinite-valued postconditions would require a new duality allowing +∞ costs throughout; the current proof stops at bounded Q.
A separable-coupling analogue of the quantum Strassen duality is not known; if one existed, the same duality-rule architecture might yield completeness for separable-coupling relational logics, which the paper leaves open.
The probabilistic completeness result indicates the same optimal-transport duality pattern recurs classically, so one might expect a single cost-based relational logic generalizing both the quantum and probabilistic cases.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Bottom line: this is the completeness result the field was missing. It builds a sound and complete relational Hoare logic for almost-surely terminating quantum programs with bounded postconditions, and it does so by a route that is clever but also checkable: split postconditions are handled by structural weakest preconditions, and arbitrary bounded postconditions are reduced to split ones by a duality rule derived from a quantum Strassen theorem with defects. The infinite-valued predicates and partial couplings are not just ornament; they are what allow projective preconditions and non-trace-preserving programs to fit in the same framework. The embeddings of projective-predicate logics and the characterizations of program equivalence, diamond norm, Wasserstein semi-distance, non-interference, and quantum differential privacy are useful dividends.

The proof is structurally coherent. The central load-bearing item is Theorem III.3, the defect version of Strassen's theorem, proved in Appendix B via SDP strong duality. The stress-test worry is that strong duality fails when the marginals are singular because the primal coupling polytope may lack an interior point. I think that worry does not land: the dual is strictly feasible by taking Y1=Y2=λI for large λ, so Slater holds on the dual side. The paper does not explicitly verify this, so it is worth a referee's attention, but it is a minor gap in presentation, not a flaw in the argument.

The soft spots are the usual ones for a paper of this density. The appendix is long and no part is machine-checked, so subtle bookkeeping errors are possible. The completeness proof for bounded postconditions goes through the duality rule with n quantified over naturals; since the underlying duality holds for reals, this is fine, but the mismatch is a little jarring. The two-sided rules are not needed for completeness and the presentation is brief; they are clearly marked as optional.

Who this is for: researchers in quantum program logics, verification, and relational reasoning. It deserves a serious referee and will likely become a standard reference. Send it to review.

Referee Report

2 major / 4 minor

Summary. The paper introduces qOTL, a quantitative relational Hoare logic for quantum while-programs, with assertions ranging over a new infinitary extension of PSD operators, judgments parameterized by logical variables, and validity based on partial quantum couplings. It proves soundness (Theorem VI.3) and two completeness results: completeness for split postconditions (Theorem VI.6) and completeness for bounded postconditions for almost surely terminating programs (Theorem VI.7), the latter obtained by reducing arbitrary bounded postconditions to universally quantified split postconditions through a duality rule. The duality rule is justified by a quantum Strassen theorem with defects (Theorem III.3) and a duality-under-data-processing theorem (Theorem IV.4). The paper also gives a complete semantic embedding of projective relational Hoare logic into qOTL using infinite-valued predicates, and derives characterizations of program equivalence, trace distance and diamond norm, quantum Wasserstein semi-distance, non-interference, and differential privacy. An extended appendix contains the main proofs, including SDP-based proofs of the duality theorems, and a probabilistic corollary establishing completeness of eRHL.

Significance. If the stated results hold, this is a substantial advance: it provides the first completeness theorem for a relational Hoare logic over quantum programs, and it does so by an elegant route that separates split-postcondition completeness from a Kantorovich-Rubinstein-style duality step. The introduction of infinite-valued PSD predicates is a useful unification of projective and quantitative assertions, and the embedding of pqRHL into qOTL (Proposition VII.2, Theorem VII.3) is a genuine contribution. The split-completeness proof (Lemmas VI.4 and VI.5, Theorem VI.6) is clean and detailed, and the applications in Section VIII are nontrivial. The main caveat is that the central Theorem III.3 depends on an asserted SDP strong-duality step that is not verified in the appendix; this is likely repairable, but it is currently a gap in the proof of the main completeness theorem. The paper is not machine-checked, but the appendix is unusually detailed and the proof structure is coherent.

major comments (2)

[Appendix B, proof of Theorem III.3] The proof of direction (2 => 1) rests on the assertion that the coupling SDP 'can be shown to satisfy strong duality', but no proof, constraint qualification, or precise SDP duality theorem is supplied. This is load-bearing because the primal feasible set consists of couplings with fixed singular marginals and may lack a relative interior point; strong duality must then be established via a Slater point on the dual side. Such a point exists (e.g., Y1 = Y2 = λI for sufficiently large λ makes Φ†(Y) strictly greater than I - X), but this must be stated explicitly, together with the exact strong-duality theorem being invoked. Since Theorem IV.4, the duality rule, and hence Theorem VI.7 all depend on Theorem III.3, this missing verification is a substantive gap in the submitted proof, even though it appears readily fixable.
[Theorem IV.4 and Appendix C, proof of Theorem C.7] The reduction from condition (1) to condition (2) in Theorem IV.4 is presented as a direct consequence of Theorem III.3, but the passage from arbitrary Hermitian witnesses to PSD witnesses via a shift by nI, and the restriction of n to natural numbers, is not explicitly verified. In finite dimension one can choose an integer n with Y2 ⊑ nI for any PSD Y2, and the shift argument in the proof of Theorem III.3 is pointwise, so no uniformity issue arises; however, the proof as written skips these steps. Because the side conditions of the duality rule in Figure 1 mirror exactly the set Y of Theorem IV.4, the completeness proof of Theorem VI.7 should spell out this correspondence.

minor comments (4)

[Section II.C and Definition A.6] The definition of X | A as A + ∞·X⊥ in Section II.C and the 'equivalently' formula in Definition A.6, namely ((X ∨ X_A⊥)P_A(X ∨ X_A⊥), X⊥ ∨ X_A), do not appear to coincide when A has a nontrivial infinite part and X does not commute with X_A. Please clarify the intended definition, since Lemma A.7 relies on these extended operations.
[Theorem VI.7, proof] The displayed line '⊢Z : {P} S1 ~ S2 {Q} ⇐⇒ ⊢Z,(Y1,Y2,n) ∈ Y : {P+nI} S1 ~ S2 {Y1⊗I + I⊗(nI−Y2)}' is not literally an equivalence of judgments; it describes the condition under which the duality rule applies. Replacing the biconditional with an implication or a stated 'it suffices to prove' would avoid confusion.
[Proposition IV.6] The statement contains a typo: 'tr(tr2(Y2))ρ2)' should read 'tr(tr2(Y2)ρ2)'. Please correct the parenthesis.
[Theorem C.7 / proof of Theorem IV.4] In the proof of Theorem C.7, n is first treated as a real scalar in the shift argument and then as a natural number in the set Y. Since finite-dimensional operators have bounded spectra, the integer choice is always possible, but the proof should say this explicitly to avoid a perceived gap.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; completeness rests on a self-contained proof of a generalized Strassen theorem.

full rationale

The central completeness theorem (Theorem VI.7) reduces valid judgments to split postconditions via the duality rule, whose soundness is Theorem IV.4, proved from Theorem III.3 (quantum Strassen with defects). Theorem III.3 is not assumed from the authors' earlier work: Appendix B gives a proof via SDP strong duality, extending [7] to arbitrary PSD costs and infinite-valued defects. The proof does cite [7] for the SDP setting, but the equivalence is re-proved in the appendix and the strong duality assertion is a standard external fact, not an input to the logic. The split-postcondition completeness (Theorem VI.6) is proved by structural induction with weakest preconditions, independent of the duality theorem. The applications and embeddings are corollaries of the proved completeness and do not fit parameters or rename a known result by definition. The skeptic's concern about Slater's condition for singular marginals is a possible correctness gap in the SDP duality argument, not a circularity: it questions whether Theorem III.3 holds, rather than showing that the theorem is assumed. Therefore no circular steps are present.

Assumptions & free parameters 0 free parameters · 4 assumptions · 3 invented entities

The paper introduces no fitted numerical parameters. It relies on standard finite-dimensional quantum mechanics, SDP strong duality, and the stabilized QOT characterization of [11]. New mathematical definitions, Pos∞ and partial couplings, are justified inside the paper through internal theorems but are not independently evidenced entities.

assumptions (4)

domain assumption All Hilbert spaces are finite-dimensional and qWhile programs are interpreted via the CPO semantics with the Löwner order over partial density operators.
Section II and Section V define this setting; all theorems inherit finite-dimensionality.
standard math SDP strong duality holds for the semidefinite program used in the proof of the quantum Strassen theorem with defects.
Used in Appendix B, proof of Theorem B.1; stated but not proved in the paper.
standard math Stabilized quantum optimal transport satisfies Ts(ρ,σ) = T(ρ⊗I/2, σ⊗I/2), following [11] with a proof sketch in Appendix G.
Used for the program equivalence characterization in Proposition IV.6 and Theorem VIII.1; the appendix proof relies on Haar measure and Schur-Weyl duality.
domain assumption Partial couplings are adopted as the semantic notion of validity, with the trace inequality tr(ρ1)+tr(ρ2) ≤ 1+tr(ρ).
Definition III.5 in Section III.B; this is a design choice to handle non-trace-preserving programs and while loops, related to ⋆-couplings from [4].

invented entities (3)

Infinite-valued predicates Pos∞(H)
purpose: Allow PSD assertions with a possible +∞ eigenspace, enabling projective preconditions of the form X|A and unifying projective and quantitative predicates.
A new mathematical construct introduced by the paper; its value is internal expressiveness and it has no external falsifiable handle.
Partial couplings
purpose: Generalize quantum couplings to partial states by allowing the coupling to omit uncorrelated parts, subject to the trace inequality tr(ρ1)+tr(ρ2) ≤ 1+tr(ρ).
A definitional extension of couplings adapted from ⋆-couplings; no independent empirical evidence is provided or expected.
Logical variables Z parameterizing assertions
purpose: Enable quantification over external parameters in judgments, used in the duality rule and in encodings of trace distance and differential privacy.
A standard device in relational logics; the paper uses it to make universal quantifications part of the proof system.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Complete Quantum Relational Hoare Logics from Optimal Transport Duality." pith.science (2026). https://pith.science/paper/MIOIGZZG

@misc{pith2026250115238,
  author       = {Pith},
  title        = {Pith review of: Complete Quantum Relational Hoare Logics from Optimal Transport Duality},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MIOIGZZG}},
  note         = {Machine review of arXiv:2501.15238}
}

read the original abstract

We introduce a quantitative relational Hoare logic for quantum programs. Assertions of the logic range over a new infinitary extension of positive semidefinite operators. We prove that our logic is sound, and complete for bounded postconditions and almost surely terminating programs. Our completeness result is based on a quantum version of the duality theorem from optimal transport. We also define a complete embedding into our logic of a relational Hoare logic with projective assertions.

Figures

Figures reproduced from arXiv: 2501.15238 by the authors.

**Figure 1.** Rules for qOTL Theorem VI.9. For AST programs S1, S2, and measurements M = {M1, · · · , Mk} and N = {N1, · · · , Nk}, the following are equivalent: 1) ∅ (S1,S2) M ≈ N; 2) (Y1, · · · , Yk, Z1, · · · , Zk, n) ∈ Yk : {nI}S1 ∼ S2 ( P iM† i YiMi)⊗I+I⊗ [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗

**Figure 2.** Extra two-side rules for qOTL. This formulation has several advantages compared to its quantitative counterpart: the resulting logic often has simpler rules, and several non-trivial properties have much simpler formulations. Crucially, this is possible only because pqRHL allows one to enforce projective preconditions, i.e., membership of the initial state in a particular subspace. For example, equivalence between t… view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
quant-ph 2025-10 conditional novelty 7.0 of 10

Sound and complete relational logic for classical-quantum programs with unbounded assertions, built on a new classical-quantum optimal-transport duality theorem.

Reference graph

Works this paper leans on

101 extracted references · 57 canonical work pages · cited by 1 Pith paper

[1]

Quantum relational hoare logic,

D. Unruh, “Quantum relational hoare logic,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, p. 1–31, Jan. 2019. [Online]. Available: http://dx.doi.org/10.1145/3290346

doi:10.1145/3290346 2019
[2]

Relational proofs for quantum programs,

G. Barthe, J. Hsu, M. Ying, N. Y u, and L. Zhou, “Relational proofs for quantum programs,” Proc. ACM Program. Lang., vol. 4, no. POPL, Dec. 2019

2019
[3]

Quantum Relational Hoare Logic with E x- pectations,

Y . Li and D. Unruh, “Quantum Relational Hoare Logic with E x- pectations,” in Proceedings of the 48th International Colloquium on Automata, Languages, and Programming, vol. 198, 2021, pp. 136:1– 136:20

2021
[4]

A quantitative probabilistic relational hoare logic,

M. Avanzini, G. Barthe, D. Davoli, and B. Gr´ egoire, “A quantitative probabilistic relational hoare logic,” Proc. ACM Program. Lang., vol. 9, no. POPL, Jan. 2025. [Online]. Available: https://doi.org/10.1145/3704876

doi:10.1145/3704876 2025
[5]

M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010

2010
[6]

The existence of probability measures wit h given marginals,

V . Strassen, “The existence of probability measures wit h given marginals,” The Annals of Mathematical Statistics , pp. 423–439, 1965. [Online]. Available: http://projecteuclid.org/euclid. aoms/1177700153

arXiv 1965
[7]

Strassen’s theorem for quantum couplings,

L. Zhou, S. Ying, N. Y u, and M. Ying, “Strassen’s theorem for quantum couplings,” Theoretical Computer Science, vol. 802, pp. 67–76, 2020. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0304397519305225

2020
[8]

On quantum optimal transport,

S. Cole, M. Eckstein, S. Friedland, and K. ˙Zyczkowski, “On quantum optimal transport,” Mathematical Physics, Analysis and Geometry, vol. 26, no. 2, p. 14, Jun 2023. [Online]. Availabl e: https://doi.org/10.1007/s11040-023-09456-7

doi:10.1007/s11040-023-09456-7 2023

Show all 101 references

[9]

M´ emoire sur la th´ eorie des d´ eblais et des re mblais,

G. Monge, “M´ emoire sur la th´ eorie des d´ eblais et des re mblais,” Mem. Math. Phys. Acad. Royale Sci., pp. 666–704, 1781
[10]

Monotonicity of a quantum 2-wasserstein distance,

R. Bistro´ n, M. Eckstein, and K. ˙Zyczkowski, “Monotonicity of a quantum 2-wasserstein distance,” Journal of Physics A: Mathematical and Theoretical, vol. 56, no. 9, p. 095301, feb 2023. [Online]. Available: https://dx.doi.org/10.1088/1751-8121/acb9c8

2023 doi
[11]

On the monotonicity of a quantum op timal transport cost,

A. M¨ uller-Hermes, “On the monotonicity of a quantum op timal transport cost,” 2022. [Online]. Available: https://arxiv.org/abs /2211.11713

2022 arXiv
[12]

Quantum earth mover ’s distance, a no-go quantum Kantorovich–Rubinstein theorem, and quant um marginal problem,

L. Zhou, N. Y u, S. Ying, and M. Ying, “Quantum earth mover ’s distance, a no-go quantum Kantorovich–Rubinstein theorem, and quant um marginal problem,” Journal of Mathematical Physics, vol. 63, no. 10, p. 102201, 10 2022. [Online]. Available: https://doi.org/10 .1063/5.0068344

2022
[13]

Monogamy of quantum entanglem ent and other correlations,

M. Koashi and A. Winter, “Monogamy of quantum entanglem ent and other correlations,” Physical Review A, vol. 69, no. 2, p. 022309, 2004

2004
[14]

Floyd–hoare logic for quantum programs,

M. Ying, “Floyd–hoare logic for quantum programs,” ACM Trans. Program. Lang. Syst., vol. 33, no. 6, Jan. 2012. [Online]. Available: https://doi.org/10.1145/2049706.2049708

2012
[15]

San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2016

——, Foundations of Quantum Programming , 1st ed. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2016

2016
[16]

Approximate relational rea soning for quan- tum programs,

P . Y an, H. Jiang, and N. Y u, “Approximate relational rea soning for quan- tum programs,” in Computer Aided V eriﬁcation, A. Gurﬁnkel and V . Ganesh, Eds. Cham: Springer Nature Switzerland, 2024, pp . 495– 519

2024
[17]

An applied quantum hoare log ic,

L. Zhou, N. Y u, and M. Ying, “An applied quantum hoare log ic,” in Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI 2019. New Y ork, NY , USA: Association for Computing Machinery, 2019, p. 1149 –1162. [Online]. Avail...

2019 doi
[18]

Quantitative robustness analysis of quantum programs,

S.-H. Hung, K. Hietala, S. Zhu, M. Ying, M. Hicks, and X. W u, “Quantitative robustness analysis of quantum programs,” Proc. ACM Program. Lang., vol. 3, no. POPL, Jan. 2019. [Online]. Available: https://doi.org/10.1145/3290344

2019 doi
[19]

Glei pnir: toward practical error analysis for quantum programs,

R. Tao, Y . Shi, J. Y ao, J. Hui, F. T. Chong, and R. Gu, “Glei pnir: toward practical error analysis for quantum programs,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , ser. PLDI 2021. New Y ork, NY , USA:...

2021 doi
[20]

Quantum Computing in the NISQ era and beyo nd,

J. Preskill, “Quantum Computing in the NISQ era and beyo nd,” Quantum, vol. 2, p. 79, Aug. 2018. [Online]. Available: https://doi.org/10.22331/q-2018-08-06-79

2018 doi
[21]

M. M. Wilde, Quantum Information Theory, 2nd ed. Cambridge University Press, 2017

2017
[22]

Quantum circuits with mixed states,

D. Aharonov, A. Kitaev, and N. Nisan, “Quantum circuits with mixed states,” in Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, ser. STOC ’98. New Y ork, NY , USA: Association for Computing Machinery, 1998, p. 20–30. [Onli ne]. Available: https://doi.o...

1998
[23]

Quantum information-ﬂow se curity: Noninterference and access control,

M. Ying, Y . Feng, and N. Y u, “Quantum information-ﬂow se curity: Noninterference and access control,” in 2013 IEEE 26th Computer Security Foundations Symposium, 2013, pp. 130–144

2013
[24]

Gentle measurement of q uantum states and differential privacy,

S. Aaronson and G. N. Rothblum, “Gentle measurement of q uantum states and differential privacy,” in Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing , 2019, p. 322–333

2019
[25]

Differential privacy in quantum co mputation,

L. Zhou and M. Ying, “Differential privacy in quantum co mputation,” in 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 2017, pp. 249–262

2017
[26]

For mal certiﬁcation of code-based cryptographic proofs,

G. Barthe, B. Gr´ egoire, and S. Zanella B´ eguelin, “For mal certiﬁcation of code-based cryptographic proofs,” in Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009, p. 90–101

2009
[27]

A pre-expectation calculus for probabilistic sensitivity,

A. Aguirre, G. Barthe, J. Hsu, B. L. Kaminski, J. Katoen, and C. Matheja, “A pre-expectation calculus for probabilistic sensitivity,” Proc. ACM Program. Lang., vol. 5, no. POPL, pp. 1–28, 2021. [Online]. Available: https://doi.org/10.1145/3434333

2021 doi
[28]

Asynchronous probabilistic couplings in hig her-order separation logic,

S. O. Gregersen, A. Aguirre, P . G. Haselwarter, J. Tassa rotti, and L. Birkedal, “Asynchronous probabilistic couplings in hig her-order separation logic,” Proc. ACM Program. Lang., vol. 8, no. POPL, pp. 753–784, 2024. [Online]. Available: https://doi.org/10. 1145/3632868

2024
[29]

The monge distance between quantum states,

K. Zyczkowski and W. Slomczynski, “The monge distance between quantum states,” Journal of Physics A: Mathematical and General, vol. 31, no. 45, p. 9095, nov 1998. [Online]. Availa ble: https://dx.doi.org/10.1088/0305-4470/31/45/009

1998 doi
[30]

The monge metric on the sphere and geometry of quantum states,

——, “The monge metric on the sphere and geometry of quantum states,” Journal of Physics A: Mathematical and General , vol. 34, no. 34, p. 6689, aug 2001. [Online]. Available: https://dx.doi.org/10.1088/0305-4470/34/34/311

2001 doi
[31]

On the mean ﬁeld and cla ssical limits of quantum mechanics,

F. Golse, C. Mouhot, and T. Paul, “On the mean ﬁeld and cla ssical limits of quantum mechanics,” Communications in Mathematical Physics, vol. 343, no. 1, pp. 165–205, Apr. 2016

2016
[32]

Quantum and Semiquantum Pseudome trics and applications,

F. Golse and T. Paul, “Quantum and Semiquantum Pseudome trics and applications,” Journal of Functional Analysis, 2022. [Online]. Available: https://hal.science/hal-03136855

2022
[33]

To- wards Optimal Transport for Quantum Densities,

E. Caglioti, F. Golse, and T. Paul, “To- wards Optimal Transport for Quantum Densities,” Annali della Scuola Normale Superiore di Pisa, Classe di Sci enze,
[34]

Quantum optimal transport is cheaper,

——, “Quantum optimal transport is cheaper,” Journal of Statistical Physics, vol. 181, no. 1, pp. 149–162, Oct. 2020

2020
[35]

Quantum optimal transport with quantum channels,

G. De Palma and D. Trevisan, “Quantum optimal transport with quantum channels,” Annales Henri Poincar´ e, vol. 22, no. 10, pp. 3199–3234, Oct. 2021

2021
[36]

Cham: Springer Nature Switzerland, 2024, pp

——, Quantum Optimal Transport: Quantum Channels and Qubits . Cham: Springer Nature Switzerland, 2024, pp. 203–239. [Onl ine]. Available: https://doi.org/10.1007/978-3-031-50466-2 4

2024 doi
[37]

Li mitations of variational quantum algorithms: A quantum optimal trans port approach,

G. De Palma, M. Marvian, C. Rouz´ e, and D. S. Franc ¸a, “Li mitations of variational quantum algorithms: A quantum optimal trans port approach,” PRX Quantum, vol. 4, p. 010309, Jan 2023. [Online]. Available: https://link.aps.org/doi/10.1103/PRXQuantum.4.010309

2023 doi
[38]

Quantum concentration inequalities and equivalence of the thermodynamical ensem bles: an optimal mass transport approach,

G. D. Palma and D. Pastorello, “Quantum concentration inequalities and equivalence of the thermodynamical ensem bles: an optimal mass transport approach,” 2024. [Online]. Avail able: https://arxiv.org/abs/2403.18617

2024 arXiv
[39]

Quantum monge-kantorovich problem and transport distance between density matrices,

S. Friedland, M. Eckstein, S. Cole, and K. ˙Zyczkowski, “Quantum monge-kantorovich problem and transport distance between density matrices,” Physical Review Letters, vol. 129, p. 110402, Sep 2022

2022
[40]

Quantum earth mover ’s distance, a no-go quantum kantorovich–rubinstein theorem , and quantum marginal problem,

L. Zhou, N. Y u, S. Ying, and M. Ying, “Quantum earth mover ’s distance, a no-go quantum kantorovich–rubinstein theorem , and quantum marginal problem,” Journal of Mathematical Physics, vol. 63, no. 10, p. 102201, 10 2022. [Online]. Available: https://doi.org/10 .1063/5.0068344

2022
[41]

A categorical semantics of q uantum proto- cols,

S. Abramsky and B. Coecke, “A categorical semantics of q uantum proto- cols,” 2007. [Online]. Available: https://arxiv.org/abs /quant-ph/0402130

2007 arXiv
[42]

Coecke and A

B. Coecke and A. Kissinger, Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017

2017
[43]

Heunen and J

C. Heunen and J. Vicary, Categories for Quantum Theory: An Introduction. Oxford University Press, 11 2019. [Online]. Available: https://doi.org/10.1093/oso/9780198739623.001.0001

2019
[44]

Interacting quantum observab les,

B. Coecke and R. Duncan, “Interacting quantum observab les,” in Automata, Languages and Programming, L. Aceto, I. Damg˚ ard, L. A. Goldberg, M. M. Halld´ orsson, A. Ing´ olfsd´ ottir, and I. Walukiewicz, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 298–310

2008
[45]

Zh: A complete graphical c alculus for quantum computations involving classical non-lineari ty,

M. Backens and A. Kissinger, “Zh: A complete graphical c alculus for quantum computations involving classical non-lineari ty,” Electronic Proceedings in Theoretical Computer Science , vol. 287, p. 23–42, Jan
[46]

A diagrammatic axiomatisation fo r qubit entan- glement,

A. Hadzihasanovic, “A diagrammatic axiomatisation fo r qubit entan- glement,” 2015. [Online]. Available: https://arxiv.org/ abs/1501.07082

2015 arXiv
[47]

Automating equational pr oofs in dirac notation,

Y . Xu, G. Barthe, and L. Zhou, “Automating equational pr oofs in dirac notation,” Proc. ACM Program. Lang., vol. 9, no. POPL, Jan. 2025. [Online]. Available: https://doi.org/10.1145/3704878

2025 doi
[48]

Algebraic effects, linearity, and quantum programming languages,

S. Staton, “Algebraic effects, linearity, and quantum programming languages,” in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’15. New Y ork, NY , USA: Association for Computing Machinery, 2015, p. 395–406. [Onli...

2015
[49]

Wit h a few square roots, quantum computing is as easy as pi,

J. Carette, C. Heunen, R. Kaarsgaard, and A. Sabry, “Wit h a few square roots, quantum computing is as easy as pi,” Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, p. 546–574, Jan
[50]

A process algebraic approach to concurrent and distributed quantum computation: Operational semanti cs,

M. Lalire and P . Jorrand, “A process algebraic approach to concurrent and distributed quantum computation: Operational semanti cs,” 2004. [Online]. Available: https://arxiv.org/abs/quant-ph/0407005

2004 arXiv
[51]

Communicating quantum proces ses,

S. Gay and R. Nagarajan, “Communicating quantum proces ses,” 2004. [Online]. Available: https://arxiv.org/abs/quant-ph/0409052

2004 arXiv
[52]

Quantum bisimilarity via barbs and contexts: Curbing the power of no n- deterministic observers,

L. Ceragioli, F. Gadducci, G. Lomurno, and G. Tedeschi, “Quantum bisimilarity via barbs and contexts: Curbing the power of no n- deterministic observers,” Proc. ACM Program. Lang., vol. 8, no. POPL, jan 2024. [Online]. Available: https://doi.org/10.1145/ 3632885

2024
[53]

An algebra of quantu m processes,

M. Ying, Y . Feng, R. Duan, and Z. Ji, “An algebra of quantu m processes,” 2010. [Online]. Available: https://arxiv.or g/abs/0707.0330

2010 arXiv
[54]

Relationa l proofs for quantum programs,

G. Barthe, J. Hsu, M. Ying, N. Y u, and L. Zhou, “Relationa l proofs for quantum programs,” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, Dec. 2019

2019
[55]

Introduction to Haar Measure Tools in Quant um Informa- tion: A Beginner’s Tutorial,

A. A. Mele, “Introduction to Haar Measure Tools in Quant um Informa- tion: A Beginner’s Tutorial,” Quantum, vol. 8, p. 1340, 2024

2024
[56]

N OTATIONS AND PRELIMINARIES

C. Villani, Optimal transport – Old and new. Springer Berlin, Heidelberg, 2008, vol. 338. APPENDIX A DEFERRED PROOFS IN “N OTATIONS AND PRELIMINARIES ” S ECTION We ﬁrst brieﬂy review some basic concepts and propositions i n linear algebra and quantum computing. Quantum States....

2008
[60]

If ǫ = +∞, then both (1) and (2) trivially hold

F or anyY1 ∈ Pos(H1) and Y2 ∈ Pos(H2) such that X ⊒Y1 ⊗I2 −I1 ⊗Y2, it holds that tr(Y1ρ1) ≤ tr(Y2ρ2) +ǫ Proof. If ǫ = +∞, then both (1) and (2) trivially hold. So we consider the case that ǫ ∈ R+, i.e., ǫ is ﬁnite. • (1 =⇒ 2). Suppose ρ1X # ǫ ρ2, let ρ : ⟨ρ1,ρ 2⟩ be the witnes...
[61]

• For any A ∈ Pos(H1 ⊗ H2), we deﬁne A⋆ ∈ Pos(H⋆ 1 ⊗ H⋆

is a ⋆-coupling of ρ1 and ρ2, written ρ : ⟨ρ1,ρ 2⟩⋆, if ρ : ⟨ρ⋆ 1,ρ⋆ 2⟩. • For any A ∈ Pos(H1 ⊗ H2), we deﬁne A⋆ ∈ Pos(H⋆ 1 ⊗ H⋆
[62]

• For ρ ∈ D(H⋆ 1 ⊗ H⋆ 2), we deﬁne the projection: Π ⊥ ⋆ (ρ) = (P ⊥ ⋆ ⊗P ⊥ ⋆ )ρ(P ⊥ ⋆ ⊗P ⊥ ⋆ ) ∈ D(H1 ⊗ H2)

as the embedding of A. • For ρ ∈ D(H⋆ 1 ⊗ H⋆ 2), we deﬁne the projection: Π ⊥ ⋆ (ρ) = (P ⊥ ⋆ ⊗P ⊥ ⋆ )ρ(P ⊥ ⋆ ⊗P ⊥ ⋆ ) ∈ D(H1 ⊗ H2). • For any ρ ∈ D(H1 ⊗ H2) such that ρ : ⟨ρ1,ρ 2⟩p, deﬁne ρ↑ =(1 + tr(ρ) − tr(ρ1) − tr(ρ2))|⋆⋆ ⟩⟨⋆⋆ | + (ρ1 − tr2(ρ)) ⊗ |⋆⟩⟨⋆| + |⋆⟩⟨⋆| ⊗ (ρ2 − tr1...
[63]

Any ⋆-coupling provide a partial-coupling, i.e., Π ⊥ ⋆ (ρ) : ⟨ρ1,ρ 2⟩p if ρ : ⟨ρ1,ρ 2⟩⋆
[64]

In fact, Π ⊥ ⋆ (ρ↑) = ρ

W e can construct ⋆-coupling from a partial-coupling, i.e., ρ↑ : ⟨ρ1,ρ 2⟩⋆ if ρ : ⟨ρ1,ρ 2⟩p. In fact, Π ⊥ ⋆ (ρ↑) = ρ
[65]

As a consequence, if ρ : ⟨ρ1,ρ 2⟩p, then tr(A⋆ρ↑) = tr(Aρ)

If ρ : ⟨ρ1,ρ 2⟩⋆, tr(A⋆ρ) = tr(AΠ ⊥ ⋆ (ρ)). As a consequence, if ρ : ⟨ρ1,ρ 2⟩p, then tr(A⋆ρ↑) = tr(Aρ). Proof. (1). Suppose ρ : ⟨ρ1,ρ 2⟩⋆. Compute tr2(Π ⊥ ⋆ (ρ)) = tr 2((P ⊥ ⋆ ⊗P ⊥ ⋆ )ρ(P ⊥ ⋆ ⊗P ⊥ ⋆ )) =P ⊥ ⋆ tr2((I⋆ ⊗P ⊥ ⋆ )ρ(I⋆ ⊗P ⊥ ⋆ ))P ⊥ ⋆ ⊑P ⊥ ⋆ tr2(ρ)P ⊥ ⋆ =P ⊥ ⋆ ρ⋆ 1P ...
[66]

Π ⊥ ⋆ (ρ↑) = ρ is trivial by computation

Thus, ρ↑ : ⟨ρ⋆ 1,ρ⋆ 2⟩, or equivalently, ρ↑ : ⟨ρ1,ρ 2⟩⋆. Π ⊥ ⋆ (ρ↑) = ρ is trivial by computation. (3). Note that, A⋆ is preserved under the projection P ⊥ ⋆ ⊗P ⊥ ⋆ , so : tr(A⋆ρ) = tr(A⋆(P ⊥ ⋆ ⊗P ⊥ ⋆ )ρ(P ⊥ ⋆ ⊗P ⊥ ⋆ ))) = tr(AΠ ⊥ ⋆ (ρ)). Proposition B.4 ((Sub-)convex Combinat...
[67]

There exists partial-coupling ρ : ⟨ρ1,ρ 2⟩p such that tr(Aρ) ≤ǫ
[68]

F or anyy1,y 2 ∈ R+,Y1 ∈ Pos(H1),Y 2 ∈ Pos(H2), such that y1 ≤y2,Y1 ≤y2I1,y1I2 ≤Y2 andA ⊒Y1 ⊗I2 −I1 ⊗Y2, it holds that: y1(1 − tr(ρ1)) + tr(Y1ρ1) ≤y2(1 − tr(ρ2)) + tr(Y2ρ2) +ǫ. Proof. Ifǫ = +∞, then both (1) and (2) trivially hold. So we consider the case thatǫ ∈ R+, i.e., ǫ i...
[69]

• (1 ⇒ 3)

There exists star-coupling ρ : ⟨ρ1,ρ 2⟩⋆, i.e., ρ : ⟨ρ⋆ 1,ρ⋆ 2⟩, such that tr(A⋆ρ) ≤ǫ. • (1 ⇒ 3). Let ρ be the witness of (1), then ρ↑ : ⟨ρ1,ρ 2⟩⋆ by Lemma B.3(2). According to Lemma B.3(3), tr(A⋆ρ↑) = tr(Aρ) ≤ǫ. • (3 ⇒ 1). Let ρ be the witness of (3), then Π ⊥ ⋆ (ρ) : ⟨ρ1,ρ 2...
[70]

such that A⋆ ⊒Z1 ⊗I2⋆ −I1⋆ ⊗Z2, it holds that tr(Z1ρ⋆
[71]

What remaining to be shown is (2) equivalent to (4)

+ǫ. What remaining to be shown is (2) equivalent to (4). • (4 ⇒ 2). Set Z1 =y1|⋆⟩⟨⋆| +Y1 and Z2 =y2|⋆⟩⟨⋆| +Y2. Obviously, Z1 ∈ Pos(H⋆
[72]

and Z2 ∈ Pos(H⋆ 2). Observe that: A⋆ − (Z1 ⊗I2⋆ −I1⋆ ⊗Z2) = A − (y1|⋆⟩⟨⋆| +Y1) ⊗ (|⋆⟩⟨⋆| +I2) + (|⋆⟩⟨⋆| +I1) ⊗ (y2|⋆⟩⟨⋆| +Y2) = (A − (Y1 ⊗I2 −I1 ⊗Y2)) + (y2 −y1)|⋆⋆ ⟩⟨⋆⋆ | + (y2I1 −Y1) ⊗ |⋆⟩⟨⋆| + |⋆⟩⟨⋆| ⊗ (Y2 −y1I2) ⊒ 0. So, tr(Z1ρ⋆
[73]

• (2 ⇒ 4)

+ǫ, or equivalently, y1(1 − tr(ρ1)) + tr(Y1ρ1) ≤y2(1 − tr(ρ2)) + tr(Y2ρ2) +ǫ. • (2 ⇒ 4). For any Z1 ∈ Pos(H⋆
[74]

Furthermore, observe that tr(Z1ρ⋆

such that A⋆ ⊒ Z1 ⊗I2⋆ −I1⋆ ⊗Z2, by projecting it to P⋆ ⊗P⋆, P ⊥ ⋆ ⊗P⋆, P⋆ ⊗P ⊥ ⋆ and P ⊥ ⋆ ⊗P ⊥ ⋆ , the L¨ owner preserves, and thus: y1 −y2 ≤ 0 y1I2 −Y2 ⊑ 0 Y1 −y2I1 ⊑ 0 Y1 ⊗I2 −I1 ⊗Y2 ⊑A where Z1 = (y1 · · Y1 ) and Z2 = (y2 · · Y2 ) . Furthermore, observe that tr(Z1ρ⋆
[75]

Q UANTUM OPTIMAL TRANSPORT

− tr(Z2ρ⋆ 2) = y1(1 − tr(ρ1)) + tr(Y1ρ1) − (y2(1 − tr(ρ2)) + tr(Y2ρ2)) ≤ ǫ by employing (2), and this completes the proof. APPENDIX C DEFERRED PROOFS IN “Q UANTUM OPTIMAL TRANSPORT ” S ECTION Proposition C.1. Given ρ1 ∈ D (H1) and ρ2 ∈ D (H2) where H1 and H2 are ﬁnite-dimensio...
[77]

F or allρ1 ∈ D 1(H1) and ρ2 ∈ D 1(H2), TCo(E1(ρ1), E2(ρ2)) ≤TCi(ρ1,ρ 2). Proof. (1 ⇒ 2) is trivial. For (2 ⇒ 1), by deﬁnition, it is sufﬁcient to show that, for all ρ1 ∈ D (H1), ρ2 ∈ D (H2) and ρ : ⟨ρ1,ρ 2⟩p, there exists σ : ⟨E1(ρ1), E2(ρ2)⟩p such that : tr(Coσ) ≤ tr(Ciσ). Si...
[78]

On the other hand, 1 + tr(cσ) = 1 −c +c(1 + tr(σ)) ≥ 1 −c +c(tr(E1(ρ′ 1/c)) + tr(E2(ρ′ 2/c))) = 1 −c + (tr(E1(ρ′ 1)) + tr(E2(ρ′ 2)))

⊑ E 1(ρ1) and similarly, tr1(cσ) ⊑ E 2(ρ2). On the other hand, 1 + tr(cσ) = 1 −c +c(1 + tr(σ)) ≥ 1 −c +c(tr(E1(ρ′ 1/c)) + tr(E2(ρ′ 2/c))) = 1 −c + (tr(E1(ρ′ 1)) + tr(E2(ρ′ 2))). Notice that tr(ρ1 −ρ′
[79]

≥ tr(E1(ρ1 −ρ′ 1)) sinceρ′ 1 ⊑ρ1 and E1 is a quantum operation, and similarly holds for ρ2,ρ ′ 2, we get: tr(E1(ρ′ 1)) + tr(E2(ρ′ 2)) ≥ tr(E1(ρ1)) + tr(E2(ρ2)) − (tr(ρ1) + tr(ρ2)) + tr(ρ′
[80]

Lemma C.4 (Monotonicity for Quantum Channels)

+ tr(ρ′ 2) ≥ tr(E1(ρ1)) + tr(E2(ρ2)) − (1 + tr(ρ)) + 2 tr(ρ) = tr( E1(ρ1)) + tr(E2(ρ2)) − 1 +c Combine these two inequalities, we obtain: 1 + tr(cσ) ≥ tr(E1(ρ1)) + tr(E2(ρ2)), which completes the proof. Lemma C.4 (Monotonicity for Quantum Channels) . Suppose E1 ∈ QC (H1), E2 ∈...
[81]

(E1, E2) is monotone w.r .t

Backward. (E1, E2) is monotone w.r .t. (E † 1 ⊗ E † 2 )(C) and C. Here, E † is the dual of E, which satisﬁes tr(AE(B)) = tr(E †(A)B) for all linear operator A,B
[82]

Suppose (E1, E2) is monotone w.r .t

Consequence. Suppose (E1, E2) is monotone w.r .t. C′ i and C′ o, and C′ i ⊑Ci, Co ⊑C′ o, then (E1, E2) is monotone w.r .t. Ci and Co
[83]

Suppose (E1, E ′

Sequential composition. Suppose (E1, E ′
[84]

Ci and Cm, and (E2, E ′

is monotone w.r .t. Ci and Cm, and (E2, E ′
[85]

Cm and Co, then (E2 ◦ E1, E ′ 2 ◦ E ′

is monotone w.r .t. Cm and Co, then (E2 ◦ E1, E ′ 2 ◦ E ′
[86]

F or any super-operatorE, its dual E † is another super-operator

is monotone w.r .t.Ci and Co. F or any super-operatorE, its dual E † is another super-operator . Whenever E is a quantum operation with Kraus operator {Ei}, then E † has Kraus representation {E† i }. ◦ is the composition of two quantum operations, i.e., for all ρ, (E1◦E2)(ρ) ≜...
[87]

(E1, E2) is monotone w.r .t.Ci and Co
[88]

only if” part holds directly by the monotonicity of stab le QOT under data processing [11]. For the “if

for all (Y1,Y 2,n ) ∈ Y , (E1, E2) is monotone w.r .t.Ci +nI and Y1 ⊗I +I ⊗ (nI −Y2), where Y ≜ {(Y1,Y 2,n ) | n ∈ N; 0 ⊑Y1; 0 ⊑Y2 ⊑nI;Co ⊒Y1 ⊗I −I ⊗Y2}. Proof. As E1 and E2 are quantum channels, we employ Lemma C.4 to interpret monot onicity. (1) says that for all ρ ∈ D (H1 ⊗...
[89]

F or allY1,Y 2 ∈ Pos(H ⊗ H2) such that P ⊥ sym[H ⊗ H2] ≥ 2(Y1 ⊗I −I ⊗Y2), it holds that: tr(tr2(Y1)ρ1) ≤ tr(tr2(Y2))ρ2) +ǫ. Proof. By the property of Ts, we ﬁrst observe: Ts(ρ1,ρ 2) = inf τ :⟨ρ1⊗ I 2,ρ2⊗ I 2 ⟩ (P ⊥ sym[H ⊗ H2]τ ), which implies that, (1) is equivalent to (ρ1 ⊗...
[90]

A Q UANTUM RELATIONAL HOARE LOGIC

for all Y1,Y 2 ∈ Pos(H ⊗ H2) such that P ⊥ sym[H ⊗ H2] ≥Y1 ⊗I −I ⊗Y2, it holds that: tr ( Y1 ( ρ1 ⊗ I 2 ) ) ≤ tr ( Y2 ( ρ2 ⊗ I 2 ) ) +ǫ. Notice that, tr(Yi(ρi ⊗ I 2 )) = tr(tr 2(Yi 2 )ρi) for i = 1, 2, direct substitutions of Y ′ i = Yi 2 translate (3) to (2). APPENDIX D DEFER...
[91]

⊨ (Y1, · · ·,Yk,Z 1, · · ·,Zk,n ) ∈ Yk : {nI}S1 ∼ S2 { (∑ iM † iYiMi) ⊗I +I ⊗ [ nI − (∑ iN † iZiNi) ]} where Yk = {(Y1, · · ·,Yk,Z 1, · · ·,Zk,n ) | ∀i, 0 ⊑Yi, 0 ⊑Zi ⊑nI,Yi ⊗I −I ⊗Zi ⊑ 0, ∀j ⁄=i, Yi ⊗I −I ⊗Zj ⊑I}. Proof. (1 ⇒ 2). By Lemma D.3 , for any ρ ∈ D (HS1 ⊗ HS2 ), set ...
[92]

≤ tr(Zσ ′ 2). Now, back to (2) which we aim to prove, for any (Y1, · · ·,Yk,Z 1, · · ·,Zk,n ) ∈ Yk, set Y = ∑ i |i⟩⟨i| ⊗Yi and Z = ∑ i |i⟩⟨i| ⊗Zi, we check that: Y ⊗ (Ik ⊗IS1 ) − (Ik ⊗IS2 ) ⊗Z = (∑ i |i⟩⟨i| ⊗Yi ) ⊗ (∑ j |j⟩⟨j| ⊗IS2 ) − (∑ i |i⟩⟨i| ⊗IS1 ) ⊗ (∑ j |j⟩⟨j| ⊗Zj ) = ...
[93]

≤ tr(Zσ ′ 2), or equivalently, 0 ≥ tr(Yσ ′
[94]

A PPLICATIONS

= tr ((∑ i |i⟩⟨i| ⊗Yi )( ∑ i |i⟩⟨i| ⊗Miσ1M † i )) − tr ((∑ i |i⟩⟨i| ⊗Zi )( ∑ i |i⟩⟨i| ⊗Niσ2N † i )) = ∑ i tr(YiMiσ1M † i ) − ∑ i tr(ZiNiσ2N † i ) = tr ( (∑ iM † iYiMi)σ1 ) − tr ( (∑ iN † iZiNi)σ2 ) . Note that tr(ρ) = tr(σ1) = tr(σ2) and set it as p. Let σ ≜ σ1 ⊗σ2/p, realizin...
[95]

TD(/llbracketS1/rrbracket(ρ1), /llbracketS2/rrbracket(ρ2)) ≤ tr(Φ1ρ1) + tr(Φ2ρ2) for all z ∈Z and ρ1X #ρ2
[96]

3We could also just ask all programs to be interpreted over H = Hall variables, or over H = Hvar(S1)∪ var(S2)

⊨ 0 ⊑P ⊑I : {X | (I +Φ1 ⊗I +I ⊗Φ2)} S1 ∼S2 {P ⊗I +I ⊗ (I −P )}. 3We could also just ask all programs to be interpreted over H = Hall variables, or over H = Hvar(S1)∪ var(S2). Proof. Firstly, (2) is equivalent to saying that for all ρ : ⟨ρ1,ρ 2⟩,P there exists a coupling σ such...
[97]

W (/llbracketS1/rrbracket(tr2(ρ)), /llbracketS2/rrbracket(tr1(ρ))) ≤λ ·W (tr2(ρ), tr1(ρ)) for all ρ ∈ D(HS1 ⊗ HS2)
[98]

⊨ {λ2P ⊥ sym} S1 ∼S2 {P ⊥ sym}. Proof. By deﬁnition, we know that the second condition is equivalen t to: for every ρ ∈ D (HS1 ⊗ HS2), there is a coupling σ : ⟨/llbracketS1/rrbracket(tr2(ρ)), /llbracketS2/rrbracket(tr1(ρ))⟩ such that λ2 tr(ρP ⊥ sym) ≥ tr(σP ⊥ sym). Note that σ...
[99]

S1 is (ε,δ )-differentially private
[100]

HerePi,sym =Psym[H[n]−i] ⊗ (Ii⟨1⟩ ⊗Ii⟨2⟩) for i ∈ [n]

⊨ i ∈ [n], 0 ⊑M ⊑I : {Pi,sym|(exp(ε) +δ)I} S1 ∼S1 {M ⊗I + exp(ε)I ⊗ (I −M )}. HerePi,sym =Psym[H[n]−i] ⊗ (Ii⟨1⟩ ⊗Ii⟨2⟩) for i ∈ [n]. Proof. We ﬁrst notice that, 1) states that ∀M,S and ∀ρ,σ , if ∃i ∈ [n] such that tri(ρ) = tri(σ), then Pr[E(ρ) ∈M S] ≤ exp(ε) · Pr(E(σ) ∈M S) +δ...
[101]

‖/llbracketS1/rrbracket− /llbracketS2/rrbracket‖⋄ ≤ 2c
[102]

ﬁnite” component of A, and XA = ∑ λi=+∞Xi is the “inﬁnite

⊨ 0 ⊑P ⊑IH⊗H : {Psym[H ⊗ H] | (1 +c)I} S1 ∼S2 {P ⊗I +I ⊗ (I −P )}. Proof. This is direct by applying Proposition VIII.3 with X =Psym[H ⊗ H],Φ1 =Φ2 =cI/2, and the deﬁnition of diamond distance for completely positive and trace non-increasing linear maps. APPENDIX G STABILIZED Q...
[2019]

Available: http://dx.doi.org/10.4204/E PTCS.287.2

[Online]. Available: http://dx.doi.org/10.4204/E PTCS.287.2

doi
[2022]

Available: https://hal.science/hal-019 63667

[Online]. Available: https://hal.science/hal-019 63667
[2024]

Available: http://dx.doi.org/10.1145/3 632861

[Online]. Available: http://dx.doi.org/10.1145/3 632861

doi

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [1]

Quantum relational hoare logic,

D. Unruh, “Quantum relational hoare logic,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, p. 1–31, Jan. 2019. [Online]. Available: http://dx.doi.org/10.1145/3290346

doi:10.1145/3290346 2019

[2] [2]

Relational proofs for quantum programs,

G. Barthe, J. Hsu, M. Ying, N. Y u, and L. Zhou, “Relational proofs for quantum programs,” Proc. ACM Program. Lang., vol. 4, no. POPL, Dec. 2019

2019

[3] [3]

Quantum Relational Hoare Logic with E x- pectations,

Y . Li and D. Unruh, “Quantum Relational Hoare Logic with E x- pectations,” in Proceedings of the 48th International Colloquium on Automata, Languages, and Programming, vol. 198, 2021, pp. 136:1– 136:20

2021

[4] [4]

A quantitative probabilistic relational hoare logic,

M. Avanzini, G. Barthe, D. Davoli, and B. Gr´ egoire, “A quantitative probabilistic relational hoare logic,” Proc. ACM Program. Lang., vol. 9, no. POPL, Jan. 2025. [Online]. Available: https://doi.org/10.1145/3704876

doi:10.1145/3704876 2025

[5] [5]

M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010

2010

[6] [6]

The existence of probability measures wit h given marginals,

V . Strassen, “The existence of probability measures wit h given marginals,” The Annals of Mathematical Statistics , pp. 423–439, 1965. [Online]. Available: http://projecteuclid.org/euclid. aoms/1177700153

arXiv 1965

[7] [7]

Strassen’s theorem for quantum couplings,

L. Zhou, S. Ying, N. Y u, and M. Ying, “Strassen’s theorem for quantum couplings,” Theoretical Computer Science, vol. 802, pp. 67–76, 2020. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0304397519305225

2020

[8] [8]

On quantum optimal transport,

S. Cole, M. Eckstein, S. Friedland, and K. ˙Zyczkowski, “On quantum optimal transport,” Mathematical Physics, Analysis and Geometry, vol. 26, no. 2, p. 14, Jun 2023. [Online]. Availabl e: https://doi.org/10.1007/s11040-023-09456-7

doi:10.1007/s11040-023-09456-7 2023