Re: [isabelle] Executing real numbers as approximating functions
Le Wed, 08 Aug 2012 21:47:37 +0200, Florian Haftmann
<florian.haftmann-jNDFPZUTrfRoctOpMxdO53BFZrOObVGws0AfqQuZ5sE at public.gmane.org>
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and