期望代价分析的指称语义基础
Denotational Foundations for Expected Cost Analysis
AI总结：
本文提出基于按值传递调用（CBPV）的元语言 cert，定义代价与期望代价两种指称语义，证明其可靠性、充分性及效应模拟性质，并通过案例展示其表达能力。
摘要：
关于程序执行代价的推理是计算机科学中的基本问题之一。然而，在带概率的程序设计语境中，代价的概念不再是确定性的，因为它取决于程序执行过程中所做的概率采样。这种交互又因代价、递归和求值策略之间非平凡的相互作用而进一步复杂化。在本工作中，我们引入了 $\mathbf{cert}$：一种用于推理概率代价的按值传递调用（CBPV）元语言。我们为 $\mathbf{cert}$ 配备了操作代价语义，并定义了两种指称语义——一种代价语义和一种期望代价语义。我们证明了操作可靠性和充分性对于指称代价语义，以及一个代价充分性定理对于期望代价语义。我们通过陈述并证明 CBPV 的一个新颖的效应模拟性质，正式地关联了这两种指称语义。我们还基于单子概率语义的最新进展，证明了期望代价语义作为期望代价和概率的最小语义的规范性性质。最后，我们通过展示从随机算法到随机过程的一系列案例研究，说明了 $\mathbf{cert}$ 和期望代价语义的表达能力，并展示了我们的语义如何捕获它们预期的期望代价。
英文摘要：
Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the probabilistic samples made throughout the execution of the program. This interaction is further complicated by the non-trivial interaction between cost, recursion and evaluation strategy. In this work we introduce $\mathbf{cert}$: a Call-By-Push-Value (CBPV) metalanguage for reasoning about probabilistic cost. We equip $\mathbf{cert}$ with an operational cost semantics and define two denotational semantics -- a cost semantics and an expected-cost semantics. We prove operational soundness and adequacy for the denotational cost semantics and a cost adequacy theorem for the expected-cost semantics. We formally relate both denotational semantics by stating and proving a novel \emph{effect simulation} property for CBPV. We also prove a canonicity property of the expected-cost semantics as the minimal semantics for expected cost and probability by building on recent advances on monadic probabilistic semantics. Finally, we illustrate the expressivity of $\mathbf{cert}$ and the expected-cost semantics by presenting case-studies ranging from randomized algorithms to stochastic processes and show how our semantics capture their intended expected cost.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
