Hacker News Reader

Comment by garganzol | Hacker News Reader

Only from algebraic and philosophical standpoints. This knowledge is not 100% precise unless a specific number is found.

View on HN

Nobody cares about the halting problem from a specific standpoint. If it's algebraically guaranteed to halt, it halts. When it halts is entirely meaningless for purposes of the halting problem.

But the thing is, it isn't algebraically guaranteed either - we still don't know if an odd perfect number exists. (I'm not sure where the "Definitely. Somewhere in 10^300 range." is coming from. There's nothing definite about the existence, only constraints that need to be satisfied if it exists)

In fairness, though, the halting problem doesn't care if you can predict if SOME programs halt... you have to predict if ALL programs halt.

There's that, too. (Well, we don't have to predict anything. We have to show that halting or not is a decidable condition, and we've shown it isn't. Even if we had shown it was decidable, there still might be programs where we practically can't figure out it halts. So is the beauty of math - it gives us the gestalt of the world without caring about the world :)

> Nobody cares about the halting problem from a specific standpoint. If it's algebraically guaranteed to halt, it halts. When it halts is entirely meaningless for purposes of the halting problem.

Halting problem from a specific standpoint is a popular area of research. Microsoft Research in particular has been active in this area, and Windows device drivers and other kernel event handlers are analyzed to prove that they will halt in a reasonable amount of time to avoid locking up the OS.

https://www.microsoft.com/en-us/research/publication/t2-temp...

If you've prove a finite upper bound,then you've proven the program will halt. You don't need to know what the exact number is.

The trick with boundaries does not stand true for evasive predicates on unbounded data.

Please note that suggested odd perfect number search algorithm in Python uses an evasive predicate on a big integer which is unbounded.

This means that a typical tracer (or verifier in Turing terms) won't be able to infer the upper bound for the given example.

Reply on news.ycombinator.com