What Mike says is correct. I oversimplified for the sake of keeping the story short. The core truth of what I said is that real programming languages (such as Haskell) can deal with infinite structures that represent real numbers exactly, and can do arithmetic on them. But, for the reasons Mike referred to, they do not use decimal (or binary) expansions. One simple alternative is to use infinite sequence of signed binary digits +1, 0 or -1. This is highly redundant - there may be many representations of any given real. But the redundancy has the effect that output can always proceed and doesn't get blocked. Example: In ordinary binary fractions, 1/4 can be either .0100000 ... or .0011111 ... If you add these together, you can never get even a single digit. At any given finite stage, for all you know the answer may be very slightly less than 1/2, in which case the first digit would have to be 0, or very slightly more, in which case the first digit would have to be 1. With the added flexibility of negative digits, you can safely output +1 for the first digit since negative digits later can take the answer back below 1/2. Sorry if anyone was misled, Steve Vickers. On 9 Jun 2005, at 20:39, Michael Barr wrote:
I don't have any problem with the general idea expressed below and my objection doesn't apply at all to the free category construction, but I just wanted to point out that seeing constructible numbers as infinite decimals just does not work. Bishop in his book Constructive Analysis, gives an example of two numbers with constructible decimal expansion of which no single digit of the sum is (currently) constructible. I don't think this problem would arise in pi^2, but who knows. At any rate, for him a constructible is given by a sequence of rationals q_1,q_2,..., whose numerators and denominators are recursively enumerable sequences of integers and for which |q_n - q_m| < 1/n + 1/m. When you add two such sequences, you have to take every second term of the sum and multiplication involves more drastic trimming. Moreover, division is possible only if you can prove that eventually |q_n| > 1/N for some fixed N. So what you get is a local ring, not a field.
10-Jun-2005 11:54:26 -0300,3729;000000000000-0000000c