Type-two polynomial-time and restricted lookahead (Q1989320)

This paper is a contribution to second-order complexity theory, providing an alternative characterisation of type-two polynomial-time computability. In the introduction, a connection to first-order complexity theory, together with a summary of previous work on the subject, are given. A useful review of the computational model for type-two polynomial-time functionals \(\mathrm{P}\) using oracle Turing machines, developed by \textit{B. M. Kapron} and \textit{S. A. Cook} [SIAM J. Comput. 25, No. 1, 117--132 (1996; Zbl 0843.68028)], follows. Cook's class \(\mathrm{OPT}\) of operators computed by a machine running in oracle polynomial-time is defined, and a proof of the strict inclusion \(\mathrm{P} \subsetneq \mathrm{OPT}\) is included. In Section 2, the class \(\mathrm{SPT}\) of strongly polynomial-time computable operators is defined, based on the notion of an oracle machine that runs with finite length revision, which was introduced by \textit{A. Kawamura} and \textit{F. Steinberg} [LIPIcs -- Leibniz Int. Proc. Inform. 84, Article 23, 18 p. (2017; Zbl 1434.03117)]. The strict inclusion \(\mathrm{SPT} \subsetneq \mathrm{P}\) is shown. In addition, the class \(\mathrm{MPT}\) of moderate polynomial time operators is defined, based on the introduced notion of an oracle machine running with finite lookahead revision. Among other results, the inclusions \(\mathrm{SPT} \subseteq \mathrm{MPT} \subsetneq \mathrm{P}\) are shown. In Section 3, among other facts, the main result of the paper is shown. Namely, the closure of \(\mathrm{SPT}\) and of \(\mathrm{MPT}\) under lambda-abstraction and application is \(\mathrm{P}\). Moreover, results on composition, like the inclusion \(\mathrm{MPT} \subseteq \mathrm{SPT} \circ \mathrm{SPT}\), are shown. A final section on conclusions and future tasks, and an appendix on lambda-definability complete this paper.