一句话:为λ演算引入概率选择算子,建立按值/按名语义下的合流与标准化理论。
论文研究概率计算在λ演算中的基础语义。作者提出两种扩展Λ⊕cbv与Λ⊕cbn,分别在按值调用和按名调用下加入概率选择算子,用于建模概率程序。为处理概率项的渐近行为,他们重新审视合流性与标准化定理,并将其推广到概率情形。两种演算共享一个基于线性逻辑的更基础演算Λ⊕!,通过它给出统一且模块化的证明方法。结果表明,两类概率λ演算均满足扩展意义下的合流与标准化,从而为概率函数式语言提供语义基础。
We introduce two extensions of the λ -calculus with a probabilistic choice operator, Λ⊕cbvand Λ⊕cbn, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, Λ⊕!, which allows us to develop a unified, modular approach.