Complete and tractable machine-independent characterizations of second-order polytime
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2022)(2022)
摘要
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.
更多查看译文
关键词
Basic feasible functionals, Type 2, Second-order, Polynomial time, Tiering, Safe recursion
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要