Rice’s Theorem: An interactive tutorial
busy-beavers.tigyog.app
busy-beavers.tigyog.app
My only quibble with this one is with step 19 ("hangIf3") which relies on "infinity is not considered even" — that is a distraction IMO, and if I understand correctly (have not thought about this carefully) the example could be replaced with something that involves an actual odd number.
Indeed, you could just replace haltIf3or7 by haltIf3or5or7 (or whatever). (And, of course, whether or not infinity is considered even cannot be deduced from the information given, so relying on this technicality here I'd argue is beyond distracting and into the realm of so underspecified that it might be wrong. Or we could raise the same objection mentioned earlier, that it's not specified what kind of object `n` is, and numeric types often have only finitely many inhabitants ….)
p.s. thanks for the compliments on the format! If you (or anyone else) wants to create tutorials in this format, https://tigyog.app/ is a full platform for that! WYSIWYG editor and all :-)
This stay valid js without mixed case found in usual code in the wild sticking to ascii. To my mind it feels like avoidable visual clutter, all the more in didactic work.
Apart from that, it was nicely done all the way, congratulations and thanks for the pleasing moment.
This may be a semantic issue, where the author is asking if it accurately predicts halting for a single input.
But that is not the definition of the "halting problem".
The format is effective and interesting. But it does need some edits/clarifications.
A good introduction to this subject is the book “Type Driven Development in Idris” or one of the Agda books.
In any case, you don't need dependent types for a compiler to prove termination, it's just that most languages don't care about termination except those with dependent types. You could create a compiler for Rust that has similar termination checking to Coq, if you wanted.
> Turing famously showed that computers can’t decide whether your code halts.
I would say this is actually false, even though almost everybody thinks it's true. At least, if you're interested in actually solving problems rather than being interested in what is mostly a mathematical/theoretical curiosity.
The Halting Problem is famously only undecidable if the code you're analyzing is being modeled on a "Turing machine" or something equally "powerful" to it. The problem is, computers are not as powerful as Turing machines, and furthermore, Turing machines (or something equivalent to them) neither exist nor can ever exist in practice, because it's impossible to build a "machine" with truly infinite memory.
In fact, if the machine where the code is running has finite memory, then the Halting problem is actually very easily solved (well, in theory). And there already exists various known algorithms that detect cycles of values (where the "value" in this context is the state of the program):
https://en.wikipedia.org/wiki/Cycle_detection
As you can see, if you use one of these cycle detection algorithms, then the Halting Problem is not undecidable. It's easily solvable. The problem is that, while these known algorithms are able to solve the problem in constant memory, there are no known algorithms to solve it in a time-efficient way yet. But again, it is decidable, not undecidable.
Now, I understand how Turing machines as a model can be useful, as the simplifying assumption of never having to worry about a memory limit might allow you to more easily do types of analysis that could be more difficult to do otherwise. And sure, the way the Halting Problem was "solved" was very clever (and I actually suspect that's a major reason why it has reached its current legendary status).
But this simplifying assumption should have never allowed a result like the Halting Problem which is known to be wrong for the type of computing that we actually care about to be elevated to the status that it currently has, and by that I mean, to mislead everyone into thinking that the result applies to actual computers.
So again, I would say, be careful whenever you see a Turing machine being mentioned. I would say it would be better to view them as mostly a mathematical/theoretical curiosity. And yes, they can also be a powerful and useful tool IF you understand its limitations. But you should never confuse this model for what actually is the real world.
> Henry Rice proved a much more devastating result: “computers can’t decide anything interesting about your code’s input-output!”
Since Rice's theorem (and many other computer science results!) depends on the Halting Problem being true, while it is actually false for real-world machines, my understanding is that Rice's theorem is also false for real-world machines.
But Rice's theorem (and sentences like the article is using) is absolutely another example of a huge number of cases where the Halting Problem has seemingly mislead almost everyone into thinking that something can't be solved when it actually can be solved.
I wonder how much more research could have advanced (like for example, in SMT solvers, formal methods, etc) if everyone actually believed that it's possible for an algorithm to decide whether your program has a bug in it.
How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case?
Now, I'm not a computer scientist nor a mathematician or logician. So I could be wrong. If so, I would be interested in knowing how I'm wrong, as I've never seen this issue being discussed in a thorough way.
Edit: another (according to my understanding) completely misleading phrase in the tutorial exemplifying what I'm describing:
> we learned Turing’s proof that halts is actually impossible to implement: any implementation you write will have a bug!
Now, to be clear I'm not blaming the author of the tutorial, as this is just one very tiny example of what actually is an extremely widespread belief across the whole industry.
Is that actually proven?
Or is it possible that in fact, there might be an efficient algorithm for solving the halting problem in practice for computers, but it's just that we haven't discovered it yet?
Just because the state space is big doesn't mean that there aren't shortcuts to figure out in a much more efficient way whether a program loops forever.
It seems incredibly likely that this question has a complexity of O(exp(N)) which very quickly makes the halting problem infeasible to solve for modern computers.
That's an oxymoron, because Turing machines have a state space of infinite bits by definition. I understand you mean "deterministic finite-state machines" rather than "Turing machines".
> It seems incredibly likely that this question has a complexity of O(exp(N)) which very quickly makes the halting problem infeasible to solve for modern computers.
I mean, I agree that it's likely, but again, is this proven?
I'm not aware that it is and therefore I think this is actually missing many of the points I mentioned.
It could be false for all we know.
I meant "Turing machines with X states and a type limited to Y bits, with X + Y = N". You can, of course, cast those as Deterministic Finite State Machines, but that will require incredibly many states.
Could we solve it without brute force? Well, there are plenty of math problems we can’t prove; we can write a program that only halts if counter example is found, and we would be unable to prove if the program halts. We can also write program that will halt if it can prove ZF set theory is false, but we already know it’s impossible to prove that (it only possible to prove it is false). So symbolically deciding if a program halts is also impossible in the general case.
Yes, but again, you're missing my point: you would be able to prove if the program halts.
It's just that in this particular case it would not necessarily be useful, because it just might happen that to solve the mathematical problem it would require more memory than you have available.
So if the halting detector says: "the program halted due to running out of memory", the results would be inconclusive for answering a difficult mathematical problem.
But that's not what most programs do, in fact, the vast majority of programs would benefit immensely from knowing whether they will exceed some finite memory limit.
> We can also write program that will halt if it can prove ZF set theory is false, but we already know it’s impossible to prove that (it only possible to prove it is false).
The same point above applies.
> So symbolically deciding if a program halts is also impossible in the general case.
No, it's not. You completely missed my point. It is 100% decidable. It's only undecidable if you're imagining running this program on an imaginary machine which cannot physically be constructed.
Attempting to overflow it is impractical using cpu cache memory sizes, no hard drive needed. No matter how fast you go through states, there are too many possible states in the cpu, and too many states even a small program can iterate through while still eventually terminating.
What limitations of math exactly? What you're talking about is not related to efficiency of solving the Halting problem on a machine with a finite number of states.
> Attempting to overflow it is impractical using cpu cache memory sizes, no hard drive needed. No matter how fast you go through states, there are too many possible states in the cpu, and too many states even a small program can iterate through while still eventually terminating.
You are assuming that you have to simulate going through all the running states of a program to determine whether it halts or not.
Why do you assume that you have to run a complete simulation of the program to analyze it?
see if you follow this one one, for a real computer:
Suppose I pick a n bit key, and encrypt a phrase with it. I will provide you the plain text phrase and either a real or fake cipher text. You have to determine if a program which loops through all the keys will decrypt the ciphertext into a the phrase.
Either you know weaknesses in the crypto system, or you have no choice but to iterate though each key to see if the output matches the phrase.
There is a relationship with proof of work crypto as well. Even all the Bitcoin mining has trouble finding hashes with a certain number of leading zeroes, add a few more zeros and no one will ever find a working seed again. There is no way to speed up the process beyond iterating over the seeds.
You can tie this to the halting problem by just saying to go back the key 0 once the key space is exhausted.
> There is a relationship with proof of work crypto as well. Even all the Bitcoin mining has trouble finding hashes with a certain number of leading zeroes, add a few more zeros and no one will ever find a working seed again.
Yup, I know. But here's the part I think you're missing:
None of those crypto systems you're mentioning are proven not to have weaknesses. In fact, weaknesses in hashing and encryption algorithms are encountered every now and then, even for those that have been considered state-of-the-art.
So yes, I agree that in practice we don't know how to solve this problem efficiently yet. Which means it's currently impractical, and would currently requiring brute forcing through all the states.
But I haven't seen a proof that it's not possible to find a practical algorithm.
There are also lesser problems that have been around a while which we haven’t been able to prove, but might be provable… you can iterate over numbers looking for an counter example to the Collatz conjecture… I think that’s the best example of a simple program that is outside our current knowledge of math (better than the crypto one), but maybe someday we will have an answer.
Furthermore, it is true that computers have a finite number of states, but this number is intractable for most problems in verification. There are several well known cryptographic problems that take on the order of the lifetime of the universe to solve in bounded memory... if you're trying to write a program to verify one of these algorithms the boundedness of memory will probably not help you much.
I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever.
In fact, this would be a huge, huge deal if you could solve it in an efficient way.
> There are several well known cryptographic problems that take on the order of the lifetime of the universe to solve in bounded memory... if you're trying to write a program to verify one of these algorithms the boundedness of memory will probably not help you much.
I think you missed one of my points:
> while these known algorithms are able to solve the problem in constant memory, there are no known algorithms to solve it in a time-efficient way yet
Yet being the key word here. As far as I know it's not proven that it's impossible to build a time-efficient algorithm, only that (as far as I understand) it's unlikely unless P=NP. But we don't know whether P=NP.
And there's another issue here as well: I'm not even sure if P=NP actually has any meaning in this context, because I assume issues related to P=NP are usually analyzed in the context of Turing machines.
This actually ties into the other point I mentioned:
> How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case?
Fair for many applications. I work with computers that write proofs.
> Yet being the key word here. As far as I know it's not proven that it's impossible to build a time-efficient algorithm, only that (as far as I understand) it's unlikely unless P=NP. But there's another issue here as well: we don't know whether P=NP.
There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem.
> How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case?
Well, not me! Formal methods and program synthesis are alive and well, but it's important to researchers in these areas to understand what parts of our work are decidable and what aren't. I should mention that Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, and tailoring tools to real user patterns can really blunt the problem of undecidability in practical use cases.
I mentioned this in another comment: isn't EXPTIME only defined for Turing machines?
Which again, just touches on all of my points.
For all we know, if you've reached the conclusion that an algorithm's complexity is EXPTIME, this conclusion could be just as false as the Halting problem and Rice's theorem are for real-world computers.
> Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable,
My point is that you shouldn't believe that the theories are undecidable because those analysis were done using Turing machines as models.
And the other point is that sure, there are many people doing formal methods, etc. But how many more would there be if most people believed the problem to be solvable?
- There's a subtle difference between "infinite" and "unbounded". Turing machines use at most a finite amount of memory after any finite amount of steps (the tape always ends in an infinite sequence of empty cells), so a machine which starts with one cell and allocates one new cell every step is equivalent to a TM.
- Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity.
- We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe.
- Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. No stronger method of computation which can also be physically implemented is known to exist.
edit: typo
Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me.
So I'm not 100% sure that those measures of complexity have the same real-world meaning, for similar reasons.
> - We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe.
Yes, but even in that case, the amount of memory would be finite. Because the universe is expanding faster than the speed of light, there's only a finite amount of energy that is accessible at any point of spacetime (as far as I understand).
So even in theory you can't say the amount of memory can scale infinitely (not to mention in practice).
> - Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable.
The theories are undecidable only if you assume a model of computation with infinite memory. Which can be interesting from the mathematical point of view, but not for applying those results to real-world problems, because now you've made a grave mistake: you believe something is undecidable when it is in fact decidable.
I mean, sure, I can also invent a new super-duper-amazing model of computation that is even more powerful than Turing machines and can perform incredible Oracle-like feats and, say, run all programs in constant-time (yeah!), but it would not be correct to say that all the results obtained in this model apply to the real world.
If an SMT solver is trying to prove that my program has a bug, even though some theory says that the problem is undecidable if my program was running on a theoretical Turing machine, this is meaningless to me (and quite misleading) because the problem is actually decidable given that my program is going to run on a computer.
> No stronger method of computation which can also be physically implemented is known to exist.
You say that like Turing machines can be physically implemented.
What made it decidable was rather the fact that you did not use all of the power that your programming language makes available to you, you did not steer the program last the bounds where the heuristics work.
This kind of becomes a little more obvious when you port Turing’s proof of the halting theorem to a “normal” programming language. The thing you immediately notice is a type error, “does the analyzer halt when given itself as an input?”... well, it doesn't know what to do, it was expecting an argument of type `ParseTree x` for some x and you handed it an argument of type `∀x. ParseTree x → Bool`...
To get around this and build the liar paradox which makes the proof “go,” is not too hard: but you are basically forced to produce a quine instead and those techniques are non-trivial. In our normal programming lives, you could apply a heuristic that assumes we never do such things, and life is good.
The focus on finite versus infinite memory is a huge distraction. If your halting detector applied to the above quine tried to not be a heuristic by salvaging the case where it runs out of memory while analyzing, you would get the result “this program will OOM, but if you run me in a machine with 1 meg less memory I will stop an odd number of cycles earlier and the program will not OOM, but will instead halt successfully telling you that the next cycle would OOM.” Suddenly your tests that you build with this thing are all flaky, because it didn't have the humility to be a heuristic and say “I don't know this is too complex for me,” and in the real world you are running on Linux and you don't know how many megs you really have available. Better just to not play any of that game.
So yeah the problem with Turing machines is not that they have infinite memory, infinite memory is in fact a standard assumption that most programmers in GCed languages make when programming most of their programs. This is why “your problem isn't the garbage collector, it's that you're swimming in garbage” and all that.
Put another way, Turing machines suck even if you enhance them to have 5 parallel tapes (God why do they not have parallel tapes by default, should have at least one for output, one for main memory, one for a stack, and some more as scratchpads) of bytes (seriously why are they still not bytes in textbooks) and enforce that the tapes each only have 1 billion symbols and any attempt to go off the edge crashes the Turing machine. You are joyous because it now only has finite memory, I can run a cycle detection with 10^{1 billion} nodes in the graph or whatever, so cycle detection is in principle solved! If you are as pragmatic as you say you are, you see that this is no help, halting is still effectively impossible.
You answered your question as you asked it. If you juice up your Turing machine like that, it will still suck so much that nobody will actually write programs for it, but it will be more complicated to describe and analyse.
But for those who may not know, you can emulate an n-tape Turing machine with a single-tape one, they are computationally equivalent (and in fact, there is no stronger model of computability)
Of course. Why would you do that? You don't have to.
You can write a program in a Turing-complete language and yet analyze how it will run on a machine with a finite amount of memory.
For example, when you analyze cycle detection algorithms, which assume that the program being analyzed runs on a machine with a finite amount of states (even if it is implemented in a Turing-complete language), you don't do any of that.
And the currently-known algorithms are very simple to analyze.
And what does that say about the problem, that current SMT solvers fail?
It only implies that it's a difficult problem to solve (i.e. that the time complexity may be large, possibly), but it doesn't prove that it necessarily has to be that way.
> (And that's more or less the claim of the halting theorem, not that nothing useful can be done, but that anything done can only be heuristic.)
I don't think the Halting problem proves anything about the complexity of the problem or whether you can only apply heuristics and not solve the problem in a principled way. In fact, cycle detection algorithms work deterministically, without any use of heuristics.
The proof of the Halting problem only works because in Turing machines, programs are allowed to consume memory infinitely without ever running into a cycle. If you don't allow that, then the Halting theorem doesn't say anything.
> This kind of becomes a little more obvious when you port Turing’s proof of the halting theorem to a “normal” programming language
You mean, Turing-complete languages. In which case I agree, normal programming languages also make the simplifying assumption that the computer has infinite memory.
Which is actually OK!
That these programs are written in such languages doesn't prevent an algorithm from determining whether an arbitrary program written in such a language will halt or not, if it were to be executed in a machine with a finite amount of memory.
> you would get the result “this program will OOM, but if you run me in a machine with 1 meg less memory I will stop an odd number of cycles earlier and the program will not OOM, but will instead halt successfully telling you that the next cycle would OOM.”
Yes, exactly!
> Suddenly your tests that you build with this thing are all flaky, because it didn't have the humility to be a heuristic and say “I don't know this is too complex for me,” and in the real world you are running on Linux and you don't know how many megs you really have available. Better just to not play any of that game.
Actually, I would argue that it would be immensely useful to be able to run such a tool and that it would tell me:
"Hey, your program will OOM even if you run it with 1 TB of memory!"
Or even, say, 16 GB of memory.
Of course, with this value being configurable. And also, take into consideration that you'd be able to know exactly why that happens.
> So yeah the problem with Turing machines is not that they have infinite memory, infinite memory is in fact a standard assumption that most programmers in GCed languages make when programming most of their programs.
Yes, and I see nothing wrong with that. Although I would like a tool like described above which would determine whether my program is buggy.
> Put another way, Turing machines suck even if you enhance them to have 5 parallel tapes (God why do they not have parallel tapes by default, should have at least one for output, one for main memory, one for a stack, and some more as scratchpads) of bytes (seriously why are they still not bytes in textbooks) and enforce that the tapes each only have 1 billion symbols and any attempt to go off the edge crashes the Turing machine
Sure, but why would you do that? When analyzing cycle detection algorithms (which assume a finite amount of possible states) you don't do any of that crap :)
> You are joyous because it now only has finite memory, I can run a cycle detection with 10^{1 billion} nodes in the graph or whatever, so cycle detection is in principle solved! If you are as pragmatic as you say you are, you see that this is no help, halting is still effectively impossible.
Yes, it's solved! Awesome!
Not let's focus on how to reduce the time complexity, which is the actual important problem!
And don't assume that cycle detection needs to run a program step by step through all of the states of the program.
By your definition, all problems of the form “does program X have property Y” are decidable, because you can just simulate X on all possible inputs until it halts or cycles, and observe whether Y holds in each case.
Yes! Thank you! That's exactly what I'm saying.
Now the question is: how can we do this without having to simulate running the program step-by-step on all possible inputs?
Or in other words, how can we reduce the time complexity of the currently-known algorithms for solving this problem?
That's the actual interesting question!
I suppose we could pick a very large resource number N (allocatable between time and memory space?) and agree that we will create a large body of math and algorithms with the assumption of that limit, so all our theorems and programs within that finite math area are consistent.
But a great deal of math would have to be reconsidered every time N was increased.
Why do you believe that?
The existence of the cycle detection algorithms that I mentioned earlier don't assume any particular number N and yet they prove that the problem is decidable as long as N is assumed to be a finite number.
Why?
Why are you assuming that the only way to figure out if a program halts is by simulating running it step by step?
And not by analyzing the description of the program?
So, will you believe that these people (I believe Gödel was praised highly by even Neumann!) weren’t talking out of their asses? :D
What does that have to do with how long a specific algorithm takes to run?
So you're saying that there are only 2 options:
1. You either simulate running the program step-by-step (which has an extreme time complexity problem).
2. Or, you try to analyze it within some system of logic. But if you do so, then there are things that you can't prove because logic itself can't prove certain statements.
This is an interesting argument. But I think point 1 sort of disproves point 2.
Point 1 means that you can always analyze such programs, it's just that it might take a really long time to achieve that.
So I think point 2 is not valid in this specific context. Because you can always prove whatever you want (given that when you simulate running a program, you are necessarily doing it within a system of logic), it's just that we don't know how long that could take in theory (of course, in practice, it's currently intractable).
So if you can always prove whatever you want, that means Godel's results about the undecidability of certain statements don't apply when analyzing finite-state computation systems, only infinite ones.
Great. And the entire field of static analysis is available for you to do this. But when discussing the formal consequences of the halting problem it is just completely pedantic to show up and point out that actually you can run Coverity and it'll spit out some pretty useful results on most programs.
I'm glad that my points were so clear and obvious to you!
>> How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case?
Few if any, as those who are good enough have no difficulty understanding both the seminal importance of Turing's work and the realities of actual computing devices.
Yes, it halts No, it loops forever Can't decide.
Wouldn't that still be useful in practice?
Especially if "can't decide" means "can't decide using the resources limit you provided" so that the test returns consistent results. (As apposed to different results depending on the differing resources between machines the test ran on.)
while(random() != 0) {
wait(1second);
}
You can use cycle detection to reject programs that have cycles as "may halt" but not "will halt"
Now if you were to use a pseudo-random generator, and presume that this is the only function sampling from it, then all of a sudden the halting problem for this generator is well-defined. It also becomes a very simple question about the pseudo-random generator. If the random() function is truly random, then you are talking about a machine more powerful than a turing machine.
For cryptographic quality random generators, I am not sure how much is known.
In any case, the question is a simple one, though answering it can be difficult in some cases.
By the time hierarchy theorem, class P (polynomial time algorithms) is a strict subset of EXPTIME.
Accordingly, this proves that in your suggested finite machine, the halting program cannot be solved by a polynomial time algorithm.
Isn't EXPTIME completeness only defined for Turing machines?
Which again, just proves all of my points.
For all we know, if you've reached the conclusion that an algorithm is EXPTIME-complete, this conclusion could be just as false as the Halting problem and Rice's theorem are for real-world computers.
Can you point me somewhere that proves this exact statement you're making? Or at least, explains why it is true.
I'm interested in reading about it.
I mean, assuming you are correct (and I have no reason to believe you aren't) it still doesn't guarantee that the problem is intractable (as EXPTIME-complete algorithms can still run very quickly in practice), but yes, I think it would suggest that it is intractable (for real-word applications).
https://www.quantamagazine.org/the-busy-beaver-game-illumina...
The busy beaver problem, again, assumes it is running on a Turing machine with infinite memory.
Don't confuse a program defined using a finite number of states with a machine that can only have a finite number of states. It's just another example of the points I'm making about how a theoretical mathematical problem is an interesting curiosity and might even be an interesting problem to solve but it does not necessarily apply to the real world. And how everyone seems to think that this mathematical problem applies to programs running in real-world computers.
Someone else mentioned the busy beaver problem and I've given a more complete answer there:
In the real world, a program will either halt, loop, or crash, but this doesn’t help us if a 6 instruction program can take longer than the age of the universe to run while still terminating. No matter how fast you go through its states. 64mb leaves a lot of room for unique states without a cycle.
Why do you assume that you have to go through all the states of the program to determine whether it will run into a cycle?
To not believe my assumption would require you to believe that such algorithms do not exist.
Since the assumption has not been proven, this is why the foundation of cryptography is still on a bit of a shaky ground, as none of those algorithms are proven to be unbeatable (the one-time pad being the exception, although it's not very useful in practice).
It's probably also why weaknesses in cryptographic algorithms are still being discovered every now and then, unfortunately.
However, it is simple to show that this is at least as hard as NP complete. For instance, you can map the Hamiltonian cycle problem to a halting problem over programs that do an infinite walk on graphs without a Hamiltonian cycle and those that stop whenever they complete a walk along a Ham cycle.
At this time P vs NP is still wide open and, in general, statements in complexity theory are usually dependent on some unproven hypothesis so I still don't understand what is your point exactly.
Among other things, because the P vs NP issue is still wide open, yes.
I'd just like to add three more minor points:
1. Many people believe the above to be false, because they believe that the problem is undecidable also for programs with a bounded number of states.
2. That I would like if more people focused on finding such an efficient algorithm.
3. And that I think that even some people who believe that the problem is decidable think that it's impossible to have an efficient algorithm because of the Halting problem and Rice's theorem, which formally speaking, neither of them say anything about whether such efficient algorithms exist or not.
The P vs NP question is open but the conditional results are not merely novelties. There are many results that show very weird consequences for having P=NP. So either the nature of computing is utterly bizarre or in fact there are many common problems which are simply impossible to solve exactly in a reasonable amount of time.
You can of course try to find good heuristics that cover some common cases or even approximations of NP hard problems in some cases. There are literally thousands of researchers doing that every day.
I hope you are correct :-)
> There are many results that show very weird consequences for having P=NP. So either the nature of computing is utterly bizarre or in fact there are many common problems which are simply impossible to solve exactly in a reasonable amount of time.
Wow, that's very interesting! Can you recall an example or two of such consequences? I would be really interested in reading about that.
Edit: Donald Knuth seems to believe that P=NP and also says there would be no major implications if we found such a proof...
> You can of course try to find good heuristics that cover some common cases or even approximations of NP hard problems in some cases. There are literally thousands of researchers doing that every day.
Completely agreed!
Perhaps you are right and my worries are unfounded.
A nice presentation by Wigderson may also help to see consequences of P=NP in a less rigorous phrasing ("'Creativity' can be efficiently automated [if P=NP]"). https://view.officeapps.live.com/op/view.aspx?src=https%3A%2... There is a more formal text as well: https://www.math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/W06/w06....
Another class of results that I find interesting are inapproximability results. Namely, for certain NP hard problems, it is impossible to have a polynomial algorithm that computes the right value (for all instances) within a certain approximation factor unless P=NP. In https://dl.acm.org/doi/10.1145/1132516.1132612 Zuckerman shows that approximating MAX-CLIQUE is hopeless unless P=NP.
This is of course just a mountain of evidence and not a proof. It does mean that there are potentially many ways in which one could prove P=NP without necessarily achieving anything practical. This is what I think Knuth means: you could have a non-constructive proof of P=NP or perhaps an algorithm with complexity n^10^10^10 that solves an NP-complete problem.
[1] https://cs.stackexchange.com/questions/112684/halting-proble...
I'm following so far.
> This is in EXPTIME [1][2] given that the input n is encoded in log(n) bit.
Perhaps I'm reading this incorrectly, but these proofs seem to assume that you're simulating the machine running step by step?
Is it proven that the only way to solve the bounded Halting problem is by running the program step by step?
If not, it seems that this is only proving a high complexity bound (i.e. that the problem is not more complex that EXPTIME), not a low bound (i.e. that the problem can be solved in less complexity than EXPTIME).
I routinely solve instances of problems in EXPTIME to solve practical problems with no difficulty…
But often mathematical models are more informative and interesting than the concrete physical objects they abstract.
Yes, I agree.
But a model of a machine with finite states is more informative and interesting for applying it to real-world computers than a model of a Turing machine.
Why? Because the first model tells you the Halting problem is decidable and the second one tells you it's undecidable. And as I mentioned, for programs running on real-world computers the Halting problem is decidable.
I don't agree at all. I do static analysis for my career. Trying to model the actual set of available memory configurations of a physical machine is going to scale way way way worse for most meaningful problems than approaching this the usual way.
I don't really understand your argument.
I didn't say anything about how you need to solve problems like those described by the Halting problem and Rice's theorem for finite-state machines.
So I'm not constraining how you would have to solve this issue. You can model the memory configuration if you want. But you don't have to model it in your algorithm. It's just that your algorithm is allowed to assume that the amount of memory available for the program being analyzed is finite (if it wants to).
But anyway, the complexity / efficiency of an algorithm that solves the problem is a different issue that than the decidability of the problem, the latter of which many people get it wrong.
What I am saying is that in practice, for the huge majority of interesting problems, it is not useful to finitize the actual program but instead to abstract over the program that assumes no meaningful resource constraints. Wandering off down a road of looking for efficient algorithms that take advantage of the actual finite nature of real programs will only harm you in the enormous majority of cases.
> But anyway, the complexity / efficiency of an algorithm that solves the problem is a different issue that than the decidability of the problem, the latter of which many people get it wrong.
Again, people only "get it wrong" if you are being maximally pedantic in a way that provides negative value to thinking about these problems.
You may very well be correct, but there's no formal result that proves that, right? So your assertion could be wrong.
> Again, people only "get it wrong" if you are being maximally pedantic in a way that provides negative value to thinking about these problems.
If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms.
Fortunately, some people have proven that these algorithms exist and have created such algorithms. Some have even created new such algorithms, improving their efficiency.
I just want more people to try and find more efficient versions of those, which is why we should not be spreading mistaken beliefs that the Halting problem is undecidable when a program runs on a computer.
Which is why I would argue, in fact, that saying the Halting problem is undecidable is what provides negative value, because this is only of theoretical interest and generally speaking, it's only a useful result in practice if the program you're analyzing is trying to solve a mathematical question (i.e. one about infinity).
For most real-world programs, the question of whether they would halt (or whether they behave correctly, in general) if they weren't allowed to consume infinite memory is much more interesting and useful, and actually decidable!
So let's focus instead on improving the time complexity of such algorithms. Let's not focus on saying that they are impossible to solve, which prevents from focusing on the former.
GP wasn’t making a formal statement, so of course there isn’t. They were making an intuitive judgment about which of two mathematical theories corresponds more usefully to the real world.
> If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms.
This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible.
Ok, I see your points.
> This is a non-sequitur because the non-decidability of the halting problem doesn’t imply anything about whether cycle-detection algorithms are possible.
It doesn't?
I thought the halting problem was the problem of constructing an algorithm that decides whether a machine that runs an arbitrary program will keep cycling between states or not (which in the case of a Turing machine, includes the state of the tape).
If you say it's undecidable, it implies no such algorithm can exist.
It implies (rather, it’s just another way of saying) that no strictly correct algorithm can exist for detecting cycles on the state-space graphs of arbitrary Turing machines.
It does not imply that “cycle detection” is an impossible task under any circumstances, possibly on different classes of graphs, or possibly sacrificing strict correctness.
I honestly think you understand this and are just being intentionally obtuse.
Yes, what you said is strictly correct, but that's not how the Halting problem is usually presented nor how it is usually understood.
Normally, you don't hear people saying: "the Halting problem is undecidable for Turing machines", and that's it, everybody understands what's going on and the limitations of that statement.
Instead, it is usually said: "The Halting problem is undecidable". And then they say: "Here, let me show you that it's undecidable using this clever proof, which uses a Turing machine as a model".
And then, more crucially, they don't say "But of course, this proof is completely wrong if you assume that the program runs on a finite-state machine. And not just that, but it is proven that it is decidable in such circumstances".
> I honestly think you understand this and are just being intentionally obtuse.
I understand in general, but I might misunderstand particular statements in some precise way. I'm not intentionally being obtuse, I promise you.
There's a lot of nuance in this topic and when we're not being mathematically precise it's easy to misunderstand each other.
Of course they don’t, because it’s extremely obvious that it’s decidable for finite state machines.
However, in practical terms computers are more usefully modeled as Turing machines than as FSMs (yes, even though pedantically speaking they are FSMs).
Wow, that's quite an interesting statement to make. And it doesn't explain dozens and dozens of statements that I've read over the years implying that people don't actually understand this.
Hell, even the tutorial that this post is about claims the following, right in the beginning:
> Turing famously showed that computers can’t decide whether your code halts.
Which, of course, is not true, unless you interpret this in a bit of a twisted way by imagining that the algorithm that does the halting analysis is running on a computer but it is only allowed to analyze the program as if it were running on a Turing machine, which is the least useful way to solve this problem.
> However, in practical terms computers are more usefully modeled as Turing machines than as FSMs
I'd argue the exact opposite, because it's obvious that if you do that, it will result in you proving that something is true when for what the real-world cases we care about it is actually false, as well as the "true" proof not actually being useful for almost anything interesting (except math-related results having to do with infinity).
But since you truly understand the implications, then I accept your difference of opinion.
I'm truly interested in hearing your reasoning beyond "it is obvious to me." What background do you have in this field? Because if we wander over to the papers published in SAS we can look through the ways in which various systems model programs and they do not choose to model physical computers as FSMs. We've got decades of people thinking hard about this problem who've come down on the complete opposite side as you. Maybe literally the entire field is wrong about this. I doubt it.
But they do a huge simplifying assumption which is that the program can use an infinite amount of memory.
This is OK in some cases, but it is not OK in others, especially when it comes to analyzing decidability (of programs that are not trying to compute mathematical answers, i.e. answers with infinite bounds).
For example, I think it is immensely useful to model computer programs in Turing-complete languages. I see no major reason why we should always use programming languages with enforced memory limits at the language level, currently.
Because, it's one thing to write a program, and it's another thing to execute it.
So, I'm not saying Turing machines are always inadequate. But I wish we would be more careful using them, so as to not make fundamental mistakes about what is true and what is false for important things that we actually care about (rather than strictly theoretical questions about programs that we will never be able to run successfully).
The entire thread started off by you rejecting the formalism provided by folks like Turing in favor of the practical argument. I'm speaking from a practical perspective of building actual static analysis tools. When writing real systems, considering things like "oh well actually there is a stack depth limit" is zero help at best.
> If everyone believed that the Halting problem is undecidable, then nobody would even try to find cycle detection algorithms.
No that's not true. Not at all. We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice. We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems.
There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time. Actual deployed algorithms have some number of false positives or false negatives (or both).
That's not what I'm arguing at all. I'm arguing that as long as you restrict the programs being analyzed to the subset of programs that use a finite amount of memory (i.e. those that can run on a computer), then all so-called undecidable theories suddenly become decidable. And that this could be a property that we could perhaps exploit to analyze programs more efficiently.
But you don't have to make your models more complicated. It's simply a property that you can exploit, whenever you want to.
> We write static analyses that operate on abstractions of a program, which will generate some false positives or false negatives for whatever thing we are looking for but end up with a system that works well in practice.
Exactly. Wouldn't it be better if you could always have true positives and true negatives?
To be clear, I'm not saying that we can do this right now. But it's an avenue worth pursuing, IMHO.
> We have not "solved the Halting Problem" nor do we believe that it is actually decidable when we build these systems.
It is decidable, that's my entire point! If there's a finite amount of memory, the theories become decidable!
Perhaps you're just confusing time complexity with decidability?
> There is no cycle detection algorithm (of actual program semantics - not finding loops in CFGs or whatever) that will never produce a false positive or a false negative that runs on all possible programs and terminates in anything resembling a reasonable time.
Exactly, there isn't! Which is why we should find one that terminates in a reasonable amount of time. That's what I'm arguing.
> Actual deployed algorithms have some number of false positives or false negatives (or both).
Agreed.
Well this one is just plain wrong. It is "if my grandmother had wheels she'd be a lawnmower." What you are saying is "if you change the problem, the properties of the problem change." Yes, the set of turing machines that halt in fewer than some fixed N steps is decidable. This is not interesting. It is pedantry.
> Exactly. Wouldn't it be better if you could always have true positives and true negatives? To be clear, I'm not saying that we can do this right now. But it's an avenue worth pursuing, IMHO.
But it isn't. And I've told you. You'll increase the running time of useful programs by hideous amounts. Like "won't finish executing until the universe ends" amounts.
> Perhaps you're just confusing time complexity with decidability?
I am not.
That is NOT the problem I mentioned. Programs that use a finite amount of memory do not necessarily halt, ever!
But the problem I mentioned is also decidable. We already know of algorithms that can always determine if a program that uses a finite amount of memory halts or not.
> This is not interesting. It is pedantry.
Actually, what is not interesting is analyzing problems that can only exist on super-powerful imaginary machines (i.e. with a truly mathematically infinite tape, which is a very absurd feature to have) that do not fundamentally represent what computers can do.
In the real world, truly infinitely-large things (and I'm talking about true mathematical infinity) cannot ever exist or be built. And even if they were to exist, they would never be accessible to us.
So I'd prefer to have a model of computation that functionally represents what computers can actually do and then extract my conclusions using this model (in which many problems are decidable), rather than an imaginary super-powerful model which actually has more limitations (as many problems are undecidable) than models of computers.
I mean, if you like solving imaginary problems that do not represent what can exist or be built in the real world, I mean, sure, fine, that's OK with me. But if you use such an absurd model, then don't extract absurd conclusions and then tell me that these conclusions apply to real computers.
> But it isn't. And I've told you. You'll increase the running time of useful programs by hideous amounts. Like "won't finish executing until the universe ends" amounts.
No. Restricting yourself to analyzing a subset of problems does not "increase the running time" of anything.
Why? Because you can use the same algorithms that work for analyzing programs that use infinite memory (the undecidable ones) and you can also use additional algorithms that only work for programs that use finite memory (the decidable ones).
Which means that you have additional tools at your disposal, which means that the problem can be solved in an equal or better way.
To be clear, I'm not saying that we currently know of such efficient algorithms that only work for programs that use finite memory.
I'm saying that it might be possible to create such algorithms given that the problem is decidable.
You keep insisting that this reframing can somehow lead to more efficient practical systems. It will not. As evidence, I point to five decades of research on practical static analysis where nobody has come to the conclusion that explicitly modeling the finite nature of real computers is useful in the slightest. The "additional tools at your disposal" are literally useless.
And if you ignore this property (as you now mention) then what have you gained through your reframing? Nothing. All you've done is added additional complexity to a problem formulation for no gain.
You keep hiding behind "might." This is just magical thinking.
But I will disagree with you on "it's not theoretically interesting".
Almost the entire field of computer science is based on Turing machines and on the following definition of "computable function": "computable functions are exactly the functions that can be calculated using a mechanical calculation device given unlimited amounts of time and storage space".
Now, of course, I can argue that this definition of computable function and Turing machines are ridiculous and will lead to ridiculous conclusions, but I think I already did that elsewhere, so let's move on.
Now imagine that instead of Turing machines, computer science would use deterministic linear bounded automatons (deterministic LBAs, which are the closest finite approximation of Turing machines).
And instead of that definition of computable function, let's use this one: "computable functions are exactly the functions that can be calculated using a mechanical calculation device given unlimited amounts of time but limited amounts of storage space".
What would be different in computer science?
Well, at least the following would be different:
1. The Halting problem becomes decidable
2. Rice's theorem becomes false, which means we can decide properties about computable functions.
3. As an example, perhaps you're familiar with the busy beaver problem, which is defined over Turing machines and is a function of N, where N is the number of states of the Turing machine. It is impossible to create an algorithm to decide whether a Turing machine is a busy beaver.
If you defined the busy beaver problem over deterministic linear bounded automatons (LBAs) adding an additional parameter K for the length of the tape, then suddenly it becomes possible to create an algorithm that determines whether a given LBA is a busy beaver!
Similarly, the busy beaver function is defined over Turing machines and is a function of N (where N = number of states).
In my redesigned field of computer science, the busy beaver function would also be defined over deterministic LBAs and would be a function of N and K, where N is the same as above, and K is the length of the LBA tape.
This would also have interesting consequences.
First of all, the busy beaver function would become a computable function instead of non-computable.
It would also become more meaningful in the real world, because we could answer the question: my computer has K bits, how many 1 bits could a halting program with N states write?
And you would still be able to answer the original questions about the original busy beaver, which you would realize is not a computing question, but it is actually a mathematical question concerning infinite Ks, which is: "for a fixed N and for all K, what is max(busy_beaver_function(N, K))?".
There's also an interesting additional mathematical question that would come up: for all N and for all K, is it true that if busy_beaver_function(N, K) = busy_beaver_function(N, K+1) then there is no J such that busy_beaver_function(N, J) > busy_beaver_function(N, K)?
In other words, if you increase K and the busy beaver function gives you the same result, does that mean that there is no point in increasing K any more because no higher K will give you a larger result?
What if you step-wise increase K by multiplying by 2 instead of adding 1?
Presumably, the above questions have to be false, otherwise the original busy beaver function would be computable, but it would still be interesting to have separate proofs, which could lead to new insights, especially if you didn't know that the original busy beaver function was non-computable!
All sorts of similar reasoning would apply to all sorts of other problems. Many undecidable problems become decidable. Many non-computable functions would become computable. Many questions that were previously about Turing machines suddenly become more meaningful for actual computers. You would naturally ask more interesting (finite and infinite) questions as functions of state size.
And, you could still answer the same mathematical questions about them (that we currently use Turing machines for), just by introducing a "for all" quantifier in the state size. Which would also make many things a lot clearer.
I could go on and on.
(To be clear: a computable function does not imply that it can be efficiently computed, i.e. computed within a reasonable amount of time. This is true both for the current definition and my definition).
You need to read this book:
https://www.amazon.com/Quantum-Computing-since-Democritus-Aa...
(The title notwithstanding, this book is about a lot more than just quantum computing. In particular, it is about computational complexity theory, which is exactly where your line of inquiry leads. It is a very productive area of research.)
I think that’s what makes computability theory interesting, especially if you add that our very Mathematics “break down” at a “trivially” small scale and that Turing machines will happily go on and on, literally being mathematically reasoned about, because we hit the edges of it sooner!
Not the whole universe, exactly. Just the parts that are possible to access :)
> I’m not really sure it is a good rebuke of the Halting problem that “we can brute force our way out of it”.
Why do you think the only way to solve the Halting problem on a model of a machine with finite memory is to brute-force our way out of it?
Another person mentioned the same thing, that it would take an exponential number of steps (in the number of bits in the state space) to simulate running a program.
But why are you both assuming we can only solve the problem by simulating running the program and not by analyzing the program description?
How so?
We know the Halting theorem and Rice's theorem to be decidable for finite-state machines, so how does that prove anything about the time complexity of analyzing whether the program halts?
> The only question here is whether a computer is a Turing-machine
For me that's an absurd question, as it's impossible to build a machine as powerful as a Turing machine.
> With arbitrary side effects, you are back to “can the heat death of the universe be considered O(1)”, which is, well an interesting thought, but that just demonstrates infinity’s “size”.
Sorry, I don't understand this argument :)
My point regarding the heat death of the universe is that ad absurdum you can only use that amount of energy for your calculations, if every “Turing machine”-step takes a fixed amount of energy, which will indeed be a final number, and thus the O notation applies to that, making everything O(1), QED. But.. I don’t see why would the Turing machine model break down as an analogy to existing computers, programs, hell, real life (as it is one way to represent everything computable).
Using cycle detection for solving the finite version of the halting problem is a good example of this. You are not even trying to solve the problem. You are simply brute-forcing it by running two copies of the program at different speeds and comparing their internal states.
An actual solution would try to analyze the program to see whether it a) halts; b) enters a cycle; or c) attempts to use more memory than the space bound. But it feels unnatural that you could do that analytically without being able to say that the program attempts to use ever-increasing amounts of memory. Based on what we understand of computation, it's more plausible that analyzing a program is impossible in the general case, and finite bounds simply give us the ability to simulate the outcome.
After computability theory was "solved", complexity theory became the new frontier. But it turned out to be much harder. While you can teach many of the key proofs in computability theory to undergrads, complexity theorists still haven't managed to solve basic questions like P vs. NP. While you can simulate an arbitrary program, reasoning about its behavior seems to be effectively impossible in the general case.
My problem is when Turing machines are used to justify something being true when it is actually false for the vast majority of cases that we actually care about.
Sure, the problem is undecidable if your program requires infinite memory because it's trying to solve some mathematical problem (i.e. something related to infinity).
But for most programs, we would actually prefer knowing whether they will run into a memory limit or whether they cycle forever (or not), which is a decidable problem.
> You are not even trying to solve the problem. You are simply brute-forcing it by running two copies of the program at different speeds and comparing their internal states.
Indeed! But at least now we know that it's possible to solve the problem.
So here's a question which is actually more interesting, now that we know it's possible to solve it: can we solve the same problem without simulating how the program runs step-by-step?
Or in other words, can we reduce the time complexity and/or increase the efficiency of such algorithms?
That's the actual interesting question to me.
I agree with the rest of your comment.
Despite a century of research, simulation is still pretty much the only tool we have. Simulation can also be used to rule out many hypothetical solutions using similar tricks to the proof of Rice's theorem.
Assume that program A, with input X, decides whether program X with input X halts within a fixed resource bound. Assume that the resource bound is high enough that running A with an input of size |A| + C, for a reasonable constant C, uses much less resources than the bound. Then we can write a program A' that runs A with the input. If A says that the input halts (within the bound), A' enters an infinite loop. If A says that the input does not halt (within the bound), A' halts. If we run A' with input A', it halts iff A says A' does not halt (within the bound) with input A'.
We can avoid the situation by allowing A to make mistakes, by allowing it to say "don't know", or by allowing it to exceed the resource bound.
Exactly.
When running A, in some cases you would necessarily need more memory to run it than the memory bound that you defined for the input program, if you want it to work for all input programs without mistakes and without saying "don't know".
But that doesn't say anything about the time complexity, or does it?
So instead of saying: does program X with input X halt?
You redefined the problem to be: does program X with input X halt within T time steps?
Then you reach the conclusion: A' halts with input A' iff A says A' does not halt within the desired time bound with input A'.
But OK, imagine that we define the time bound T to be 10 steps and so A can always tell you whether a program halts within 10 steps, and always gives the correct answer in 1 step. What does that tell us?
> Then we can write a program A' that runs A with the input. If A says that the input halts (within the bound), A' enters an infinite loop.
So:
1. If A says (in 1 step) that X halts in the first 10 time steps, then A' enters an infinite loop.
2. If A says (in 1 step) that X doesn't halt in the first 10 time steps, then A' halts (say, in the second step).
Now you run A' with A' as input and:
1. If A says (in 1 step) that A' halts in the first 10 time steps, then A' enters an infinite loop.
2. If A says (in 1 step) that A' doesn't halt in the first 10 time steps, then A' halts (say, in the second step).
But here's the thing: A can only efficiently, correctly and always prove whether X halts if A is able to use more memory than X would use (otherwise we'd run into the exact same undecidability problem as with Turing machines).
This implies that besides the time bound, A also needs to analyze whether X halts within a defined memory bound.
So when you run A' with A', for A to work correctly then A would have to use more memory than A' would use, which is a contradiction because A' needs to use as much or more memory than A.
So isn't it impossible to use A' with A' as an input if you want A to always give you a correct answer, regardless of the time complexity bound? Because the memory bound would always be exceeded.
Does that actually prove that it's impossible to construct such a time-efficient A that works for all X that use less memory, or does it only prove that it's impossible to run A with A' as input correctly because the memory bound would always be exceeded?
Rice's theorem is much easier for computers with finite memory than for those with infinite memory. This is because a finite amount of memory gives a bound on the combined size of an analyzing program and the analyzed program. In particular, the only program that can analyze all programs is the empty program.
For your proposed example, a cycle detection program executed on a computer with finite memory cannot analyze all programs the computer can execute (unless it doesn't analyze them at all). Consequently, if there are both programs that halt and programs that do not, the computer cannot determine whether they have a cycle or not, i.e. halting is undecidable unless it is trivially decidable.
I'd be curious whether this suffices to convince you the halting problem exists for computers in the real world as well. If not, I'd be curious to read your objections.
That is correct. A cycle detection program that can analyze all input programs with a memory bound of "N bytes" would need more than N bytes of memory to run for some input programs.
For example, the tortoise and hare algorithm needs at most 2*N bytes of memory to analyze any program that runs with a memory limit of N bytes.
> I'd be curious whether this suffices to convince you the halting problem exists for computers in the real world as well. If not, I'd be curious to read your objections.
It does not. That only means that you if you, say, want to analyze how a program behaves when ran in a computer with 16 GB of state, you need to analyze it on a computer that has more than 16 GB of state.
It would be an incredibly useful analysis if we could discover time-efficient algorithms to accomplish this.
Then we must differ on what the "halting problem" refers to. I would say that a computer suffers from the halting problem if there is no program it can run that can determine whether arbitrary programs it can run halt or not. You seem to agree that this is the case for a computer with a fixed amount of memory (as you say, a computer with more memory is needed to analyze all programs for such a computer).
I can then only ask what is this thing that is not the halting problem (as I understand it) that you think does not exist for computers in the real world?
Well, but even if you define it your way, then computers don't necessarily suffer from that problem, do they?
Because you can limit how much memory usage a program can run with. So for example, if you have a computer which can handle 16 GB of state, you can analyze an arbitrary program X on this computer, where the analyzer is able to use the entire 16 GB of state.
The analyzer can say: this program X will halt if you give it 8 GB of state to run.
So now you run program X with an operating-system-enforced RAM+disk limit of 8 GB and you'd be quite happy to know that it will always halt.
This would be a very interesting and useful thing to do.
The analyzer would also always be able to tell if the program crashes because it ran out of memory (and why). So you could tell that 8 GB is not enough to run this program, which would also be very interesting to know, because this would imply that the program would crash in production.
What is not clear to me is this scenario that you're thinking:
Let's say your computer has 16 GB of state.
But your analyzer is not able to tell what happens to the program if it needs 16 GB of state or more to run.
But... your computer can't even run programs with more than 16 GB of state!
So... how is it useful to not know this? Why is this version of the Halting problem more useful than my version?
> I can then only ask what is this thing that is not the halting problem (as I understand it) that you think does not exist for computers in the real world?
The Halting problem is not usually defined like I define it or like you seemed to have defined it.
It's usually defined assuming that the program being analyzed can run with literally unbounded memory, which is not useful for most real-world programs because real-world programs cannot use an unbounded amount of memory.
The Halting Problem applies as long as you're able to programmatically combine two programs into a program that executes one with the other as its input. Given such a facility you can write a literal program whose input is a halting analyzer and whose output is a program on which the halting analyzer does not halt. Moreover the size of the output program seems to be something like twice the size of the analyzer plus the size of the program that combines pairs of programs as above.
On computers with finite memory, this program (deriving from an analyzer a program on which the analyzer fails to halt) may itself not halt only if it runs out of memory. One conclusion is then a lower bound for the size of an analyzer as a fraction of available memory, and it seems the fraction would be close to a third.
My personal opinion is this makes it practically impossible to make an analyzer. I think this because the size measure of the analyzer relative to memory is not in bytes but in terms of information content. What I mean is that size may refer to the size of a decompossion program plus a compressed archive of the would-be analyzer (this is an equivalent analyzer of smaller size). So the analyzer program would have compressed source code on the order of a third of available memory. Even worse, if we continue making computers with more memory, we would need bigger and bigger analyzers. Moreover, these cannot be procedurally generated by some algorithm that takes as input memory size, as this would violate the unbounded computation halting problem. So we would need bespoke large analyzer algorithms. Finally, just proving the correctness of such a code base that is not generated in some principled manner (as it would then be compressible) is also something practically impossible. In conclusion, such effort would be better spent on designing Turing-incomplete domain-specific languages with guaranteed behavior for which an analyzer is unnecessary. The latter is what people actually work with.
In any case, below is the algorithm which takes as input a halting analyzer H and produces a program QQ on which the halting analyzer does not halt. It would perhaps be instructive to implement it and apply it to the cycle detection problem.
---
Let H be some halting analyzer. By that I mean a program with the property that if HP, the program executing H with input P, halts with output 0, then executing P would not halt.
Let N be a program that halts on input 0 and does not halt otherwise.
Let N(HP) be the program that executes HP, and if the latter halts, executes N with input the result of executing HP. The behavior of N(HP) is that it halts if executing P would not halt in a way H could detect, and does not halt otherwise.
Let Q be the program which takes input P and executes the program N(H(PP)). That is such that program QP, which executes Q on input P, halts if executing PP would not halt in way H can detect, and does not halt otherwise.
Consider now the behavior of the program QQ, which excecutes Q with itself as input. It halts if executing QQ would not halt in a way H could detect, which is self-contradictory. So QQ most definitely does not halt.
It follows that H(QQ) either does not halt or outputs 0. Outputting 0 is again self-contradictory, because that would mean executing N(H(QQ)) would halt, and by assumption QQ, which does not halt, is the program which executes N(H(QQ)).
In conclusion, any halting analyzer H does not halt on input QQ, that is, the program which executes Q on itself as input, where Q is the program which takes input P, generates the program PP which would execute P on itself as input, and then executes N(H(PP)).
If the program P, which is the program being analyzed, uses at most N bytes of memory, then the Tortoise and Hare algorithm will always successfully determine whether P halts or not, if you give it 2*N bytes of memory.
Specifically, if you run "QQ" with the Tortoise and Hare algorithm, you have 2 options:
1) If you give it a finite amount of memory (i.e. if you run it on a computer or some other kind of deterministic finite-state machine), then it will not do what you think it does.
This is because the Tortoise and Hare algorithm, when applied to itself and having a finite memory limit, would exit unsuccessfully due to running out of memory, which would tell you nothing about whether it halts or not.
2) If you would analyze what it does on a Turing machine (i.e. an imaginary machine with infinite memory), then it would never halt, because it would always be trying to use more memory.
I don't know if you realize this, but the underlying issue is that a Halting analyzer always needs to use more memory to analyze an input program than the amount of memory that the input program uses.
Which means, of course, that when you apply the Halting analyzer to itself, it would need to use infinite memory in order to finish successfully, which is impossible.
This is why the Halting problem is undecidable when programs are allowed to use infinite memory: because the Halting analyzer uses more memory than the input program.
It is also why the Halting problem is decidable for finite-state machines.
Q is a program that takes one input P.
But then you said "QQ is a program which executes Q with itself as input".
So in the program QQ, the first Q uses the second Q as input, but what does the second Q use as input?
But Q is the source code of a program that needs an input.
How would you determine if Q halts or not, if you don't give it an input?
For instance, question 8 describes a function that does not halt, it asks you to answer whether it halts or not (the answer is no) then it tells you it does halt (wtf) if you implement it on Javascript (wtfx2).
This theory has to be approached from an abstract point of view, that kind of argument is conceptually equivalent to "it does halt because I will destroy the computer with a hammer, lol". From there it just becomes more and more deranged with each question.
Its just a lim/tends to problem.
Which depends entirely on how you define infinity.
for () {}If infinite is formally defined then detecting if any function equals or tends to it is fairly trivial.
quick and useful defs are "can exceed a time limit", or "can exceed the error bounds of floating point math"
I'd guess you can do it formally by catching the 6 or 7 definitions of infinite, but I've never come close to needing to go that far, for most, just programatically constructing a graph of the logic and detecting infinite loops in it has proved more than sufficient.
"Oh, computers have finite memory so actually they are finite state machines" is just needless pedantry that is not useful for the actual mathematical relevance of Turing's proof and its consequences. Yes, the field of static analysis makes practical (though not flawless) solutions to undecidable problems every day. This is not relevant here.
Only an infinite number of subclasses of instances to go.
That's proven job safety for computer science researchers.
There's only one subclass of instances for which the problem is undecidable: those where the program being analyzed is allowed to consume infinite memory.
Which is not the same thing as saying that the program is implemented in a Turing-complete language.
Because you can write a program in a Turing-complete language and yet, run it on a machine with finite memory (i.e. a computer).
The interesting bit about Turing's result is that it can be adapted to a wide class of mathematical and real objects. Physical systems? Yep. Time and/or space bounded machines? You bet. Actually, at its core Turing's result is itself an adaptation of Gödel's, who more broadly talks about the context of first-order mathematical theories.
If one want to bring these concepts to practice (where by practice I mean the realm of proving results in theoretical cs), it's a lot more effort than comparing claims to a simple sequence with an easy to derive limit. For an introductory example of the subtlety involved, while the two series (1/2 + 1/4 + 1/8 + ...) and (2 - 1/2 - 1/4 - 1/8 - ...) both approach 1 in opposite directions, most uncomputable numbers cannot be approached from both sides simultaneously (by a computably enumerable process, anyway). For example, while Chaitin's number is a definite number, you cannot write down any program whose sequence of outputs converges to it from above. They're all wrong. Comparing that to probably the most basic convergent infinite series in mathematics (that doesn't end in all zeros) is quite a disservice to the complexity and beauty of the field.
But nice deflect, no idea why this particular topic is so rife with fud, but you keep sticking with your deadlocking programs, and I'll stick with instant reports that my code will not halt and we can both go our separate ways. thnx.
Or are you basing your conclusions purely on someone elses opinion?
Actually, it is possible, if the program is not allowed to consume infinite memory.
That's what these algorithms do (where "value" is the state of the finite-state machine):
for (let i = 0; i <= i; i++); // hmm
`return s.length === 3;`
>If you implement halts using canBeRegex, you’ve got a proof by contradiction that canBeRegex can’t exist.
This is plainly false. I can also implement halts using addition, that does not imply that addition can not exist.
The author is clearly writing for a more general audience and I know what he means. But I think that if you are writing for a more general audience you should be more careful in your language and I think the article is sonewhat lacking there.
If you can implement halt using addition, addition cannot exist.
Ex falso quod libet - if you can prove a single false statement, every statement is true.
function haltWithAdd(code) { var a = 1 + 2; return halt(code); }
This clearly solves the halting problem (we assumed the existence of halt as the first step of our proof by contradiction). And it clearly uses addition (surely you can find where it does). By the logic (as written) of the article the implication is that '+' does not exist.
Implementing the halting problem using addition does not assume the existence of halt. It assumes the existence of addition, and you use that to show that halt must also exist. And that's not possible to do.
To implement halts using addition, you need to:
- Take the input to halts, namely the source code to a program.
- Convert that into an input to addition, namely two numbers.
- Call into addition, which adds the numbers.
- Use the result of that addition to infer whether the original program halts or not.
The code very clearly:
- is an implementation of the halting problem. If halt existed it would undoubtly solve the halting problem
- it uses '+'
You are prentending I didn't know what the author meant. The point is that what the author says is simply not true, if you take the statement as written. What he wants to show is that if canBeRegex is computable then halt is computable, but that isn't what he is saying.
I know what the author wants to say, but it isn't what he actually says.
In general: Let P be a statement. Lets assume that the Turing Machine T solves the halting problem - let's call this assumption H.
Now we assume P is false. Now we have a contradiction - H says that T solves the halting problem, but we know that there is not Turing machine that can solve the halting problem! Thus P must be true!
Notice that P is arbitrary.
Plainly speaking: If you assume that the halting problem can be solved, I can formally prove you that addition does not exist (i.e. there is no operation +, such that it forms a group on Z)
> By the logic (as written) of the article the implication is that '+' does not exist.
This is actually true. With that strong assumption, + does not exist.
Why are you pretending I do not understand the basics of logic while missing the actual argument by a mile?
In the article the author says: "If you implement halts using canBeRegex, you’ve got a proof by contradiction that canBeRegex can’t exist."
Which is plainly a false statement. What he means is the following statement: "If you show that if canBeRegex is computable then halts is computable, you’ve got a proof by contradiction that canBeRegex can’t exist."
Those two statements are clearly not equivalent. And only the second one is true.
I think that is pretty obvious. This is beyond nitpicking.
No. "Implemented" is in fact irrelevant, it is clearly not the term to use here. Because what the implementation uses is irrelevant, the question is about whether computability in one can be derived from computability of the other. In his example the implementation also uses ".length", whether it does or doesn't is irrelevant though. Since it is not a question of implementation.
>This is beyond nitpicking.
Also known as standard practice in mathematics.
Standard practice in mathematics would apply here if what was said is wrong. This time it is about an interpretation that no one shares with you.
[edit] After reading again your comment I realized that maybe you are not applying the logic correctly. If the reduction "implementation" uses both length and foo, then the conclusion is that at least one of length or foo cannot be computable. Since length is trivial, then it must be foo that is not computable.
Replace X with .length and read your statement again.
"If halt can be implemented by using .length that means you can reduce .length to halt."
Please just answer whether you believe that statement is true or false (or undecidable).
Reductions in complexity theory work like this. An explicit algorithm invokes a black box and this shows that either the black box does not exist or you can solve the original problem. Typically you care about the complexity of the reduction to establish that the problem is inside a given complexity class (e.g. NP complete).
The statement is obviously false by the way, as you can see in the article where the author does exactly that. You rephrasing the statement to make it true, is just ignoring the point.
I would encourage you to engage in some studying of reading comprehension. It is an important skill in mathematics and related disciplines.
If <absurd condition> then <some even more absurd thing> is a perfectly sound logic statement.
I explained already how reduction proofs work. Why don't you read on that instead of posting non sense?
None of what you are saying is even remotely a response to my criticism. You can tell me that I failed basic logic all you want, but your reading comprehension sucks so much that you still have not been able to figure out what I am even talking about.
I think you still haven't understood that I never said his intended reasoning was wrong. But that his statement as written is plainly false. There is no argument against the logic by me, so the fact that you keep going on and on about "logic" just shows that you haven't even understood yet that nobody disagrees with the logic. I know how a proof by contradiction works, you do not seem to want to understand that "computes" and "implements" are different words. And that by repeatedly arguing that the authors reasoning is valid if you change the statement to make it correct you are proving my point again and again.
Compute and implements are different words, nobody is arguing that. To me and everyone literate in math/cs, the role of "implementing" here is in the proof by reduction, which in the case of computability is used to establish by contradiction that some other problem is not computable by reducing a known incompatible problem to it.
Just like when you show an algorithmic implementation that maps any SAT instance to another problem using a polynomial time algorithm, then it follows that this other problem is NP-complete.
Read the first post. You should have done that before responding I think.
This is true. The condition is false (halt cannot be implemented by using length), thus the implication is true, regardless of the implicant.
Not in the sense of solving the halting problem with a function which has an occurrence of X.