The Coq mailing list

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

I always mean “computable” when I say “function”.

A “function” which doesn’t “function” shouldn’t be called a “function”. :-)

Please burn your set theory books.

Sure, I define the reals as a quotient so any function will have to respect the equivalence.

So in my book any function over the reals is well defined and computable. Just call it a function for simplicity.

Thorsten

From: Daniel Schepler <dschepler AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tue, 9 Dec 2014 16:36:07 +0000
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A few questions about reals

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.

-- 

Daniel Schepler

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.