Halting problem

Posted Dec 4, 2018 17:40 UTC (Tue) by excors (subscriber, #95769)
In reply to: Halting problem by dskoll
Parent article: Bounded loops in BPF programs

Oh, sure - I think what I'm trying to get at is that there are two completely separate realms, one of theoretical computer science (which is really just computer-themed mathematics) where the halting problem and busy beavers and Turing machines are relevant, and most finite things are trivial; and one of practical reality where the difference between "1 msec" and "after the heat death of the universe" is an important distinction. Applying theoretical tools to practical problems doesn't give useful results, and that's why the halting problem isn't relevant to BPF.

Halting problem

Posted Dec 4, 2018 19:35 UTC (Tue) by dskoll (subscriber, #1630) [Link]

I wouldn't say the halting problem isn't relevant at all to BPF, but it's not the only problem with trying to make it work practically.

But yeah, mostly it's just fun to point out weird edge cases that distinguish theory from practice. :)

Halting problem

Posted Dec 4, 2018 23:53 UTC (Tue) by nix (subscriber, #2304) [Link]

Yes, except that this stuff is also tied up with complexity theory, and that *is* extremely relevant (a lot of algorithms exist that would be really nice to use in compilers except that their time or space complexity is in very much the wrong class, should we say... so one uses approximations, or a less optimal algorithm, and wishes we lived in a perfect world.)

Halting problem

Posted Dec 5, 2018 10:46 UTC (Wed) by farnz (subscriber, #17727) [Link]

It's also not relevant because the halting problem says that you can't sort all programs into "does not halt" and "does halt". If you accept a third bucket - "may or may not halt", then the problem falls away; you can sort all programs into those three buckets in theory, and then it's just a practical problem.

This is not a new insight - it's basically a conservative approximation to the halting problem (where you treat "may or may not halt" as "does not halt", and accept that you are rejecting some programs that do halt), and is a common process in compilers.