paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Taylor subsumes Scott, Berry, Kahn and Plotkin

Taylor 涵摄 Scott、Berry、Kahn 与 Plotkin
POPL 4(POPL)2019匹配度 2/10 · 该论文属于纯 λ 演算与形式语义理论研究,讨论 Taylor 展开、资源敏感语义及经典连续性/顺序性结果的统一证明;虽与 PL 理论相关,但未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 15 inbox
Davide Barbarossa, Giulio Manzonetto
crossref: 2026-09-10

AI 速览

一句话:用 Taylor 展开的资源敏感理论,统一并简化 λ 演算中原本依赖 Scott、Berry 与 Kahn–Plotkin 理论的重要证明。

论文主张用基于 Taylor 展开与微分 λ 演算的资源消耗理论,取代以语法连续性为基础的传统程序近似理论。作者展示该资源敏感框架能证明 λ 演算中若干通常依赖 Scott 连续性、Berry 稳定性或 Kahn–Plotkin 顺序性的重要结果。方法依赖资源近似项的三个性质:强规范化、合流性与线性性,使证明常可简化为归纳。代表性案例是 Böhm 树语义的 Perpendicular Lines Lemma(垂直线引理),其证明因此变得直接。该工作表明 Taylor 展开在理论层面涵摄上述几类语义框架。

问题
传统 λ 演算中的程序近似与语义结果常依赖 Scott 连续性、Berry 稳定性或 Kahn–Plotkin 顺序性;能否用基于 Taylor 展开的资源消耗理论统一证明这些结果?
方法
采用微分 λ 演算启发的 Taylor 展开与资源近似项,利用其强规范化、合流性和线性性,以归纳等简单方式重构重要定理的证明。
评估
以 Böhm 树语义的 Perpendicular Lines Lemma 为范例,用资源近似项的性质给出简化证明,并论证 Taylor 展开可涵摄 Scott、Berry、Kahn 与 Plotkin 的框架。
原文摘要(Abstract)

The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.

链接与引用

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

BibTeX
@article{paperbot536,
  title = {Taylor subsumes Scott, Berry, Kahn and Plotkin},
  author = {Davide Barbarossa and Giulio Manzonetto},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3371069}
}