Is solving the halting problem easier than people think?

Question

Although the general case is undecidable, many people still do solve problems that are equivilent well enough for day to day use.

In cohen's phd thesis on computer viruses, he showed how virus scanning is equivilent to the halting problem, yet we have an entire industry based around this challenge.

I also have seen microsoft's terminator project - http://research.microsoft.com/Terminator/

Which leads me to ask - is the halting problem overrated - do we need to worry about the general case?

Will types become turing complete over time - dependant types do seem like a good development?

Or, to look the other way, will we begin to use non turing complete languages to gain the benefits of static analysis ?

Answer 1

The Halting Problem is really only interesting if you look at it in the general case, since if the Halting problem were decidable, all other undecidable problems would also be decidable via reduction.

So, my opinion on this question is, no, it is not easy in the cases that matter. That said, in the real world, it may not be such a big deal.

See also: http://en.wikipedia.org/wiki/Halting_problem#Importance_and_consequences

Answer 2

As a day-to-day programmer, I'd say it's worthwhile to continue as far down the path to solving halting-style problems, even if you only approach that limit and never reach it. As you pointed out, virus scanning proves valuable. Google search doesn't pretend to be the absolute answer to "find me the best X for Y," but it's also notably useful. If I unleash a novel virus (muwahaha), does that create a bigger solution set, or just cast light on an existing problem area? Regardless of the technical difference, some will pragmatically develop and charge for follow-up "detection and removal" services.

I look forward to real scientific answers for your other questions...

Answer 3

Is solving the halting problem easier than people think?

I think it is exactly as difficult as people think.

Will types become turing complete over time?

My dear, they already are!

dependant types do seem like a good development?

Very much so.

I think there could be a growth in non-Turing complete-but-provable languages. For quite some time, SQL was in this category (it isn't any more), but this didn't really diminish its utility. There is certainly a place for such systems, I think.

Answer 4

Incidentally, I think that the Turing completeness of templates shows that halting is overrated. Most languages guarantee that their compilers will halt; not so C++. Does this diminish C++ as a language? I don't think so; it has many flaws, but compiles that don't always halt aren't one of them.

Answer 5

I don't know how hard people think it is, so I can't say if it is easier. However, you are right in your observation that undecidability of a problem (in general) does not mean that all instances of that problem are undecidable. For instance, I can easily tell you that a program like while false do something terminates (assuming the obvious semantics of the while and false).

Projects like the Terminator project you mentioned obviously exist (and probably even work in some cases), so it is clear that not all is hopeless. There is also a contest (I believe every year) for tools that try to prove termination for rewrite systems, which are basically a model of computation. But it is the case that termination in many cases is very hard to prove.

The easiest way to look at it is perhaps to see the undecidability as a maximum on the complexity of instantiations of a problem. Each instantiation is somewhere on the scale of trivial to this maximum and with a higher maximum you typically have that the instantiations are harder on average as well.

Answer 6

There are plenty of programs for which the halting problem can be solved and plenty of those programs are useful.

If you had a compiler that would tell you "Halts", "Doesn't halt", or "Don't know" then it could tell you which part of the program caused the "Halt" or "Don't know" condition. If you really wanted a program that definitely halted or didn't halt then you'd fix those "don't know" units in much the same way we get rid of compiler warnings. I think we would all be surprised at how often trying to solve this generally-impossible problem proved useful.

Answer 7

Wow, this is one confused question.

First: The Halting Problem is not a "problem" in a practical sense, as in "a problem that needs to be solved." It is rather a statement about the nature of mathematics, analogous to Gödel's Incompleteness Theorem.

Second: The fact that building a perfect virus scanner is intractable (due to its being equivalent to the Halting Problem) is precisely the reason that there is "an entire industry built around this challenge." If an algorithm for perfect virus scanning could be designed, it would simply be a matter of someone doing it once, and then there's no need for an industry any more. Story over.

Third: Working in a Turing Complete language does not eliminate "the benefits of static analysis"-- it merely means that there are limits to the static analysis. That's ok-- there are limits to almost everything we do, anyway.

Finally: If the Halting Problem could be "solved" in any way, it would definitely be "easier than people think", as Turing demonstrated that it is unsolvable. The general case is the only relevant case, from a mathematical standpoing. Specific cases are matters of engineering.