paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On properties of $B$-terms

论 B-项的性质
LMCS vol.Volume 16, Issue 22020匹配度 2/10 · 该论文研究 B 组合子项的循环性质与等式公理化，属于纯组合子逻辑/形式语义理论，与用户关注的 PL 与 AI/LLM/Agent 交叉、浮点程序分析、贝叶斯程序分析等核心方向基本无关。虽然涉及形式化与定理证明，但未触及静态分析、机器学习系统或 LLM 工具链。引用 3 inbox
Mirai Ikebuchi, Keisuke Nakano
定理证明与证明工程形式语义
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：研究仅由 B 组合子构成的 B-项在重复右应用下是否循环，给出等式公理化与检测循环的规范表示算法。

本文研究仅由 B 组合子（B ≡ λfgx. f(g x)）构成的 B-项的一个性质：对 B-项重复进行右应用时是否会出现循环。作者通过可靠且完备的等式公理化来刻画 B-项具有或不具有该循环性质的条件。文中给出了具有循环性质的 B-项实例，并证明不具有该性质的 B-项有无穷多个。此外，文章还引入 B-项规范表示的一个新性质，该表示可用于检测循环，或等价地证明循环性质，并给出有效算法。本文为 LMCS 期刊版本。

问题
B-项在重复右应用下是否循环，以及如何判定或证明这一性质。
方法
利用可靠且完备的等式公理化刻画循环性质，并引入 B-项的规范表示与检测算法。
评估
通过构造具有循环性质的实例、证明无穷多个 B-项不具有循环性质，并给出检测循环的有效算法进行理论验证。
原文摘要（Abstract）

$B$-terms are built from the $B$ combinator alone defined by $B\equiv\lambda fgx. f(g~x)$, which is well known as a function composition operator. This paper investigates an interesting property of $B$-terms, that is, whether repetitive right applications of a $B$-term cycles or not. We discuss conditions for $B$-terms to have and not to have the property through a sound and complete equational axiomatization. Specifically, we give examples of $B$-terms which have the cyclic property and show that there are infinitely many $B$-terms which do not have the property. Also, we introduce another interesting property about a canonical representation of $B$-terms that is useful to detect cycles, or equivalently, to prove the cyclic property, with an efficient algorithm.Comment: Journal version in Logical Methods in Computer Science. arXiv admin note: substantial text overlap with arXiv:1703.10938

链接与引用

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

BibTeX 
@article{abs-1901-11010,
  title = {On properties of $B$-terms},
  author = {Mirai Ikebuchi and Keisuke Nakano},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 2},
  year = {2020},
  doi = {10.23638/lmcs-16(2:8)2020}
}