一句话：首次给出 BFF（二阶多项式时间泛函）的多项式时间可判定、可靠完备且隐含的刻画。
Basic Feasible Functionals（BFF）是一阶多项式时间可计算函数在二阶上的对应类。本文基于带类型的项语言给出 BFF 的若干隐含刻画：项可调用非递归命令式过程，类型系统分两层，项遵循简单类型，过程遵循分层（tier-based）类型。BFF 恰好等于可由可类型化且终止的程序计算的二阶泛函。即使没有 lambda-抽象，完备性仍成立；终止性可表示为保持完备性的实例，并可在程序规模的二次时间内判定。由于类型检查是多项式时间可判定的，作者得到首个可处理、可靠、完备且隐含的 BFF 刻画，解决了悬置二十多年的问题。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2208-14739,
title = {Complete and tractable machine-independent characterizations of second-order polytime},
author = {Emmanuel Hainry and Bruce M. Kapron and Jean-Yves Marion and Romain Péchoux},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:5)2025}
}