paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Normal-order reduction grammars

正规序归约文法
JFP vol.272017匹配度 2/10 · 论文研究 SK 组合子项的正规序归约文法与生成函数,属于组合子逻辑和形式语言理论,虽与形式化/证明工程有间接联系,但未涉及用户核心关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。引用 6 inbox
MACIEJ BENDKOWSKI
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:提出为给定 n 生成无歧义正则树文法,刻画恰需 n 步正规序归约的 SK 组合子项。

本文研究如何句法刻画在组合逻辑中恰需 n 步正规序归约才能规范化的 SK 组合子项。作者提出一个算法:对给定 n 生成无歧义正则树文法,其语言正是这类项;借助 Curry 与 Feys 的标准化定理,该文法给出所有可规范化 SK 组合子项的完全句法刻画。进一步地,作者由这些文法递归构造普通生成函数,用于计数恰需 n 步正规序归约的 SK 组合子项,并考察所生成文法的规模,给出原始递归上界。

问题
如何为组合逻辑中恰需 n 步正规序归约的 SK 项建立句法刻画,并对其计数及分析生成文法规模。
方法
对给定 n 构造无歧义正则树文法,利用 Curry–Feys 标准化定理保证刻画完全性,并递归构造普通生成函数。
评估
通过理论证明给出可规范化项的完全句法刻画、计数递推方法,以及生成文法大小的原始递归上界。
原文摘要(Abstract)

Abstract We present an algorithm which, for given n , generates an unambiguous regular tree grammar defining the set of combinatory logic terms, over the set {S, K} of primitive combinators, requiring exactly n normal-order reduction steps to normalize. As a consequence of Curry and Feys's standardization theorem, our reduction grammars form a complete syntactic characterization of normalizing combinatory logic terms. Using them, we provide a recursive method of constructing ordinary generating functions counting the number of SK -combinators reducing in n normal-order reduction steps. Finally, we investigate the size of generated grammars giving a primitive recursive upper bound.

链接与引用

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

BibTeX
@article{Bendkowski16,
  title = {Normal-order reduction grammars},
  author = {MACIEJ BENDKOWSKI},
  journal = {Journal of Functional Programming},
  volume = {27},
  year = {2017},
  doi = {10.1017/s0956796816000332}
}