Complete and tractable machine-independent characterizations of second-order polytime

TL;DR

This paper provides the first polynomial-time decidable, sound, and complete implicit characterization of the Basic Feasible Functionals, a second-order polynomial-time computability class, using a typed programming language with a tier-based type discipline.

Contribution

It introduces a tractable, implicit characterization of BFF based on a typed language, resolving a long-standing open problem in computational complexity.

Findings

Characterization of BFF via typable and terminating programs

Decidability of termination in quadratic time

Type checking is polynomial-time decidable

Abstract

The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem opened for more than 20 years.