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