A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics

• URL: http://arxiv.org/abs/2510.07051v1
• Date: Wed, 08 Oct 2025 14:19:03 GMT
• Title: A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
• Authors: Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Li Zhou,
• Abstract summary: We use duality theorems for countable probability distributions and finite-dimensional quantum states to build relational program logics for classical-quantum programs.<n>We establish soundness and completeness of a new relational program logic, called $mathsfcqOTL$, for classical-quantum programs.
• Score: 6.445494669467905
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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).

Related papers

• Quantum automated theorem proving [15.134110328567838]
  We propose a generic framework for quantum automated theorem proving.<n>We introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks.<n>We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic.
  arXiv  Detail & Related papers  (2026-01-12T19:39:33Z)
• Constraint-oriented biased quantum search for general constrained combinatorial optimization problems [0.0]
  We present a quantum algorithmic routine that tackles efficiently optimization problems with arbitrary computable objective and constraint functions.<n>Building on previously developed quantum methods, we generalize the approach to encompass a broader class of problems in discrete domains.
  arXiv  Detail & Related papers  (2025-12-09T09:11:54Z)
• Entanglement and Minimal Hilbert Space in the Classical Dual States of Quantum Theory [0.0]
  We investigate Quantum Entanglement with the new approach APL Quantum 2, 016104 (2025) on dual Classicalization.<n>Some of the results of this paper involves the computation and analysis of the entanglement for different types of coherent (coset and non coset) states and topologies.
  arXiv  Detail & Related papers  (2025-11-28T13:17:15Z)
• A Practical Quantum Hoare Logic with Classical Variables, I [5.341843260877702]
  We present a Hoare-style logic for reasoning about quantum programs with classical variables.<n>Our approach offers several improvements over previous work.<n>It applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates.
  arXiv  Detail & Related papers  (2024-12-13T05:28:19Z)
• Semidefinite programming relaxations for quantum correlations [42.72938925647165]
  We discuss how the core idea of semidefinite relaxations can be adapted for a variety of research topics in quantum correlations.<n>These topics include nonlocality, quantum communication, quantum networks, entanglement, and quantum cryptography.
  arXiv  Detail & Related papers  (2023-07-05T18:00:07Z)
• Guidable Local Hamiltonian Problems with Implications to Heuristic Ansätze State Preparation and the Quantum PCP Conjecture [0.0]
  We study 'Merlinized' versions of the recently defined Guided Local Hamiltonian problem. These problems do not have a guiding state provided as a part of the input, but merely come with the promise that one exists. We show that guidable local Hamiltonian problems for both classes of guiding states are $mathsfQCMA$-complete in the inverse-polynomial precision setting.
  arXiv  Detail & Related papers  (2023-02-22T19:00:00Z)
• Stochastic approximate state conversion for entanglement and general quantum resource theories [41.94295877935867]
  An important problem in any quantum resource theory is to determine how quantum states can be converted into each other. Very few results have been presented on the intermediate regime between probabilistic and approximate transformations. We show that these bounds imply an upper bound on the rates for various classes of states under probabilistic transformations. We also show that the deterministic version of the single copy bounds can be applied for drawing limitations on the manipulation of quantum channels.
  arXiv  Detail & Related papers  (2021-11-24T17:29:43Z)
• Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
  We introduce a high-fidelity gate set inspired by a proposal for near-term quantum advantage in optimization problems. By orchestrating coherent, multi-level control over three transmon qutrits, we synthesize a family of deterministic, continuous-angle quantum phase gates acting in the natural three-qubit computational basis.
  arXiv  Detail & Related papers  (2021-08-03T17:49:09Z)
• Error mitigation and quantum-assisted simulation in the error corrected regime [77.34726150561087]
  A standard approach to quantum computing is based on the idea of promoting a classically simulable and fault-tolerant set of operations. We show how the addition of noisy magic resources allows one to boost classical quasiprobability simulations of a quantum circuit.
  arXiv  Detail & Related papers  (2021-03-12T20:58:41Z)
• Towards a Probabilistic Foundation of Relativistic Quantum Theory: The One-Body Born Rule in Curved Spacetime [0.0]
  This work is based on generalizing the quantum-mechanical Born rule for determining particle position probabilities to curved spacetime. A principal motivator for this research has been to overcome internal mathematical problems of quantum field theory. The main contribution of this work to the mathematical physics literature is the development of the Lagrangian picture.
  arXiv  Detail & Related papers  (2020-12-09T18:22:18Z)
• Emergence of classical behavior in the early universe [68.8204255655161]
  Three notions are often assumed to be essentially equivalent, representing different facets of the same phenomenon. We analyze them in general Friedmann-Lemaitre- Robertson-Walker space-times through the lens of geometric structures on the classical phase space. The analysis shows that: (i) inflation does not play an essential role; classical behavior can emerge much more generally; (ii) the three notions are conceptually distinct; classicality can emerge in one sense but not in another.
  arXiv  Detail & Related papers  (2020-04-22T16:38:25Z)
• From a quantum theory to a classical one [117.44028458220427]
  We present and discuss a formal approach for describing the quantum to classical crossover. The method was originally introduced by L. Yaffe in 1982 for tackling large-$N$ quantum field theories.
  arXiv  Detail & Related papers  (2020-04-01T09:16:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.