“This Turing machine won’t halt in 3^^^3 steps” is a falsifiable prediction. Replace 3^^^3 with whatever number is enough to guarantee whatever result you need.
“This Turing machine won’t halt in 3^^^3 steps” is a falsifiable prediction.
Really? First, 3^^^3 is an absurdly large number of steps, much more steps than you could feasibly go through before the heat death of the universe or whatever horrible fate awaits us. Second, after enough steps your confidence in the outcome of any computation can be made arbitrarily low because of possible errors, e.g. errors caused by cosmic rays.
Replace 3^^^3 with whatever number is enough to guarantee whatever result you need.
But how do you know what number that is? The function “the number of steps needed to guarantee that a Turing machine won’t halt” is not a computable function of Turing machines, because if it were you could solve the halting problem. So how do you compute a function that’s, y’know, not computable?
First of all, I shouldn’t have used the number 3^^^3. That was a stupid idea, and I’ve forgotten what the notation means. So just replace that with “generic really big number”, let’s just say a googolplex (and, yes, I’m aware that’s nowhere close to 3^^^3).
To answer your question, I doubt FAI is going to care about whether Turing machine X halts; it’s going to be looking for a proof of a certain result regarding its own algorithms. It’s possible that it only needs to prove that its algorithms will work for “generic really big number” amount of steps, and thus could use a bounded quantifier instead of a universal quantifier. Using bounded quantifiers makes your system much weaker, but also moves it closer to being decidable (I mean this in a metaphorical sense; the system still won’t be decidable). Also, regarding searching for proofs, we’ll have to set an upper bound for how long we search, as well. So we need to specify some specific number in that context, too.
Specifically which numbers to select is something I have no idea about; I’m not an AI researcher. Maybe I’ll have some kind of idea (but very probably not) when a more formal problem specification is given, but this article is still discussing theoreticals, not applications yet.
Interesting article! What do you mean, though? Are you saying that Knuth’s triple up-arrow is uncomputable (I don’t see why that would be the case, but I could be wrong.)?
No, Solvent is making the same point as in my answer: in order to write down large enough numbers to guarantee that Turing machines don’t halt, you need to write down a function larger than the busy beaver function, and any such function fails to be computable because you can use it to solve the halting problem.
Basically, the busy beaver function tells us the maximum number of steps that a Turing machine with a given number of states and symbols can run for. If we know the busy beaver of, for example, 5 states and 5 symbols, then we can tell you if any 5 state 5 symbol Turing machine will eventually halt.
However, you can see why it’s impossible to in general find the busy beaver function- you’d have to know which Turing machines of a given size halted, which is in general impossible.
“This Turing machine won’t halt in 3^^^3 steps” is a falsifiable prediction. Replace 3^^^3 with whatever number is enough to guarantee whatever result you need.
Edit: But you’re right.
Really? First, 3^^^3 is an absurdly large number of steps, much more steps than you could feasibly go through before the heat death of the universe or whatever horrible fate awaits us. Second, after enough steps your confidence in the outcome of any computation can be made arbitrarily low because of possible errors, e.g. errors caused by cosmic rays.
I already saw your comments; I upvoted you. If this objection was made in your thread, I would have said, “Assuming ultrafinitism is wrong...”
It seemed to me that ultrafinitism wasn’t his true rejection.
Edit: But you’re right.
Okay, non-ultrafinitist objection:
But how do you know what number that is? The function “the number of steps needed to guarantee that a Turing machine won’t halt” is not a computable function of Turing machines, because if it were you could solve the halting problem. So how do you compute a function that’s, y’know, not computable?
First of all, I shouldn’t have used the number 3^^^3. That was a stupid idea, and I’ve forgotten what the notation means. So just replace that with “generic really big number”, let’s just say a googolplex (and, yes, I’m aware that’s nowhere close to 3^^^3).
To answer your question, I doubt FAI is going to care about whether Turing machine X halts; it’s going to be looking for a proof of a certain result regarding its own algorithms. It’s possible that it only needs to prove that its algorithms will work for “generic really big number” amount of steps, and thus could use a bounded quantifier instead of a universal quantifier. Using bounded quantifiers makes your system much weaker, but also moves it closer to being decidable (I mean this in a metaphorical sense; the system still won’t be decidable). Also, regarding searching for proofs, we’ll have to set an upper bound for how long we search, as well. So we need to specify some specific number in that context, too.
Specifically which numbers to select is something I have no idea about; I’m not an AI researcher. Maybe I’ll have some kind of idea (but very probably not) when a more formal problem specification is given, but this article is still discussing theoreticals, not applications yet.
Are you aware of the busy beaver function? Read this.
Basically, it’s impossible to write down numbers large enough for that to work.
Interesting article! What do you mean, though? Are you saying that Knuth’s triple up-arrow is uncomputable (I don’t see why that would be the case, but I could be wrong.)?
No, Solvent is making the same point as in my answer: in order to write down large enough numbers to guarantee that Turing machines don’t halt, you need to write down a function larger than the busy beaver function, and any such function fails to be computable because you can use it to solve the halting problem.
Ah, I see now, thanks!
Basically, the busy beaver function tells us the maximum number of steps that a Turing machine with a given number of states and symbols can run for. If we know the busy beaver of, for example, 5 states and 5 symbols, then we can tell you if any 5 state 5 symbol Turing machine will eventually halt.
However, you can see why it’s impossible to in general find the busy beaver function- you’d have to know which Turing machines of a given size halted, which is in general impossible.