3 ms·

> Proving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly

> Proving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly for proof languages, where it’s useful to write proofs about functions that you never run. If the function provably terminates, you can assume that whatever value it returns exists, without calculating it. In practical algorithms of significance, we can often do much better than this, proving both termination, and the time complexity of that termination. For instance, a DFA of a regular language will terminate in O(n) of the length of the haystack, and we also have a bound for the time it takes to construct that DFA. Sometimes, as you're alluding to, we know something terminates, but the time complexity is impractical: exhaustive naïve search for Traveling Salesman will, in principle, halt. This is, itself, useful information. The article claims (I believe correctly) not just that H-M inference halts, but that it does so in "near-linear" time. That's a much tighter bound than merely proving termination.

skybrian 2y ago
Yes, agreed.
nextaccountic 2y ago
Complexity sometimes is still too little, because the constants can overwhelm your O(n) for all n that you care about in practice. Or rather, complexity can't help you to select between two competing O(n) algorithms However, without a precise cost model of your operations (say, you just know each operation has a bounded time and such they are each O(1 ) but nothing beyond that), that's often the best you can do There's something called resource aware computation that can do more finer grained bounds on the runtime and memory usage of functions (and other resource usage like stack space so you can prove you always use less than 8MB or whatever number) not only complexity but also the constants. With the right cost model you could model CPU and memory latencies and other things like CPU port usage, cache usage etc, but there's an interplay with the optimizer here (this could even be used to spot performance regressions of compiler codegen even without running any benchmark)
gpm 2y ago
If "near-linear" time was a bound it would be, but it's not. HM type inference is exptime-complete. Near-linear here is just "most programs people actually write type check in something close to linear time".

skybrian 2y ago

Yes, agreed.

nextaccountic 2y ago

Complexity sometimes is still too little, because the constants can overwhelm your O(n) for all n that you care about in practice. Or rather, complexity can't help you to select between two competing O(n) algorithms However, without a precise cost model of your operations (say, you just know each operation has a bounded time and such they are each O(1 ) but nothing beyond that), that's often the best you can do There's something called resource aware computation that can do more finer grained bounds on the runtime and memory usage of functions (and other resource usage like stack space so you can prove you always use less than 8MB or whatever number) not only complexity but also the constants. With the right cost model you could model CPU and memory latencies and other things like CPU port usage, cache usage etc, but there's an interplay with the optimizer here (this could even be used to spot performance regressions of compiler codegen even without running any benchmark)

gpm 2y ago

If "near-linear" time was a bound it would be, but it's not. HM type inference is exptime-complete. Near-linear here is just "most programs people actually write type check in something close to linear time".