Speed-up Theorems in Type-2 Computation

Abstract. A classic result known as the speed-up theorem in machineindependent complexity theory shows that there exist some computable functions that do not have best programs for them [2, 3]. In this paper we lift this result into type-2 computation under the notion of our type-2 complexity theory depicted in [15, 13, 14]. While the speed-up phenomenon is essentially inherited from type-1 computation, we cannot directly apply the original proof to our type-2 speed-up theorem because the oracle queries can interfere 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 [16] does not hold, which suggests that this curious phenomenon disappears in higher-typed computation beyond type-2.