paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Lambda Calculus and Probabilistic Computation

λ演算与概率计算
LICS 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2019匹配度 4/10 · 论文研究概率λ演算的合流与标准化,属于概率计算的形式语义基础,与贝叶斯程序分析/概率编程有间接理论关联;但未涉及静态分析、LLM、浮点程序分析或工业落地,与用户当前核心方向匹配有限。引用 2 inbox
Claudia Faggian, Simona Ronchi della Rocca
crossref: 2026-09-12

AI 速览

一句话:为λ演算引入概率选择算子,建立按值/按名语义下的合流与标准化理论。

论文研究概率计算在λ演算中的基础语义。作者提出两种扩展Λ⊕cbv与Λ⊕cbn,分别在按值调用和按名调用下加入概率选择算子,用于建模概率程序。为处理概率项的渐近行为,他们重新审视合流性与标准化定理,并将其推广到概率情形。两种演算共享一个基于线性逻辑的更基础演算Λ⊕!,通过它给出统一且模块化的证明方法。结果表明,两类概率λ演算均满足扩展意义下的合流与标准化,从而为概率函数式语言提供语义基础。

问题
如何在λ演算中统一建模按值调用与按名调用的概率计算,并保持合流性、标准化等基本性质?
方法
定义带概率选择算子的Λ⊕cbv与Λ⊕cbn,并借助基于线性逻辑的Λ⊕!给出统一、模块化的分析框架。
评估
通过理论证明表明,两个演算在考虑项渐近行为的扩展定义下均满足合流性与标准化。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot4968,
  title = {Lambda Calculus and Probabilistic Computation},
  author = {Claudia Faggian and Simona Ronchi della Rocca},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785699}
}