3 ms·

A similarly misleading statement in the abstract: "the most efficient program computing some function f is also among the shortest programs provably computing

by Eliezer 17y ago

A similarly misleading statement in the abstract: "the most efficient program computing some function f is also among the shortest programs provably computing f." If this were actually true, it would reveal an extremely deep principle about efficiency. But this is not the actual "most efficient" program that is short, it is Hutter's asymptotically efficient program, which out of some strange reason Hutter has taken to calling "the fastest program", which it is not. It is never the most efficient program (it makes use of a program more efficient than itself). It is "among the shortest" such programs in the sense that it can be specified using a fixed framework plus the shortest program such that other programs which solve the problem can be proven equivalent to it, relative to the proof system. I was pretty disappointed when I worked that out - from the abstract's statement that the most efficient algorithm is always among the shortest, I was expecting to discover some deep principle about skipping unnecessary steps, or some such.

lmkg 17y ago
So am I correct in interpreting that this "fastest program" f means the function that M is fastest at identifying, proving, and executing, rather than the function whose execution time is fastest in a vacuum?
- 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 ago
    I 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.

by Eliezer 17y ago

lmkg 17y ago

So am I correct in interpreting that this "fastest program" f means the function that M is fastest at identifying, proving, and executing, rather than the function whose execution time is fastest in a vacuum?

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 ago
  I 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.