Skip to content

Comment on A gentle introduction to automated reasoningparent

Comments

Yep, it's a sort of accidental form of making perfect the enemy of better, forgetting that while a problem may be undecidable in general, there may still be a useful semi-/decidable subset. E.g. my IDE can still tell me that my program won't halt when I've been an idiot and forgot to update the `while` variable in a loop, halting problem notwithstanding

And similarly with regards to tractability and approximations. The travelling salesman problem is hard, and yet Google Maps works very well. And even when not using an approximation, sometimes n really is small enough to be tractable

there may still be a useful semi-/decidable subset.

Yes, but note that the entire language HALT is semi-decidable (or Turing-recognisable if you use Sipser’s terminology); in this case it’s only the (strictly) decidable subset that is useful.

So is there any result on "how much" of the halting problem is solvable? E.g. is there a result that says there is a program which can decide whether the input halts for "most" inputs, in some sense of "most"?

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.