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.

翻译：基本可行泛函类BFF是一阶多项式时间可计算函数类的二阶对应物。我们基于带类型的项式编程语言给出了BFF的若干隐式刻画。这些项可以调用非递归的命令式过程。类型系统包含两个层次：项遵循标准简单类型规则，而过程遵循基于分层类型的类型规则。BFF恰好由可类型化且可终止程序所计算的二阶泛函组成。令人惊讶的是，即使在缺少lambda抽象的情况下，该刻画的完全性依然成立。此外，终止性要求可被指定为一个保持完全性的实例，其判定复杂度为关于程序规模的二次时间。由于类型化可在多项式时间内判定，我们获得了首个关于BFF的可处理（即多项式时间可判定）、完备且隐式的刻画，从而解决了这一存在超过20年的开放问题。