3 ms·
Division isn't closed on the natural numbers. Total functions have to return either true or false explicitly, failure as negation doesn't work. That is where
by nyrikki 3y ago
Division isn't closed on the natural numbers.
Total functions have to return either true or false explicitly, failure as negation doesn't work.
That is where you get Gödel's 'this statement is false' from.
This is the law of the excluded middle that broke the Mathmatica Principia.
Plato, Aristotle, and Russell's use of the law of the excluded middle is what Gödel, Church, and Turning leverages.
For problems in P this distinction is harder to see because P=co-P but we think NP!=co-NP.
As NP are by definition decision problems this is important.
NP being the provable yes-instances and co-NP being the no-instances, even proving a function is total is hard.
If you accept failure as negation you may be able to build a sun-Turing machine that always halts but you won't be able to show it is complete and consistent.
That is why ZF disallows statements like 'this statement is false'.
- 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.