Reasoning about resources used during the execution of programs, such as time, is one of the fundamental questions in computer science. When programming with probabilistic primitives, however, different samples may result in different resource usage, making the cost of a program not a single number but a distribution instead. The expected cost is an important metric used to quantify the efficiency of probabilistic programs. In this work we introduce $\mathbf{cert}$, a call-by-push-value (CBPV) metalanguage extended with primitives for probability, cost and unbounded recursion, and give it denotational semantics for reasoning about the average cost of programs. We justify the validity of the semantics by presenting case-studies ranging from randomized algorithms to stochastic processes and showing how the semantics captures their intended cost.

翻译：关于程序执行过程中资源（如时间）使用的推理是计算机科学中的基本问题之一。然而，在使用概率原语进行编程时，不同的采样可能导致不同的资源消耗，使得程序的成本并非单一数值而是一个分布。期望成本是量化概率程序效率的重要指标。本文引入$\mathbf{cert}$，一种扩展了概率、成本和无界递归原语的按需调用值（CBPV）元语言，并为其赋予指称语义以推理程序的平均成本。通过从随机算法到随机过程的案例研究，我们展示了该语义如何捕捉其预期成本，从而验证了语义的有效性。