论文标题
二阶Poly的完整且可拖动的机器无关表征
Complete and tractable machine-independent characterizations of second-order polytime
论文作者
论文摘要
基本可行函数类BFF是可在多项式时间内计算的一阶函数类的二阶对应物。我们根据术语的打字编程语言介绍了BFF的几种隐性特征。这些条款可能会呼叫非恢复命令程序。该类型学科有两层：术语遵循标准的简单学科，这些过程遵循标准的基于层的类型学科。 BFF完全由通过键入和终止程序计算的二阶功能组成。令人惊讶的是，在没有Lambda-abstractraction的情况下，这种表征的完整性仍然存在。此外，可以将终止要求指定为完整性的实例，可以在程序大小上及时确定。由于在多项式时间内键入是可决定的，因此我们获得了第一个可触发的（即在多项式时间中可确定），声音，完整和隐式表征BFF，从而解决了20年以上的问题。
The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem opened for more than 20 years.
