Speed-Up Theorems in Type-2 Computations Using Oracle Turing Machines

A classic result known as the speed-up theorem in machine-independent complexity theory shows that there exist some computable functions that do not have best programs for them (Blum in J. ACM 14(2):322–336, 1967 and J. ACM 18(2):290–305, 1971). In this paper we lift this result into type-2 computations. Although the speed-up phenomenon is essentially inherited from type-1 computations, we observe that a direct application of the original proof to our type-2 speed-up theorem is problematic because the oracle queries can interfere with the speed of the programs and hence the cancellation strategy used in the original proof is no longer correct at type-2. We also argue that a type-2 analog of the operator speed-up theorem (Meyer and Fischer in J. Symb. Log. 37:55–68, 1972) does not hold, which suggests that this curious speed-up phenomenon disappears in higher-typed computations beyond type-2. The result of this paper adds one more piece of evidence to support the general type-2 complexity theory under the framework proposed in Li (Proceedings of the Third International Conference on Theoretical Computer Science, pp. 471–484, 2004 and Proceedings of Computability in Europe: Logical Approach to Computational Barriers, pp. 182–192, 2006) and Li and Royer (On type-2 complexity classes: Preliminary report, pp. 123–138, 2001) as a reasonable setup.