一句话：用分层类型系统为带 oracle 调用的命令式语言刻画 BFF2，类型推断可判定且复杂度为三次方。
本文研究 Basic Feasible Functionals BFF2 的编程语言刻画问题。BFF2 是多项式时间可计算函数类 FP 的 type-2 对应物，已有文献虽提出若干刻画，但均未给出带类型系统保证该复杂度界的编程语言。作者提出一种带 oracle 调用的命令式语言，并设计基于 tier 的类型系统，使得程序计算的泛函恰好属于 BFF2。该类型系统的类型推断是可判定的，且推断算法复杂度为程序规模的三次方，显著优于已有方法的不可行性，同时不过度限制语言表达力。
The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF$_2$ based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not overly constrain the expressive power of the language.
@article{paperbot1721,
title = {A tier-based typed programming language characterizing Feasible Functionals},
author = {Emmanuel Hainry and Bruce M. Kapron and Jean-Yves Marion and Romain Péchoux},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:33)2022}
}