An effective Procedure for Speeding up Algorithms

TL;DR

This paper introduces a method to construct algorithms that are within a factor of 5 of the fastest possible for certain problems by enumerating all provably equivalent programs, improving upon Levin search.

Contribution

It presents a provably asymptotically fastest algorithm construction that avoids Blum's speed-up theorem by focusing on programs with correctness proofs.

Findings

Constructs algorithms within a factor of 5 of the fastest for formal problems.

Extends Kolmogorov complexity with new measures for function complexity.

Shows the fastest program is also among the shortest provably correct programs.

Abstract

The provably asymptotically fastest algorithm within a factor of 5 for formally described problems will be constructed. The main idea is to enumerate all programs provably equivalent to the original problem by enumerating all proofs. The algorithm could be interpreted as a generalization and improvement of Levin search, which is, within a multiplicative constant, the fastest algorithm for inverting functions. Blum's speed-up theorem is avoided by taking into account only programs for which a correctness proof exists. Furthermore, it is shown that the fastest program that computes a certain function is also one of the shortest programs provably computing this function. To quantify this statement, the definition of Kolmogorov complexity is extended, and two new natural measures for the complexity of a function are defined.