The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Dec 9, 2014 at 9:16 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

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.

What I was trying to say is that probably, many real-world numerical algorithms won't be respectful functions from the quotient, but of course they have to be close enough (i.e. numerically stable) in order to be at all useful.  Another possibility, if you want a certified algorithm, might be to raise exceptions for example if some intermediate approximation is too close to 0.  It might happen then that with one input, it's just barely enough that you can return a certified correct answer; but with a slightly perturbed but equivalent input, it would instead raise an exception.  Example: Gaussian elimination on a real matrix, where you would need to raise an exception if at some stage all of the pivot candidates are too close to 0, but in the generic case you should usually be able to proceed without problems.

-- 

Daniel Schepler