[FOM] Primitive recursive reals
Andrej.Bauer at andrej.com
Fri Apr 21 04:09:56 EDT 2006
On Friday 21 April 2006 01:04, joeshipman at aol.com wrote:
> The whole discussion seems to suggest that maybe we should seek to
> reformulate constructive analysis in terms of a representation of real
> numbers that has nicer properties than "base b" notation;
It is a bit unfair to suggest that "constructive analysis be reformulated" in
this respect because nobody in constructive or computable analysis ever users
the usual base b notation, other to demonstrate the fact that it has awful
A common notation is the _signed_ digit representation: apart from digits
0, ..., b-1 we also allow -1, -2, ..., -b+1. It would be interesting to see
what happens to Friedman's theorems if we switch to signed digits. I would
expect them to become simpler (false?). For example, we won't be able to play
the "recurring 9's" trick.
> To meet this objection, we need some way to pass from a "primitive
> recursive real number" (in the sense that both the approximating
> rational sequence (r1,r2,r3,...) and the modulus of approximation f(n)
> are primitive recursive functions) to a canonical primitive recursive
> representation of the same number.
> Is this possible?
No, it is not, as is well known in computable analysis. We argue in Recursive
Mathematics. Let C be the set of rational Cauchy sequences and q : C --> R
the canonical quotient map. You are asking for a retraction r : C --> C such
that q = q r. This gives us a section s : R --> C defined by s(q(a)) = r(a).
Such an s would embed the connected space R into the totally disconnected
space C, which is impossible.
For details and a classical argument see Theorem 4.1.15(2) of "Computable
Analysis" by Klaus Weihrauch. The relevant chapter is even available on the
More information about the FOM