paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Pebble Minimization of Polyregular Functions

多正则（polyregular）函数的 Pebble 最小化
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 1/10 · 该论文属于纯自动机与形式语言理论（多正则函数、Pebble 转换器的表达能力刻画），与用户关注的静态分析、浮点/贝叶斯程序分析以及 LLM/Agent 交叉方向无实质关联；虽同属 PL 的形式化理论基础，但不涉及程序分析、验证或工具落地。引用 7 inbox
Nathan Lhote
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：证明多正则函数正则当且仅当输出至多线性增长，并以输出多项式次数精确刻画所需 Pebble 数。

该论文研究多正则（polyregular）字到字函数的正则性判定与 Pebble 换能器所需 Pebble 数量的最小化问题。核心结果是：一个多正则函数是正则的，当且仅当其输出大小相对于输入大小至多线性增长。作者进一步建立 Pebble 数量与输出增长次数的精确对应：一个多正则函数可由两枚 Pebble 的换能器实现，当且仅当其输出大小相对于输入为二次；可由三枚 Pebble 实现，当且仅当输出为三次；依此类推。由此，Pebble 换能器的 Pebble 数量这一计算资源被输出多项式增长阶完全刻画，给出了多正则函数层次的一个最小化/刻画结果。

问题
判定多正则字到字函数何时是正则函数，并确定实现给定多正则函数所需的最少 Pebble 数量。
方法
通过证明多正则函数的输出大小增长阶与可实现它的 Pebble 换能器的 Pebble 数量之间存在精确等价关系来刻画。
评估
理论证明：输出至多线性当且仅当函数正则；两枚 Pebble 当且仅当输出二次；三枚 Pebble 当且仅当输出三次；以此类推。
原文摘要（Abstract）

We show that a polyregular word-to-word function is regular if and only its output size is at most linear in its input size. Moreover a polyregular function can be realized by: a transducer with two pebbles if and only if its output has quadratic size in its input, a transducer with three pebbles if and only if its output has cubic size in its input, etc.

链接与引用

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

BibTeX 
@inproceedings{paperbot5487,
  title = {Pebble Minimization of Polyregular Functions},
  author = {Nathan Lhote},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394804}
}