paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the Growth Rates of Polyregular Functions

论 Polyregular 函数的增长率
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 1/10 · 该论文属于纯逻辑与自动机理论,研究 polyregular 函数的输出增长率及其 MSO 解释、pebble transducer 刻画,不涉及程序分析、静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 11 inbox
Mikołaj Bojańczyk
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:polyregular 函数输出规模 O(n^k) 当且仅当可由 k 维 MSO 解释定义,且 pebble transducer 无此刻画。

本文研究 polyregular 函数,即输出长度为输入长度多项式级的字符串到字符串函数。作者证明,一个 polyregular 函数的输出规模为 O(n^k),当且仅当它可由 k 维 MSO 解释定义:输出每个位置由一元二阶逻辑在输入位置的 k 元组上解释得到。该结果给出输出增长率的逻辑刻画。作者进一步证明该刻画不能推广到 pebble transducer:对每个 k,都存在输出规模为二次的 polyregular 函数,其计算至少需要 k 个 pebble,从而分离了两类模型的表达与资源需求。

问题
如何刻画 polyregular 函数输出规模的多项式增长率,尤其是 O(n^k) 增长与 k 维 MSO 解释之间的关系,并检验该关系是否适用于 pebble transducer。
方法
建立 polyregular 函数与 MSO 解释之间的等价刻画,并构造需要任意多 pebble 的二次输出函数作为反例。
评估
通过理论证明给出 O(n^k) 与 k 维 MSO 解释的当且仅当定理,并用反例族说明 pebble transducer 无法沿用该刻画。
原文摘要(Abstract)

We consider polyregular functions, which are certain string-to-string functions that have polynomial output size. We prove that a polyregular function has output size ${\mathcal{O}}({n^k})$ if and only if it can be defined by an MSO interpretation of dimension k, i.e. a string-to-string transformation where every output position is interpreted, using monadic second-order logic MSO, in some k-tuple of input positions. We also show that this characterization does not extend to pebble transducers, another model for describing polyregular functions: we show that for every {k ∈ 1, 2, …} there is a polyregular function of quadratic output size which needs at least k pebbles to be computed.

链接与引用

DOI 原文 · arXiv · DBLP

BibTeX
@inproceedings{Bojanczyk23a,
  title = {On the Growth Rates of Polyregular Functions},
  author = {Mikołaj Bojańczyk},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175808}
}