Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Complete Quantum Relational Hoare Logics from Optimal Transport Duality

Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou

TL;DR

The paper develops a sound and complete relational Hoare logic for quantum programs in the $\mathsf{qWhile}$ language, achieving completeness for AST programs with bounded postconditions via a duality theorem from quantum optimal transport. It introduces infinite-valued predicates to unify projective and PSD assertions and provides a complete semantic embedding of projector-based logics into the proposed framework. This yields principled, complete reasoning for program equivalence, trace/distance measures, Wasserstein distance, non-interference, and quantum differential privacy, with a dual applicability to probabilistic logics through Kantorovich–Rubinstein duality. The framework thereby advances rigorous, scalable reasoning about relational properties of quantum programs and has implications for quantum security, privacy, and correctness verification in quantum computing.

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.

Complete Quantum Relational Hoare Logics from Optimal Transport Duality

TL;DR

The paper develops a sound and complete relational Hoare logic for quantum programs in the language, achieving completeness for AST programs with bounded postconditions via a duality theorem from quantum optimal transport. It introduces infinite-valued predicates to unify projective and PSD assertions and provides a complete semantic embedding of projector-based logics into the proposed framework. This yields principled, complete reasoning for program equivalence, trace/distance measures, Wasserstein distance, non-interference, and quantum differential privacy, with a dual applicability to probabilistic logics through Kantorovich–Rubinstein duality. The framework thereby advances rigorous, scalable reasoning about relational properties of quantum programs and has implications for quantum security, privacy, and correctness verification in quantum computing.

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.
Paper Structure (44 sections, 78 theorems, 184 equations, 2 figures)

This paper contains 44 sections, 78 theorems, 184 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Notation and Preliminaries
  3. Quantum states and maps
  4. Quantum predicates
  5. Infinite-valued predicates
  6. Quantum Couplings
  7. Basic Definitions and Duality Theorems
  8. Partial Couplings
  9. Quantum Optimal Transport
  10. Basic Definitions
  11. QOT under Data Processing
  12. Characterizing Equivalence
  13. Quantum Programs
  14. Syntax
  15. Semantics
  16. ...and 29 more sections

Key Result

Theorem 3.3

For any $\rho_1 \in \mathcal{D}(\mathcal{H}_1)$ and $\rho_2 \in \mathcal{D}(\mathcal{H}_2)$ with $\mathop{\mathrm{tr}}\nolimits(\rho_1) = \mathop{\mathrm{tr}}\nolimits(\rho_2)$, for any defect $\epsilon \in \mathbb{R}^{+\infty}$ and for any $X \in \mathsf{Pos}(\mathcal{H}_1 \otimes \mathcal{H}_2)$,

Figures (2)

  • Figure 1: Rules for $\mathsf{qOTL}$
  • Figure 2: Extra two-side rules for $\mathsf{qOTL}$.

Theorems & Definitions (145)

  • Definition 3.1: Quantum Coupling
  • Definition 3.2: Quantum Lifting with Defects
  • Theorem 3.3: Quantum Strassen's Theorem with Defects
  • Lemma 3.4: Trace Equivalence
  • Definition 3.5: Partial Coupling
  • Definition 4.1: Partial Quantum Optimal Transport (c.f. QuantumOptimalTransport_Cole_2023)
  • Definition 4.2
  • Proposition 4.3
  • Theorem 4.4: Duality under Data Processing
  • Proposition 4.5
  • ...and 135 more