paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Benefit of Being Non-Lazy in Probabilistic λ-calculus

概率 λ 演算中非惰性的优势
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10 · 论文研究概率 λ 演算中非惰性归约对概率应用双模拟与上下文等价的影响，属于形式语义/概率编程理论基础；与用户关注的静态分析、LLM/Agent、浮点程序分析以及贝叶斯程序分析与 LLM 的交叉均无直接关联，仅有概率编程语义上的微弱联系。引用 1 inbox
Gianluca Curzi, Michele Pagani
形式语义量子与概率编程
crossref: 2026-09-12

AI 速览

一句话：研究概率 λ 演算中非惰性归约对概率应用双模拟与上下文等价关系的影响。

本文研究概率无类型 λ 演算中的概率应用双模拟（PAB），这是一种按特定操作语义比较概率项应用行为的共归纳关系。已有工作分别在 call-by-value（cbv）与 call-by-name（cbn）下，采用不在函数体内归约的惰性策略研究 PAB，并证明它在 cbv 下对上下文等价完全抽象，但在惰性 cbn 下不成立。本文由此考察非惰性归约策略，分析在函数体内继续归约如何影响 PAB 与上下文等价的匹配，以及为何非惰性可能为 cbn 情形带来优势。摘要未给出具体实验评估，工作属于语义与共归纳关系的理论分析。

问题
在概率无类型 λ 演算中，PAB 在 cbv 下对上下文等价完全抽象，但在惰性 cbn 下不成立，说明惰性归约策略限制了该共归纳等价的适用性。
方法
基于操作语义与共归纳定义的概率应用双模拟，比较 cbv/cbn 以及惰性与非惰性归约策略下的项行为，并分析其与上下文等价的关系。
评估
以理论证明与性质分析为主，围绕 PAB 对上下文等价是否完全抽象进行论证；摘要未提及实现或实验。
原文摘要（Abstract）

We consider the probabilistic applicative bisimilarity (PAB) --- a coinductive relation comparing the applicative behaviour of probabilistic untyped λ-terms according to a specific operational semantics. This notion has been studied by Dal Lago et al. with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body of a function. In particular, PAB has been proven to be fully abstract with respect to the contextual equivalence in cbv [6] but not in lazy cbn [16].

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot5541,
  title = {The Benefit of Being Non-Lazy in Probabilistic λ-calculus},
  author = {Gianluca Curzi and Michele Pagani},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394806}
}