[FOM] Primitive recursive reals

[Andrej Bauer]

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 
computability properties.

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 
net at 
http://www.informatik.fernuni-hagen.de/thi1/klaus.weihrauch/book.html .

Andrej Bauer