The class of basic feasible functionals (BFF) is the analog of FP (polynomial time functions) for type-two functionals, that is, functionals that can take (first-order) functions as arguments. BFF can be defined by means of oracle Turing machines of time bounded by a second-order polynomial. On the other hand, higher-order term rewriting provides an elegant formalism for expressing higher-order computation. We address the problem of characterizing the class 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. Here 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 BFF.

翻译：基本可行泛函（BFF）类是对应于FP（多项式时间函数）的二阶泛函类比，即能够将（一阶）函数作为参数的泛函。BFF可通过受二阶多项式时间约束的谕示图灵机来定义。另一方面，高阶项重写系统为表达高阶计算提供了优雅的形式化框架。我们着手研究通过高阶项重写系统刻画BFF类的问题。已有文献引入多种一阶项重写系统的解释方法，用于证明终止性及刻画（一阶）复杂度类。本文我们针对高阶项重写系统采用最近提出的代价规模解释方法，并将归约规则视为计算泛函的方式。进而证明：能接受特定类型代价规模解释的高阶项所表示的泛函类恰好就是BFF。