3 ms·
> even proving a function is total is hard. It's best left to the compiler. But if you're considering doing it, don't imagine yourself taking an existing func
by mrkeen 3y ago
> even proving a function is total is hard.
It's best left to the compiler.
But if you're considering doing it, don't imagine yourself taking an existing function like qsort and trying to prove it's total. Instead try building up a new function and only build it out of other total functions.
- nyrikki 3y agoIf your language is TC and thus supports general recursion, no algorithm can possibly exist for deciding whether a function is in fact total in the general case. As all primitive recursive functions are provably total, that is a place a compiler can work. But just using for loops gets you there too. Total functions that are also pure functions are a pretty small set so there may be other reductions like the above. But don't depend on the compiler. But I agree writing total functions from the start is the ideal if possible.