5 ms·
> They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its
by tome 10y ago
> They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration
That's the same sense in which Neel means it.
- pron 10y agoNo, he doesn't. In the type view, the computation is asked to do two things: compute the output and check a proof that the output belongs to a set. Each of these questions has its own computational complexity. You may say that the first question comes from free by deciding how to think of the apple; the second certainly doesn't. See also https://news.ycombinator.com/item?id=12403508 https://news.ycombinator.com/item?id=12403508
- tome 10y agoYes he does. If by "Which functions nat -> nat are computable" he meant "functions written in some typed language" then the answer is vacuously "all of them".
- pron 10y agoNot all functions of type nat -> nat are computable in any formalism. You can write plenty of programs that are really of type nat -> nat in say, Haskell, that try to compute a non-computable natural function. They just can't do it and they'll never terminate for some inputs. But they're still perfectly well-formed.