paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Fixed point combinators as fixed points of higher-order fixed point generators

不动点组合子作为高阶不动点生成器的不动点
LMCS vol.Volume 16, Issue 32020匹配度 2/10 · 论文属于纯 lambda 演算/组合子逻辑的形式语义研究,讨论不动点组合子生成器的结构与猜想,与用户关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接关联;仅可视为 PL 理论基础,且缺乏工程实现与工业落地。引用 2 inbox
Andrew Polonsky
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:研究弱不动点组合子生成器的结构,给出其不动点存在的充分条件并提出弱常性必要性猜想。

Böhm 发现,若 Y 是不动点组合子(fpc),则 Y(λyx.x(yx)) 仍是 fpc,这给出首个 fpc 生成方案。本文研究(弱)fpc 生成器的结构:称项序列 G1,...,Gn 为生成器,若 Y∈FPC 蕴含 Y G1...Gn∈FPC。作者通过单射性、弱常性等性质分离出若干稳健生成器类,并给出生成器存在不动点(存在 fpc Y 使 Y=Y G1...Gn)的充分条件。文章猜想弱常性是此类高阶不动点存在的必要条件,推广了 Statman 关于不存在“双 fpc”(Böhm 生成器 (λyx.x(yx)) 的不动点)的猜想。最后定义(弱)fpc 生成器的幺半群并提出结构猜想。

问题
研究(弱)不动点组合子生成器的结构,包括其分类、高阶不动点的存在条件,以及该问题与 Statman 双 fpc 猜想的关系。
方法
在无类型 lambda 演算/组合子逻辑中分析项序列,利用单射性、弱常性等初等性质分离生成器类,并给出不动点存在的充分条件;同时考察生成器构成的幺半群。
评估
以理论定义、充分条件证明、猜想提出和代数结构观察进行评估,未涉及实现或实验。
原文摘要(Abstract)

Corrado B\"ohm once observed that if $Y$ is any fixed point combinator (fpc), then $Y(\lambda yx.x(yx))$ is again fpc. He thus discovered the first "fpc generating scheme" -- a generic way to build new fpcs from old. Continuing this idea, define an $\textit{fpc generator}$ to be any sequence of terms $G_1,\dots,G_n$ such that \[ Y \in FPC \Rightarrow Y G_1 \cdots G_n \in FPC \] In this contribution, we take first steps in studying the structure of (weak) fpc generators. We isolate several robust classes of such generators, by examining their elementary properties like injectivity and (weak) constancy. We provide sufficient conditions for existence of fixed points of a given generator $(G_1,\cdots,G_n)$: an fpc $Y$ such that $Y = Y G_1 \cdots G_n$. We conjecture that weak constancy is a necessary condition for existence of such (higher-order) fixed points. This statement generalizes Statman's conjecture on non-existence of "double fpcs": fixed points of the generator $(G) = (\lambda yx.x(yx))$ discovered by B\"ohm. Finally, we define and make a few observations about the monoid of (weak) fpc generators. This enables us to formulate new a conjecture about their structure.

链接与引用

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

BibTeX
@article{Polonsky20,
  title = {Fixed point combinators as fixed points of higher-order fixed point generators},
  author = {Andrew Polonsky},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:7)2020}
}