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...
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...
(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!
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?
“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) 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.
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...
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...
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!
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?
“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) 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.