一句话：为带概率选择、递归与成本计量的λ演算定义CPS变换，使表达式应用于续延λv.0即得期望成本，并给出可靠的高阶逻辑EHOL推导紧界。
本文针对带概率选择、无界递归和tick计费算子的类型化λ演算，研究其期望成本分析问题。作者定义了一种续延传递风格（CPS）变换，将源语言翻译到非概率的λ演算，目标语言包含扩展正实数类型与不动点算子。核心结果是：将表达式M的CPS变换应用于续延λv.0，所得结果恰为M的期望成本。作者进一步提出高阶逻辑形式系统EHOL，证明其可靠性，并用它推导Coupon Collector、Random Walk等经典例子期望成本的紧上界。此外，论文将所提变换与Kaminski等人的ert-calculus建立联系，表明后者可通过对经典命令式程序到λ演算嵌入的推广应用CPS变换而恢复。最后，作者证明该CPS变换还可用于计算pre-expectation以及推理几乎必然终止。
We define a continuation-passing style (CPS) translation for a typed λ-calculus with probabilistic choice, unbounded recursion, and a tick operator — for modeling cost. The target language is a (non-probabilistic) λ-calculus, enriched with a type of extended positive reals and a fixpoint operator. We then show that applying the CPS transform of an expression M to the continuation λ v . 0 yields the expected cost of M . We also introduce a formal system for higher-order logic, called EHOL, prove it sound, and show it can derive tight upper bounds on the expected cost of classic examples, including Coupon Collector and Random Walk. Moreover, we relate our translation to Kaminski et al.’s ert-calculus, showing that the latter can be recovered by applying our CPS translation to (a generalization of) the classic embedding of imperative programs into λ-calculus. Finally, we prove that the CPS transform of an expression can also be used to compute pre-expectations and to reason about almost sure termination.
@article{paperbot1120,
title = {On continuation-passing transformations and expected cost analysis},
author = {Martin Avanzini and Gilles Barthe and Ugo Dal Lago},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473592}
}