The class of basic feasible functionals $(\mathtt{BFF})$ is the analog of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $\mathtt{BFF}$ can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant formalism for expressing higher-order computation. We address the problem of characterizing $\mathtt{BFF}$ by higher-order term rewriting. Various kinds of interpretations for first-order term rewriting have been introduced in the literature for proving termination and characterizing (first-order) complexity classes. In this paper, we consider a recently introduced notion of cost-size interpretations for higher-order term rewriting and see definitions as ways of computing functionals. We then prove that the class of functionals represented by higher-order terms admitting a certain kind of cost-size interpretation is exactly $\mathtt{BFF}$.

翻译：基本可行泛函类$(\mathtt{BFF})$是类型-2泛函（即可以接受（一阶）函数作为参数的泛函）中对应$\mathtt{FP}$（多项式时间函数）的概念。$\mathtt{BFF}$可以通过运行时间受二阶多项式限制的Oracle图灵机来定义。另一方面，高阶项重写为表达高阶计算提供了一种优雅的形式化方法。我们研究用高阶项重写刻画$\mathtt{BFF}$的问题。文献中已引入各种一阶项重写的解释方法，用于证明终止性并刻画（一阶）复杂度类。在本文中，我们考虑最近引入的高阶项重写的代价-规模解释概念，并将定义视为计算泛函的方式。随后我们证明，由允许某种代价-规模解释的高阶项所表示的泛函类恰好是$\mathtt{BFF}$。