paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Folding interpretations

折叠解释
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 2/10 · 论文属于纯 PL 理论,研究 polyregular 函数、组合子与线性逻辑启发的类型系统,与用户关注的 LLM/Agentic 程序静态分析、浮点程序分析、贝叶斯程序分析及其与 LLM 的交叉基本无关。仅在类型系统与逻辑自动机方向上有很弱的 PL 理论关联,不构成核心匹配。引用 3 inbox
Mikołaj Bojańczyk
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出带 fold 迭代机制的组合子系统,并用线性逻辑启发的类型系统将其限制到恰好生成 polyregular 函数。

本文研究 polyregular 字符串到字符串函数,这类函数输出规模为多项式,可由自动机与逻辑刻画。已有组合子系统缺少迭代机制;本文引入 fold 作为迭代原语,但无限制的 fold 能定义所有原始递归函数,因此需要加以限制。作者提出受线性逻辑启发的类型系统,对 fold 的使用施加约束,使组合子系统恰好生成 polyregular 函数。论文还给出相关系统,分别刻画量词无关函数以及字符串和树上的线性正则函数。该结果为 polyregular 函数提供了新的组合式、带类型约束的生成视角。

问题
如何用组合子系统生成 polyregular 字符串函数,并在加入 fold 迭代机制时避免其表达力过强,以至于能定义原始递归函数。
方法
引入 fold 迭代原语,并设计受线性逻辑启发的类型系统来限制 fold 的使用,从而构建恰好刻画 polyregular 函数的组合子系统;同时给出量词无关函数及字符串/树上线形正则函数的变体系统。
评估
通过表达力等价性证明进行评估:证明受限组合子系统恰好生成 polyregular 函数,并给出相关变体系统的刻画结果。
原文摘要(Abstract)

We study the polyregular string-to-string functions, which are certain functions of polynomial output size that can be described using automata and logic. We describe a system of combinators that generates exactly these functions. Unlike previous systems, the present system includes an iteration mechanism, namely fold. Although unrestricted fold can define all primitive recursive functions, we identify a type system (inspired by linear logic) that restricts fold so that it defines exactly the polyregular functions. We also present related systems, for quantifier-free functions as well as for linear regular functions on both strings and trees.

链接与引用

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

BibTeX
@inproceedings{Bojanczyk23,
  title = {Folding interpretations},
  author = {Mikołaj Bojańczyk},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175796}
}