Hacker News Reader

Did anyone understand this bit?

> The approaches using equivalence classes of Cauchy sequences ... suffer from an inability to identify when two “real numbers” are the same

Perhaps there's no computable general method, but it seems like it highlights an even bigger problem which remained unspoken. There is an inability to tell when a sequence of numbers approaches zero!

View on HN

Yup, you can define distinctness of constructive real numbers as two algorithms returning rationals that will differ by more than the approximation error ε they were given as input, for some arbitrarily small ε - but equality involves proving that two algorithms will never be apart in this way - and this cannot be done in general. As you say, even comparison with zero is problematic. So instead of equivalence relations, you need to define the apartness relation - the notion that a supposed equivalence between two such numerical algorithms can be constructively refuted. This is nothing new - it's a well-known part of constructive math, and is also the sensible way to formalize numerical analysis.

Reply on news.ycombinator.com