29 ms·
>The compiler still cannot tell when our loops will terminate (yes, this is possible). while(n < busy_bever(10)) n++ Tell me when my loop terminat
by thr_ddv 3y ago
>The compiler still cannot tell when our loops will terminate (yes, this is possible).
while(n < busy_bever(10))
n++
Tell me when my loop terminates.
- littlestymaar 3y agoThat's not a very good exemple because with BB we know the code terminates, by definition. The canonical tong-in-cheek argument is to use the Collatz conjoncture instead (but even that isn't a good example in practice: https://news.ycombinator.com/item?id=21440306 https://news.ycombinator.com/item?id=21440306)
- thr_ddv 3y agoI'm not asking if it terminates, I'm asking when it does. After all it's not much use if the number overflows the universe.
- littlestymaar 3y agoBut that's not something these kinds of tools are supposed do, even with trivial functions… These tools have no idea about the run-time (and there's no way they coule, since it depends on the load you put on the hardware in parallel of running your program)
- redjamjar 3y agoI agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).
- redjamjar 3y agoYeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.
- nine_k 3y agoFor practical reasons, it's enough to prove that it takes longer than some upper bound, say, 10 ms. The rest is not important.
- rockstar-guy-23 3y agowhile(calculate_pi_stream(10 /* substring length */) != 0987654321);
- redjamjar 3y agoHaha, yeah ... this one you would have a very hard time with :) Hopefully, though, termination of your program does not depend on this ... otherwise could be a long wait!
- nine_k 3y agoI remember there was a theorem that one can find an arbitrary substring in a long enough output of infinite (stationary) random process. I also suppose that a decimal representation of pi may count as one, then your function provably terminates. But this is of a theoretic interest. In practice the verifier says: "I can't prove that this function will terminate within (some reasonable window), program rejected". And this is what's actually needed: a program that provably has certain properties, where an automatic proof is tractable.
- xigoi 3y agoIt is currently not known whether π is a normal number (that is, its representation in any base contains any finite sequence of digits with the same density as in a uniformly random string of digits).
- jjnoakes 3y ago> Tell me when my loop terminates. I think the point is that even though one can't determine loop termination for all loops (easily provable), there are a huge number of useful loops that do useful work and for which you can prove properties like termination (and other static properties).
- redjamjar 3y ago> there are a huge number of useful loops that do useful work and for which you can prove properties like termination Exactly! If the loop doesn't terminate, then you obviously cannot show it. But if it does, then you should be able to (even if that requires some changes to help the tool)
- jcranmer 3y agoAssuming you meant 'busy_bever' to implement the busy beaver function, said function is in fact not a computable function, which means you can't write it down in a programming language.
- Smaug123 3y agoThis is true but somewhat misleading. The nth busy beaver numbers are known for n <= 4. It's within the bounds of possibility that we will some day learn the nth busy beaver numbers for n <= 10. (What we can say is that the parent's loop will never terminate for any known definition of "ever" that pertains to the physical universe.)