Comment by swatow
11 years ago
might be easier to use a language like Idris, which can check that functions are total (i.e. return a finite number in finite time).
11 years ago
might be easier to use a language like Idris, which can check that functions are total (i.e. return a finite number in finite time).
Unfortunately, if a language L has the property that all programs in it are total, that means L is not Turing-complete. In fact, that puts a hard limit on the growth speed of functions definable in L. For example, the Busy Beaver function for L won't be definable in L (because otherwise you'd get the same paradox as in the halting problem), but will be easily definable in any Turing-complete language (because you can just dovetail through all possible programs in L without worrying that any of them will loop forever).