paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A new coinductive confluence proof for infinitary lambda calculus

无穷 lambda 演算中一种新的余归纳合流性证明
LMCS vol.Volume 16, Issue 12020匹配度 2/10 · 该论文属于纯 PL 形式语义与 Coq 定理证明，研究无穷 lambda 演算中 Böhm 归约的合流性，与用户关注的 LLM/Agent 静态分析、LLM 辅助形式化验证、浮点程序分析或贝叶斯程序分析均无直接关系；仅因涉及形式化验证而与研究方向有极弱关联。引用 13 inbox
Łukasz Czajka
形式语义定理证明与证明工程
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：提出无穷 lambda 演算中 Böhm 归约合流性与规范化的新余归纳证明，并在 Coq 中形式化。

本文研究无穷 lambda 演算中 Böhm 归约的合流性与规范化问题。此前该结果的证明较为复杂，作者提出一种新的余归纳证明技术；该技术并非对既有证明的余归纳改写，而是具有独立思路。作者在 Coq 证明助手中将合流性与规范化的证明完整机器化验证。结果表明，该证明比先前证明更简洁，同时展示了余归纳方法在无穷 lambda 演算元理论形式化中的有效性。

问题
围绕无穷 lambda 演算中 Böhm 归约，需要证明其合流性与规范化，并简化已有复杂证明。
方法
采用新的余归纳证明技术，并非对旧证明的余归纳改写，并在 Coq 证明助手中形式化。
评估
通过 Coq 机器化验证整个证明，且与已有证明相比更为简洁。
原文摘要（Abstract）

We present a new and formal coinductive proof of confluence and normalisation of B\"ohm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this result. The technique of the proof is new, i.e., it is not merely a coinductive reformulation of any earlier proofs. We formalised the proof in the Coq proof assistant.Comment: arXiv admin note: text overlap with arXiv:1501.04354

链接与引用

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

BibTeX 
@article{abs-1808-05481,
  title = {A new coinductive confluence proof for infinitary lambda calculus},
  author = {Łukasz Czajka},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 1},
  year = {2020},
  doi = {10.23638/lmcs-16(1:31)2020}
}