Blum's speedup theorem seems to me that bears at least some superficial resemblance to Godels research on the length of proofs under certain axiomatic systems. Does Blum's speedup theorem have any conceptual predecessors?
1
-
1$\begingroup$ What references does Blum include in his original 1967 paper? They might suggest conceptual predecessors. $\endgroup$– Gerald EdgarJun 5, 2022 at 12:49
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
The resemblance is not superficial. There is a precise relation between computer programs and formal proofs known as the Curry–Howard correspondence that took shape in 1960s. And Godel's results on proof length were a direct inspiration for speed-up theorems starting with Blum's 1967 result, see Dawson, The Godel Incompleteness Theorem from a Length-of-Proof Perspective:
"In one year (1936) three important papers appeared, all based on considerations of the length or complexity of proofs in formal systems. One, Rosser's improvement of the Incompleteness Theorem, has already been mentioned. The others were Gentzen's consistency proof for arithmetic ([7], translated in [23, pp. 132-213]), the first of its kind, employing a transfinite induction on the complexity of derivations; and a brief and little-noticed article by Godel himself ([10], translated in [5, pp. 82-83]). The latter, titled simply "On the Length of Proofs," pointed out that, by passing to systems of "higher type" (allowing sets of integers, sets of sets of integers, etc.), not only can new theorems be proved, but "it becomes possible to shorten extraordinarily infinitely many of the proofs already available."
Translated only in 1965, Godel's length-of-proof paper was largely ignored until after the advent of the computer revolution, when concern for efficiency of computation led to Manuel Blum's creation of computational complexity theory, and Godel's proof-shortening result was resurrected to become the progenitor of a whole class of speed-up theorems (see [1, pp. 253 and 261-263])."
