While technically correct in several ways, this is a pretty naive take on the topic. A simple counterexample is trying to decide whether a program which computes the Collatz conjecture will always halt (which is equivalent to proving the conjecture itself). Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care about the mathematical object a computer is modelling, not just the computer itself.
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.
> Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care about the mathematical object a computer is modelling, not just the computer itself.
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?
> 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.
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.
> There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem.
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?
I think I see what you're getting at. A few final points:
- 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.
> - 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.
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.
> Sure, but saying a problem is undecidable when it is in fact decidable is also not a useful measure of decidability to me.
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.
> 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?
Ok, but unless you stick with some fixed resource limit N forever, the problem is undecidable again.
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.
> Ok, but unless you stick with some fixed resource limit N forever, the problem is undecidable again.
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.
Caveat, the thing that makes it decidable is not the fact that it was going to run on a computer with finite memory, the SMT solver will fail on many code chunks that can run on your computer. (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.)
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.
> 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)
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.
I think he/she was just “sarcasticly” extending Turing machines to show that even in practicality its limits apply.
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)
> 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.
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.
> Caveat, the thing that makes it decidable is not the fact that it was going to run on a computer with finite memory, the SMT solver will fail on many code chunks that can run on your computer.
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.
> 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?
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.
I agree a bit with your point, but still, given how little it is usually emphasized that the Halting problem is not valid for finite-state machines I'm not sure that even very smart people don't mistakenly end up believing that it is.
You appear to have a low opinion of other people's cognitive abilities. In that light, perhaps you should consider the possibility that your position, which strenuously attempts to imply that there is a serious cognitive dissonance here, could complicate understanding these matters for someone who is approaching them for the first time.
> 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.
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.
> 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!
Well, I may be writing stupid things in the following, but have a look at the Busy Beaver problem. Even for tiny tiny state sizes it will grow faster than any computable function — so for a sufficiently complex property you would effectively have to iterate over this problem space. No matter if even P=NP, that is just.. literally bigger than any function you could make up.
You can analyze it, and for that you would use some system like logic. But it so happens that these pesky mathematicians are everywhere, because any sufficiently complex system will fall victim of Gödel. And in fact, Math itself is limited and trivially overstepped by Turing machines, but you are free to create any other reasoning system, it will also fall short of Turing.
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
Well, if not by running them and not by analyzing them (any rule system, not just logic is affected), what is your proposed.. whatever to say whether they halt or not? Or any other non-trivial, semantic property?
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.
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.)
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.