Type-two polynomial-time and restricted lookahead

TL;DR

This paper introduces a new characterization of type-two polynomial-time computability that restricts oracle interactions to ensure feasibility, simplifying second-order complexity theory and encompassing all feasible problems.

Contribution

It refines the notion of oracle-polynomial-time by limiting lookahead revisions, providing a feasible class of functionals that includes all feasible problems and relates to existing classes.

Findings

Restricting lookahead revisions ensures polynomial-time feasibility.

The new class includes all feasible operations via lambda calculus closure.

It is strictly larger than the class of strongly polynomial-time computable operators.

Abstract

This paper provides an alternate characterization of type-two polynomial-time computability, with the goal of making second-order complexity theory more approachable. We rely on the usual oracle machines to model programs with subroutine calls. In contrast to previous results, the use of higher-order objects as running times is avoided, either explicitly or implicitly. Instead, regular polynomials are used. This is achieved by refining the notion of oracle-polynomial-time introduced by Cook. We impose a further restriction on the oracle interactions to force feasibility. Both the restriction as well as its purpose are very simple: it is well-known that Cook's model allows polynomial depth iteration of functional inputs with no restrictions on size, and thus does not guarantee that polynomial-time computability is preserved. To mend this we restrict the number of lookahead revisions, that is the number of times a query can be asked that is bigger than any of the previous queries. We prove that this leads to a class of feasible functionals and that all feasible problems can be solved within this class if one is allowed to separate a task into efficiently solvable subtasks. Formally put: the closure of our class under lambda-abstraction and application includes all feasible operations. We also revisit the very similar class of strongly polynomial-time computable operators previously introduced by Kawamura and Steinberg. We prove it to be strictly included in our class and, somewhat surprisingly, to have the same closure property. This can be attributed to properties of the limited recursion operator: It is not strongly polynomial-time computable but decomposes into two such operations and lies in our class.