The class of type-two basic feasible functionals ($\mathtt{BFF}_2$) is the analogue of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $\mathtt{BFF}_2$ 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}_2$ 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 second order rewriting as ways of computing type-2 functionals. We then prove that the class of functionals represented by higher-order terms admitting polynomially bounded cost-size interpretations exactly corresponds to $\mathtt{BFF}_2$.

翻译：类型二基本可行泛函类（$\mathtt{BFF}_2$）是类型二泛函（即能以（一阶）函数为参数的泛函）中对应于$\mathtt{FP}$（多项式时间函数）的类比。$\mathtt{BFF}_2$可通过运行时间以二阶多项式为界的Oracle图灵机来定义。另一方面，高阶项重写为表达高阶计算提供了一种优雅的形式化方法。本文致力于通过高阶项重写来刻画$\mathtt{BFF}_2$。文献中已针对一阶项重写引入各类解释方法，用于证明终止性并刻画一阶复杂性类。本文考虑最近提出的高阶项重写代价-规模解释概念，并将二阶重写视为计算类型二泛函的途径。我们进而证明：具有多项式有界代价-规模解释的高阶项所表示的泛函类恰好对应于$\mathtt{BFF}_2$。