Re: [isabelle] Executing real numbers as approximating functions

Le Wed, 08 Aug 2012 21:47:37 +0200, Florian Haftmann <florian.haftmann-jNDFPZUTrfRoctOpMxdO53BFZrOObVGws0AfqQuZ5sE at> a écrit:

Hi all,

once I have heard about a formalisation to execute real numbers as
approximating functions, i.e. where each real number r is implemented
using a function

  R :: nat => float

such that R n equals r approximated to the n-th digit (or something

Can somebody give me a reference for that?

Thanks a lot,

I'm far from being a math guru, but I dislike so called “reals” in computer programs. You have alternatives like fixed‑point arithmetic (common in the Ada world). Or you can work on an integer range instead of working on a “real range” (ex. do you computation in the range 0::nat to 1000::nat instead in the range 0.0 to 1.0, as an example). If I'm not wrong, I suspect it to be exactly the same as fixed point arithmetic, but better ask a math or safe system guru.

Was my two cents beside of the two other replies.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.