paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Many more predecessors: A representation workout

更多前驱函数:一次表示法训练
JFP vol.302020匹配度 2/10 · 该论文属于 lambda 演算与函数式编程中丘奇数/前驱表示的理论推导,与用户关注的静态分析、Agentic 程序、LLM 与程序分析交叉、浮点程序分析及贝叶斯程序分析均无直接关联。引用 1 inbox
OLEG KISELYOV
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:从丘奇数与Kleene表示出发,系统推导出更小、更快、更精确的前驱函数表示。

λ演算自始以迭代应用表示自然数:后继增加一次应用,前驱则需“撤销”应用,这长期被视为困难,连Church也认为不可能。Kleene曾以迂回视角找到一种相关表示,使前驱更易定义。本文用现代视角重审这一经典问题,梳理系统化推导方法,从丘奇数及其变体生成更多前驱函数表示,并比较其大小、速度与精确性,同时保持正确性与基本性质。结果是一组可系统推导、简洁性与性能各异的前驱实现,揭示了表示选择对λ演算数值编码的影响。

问题
如何在λ演算中为自然数表示定义前驱函数;后继只是增加一次应用,前驱却需要撤销应用,因而被认为难以实现。
方法
以现代视角重新审视丘奇数与Kleene的相关表示,系统化地推导多种前驱函数表示。
评估
通过推导和比较这些表示在大小、速度和精确性上的表现,并保持其正确性与基本性质来评估。
原文摘要(Abstract)

Abstract From the outset, lambda calculus represented natural numbers through iterated application. The successor hence adds one more application, and the predecessor removes. In effect, the predecessor un-applies a term—which seemed impossible, even to Church. It took Kleene a rather oblique glance to sight a related representation of numbers, with an easier predecessor. Let us see what we can do if we look at this old problem with today’s eyes. We discern the systematic ways to derive more predecessors—smaller, faster, and sharper—while keeping all teeth.

链接与引用

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

BibTeX
@article{Kiselyov20,
  title = {Many more predecessors: A representation workout},
  author = {OLEG KISELYOV},
  journal = {Journal of Functional Programming},
  volume = {30},
  year = {2020},
  doi = {10.1017/s095679682000009x}
}