一句话：提出 Tachis，一种带概率代价信用（cost credits）的高阶分离逻辑，用于证明概率程序的期望代价上界。
本文提出 Tachis，一种用于推理概率程序期望代价的高阶分离逻辑。受确定性程序时间信用（time credits）的启发，作者引入概率代价信用：一种分离逻辑资源，可支付操作代价，并可按采样分支的权重分配到所有可能分支，从而支持期望代价推理。将代价信用表示为分离逻辑资源赋予 Tachis 极大灵活性与表达力，例如可将多余信用作为势（potential）存入数据结构以支持摊还期望代价分析。该逻辑支持多种代价模型，包括运行时间与熵消耗。作者将 Tachis 应用于证明随机快速排序、哈希表与可合并堆等多种概率算法和数据结构的期望代价上界，所有结果均在 Coq、Iris 与 Coquelicot 实数分析库中机器化验证。
We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probabilistic cost credit. Probabilistic cost credits are a separation logic resource that can be used to pay for the cost of operations in programs, and that can be distributed across all possible branches of sampling instructions according to their weight, thus enabling us to reason about expected cost. The representation of cost credits as separation logic resources gives Tachis a great deal of flexibility and expressivity. In particular, it permits reasoning about amortized expected cost by storing excess credits as potential into data structures to pay for future operations. Tachis further supports a range of cost models, including running time and entropy usage. We showcase the versatility of this approach by applying our techniques to prove upper bounds on the expected cost of a variety of probabilistic algorithms and data structures, including randomized quicksort, hash tables, and meldable heaps. All of our results have been mechanized using Coq, Iris, and the Coquelicot real analysis library.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{HaselwarterLMG024,
title = {Tachis: Higher-Order Separation Logic with Credits for Expected Costs},
author = {Philipp G. Haselwarter and Kwing Hei Li and Markus de Medeiros and Simon Oddershede Gregersen and Alejandro Aguirre and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689753}
}