The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-12-09 17:36 GMT+01:00 Daniel Schepler <dschepler AT gmail.com>:

On Tue, Dec 9, 2014 at 2:03 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Yves makes a very good point: All the functions from the Reals to Bool are
constant because all computable functions are continuous. This clearly
limits very much what we can do with real numbers, they are a bit of a
³black hole² as far as information is concerned.

I think you mean any computable, *well defined* function from the reals is continuous.  It's easy enough to write a function which e.g. takes an approximation of the input to six decimal places, and returns true if the approximation is within 10^-5 of zero.  I think that's one sort of thing that numerical algorithms tend to do - check if some result is within some epsilon of zero, or within some epsilon of being positive, etc.  Sure, in the boundary cases that will tend to goof up, but you try to arrange things so that the algorithm works correctly in the "generic" case.

That does not seem much obvious for me. Telling if something is within 10⁻⁵ of 0 or not is as hard as telling if something is negative, or telling if some real number is equal to zero. Computing an approximation up to a certain amount of digits does not seem to be an easy thing for me. Of course, it depends on the primitive you have.

By the way, what do you mean by "well defined" ?