PS: that whole blog is pretty awesome—I got turned on to it by the post “Seemingly impossible functional programs” which demonstrates e.g. how the problem of determining equality of two black-box functions from reals in [0, 1] to booleans turns out to be computationally decidable in finite time
Oi, that’s not right. The domain of these functions is not the set of reals in [0, 1] but the set of infinite sequences of bits; while there is a bijection between these two sets, it’s not the obvious one of binary expansion, because in binary, 0.0111… and 0.1000… represent the same real number. There is no topology-preserving bijection between the two sets. Also, the functions have to be continuous; it’s easy to come up with a function (e.g. equality to a certain sequence) for which the given functions don’t work.
Of course, it happens that the usual way of handing “real numbers” in languages like Haskell actually handles things that are effectively the same as bit sequences, and that there’s no way to write a total non-continuous function in a language like Haskell, making my point somewhat moot. So, carry on, then.
Your comment is basically correct. This paper deals with the representation issue somewhat. But I think those results are applicable to computation in general, and the choice of Haskell is irrelevant to the discussion. You’re welcome to prove me wrong by exhibiting a representation of exact reals that allows decidable equality, in any programming language.
Oi, that’s not right. The domain of these functions is not the set of reals in [0, 1] but the set of infinite sequences of bits; while there is a bijection between these two sets, it’s not the obvious one of binary expansion, because in binary, 0.0111… and 0.1000… represent the same real number. There is no topology-preserving bijection between the two sets. Also, the functions have to be continuous; it’s easy to come up with a function (e.g. equality to a certain sequence) for which the given functions don’t work.
Of course, it happens that the usual way of handing “real numbers” in languages like Haskell actually handles things that are effectively the same as bit sequences, and that there’s no way to write a total non-continuous function in a language like Haskell, making my point somewhat moot. So, carry on, then.
Your comment is basically correct. This paper deals with the representation issue somewhat. But I think those results are applicable to computation in general, and the choice of Haskell is irrelevant to the discussion. You’re welcome to prove me wrong by exhibiting a representation of exact reals that allows decidable equality, in any programming language.