The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

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.

We can construct non-trivial partial computations, using the partiality
monad
(eg see http://sneezy.cs.nott.ac.uk/darcs/dtp10/slides/danielsson.pdf)
That is we can obtain interesting functions from the real into Bool_|_ for
example. 

Obviously partiality is just another black hole. There is no non-constant
function out of Bool_|_ either.

I am still disturbed by this. I always thought of non-terminating
computations as a bug. However, it seems that once you accept the reals
the bug becomes unavoidable.

The real numbers play a central role in classical Mathematics. They arise
as an idealisation of the physical world around us (the english name is
misleading they should have been called ideal numbers). An idealisation
which doesn¹t seem to play so well in a computational context. Maybe they
are overrated? 

Thorsten

P.S. Both the reals and the partiality monads make essential use of
quotients which are now (post HoTT) acceptable because they are special
cases of HITs (Higher Inductive Types).
P.P.S. Not so easy to get the reals right - see the Hott book (11.3).

On 08/12/2014 10:35, "bertot" 
<Yves.Bertot AT inria.fr>
 wrote:

>On 5/12/14 5:10 PM, CHAUVIN Barnabe wrote:
>> Hello club !
>>
>> Playing with the CoRN library, I have a few questions about how Reals
>> work :
>>  - I understood the structures from CSetoid to CReals, but I don't
>> really understand the difference between IR and CR ? I know CR stand
>> for Computational reals, but what does IR means ?
>>  - What is exactly the aim of the RasIR and IRasR definitions ? Do
>> they allow computation of coq reals (for example 4%R + 3%R ? )
>>  - When to use CR or IR or R in a proof ? (And why rather this one).
>> Of course, I guess it depends on the circumstances ..
>>  - Let's assume I have a subgoal  2<3  (the type of the number depends
>> on my previous question, but they are reals numbers), what is the best
>> way to solve it ? Use CoRN computation (I'm talking of a simple
>> inequality or equality) ?
>>
>> Thanks for your attention !
>> These questions might seem weird or even destructured, but I'm a
>> complete beginner ..
>>
>> Best regards.
>
>I hope that specialists of CCorn will answer to your questions, but
>while waiting, here are a few hints.
>
>1- real numbers are hard to compute with.  Of course, you think that
>there should be no problem computing 4%R + 3%R, but what about computing
>PI + cos 1, what does it mean to compute it?  In some sense, computing a
>number only means "find a more natural way to express the same number".
>So 7%R is a more natural way to represent 4%R + 3%R, but I am afraid
>that deciding what is the most natural way to express (PI + cos 1) is
>rather subjective...
>
>Now, another point of view around real numbers, is that they can be
>computed up to some precision: this is the "Cauchy" point of view: you
>give me a precision, I give you a value within that precision (in fact
>Cauchy is more about sequences of values, but in my mind the spirit is
>the same).
>
>The value that I give can be taken in another type, where computation
>has a more "concrete" meaning, like rational numbers.
>
>With this approach, it is easy to show that 3 < PI (by taking a
>sufficiently close approximation of PI), but there is no general
>algorithm that takes two real numbers a and b as arguments and returns
>true exactly when a < b.  Because, when a and b are the same (but I
>don't know it), every question I ask will return approximations of a and
>b that are very close to each other, but these approximations never give
>enough information to conclude that a < b is indeed not satisfied.  For
>instance, let's call v1 the first positive value where the sine function
>vanishes and let's call v2 the number (4 * (1 - 1/3 + 1/5 + ...)).  We
>know mathematically that v1 and v2 are the same.  Algorithmically, we
>can compute arbitrarily close approximations of these two values showing
>that they must be very close to each other, but we will never have, just
>by computation, a certitude that one cannot be higher than the other (we
>will always conclude that we need more precision).
>
>Note that, for rational numbers, there exists an algorithm that takes
>two rational numbers a and b as arguments and returns true exactly when
>a < b.  So the type of real numbers is, in a sense, a weaker type than
>the type of rational numbers.
>
>Yves
>





This message and any attachment are intended solely for the addressee and may 
contain confidential information. If you have received this message in error, 
please send it back to me, and immediately delete it.   Please do not use, 
copy or disclose the information contained in this message or in any 
attachment.  Any views or opinions expressed by the author of this email do 
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment 
may still contain software viruses which could damage your computer system, 
you are advised to perform your own checks. Email communications with the 
University of Nottingham may be monitored as permitted by UK legislation.