The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Thorsten,

Another idea, related to semantics of approximate computations, is this: 
instead of representing R -> Bool functions by themselves, you can 
incorporate error bounds into the definition of the function, using the type 
R * R+ -> Bool * { 0, infty }. The input here uses R+, the non-negative 
reals, for its error bounds, while the output is either known definitively, 
with error 0, or could possibly be wrong, with infinite error. Any pair of a 
value and its error bound defines a (closed) set, leading to the topology you 
would expect over the pair type. And such a function can be made continuous 
for standard real-valued predicates such as <, like this:

(x, xq) < (y, yq) = (x < y, if | x - y | <= xq + yq then infty else 0)

When you are close to the boundary, we can guess at the result but we don’t 
know for sure; i..e, the error is infinite. Also, the result can certainly 
flip, from true to false or vice-versa, when we take an arbitrarily small 
perturbation on x or y. However, if you incorporate the error bound, then you 
are still continuous, because (true, infty) and (false, infty) represent the 
same set, and are thus topologically indistinguishable.

If you still want to have just a function of type R -> Bool (which is useful 
inside a big computation), you can separate out the error bound as a separate 
function; e.g., you can have < : R -> R -> Bool and <_err : R * R+ -> R * R+ 
-> { 0, infty } as separate definitions, where < is only continuous when 
using the topology defined by <_err. It actually turns out that <_err is 
actually the error bound for < itself.

Anyway, please let me know if this sort of thing would be useful to you: I am 
currently writing up my approximation semantics ideas, and I would love for 
this to work out as an application.

-Eddy

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