paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Type-two polynomial-time and restricted lookahead

二型多项式时间与受限前瞻
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 1/10 · 论文研究二型多项式时间与预言机前瞻限制,属于高阶复杂性/可计算性理论,与用户关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关联。引用 8 inbox
Bruce M. Kapron, Florian Steinberg
crossref: 2026-09-12

AI 速览

一句话:通过限制预言机查询的前瞻修正次数,给出无需高阶运行时间的二型多项式时间可计算性新刻画。

本文研究二型(二阶)多项式时间可计算性,旨在让二阶复杂性理论更易接近。传统 Cook 的预言机多项式时间模型允许对函数输入做多项式深度的无限制迭代,且查询规模不受限,因而不能保持多项式时间可计算性。作者在 Cook 模型上限制“前瞻修正”次数,即查询规模超过此前任何查询的次数,并用普通多项式作为运行时间。由此定义的新类包含可行函数;若任务可分解为高效子任务,所有可行问题都能在该类中求解,且其在 lambda 抽象与应用下的闭包正是基本可行函数。作者还证明 Kawamura 和 Steinberg 的强多项式时间算子类严格包含于新类,但两者闭包性质相同。

问题
如何为带子程序调用的二型泛函建立可行的多项式时间可计算性模型,避免 Cook 模型允许无限制迭代函数输入而破坏多项式时间性,也避免使用高阶运行时间?
方法
在 Cook 的预言机多项式时间模型上限制前瞻修正次数(查询规模超过此前任何查询的次数),以普通多项式作运行时间,并证明所得函数类在 lambda 抽象与应用下闭包为基本可行函数;同时与 Kawamura-Steinberg 的强多项式时间算子类比较。
评估
通过数学证明确立包含关系与闭包性质:新类涵盖可行函数(在允许高效子任务分解的意义下),强多项式时间算子类被严格包含但具相同闭包性质;并分析受限递归算子的分解。
原文摘要(Abstract)

This paper provides an alternate characterization of second-order polynomial-time computability, with the goal of making second-order complexity theory more approachable. We rely on the usual oracle machines to model programs with subroutine calls. In contrast to previous results, the use of higher-order objects as running times is avoided, either explicitly or implicitly. Instead, regular polynomials are used. This is achieved by refining the notion of oracle-poly-time computability introduced by Cook. We impose a further restriction on oracle interactions to force feasibility. Both the restriction and its purpose are very simple: it is well-known that Cook's model allows polynomial depth iteration of functional inputs with no restrictions on size, and thus does not preserve poly-time computability. To mend this we restrict the number of lookahead revisions, that is the number of times a query whose size exceeds that of any previous query may be asked. We prove that this leads to a class of feasible functionals and that all feasible problems can be solved within this class if one is allowed to separate a task into efficiently solvable subtasks. Formally, the closure of our class under lambda-abstraction and application are the basic feasible functionals. We also revisit the very similar class of strongly poly-time computable operators previously introduced by Kawamura and Steinberg. We prove it to be strictly included in our class and, somewhat surprisingly, to have the same closure property. This is due to the nature of the limited recursion operator: it is not strongly poly-time but decomposes into two such operations and lies in our class.

链接与引用

DOI 原文 ·

BibTeX
@inproceedings{paperbot4364,
  title = {Type-two polynomial-time and restricted lookahead},
  author = {Bruce M. Kapron and Florian Steinberg},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209124}
}