The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

2014-12-09 5:03 GMT-05:00 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?

I wouldn't go that far, but I do think we are very far from
understanding what the reals mean in a computational context. For
instance, there is a very rich theory of L_p functions that plays a
fundamental role in numerical analysis, but I've haven't heard of any
attempts to try to model them in type theory. And I think it is fair
to say that numerical analysis is one of the most fundamental parts of
computation as a whole.

Computationally, an L_p function has to respect the topology in R^n,
but only to a certain point -- for instance, you are allowed to change
the values of your function on a 0-measure set. As a matter of fact,
the value of an L_p function at some particular point is not actually
very important, something that seems to depart a little bit from how
we see functions in type theory.

Perhaps we could define an L_p function as a quotient over Q -> Q, in
a similar way to how it's done usually. Then, instead of applying the
function to a real, one would have to "observe" that real, and that
observation would have to satisfy certain properties. I think it would
be nice investigating this sort of thing...

>
> 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.
>



-- 
Arthur Azevedo de Amorim