# gRR comments on The limited predictor problem - Less Wrong

10 21 March 2012 12:15AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Sort By: Best

You are viewing a single comment's thread.

Comment author: 21 March 2012 01:20:29AM 0 points [-]

Could you explain a little more why explicitly representing the running time is helpful for the LPP? Is it true that the agent without the "runtime(A)<g(L)" terms fails to solve the problem, while this one succeeds? I don't understand how it is possible. The running time bound would still be there in any proof of "if A()=a then U()=u", except it would be implicit...

Comment author: 21 March 2012 07:27:17AM *  0 points [-]

I guess the question is whether any proof of "if A()=a then U()=u" will be found at all. (The formulation of LPP makes it easier to prove something like "if A()=a and runtime(A)<N, then U()=u".) But maybe you're right and such a proof will be found. It's a little tricky...

Comment author: 21 March 2012 11:51:57AM 0 points [-]

Hmm. It seems to me, the following holds:

(agent proves "if A()=a then U()=u") => "if A()=a and runtime(A)<N then U()=u"
(agent proves "if A()=a and runtime(A)<N then U()=u") => "if A()=a then U()=u"

where the right parts are logically implied, but not necessarily proved by the agent, although in almost all cases they would be, the proof steps from one to the other being so small...

In any case, the idea of logically controlling the non-obvious properties of computation is splendid, thanks for writing it up!

Comment author: 21 March 2012 11:56:52AM *  0 points [-]

Thanks for the compliment ;-) but I still don't completely understand your comment. If you mean the version of A that doesn't refer to runtime(A) explicitly, what's the short proof of the second statement?

Comment author: 21 March 2012 12:27:16PM 0 points [-]

"if A()=a and runtime(A)<N then U()=u" can only be proved by an agent that represents runtime() explicitly, which means it would probably find (relatively short) general proofs of the form (max proof length)<L => runtime < some function of L,
and
agent proves X => length of proof of X < max proof length.

Although, now that I think of it more, this does not help, as in this setting the agent may easily prove X but not "agent proves X"... You're right, the proof of the second statement is not obviously short.