一句话：提出基于最优传输对偶的完备定量量子关系霍尔逻辑，并可嵌入投影断言逻辑。
本文为量子程序提出一种定量关系霍尔逻辑。其断言基于正半定算子的一种新的无穷扩展，可表达量子程序之间的定量关系。作者证明该逻辑是可靠的，并且对于有界后置条件与几乎必然终止的程序是完备的；完备性证明依托最优传输对偶定理的量子版本。此外，论文还定义了一个从带投影断言的量子关系霍尔逻辑到该逻辑的完备嵌入，表明新逻辑能统一并推广已有关系推理。工作以理论证明为主，未报告实现或实验评估。
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.
DOI 原文 ·
@inproceedings{paperbot8637,
title = {Complete Quantum Relational Hoare Logics from Optimal Transport Duality},
author = {Gilles Barthe and Minbo Gao and Theo Wang and Li Zhou},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00072}
}