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 imperative procedures, which are not recursive. 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恰好由可通过类型化且终止程序计算的二阶泛函构成。令人惊讶的是，在缺乏λ-抽象的情况下，此刻画的完备性仍然成立。此外，终止性要求可被指定为保持完备性的实例，其可在程序规模平方时间内判定。由于类型化在多项式时间内可判定，我们获得了首个可处理（即多项式时间可判定）、完备且隐式的BFF刻画，从而解决了持续二十多年的开放问题。