一句话：本文证明由多项式有界代价-尺寸解释的高阶项所表示的泛函类恰好是类型二基本可行泛函类 BFF2。
类型二基本可行泛函类 BFF2 是 FP 在类型二泛函上的类比，可由运行时间受二阶多项式限制的 oracle Turing 机定义。本文研究如何用高阶项重写刻画 BFF2。作者采用近期为高阶重写提出的代价-尺寸解释，将二阶重写视为计算类型二泛函的方式，并证明由允许多项式有界代价-尺寸解释的高阶项所表示的泛函类恰好等于 BFF2。该结果将一阶重写中用于终止性与复杂度类刻画的各种解释方法推广到高阶情形，为高阶计算的多项式时间复杂度提供了重写与解释角度的刻画。
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$.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BaillotLKV25,
title = {A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations},
author = {Patrick Baillot and Ugo Dal Lago and Cynthia Kop and Deivid Vale},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:19)2025}
}