2 ms·
I don't understand the point of arguments about constructible functions on unconstructable reals. I.e. reals with infinite digits and no finite symbolic represe
by Nevermark 7y ago
I don't understand the point of arguments about constructible functions on unconstructable reals. I.e. reals with infinite digits and no finite symbolic representation.
For anything actually computable (in finite time), on computable (in finite time) values, you will always get discrete (not continuous) functions on discrete (not continuous) values.
- vilhelm_s 7y agoThe idea of computable reals go back to at least Turing. The idea is that a real number (or an operation on real numbers) is computable if we can compute the decimal digits, one by one. This way, if the user wants to know it to any desired precision, they just have to wait until the computer has printed that many decimals. You can equivalently treat them as terminating computable functions of type (nat -> bool), which computes the n:th binary decimal. This is actually a quite constructive notion! At least, it works well with intuinistic mathematics, which is why Andrej Bauer is writing about it.
- Nevermark 7y agoOk, that makes sense. Even when restricting numbers to reals with finite symbolic/program definition, comparing two such reals requires an unknown and unbounded number of their digits to be computed. If two symbolic representations define the same number, but it isn't obvious, a complete digit comparison will never end. Got it. Thank you!