The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Dec 9, 2014 at 9:17 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

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.

I meant: do the comparison on the approximation, which is presumably a rational.

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

I mean it respects equivalence of reals, defined as some notion of "function returning increasingly close approximations with some consistency conditions", up to the returned approximations being "close enough" at each step.  So, my example would be not well defined because two different approximation functions could hover just on opposite sides of 10^-5.

-- 

Daniel Schepler