4 ms·
If I understand correctly, the "fastest program f" is the one which M not only proves to solve the problem, but also proves to solve more quickly than any other
by Eliezer 17y ago
If I understand correctly, the "fastest program f" is the one which M not only proves to solve the problem, but also proves to solve more quickly than any other provable time bound. That is, it's not so much "fastest program f" as "program f with the lowest provable time bound among programs with provable time bounds relative to the proof system". This is another critical constraint that I should have mentioned earlier - the result really is a lot weaker than the abstract makes it sound.
- anatoly 17y agoI think that's slightly incorrect. The proof M is looking for is of the following statement: "P is an algorithm that solves the problem and T is an algorithm that is guaranteed to output, for any input, an upper bound on the running time of P for that input." There's no requirement that P should be proved to be faster than some other program. Anyhow, your criticism of the result's limited applicability still stands. I can't resist offering another nitpick: it's curious that the author neglected to mentioned that the proof system must be sound.