一句话：提出定量概率关系霍尔逻辑 eRHL，克服 pRHL/apRHL 的随机对齐限制，并给出可靠性与完备性结果。
现有概率关系霍尔逻辑（如 pRHL、apRHL）受随机对齐限制，难以推理概率程序对的关系期望性质，尤其涉及程序等价、统计距离和差分隐私时。本文提出 eRHL，一种定量的关系程序逻辑，其前后条件取值于扩展非负实数，从而克服随机对齐限制。作者证明 eRHL 对所有几乎必然终止的程序具有非平凡的可靠性与完备性：相对于程序等价、统计距离和差分隐私均可靠且完备；且每个 pRHL 判断有效当且仅当可在 eRHL 中证明。文中还给出超出 pRHL 与 apRHL 能力的实例，展示其实用价值。
We introduce eRHL , a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-conditions take values in the extended non-negative reals. Thanks to its quantitative assertions, eRHL overcomes randomness alignment restrictions from prior logics, including pRHL , a popular relational program logic used to reason about security of cryptographic constructions, and apRHL , a variant of pRHL for differential privacy. As a result, eRHL is the first relational probabilistic program logic to be supported by non-trivial soundness and completeness results for all almost surely terminating programs. We show that eRHL is sound and complete with respect to program equivalence, statistical distance, and differential privacy. We also show that every pRHL judgment is valid iff it is provable in eRHL . We showcase the practical benefits of eRHL with examples that are beyond reach of pRHL and apRHL .
@article{abs-2407-17127,
title = {A Quantitative Probabilistic Relational Hoare Logic},
author = {Martin Avanzini and Gilles Barthe and Davide Davoli and Benjamin Grégoire},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704876}
}