论文标题
概率逐个呼叫的lambda-calculus-扩展版本
A Probabilistic Call-by-Need Lambda-Calculus -- Extended Version
论文作者
论文摘要
为了支持对声明性概率编程语言的理解，我们引入了一种具有公平的二进制概率选择的lambda-calculus，以同样的概率选择其参数之间。微积分的减少策略是一种逐渐呼叫的策略，该策略执行懒惰的评估并通过递归释放表达进行共享。表达式的预期收敛是所有成功减少输出的总和，其概率加权。我们将上下文等价用作程序语义：两个表达式在上下文上是等效的，并且仅当插入任何程序上下文中的表达式的预期收敛始终是相同的。我们开发并说明了证明等效性的技术，包括上下文引理，两个派生标准显示等效性和基于句法图的方法。最终，这使我们能够相对于上下文等价表明一系列程序转换的正确性。
To support the understanding of declarative probabilistic programming languages, we introduce a lambda-calculus with a fair binary probabilistic choice that chooses between its arguments with equal probability. The reduction strategy of the calculus is a call-by-need strategy that performs lazy evaluation and implements sharing by recursive let-expressions. Expected convergence of expressions is the limit of the sum of all successful reduction outputs weighted by their probability. We use contextual equivalence as program semantics: two expressions are contextually equivalent if and only if the expected convergence of the expressions plugged into any program context is always the same. We develop and illustrate techniques to prove equivalences including a context lemma, two derived criteria to show equivalences and a syntactic diagram-based method. This finally enables us to show correctness of a large set of program transformations with respect to the contextual equivalence.
