I kept expecting someone to object that “this Turing machine never halts” doesn’t count as a prediction, since you can never have observed it to run forever.
Then the statement “this Turing machine halts for every input” doesn’t count as a prediction either, because you can never have observed it for every input, even if the machine is just “halt”. And the statement “this Turing machine eventually halts” is borderline, because its negation doesn’t count as a prediction. What does this give us?
Perhaps there is a type theory for predictions, with concrete predictions like “The bus will come at 3 o’clock”, and functions that output concrete predictions like “Every monday, wednesday and friday, the bus will come at 3 o’clock” (consider the statement as a function taking a time and returning a concrete prediction yes or no).
An ultrafinitist would probably not argue with the existence of such a function, even though to someone other than an ultrafinitist, the function looks like it is quantifying over all time. From the ultrafinitist’s point of view, you’re going to apply it to some concrete time, and at that point it’s going to output a some concrete prediction.
Ultrafinitism doesn’t seem relevant here. The “type theory” you’re thinking of seems to be just the arithmetical hierarchy. A “concrete prediction” is a statement with only bounded quantifiers, “this Turing machine eventually halts” is a statement with one existential quantifier, “this Turing machine halts for every input” is a statement with one universal and one existential quantifier, and so on. Or am I missing something?
The arithmetical hierarchy is presuming a background of predicate logic; I was not presuming that. Yes, the type theory that I was gesturing towards would have some similarity to the arithmetical hierarchy.
I was trying to suggest that the answer to “what is a prediction” might look like a type theory of different variants of a prediction. Perhaps a linear hierarchy like the arithmetical hierarchy, yes, perhaps something more complicated. There could be a single starting type “concrete prediction” and a type constructor that, given source type and a destination type, gives the type of statements defining functions that take arguments of the source type and give arguments of the destination type.
The intuitive bridge for me from ultrafinitism to the question “what counts as a prediction?” is that ultrafinitists do happily work with entities like 2^1000 considered as a structure like (“^” “2” “1000″), even if they deny that those structures refer to things that are definitely numbers (of course, they can agree that they are definitely “numbers”, given an appropriately finitist definition of “number”). Maybe extreme teetotalers regarding what counts as a prediction would happily work with things such as computable functions returning predictions, even if they don’t consider them predictions.
Actually, I think “This Turing machine halts” is the more obviously troublesome one. It gives no computable expectation of when we might observe a halt. (Any computable probability distribution we would assign to halting time would put too much mass at small times as compared to the true distribution of halting times.)
If you take this objection seriously, then you should also take issue with predictions like “nobody will ever transmit information faster than the speed of light”, or things like it. After all, you can never actually observe the laws of physics to have been stable and universal for all time.
If nothing else, you can consider each as being a compact specification of an infinite sequence of testable predictions: “doesn’t halt after one step”, “doesn’t halt after two steps”,… “doesn’t halt after n steps”.
Technically speaking, you can observe the loop encoded in the Turing machine’s code somewhere—every nonhalting Turing machine has some kind of loop. The Halting theorems say that you cannot write down any finite program which will recognize and identify any infinite loop, or deductively prove the absence thereof, in bounded time. However, human beings don’t have finite programs, and don’t work by deduction, so I suspect, with a sketch of mathematical grounding, that these problems simply don’t apply to us in the same way they apply to regular Turing machines.
EDIT: To clarify, human minds aren’t “magic” or anything: the analogy between us and regular Turing machines with finite input and program tape just isn’t accurate. We’re a lot closer to inductive Turing machines or generalized Turing machines. We exhibit nonhalting behavior by design and have more-or-less infinite input tapes.
I don’t understand your notation. You have a disjunction of a formula and its negation, which is tautologically true, hence the whole statement is tautologically false.
P is a program; what meaning is intended by the predicate P(M,i)? In fact, what work is the object P doing in that formula? A Turing machine M is given an input string i; there is no other “program” involved.
every nonhalting Turing machine has some kind of loop
Formal proof needed; I in fact expect there to be something analogous to a Penrose tiling.
Moreover, to adapt Keynes’ apocryphal quote, a Turing machine can defer its loop for longer than you can ponder it.
And finally, as a general note, if you find that your proof that human beings can solve the halting problem can’t be made formal and concise, you might consider the possibility that your intuition is just plain wrong. It is in fact relevant that theoretical computer scientists seem to agree that the halting problem is not solvable by physical processes in the universe, including human beings.
And finally, as a general note, if you find that your proof that human beings can solve the halting problem can’t be made formal and concise, you might consider the possibility that your intuition is just plain wrong.
I didn’t say that it can’t be made formal. I said that the formalism isn’t concise enough for one blog comment. Most normal journal/conference papers are about ten pages long, so that’s the standard of concision you should use for a claimed formalism in theoretical CS.
And indeed, I think I can fit my formalism, when it’s done, into ten pages.
If anyone wants a go, here’s a Turing machine to try on. Does it halt?
.i=4.a=False.while not a:. a=True. for j in range(1,i):. k=i-j. b=False. for p in range(2,j):. b=b or j%p==0. for p in range(2,k):. b=b or k%p==0. a=a and b
Failing to halt and going into an infinite loop are not the same thing.
I’d appreciate some explanation on that, to see if you’re saying something I haven’t heard before or if we’re talking past each-other. I don’t just include while(true); under “infinite loop”, I also include infinitely-expanding recursions that cannot be characterized as coinductive stepwise computations. Basically, anything that would evaluate to the \Bot type in type-theory counts for “infinite loop” here, just plain computational divergence.
I think that what Joshua was talking about by ‘infinite loop’ is ‘passing through the same state an infinite number of times.’ That is, a /loop/, rather than just a line with no endpoint.
although this would rule out
(some arbitrary-size int type) x = 0;
while(true){
x++;
}
on a machine with infinite memory, as it would never pass through the same state twice. So maybe I’m still misunderstanding.
To clarify, human minds aren’t “magic” or anything: the analogy between us and regular Turing machines with finite input and program tape just isn’t accurate.
Actually, the standard Turing machine has an infinite tape. And, the role of the tape in a Turing machine is equivalent to the input, output and working memory of a computer; the Turing machine’s “program” is the finite state machine.
However, human beings don’t have finite programs, and don’t work by induction, so I suspect, with a sketch of mathematical grounding, that these problems simply don’t apply to us in the same way they apply to regular Turing machines.
It seems to me that the above suggests that humans are capable of cognitive tasks that Turing machines are not. But if this is true, it follows that human-level AGI is not achievable via a computer, since computers are thought to be equivalent in power to Turing machines.
First of all, swapped “induction” to “deduction”, because I’m a moron.
And, the role of the tape in a Turing machine is equivalent to the input, output and working memory of a computer; the Turing machine’s “program” is the finite state machine.
There’s no real semantic distinction between the original contents of the One Tape, or the finite contents of the Input Tape, or an arbitrarily complicated state-machine program, actually. You can build tape data for a Universal Turing Machine to simulate any other Turing machine.
It seems to me that the above suggests that humans are capable of cognitive tasks that Turing machines are not. But if this is true, it follows that human-level AGI is not achievable via a computer, since computers are thought to be equivalent in power to Turing machines.
No. You’re just making the analogy between Turing machines and real, physical computing devices overly strict. A simple Turing machine takes a finite input, has a finite program, and either processes for finite time before accepting (possibly with something on an output tape or something like that), or runs forever.
Real, physical computing devices, both biological and silicon, run coinductive (infinite-loop-until-it-isn’t) programs all the time. Every operating system kernel, or message loop, or game loop is a coinductive program: its chief job is to iterate forever, taking a finite time to process I/O in each step. Each step performs some definite amount of semantic work, but there is an indefinite number of steps (generally: until a special “STOP NOW” input is given). To reiterate: because these programs both loop infinitely and perform I/O (with the I/O data not being computable from anything the program has when it begins running, not being “predictable” in any sense by the program), they are physically-realizable programs that simply don’t match the neat analogy of normal Turing machines.
Likewise, human beings loop infinitely and perform I/O. Which more-or-less gives away half my mathematical sketch of how we solve the problem!
To reiterate: because these programs both loop infinitely and perform I/O (with the I/O data not being computable from anything the program has when it begins running, not being “predictable” in any sense by the program), they are physically-realizable programs that simply don’t match the neat analogy of normal Turing machines.
They match the neat analogy of Turing machines that start with possibly infinitely many non-blank squares on their tapes. All the obvious things you might like to know are still undecidable. Is this machine guaranteed to eventually read every item of its input? Is there any input that will drive the machine into a certain one of its states? Will the machine ever write a given finite string? Will it eventually have written every finite prefix of a given infinite string? Will it ever halt? These are all straightforwardly reducible to the standard halting problem.
Or perhaps you would add to the model an environment that responds to what the machine does. In that case, represent the environment by an oracle (not necessarily a computable one), and define some turn-taking mechanism for the machine to ask questions and receive answers. All of the interesting questions remain undecidable.
There’s no real semantic distinction between the original contents of the One Tape, or the finite contents of the Input Tape, or an arbitrarily complicated state-machine program, actually. You can build tape data for a Universal Turing Machine to simulate any other Turing machine.
and with this:
Real, physical computing devices, both biological and silicon, run coinductive (infinite-loop-until-it-isn’t) programs all the time. Every operating system kernel, or message loop, or game loop is a coinductive program: its chief job is to iterate forever, taking a finite time to process I/O in each step. Each step performs some definite amount of semantic work, but there is an indefinite number of steps (generally: until a special “STOP NOW” input is given).
However, I don’t see how you are going to be able to use these facts to solve the halting problem. I’m guessing that, rather than statically examining the Turing machine, you will execute it for some period of time and study the execution, and after some finite amount of time, you expect to be able to correctly state whether or not the machine will halt. Is that the basic idea?
I’m guessing that, rather than statically examining the Turing machine, you will execute it for some period of time and study the execution, and after some finite amount of time, you expect to be able to correctly state whether or not the machine will halt. Is that the basic idea?
Basically, yes. “Halting Empiricism”, you could call it. The issue is precisely that you can’t do empirical reasoning via deduction from a fixed axiom set (ie: a fixed, finite program halts x : program -> boolean). You need to do it by inductive reasoning, instead.
My reply to you is the same as my reply to g_pepper: it’s easier for me to just do my background research, double-check everything, and eventually publish the full formalism than it is to explain all the details in a blog comment.
You are also correct to note that whatever combination of machine, person, input tape, and empirical data I provide, the X Machine can never solve the Halting Problem for the X Machine. The real math involved in my thinking here involves demonstrating the existence of an ordering: there should exist a sense in which some machines are “smaller” than others, and A can solve B’s halting problem when A is “strictly larger” than B, possibly strictly larger by some necessary amount.
(Of course, this already holds if A has an nth-level Turing Oracle, B has an mth-level Turing Oracle, and n > m, but that’s trivial from the definition of an oracle. I’m thinking of something that actually concerns physically realizable machines.)
Like I said: trying to go into extensive detail via blog comment will do nothing but confusingly unpack my intuitions about the problem, increasing net confusion. The proper thing to do is formalize, and that’s going to take a bunch of time.
This is interesting. Do you have an outline of how a person would go about determining whether a Turing machine will halt? If so, I would be interested in seeing it. Alternatively, if you have a more detailed argument as to why a person will be able to determine whether an arbitrary Turing machine will halt, even if that argument does not contain the details of how the person would proceed, I would be interested in seeing that.
Or, are you just making the argument that an intelligent person ought to be able in every case to use some combination of inductive reasoning, creativity, mathematical intuition, etc., to correctly determine whether or not a Turing machine will halt?
My reply to you is the same as my reply to Richard Kennaway: it’s easier for me to just do my background research, double-check everything, and eventually publish the full formalism than it is to explain all the details in a blog comment.
It’s possible to compute whether each machine halts using an inductive Turing machine like this:
initialize output tape to all zeros, representing the assertion that no Turing machine halts
for i = 1 to infinity
. for j = 1 to i
. . run Turing machine j for i steps
. . if it halts: set bit j in the output tape to 1
Is this what you meant? If so, I’m not sure what this has to do with observing loops.
When you say that every nonhalting Turing machine has some kind of loop, do you mean the kind of loop that many halting Turing machines also contain?
When you say that every nonhalting Turing machine has some kind of loop, do you mean the kind of loop that many halting Turing machines also contain?
No, I mean precisely the fact that it doesn’t halt. You can think of it as an infinitely growing recursion if that helps, but what’s in question is really precisely the nonhalting behavior.
I’m going to make a Discussion post about the matter, since Luke wants me to share the whole informal shpiel on the subject.
It is possible to make a Turing machine that returns “HALT”, “RUNS FOREVER” or “UNSURE” and is never wrong. If the universe as we know it runs on quantum mechanics, it should be possible to simulate a mathematician in a box with unlimited data storage and time, using a finite Turing machine. This would imply the existence of some problem that would leave the mathematician stuck forever. There are plenty of Turing machines where we have no Idea if they halt. If you describe the quantum state of the observable universe to plank length resolution, what part of humans supposedly infinite minds is not described in these 2^2^100 bits of information?
“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.
I kept expecting someone to object that “this Turing machine never halts” doesn’t count as a prediction, since you can never have observed it to run forever.
Then the statement “this Turing machine halts for every input” doesn’t count as a prediction either, because you can never have observed it for every input, even if the machine is just “halt”. And the statement “this Turing machine eventually halts” is borderline, because its negation doesn’t count as a prediction. What does this give us?
Perhaps there is a type theory for predictions, with concrete predictions like “The bus will come at 3 o’clock”, and functions that output concrete predictions like “Every monday, wednesday and friday, the bus will come at 3 o’clock” (consider the statement as a function taking a time and returning a concrete prediction yes or no).
An ultrafinitist would probably not argue with the existence of such a function, even though to someone other than an ultrafinitist, the function looks like it is quantifying over all time. From the ultrafinitist’s point of view, you’re going to apply it to some concrete time, and at that point it’s going to output a some concrete prediction.
Ultrafinitism doesn’t seem relevant here. The “type theory” you’re thinking of seems to be just the arithmetical hierarchy. A “concrete prediction” is a statement with only bounded quantifiers, “this Turing machine eventually halts” is a statement with one existential quantifier, “this Turing machine halts for every input” is a statement with one universal and one existential quantifier, and so on. Or am I missing something?
The arithmetical hierarchy is presuming a background of predicate logic; I was not presuming that. Yes, the type theory that I was gesturing towards would have some similarity to the arithmetical hierarchy.
I was trying to suggest that the answer to “what is a prediction” might look like a type theory of different variants of a prediction. Perhaps a linear hierarchy like the arithmetical hierarchy, yes, perhaps something more complicated. There could be a single starting type “concrete prediction” and a type constructor that, given source type and a destination type, gives the type of statements defining functions that take arguments of the source type and give arguments of the destination type.
The intuitive bridge for me from ultrafinitism to the question “what counts as a prediction?” is that ultrafinitists do happily work with entities like 2^1000 considered as a structure like (“^” “2” “1000″), even if they deny that those structures refer to things that are definitely numbers (of course, they can agree that they are definitely “numbers”, given an appropriately finitist definition of “number”). Maybe extreme teetotalers regarding what counts as a prediction would happily work with things such as computable functions returning predictions, even if they don’t consider them predictions.
Actually, I think “This Turing machine halts” is the more obviously troublesome one. It gives no computable expectation of when we might observe a halt. (Any computable probability distribution we would assign to halting time would put too much mass at small times as compared to the true distribution of halting times.)
If you take this objection seriously, then you should also take issue with predictions like “nobody will ever transmit information faster than the speed of light”, or things like it. After all, you can never actually observe the laws of physics to have been stable and universal for all time.
If nothing else, you can consider each as being a compact specification of an infinite sequence of testable predictions: “doesn’t halt after one step”, “doesn’t halt after two steps”,… “doesn’t halt after n steps”.
Technically speaking, you can observe the loop encoded in the Turing machine’s code somewhere—every nonhalting Turing machine has some kind of loop. The Halting theorems say that you cannot write down any finite program which will recognize and identify any infinite loop, or deductively prove the absence thereof, in bounded time. However, human beings don’t have finite programs, and don’t work by deduction, so I suspect, with a sketch of mathematical grounding, that these problems simply don’t apply to us in the same way they apply to regular Turing machines.
EDIT: To clarify, human minds aren’t “magic” or anything: the analogy between us and regular Turing machines with finite input and program tape just isn’t accurate. We’re a lot closer to inductive Turing machines or generalized Turing machines. We exhibit nonhalting behavior by design and have more-or-less infinite input tapes.
I think I would use “every” where you use “any.”
Let’s just use quantifiers.
Where P is a finite program running in finite time, M is a Turing machine, and i is an input string.
I don’t understand your notation. You have a disjunction of a formula and its negation, which is tautologically true, hence the whole statement is tautologically false.
P is a program; what meaning is intended by the predicate P(M,i)? In fact, what work is the object P doing in that formula? A Turing machine M is given an input string i; there is no other “program” involved.
Formal proof needed; I in fact expect there to be something analogous to a Penrose tiling.
Moreover, to adapt Keynes’ apocryphal quote, a Turing machine can defer its loop for longer than you can ponder it.
And finally, as a general note, if you find that your proof that human beings can solve the halting problem can’t be made formal and concise, you might consider the possibility that your intuition is just plain wrong. It is in fact relevant that theoretical computer scientists seem to agree that the halting problem is not solvable by physical processes in the universe, including human beings.
I didn’t say that it can’t be made formal. I said that the formalism isn’t concise enough for one blog comment. Most normal journal/conference papers are about ten pages long, so that’s the standard of concision you should use for a claimed formalism in theoretical CS.
And indeed, I think I can fit my formalism, when it’s done, into ten pages.
If anyone wants a go, here’s a Turing machine to try on. Does it halt?
.i=4.a=False.while not a:. a=True. for j in range(1,i):. k=i-j. b=False. for p in range(2,j):. b=b or j%p==0. for p in range(2,k):. b=b or k%p==0. a=a and b
Written in python for the convenience of coders.
No. These aren’t “loops” in any meaningful sense of the word. Failing to halt and going into an infinite loop are not the same thing.
I’d appreciate some explanation on that, to see if you’re saying something I haven’t heard before or if we’re talking past each-other. I don’t just include
while(true);under “infinite loop”, I also include infinitely-expanding recursions that cannot be characterized as coinductive stepwise computations. Basically, anything that would evaluate to the\Bottype in type-theory counts for “infinite loop” here, just plain computational divergence.I think that what Joshua was talking about by ‘infinite loop’ is ‘passing through the same state an infinite number of times.’ That is, a /loop/, rather than just a line with no endpoint. although this would rule out (some arbitrary-size int type) x = 0; while(true){ x++; } on a machine with infinite memory, as it would never pass through the same state twice. So maybe I’m still misunderstanding.
Ok. By that definition, yes these are the same thing. I don’t think this is a standard notion of what people mean by infinite loop though.
Actually, the standard Turing machine has an infinite tape. And, the role of the tape in a Turing machine is equivalent to the input, output and working memory of a computer; the Turing machine’s “program” is the finite state machine.
It seems to me that the above suggests that humans are capable of cognitive tasks that Turing machines are not. But if this is true, it follows that human-level AGI is not achievable via a computer, since computers are thought to be equivalent in power to Turing machines.
First of all, swapped “induction” to “deduction”, because I’m a moron.
There’s no real semantic distinction between the original contents of the One Tape, or the finite contents of the Input Tape, or an arbitrarily complicated state-machine program, actually. You can build tape data for a Universal Turing Machine to simulate any other Turing machine.
No. You’re just making the analogy between Turing machines and real, physical computing devices overly strict. A simple Turing machine takes a finite input, has a finite program, and either processes for finite time before accepting (possibly with something on an output tape or something like that), or runs forever.
Real, physical computing devices, both biological and silicon, run coinductive (infinite-loop-until-it-isn’t) programs all the time. Every operating system kernel, or message loop, or game loop is a coinductive program: its chief job is to iterate forever, taking a finite time to process I/O in each step. Each step performs some definite amount of semantic work, but there is an indefinite number of steps (generally: until a special “STOP NOW” input is given). To reiterate: because these programs both loop infinitely and perform I/O (with the I/O data not being computable from anything the program has when it begins running, not being “predictable” in any sense by the program), they are physically-realizable programs that simply don’t match the neat analogy of normal Turing machines.
Likewise, human beings loop infinitely and perform I/O. Which more-or-less gives away half my mathematical sketch of how we solve the problem!
They match the neat analogy of Turing machines that start with possibly infinitely many non-blank squares on their tapes. All the obvious things you might like to know are still undecidable. Is this machine guaranteed to eventually read every item of its input? Is there any input that will drive the machine into a certain one of its states? Will the machine ever write a given finite string? Will it eventually have written every finite prefix of a given infinite string? Will it ever halt? These are all straightforwardly reducible to the standard halting problem.
Or perhaps you would add to the model an environment that responds to what the machine does. In that case, represent the environment by an oracle (not necessarily a computable one), and define some turn-taking mechanism for the machine to ask questions and receive answers. All of the interesting questions remain undecidable.
I agree with this:
and with this:
However, I don’t see how you are going to be able to use these facts to solve the halting problem. I’m guessing that, rather than statically examining the Turing machine, you will execute it for some period of time and study the execution, and after some finite amount of time, you expect to be able to correctly state whether or not the machine will halt. Is that the basic idea?
Basically, yes. “Halting Empiricism”, you could call it. The issue is precisely that you can’t do empirical reasoning via deduction from a fixed axiom set (ie: a fixed, finite program
halts x : program -> boolean). You need to do it by inductive reasoning, instead.What is inductive reasoning? Bayesian updating? Or something else?
My reply to you is the same as my reply to g_pepper: it’s easier for me to just do my background research, double-check everything, and eventually publish the full formalism than it is to explain all the details in a blog comment.
You are also correct to note that whatever combination of machine, person, input tape, and empirical data I provide, the X Machine can never solve the Halting Problem for the X Machine. The real math involved in my thinking here involves demonstrating the existence of an ordering: there should exist a sense in which some machines are “smaller” than others, and A can solve B’s halting problem when A is “strictly larger” than B, possibly strictly larger by some necessary amount.
(Of course, this already holds if A has an nth-level Turing Oracle, B has an mth-level Turing Oracle, and n > m, but that’s trivial from the definition of an oracle. I’m thinking of something that actually concerns physically realizable machines.)
Like I said: trying to go into extensive detail via blog comment will do nothing but confusingly unpack my intuitions about the problem, increasing net confusion. The proper thing to do is formalize, and that’s going to take a bunch of time.
This is interesting. Do you have an outline of how a person would go about determining whether a Turing machine will halt? If so, I would be interested in seeing it. Alternatively, if you have a more detailed argument as to why a person will be able to determine whether an arbitrary Turing machine will halt, even if that argument does not contain the details of how the person would proceed, I would be interested in seeing that.
Or, are you just making the argument that an intelligent person ought to be able in every case to use some combination of inductive reasoning, creativity, mathematical intuition, etc., to correctly determine whether or not a Turing machine will halt?
My reply to you is the same as my reply to Richard Kennaway: it’s easier for me to just do my background research, double-check everything, and eventually publish the full formalism than it is to explain all the details in a blog comment.
Fair enough. I am looking forward to seeing the formalism!
It’s possible to compute whether each machine halts using an inductive Turing machine like this:
Is this what you meant? If so, I’m not sure what this has to do with observing loops.
When you say that every nonhalting Turing machine has some kind of loop, do you mean the kind of loop that many halting Turing machines also contain?
No, I mean precisely the fact that it doesn’t halt. You can think of it as an infinitely growing recursion if that helps, but what’s in question is really precisely the nonhalting behavior.
I’m going to make a Discussion post about the matter, since Luke wants me to share the whole informal shpiel on the subject.
It is possible to make a Turing machine that returns “HALT”, “RUNS FOREVER” or “UNSURE” and is never wrong. If the universe as we know it runs on quantum mechanics, it should be possible to simulate a mathematician in a box with unlimited data storage and time, using a finite Turing machine. This would imply the existence of some problem that would leave the mathematician stuck forever. There are plenty of Turing machines where we have no Idea if they halt. If you describe the quantum state of the observable universe to plank length resolution, what part of humans supposedly infinite minds is not described in these 2^2^100 bits of information?
“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.