Re: Cauchy completeness of Cauchy reals

[Vaughan Pratt <pratt@CS.Stanford.EDU>]

Dear toposophers,

With constructivity of real arithmetic back on the front burner for the
moment, let P be the ring of bounded power series a0 + a1.x + a2.x^2 + ...
with integer coefficients a_i, where the bound is, for each such series,
an integer c such that |a_i| < c (3/2)^i / i^(3/2).

Let 1-2x generate the ideal I of P.  Then the quotient ring P/I turns out
to be the field of reals [AMM 105(1998), p.769].

This is more constructive than it might appear, being just an obscure
(or clear depending on your upbringing) way of representing reals in a
redundant binary notation.  The ring P permits fast arithmetic essentially
by deferring carries.  Carries are "propagated" when needed by quotienting
by I, which works by collapsing every formal power series to one all of
whose coefficients other than a0 are either 0 or 1 and which has infinitely
many 0s (equivalently, no infinite run of 1's).

In this view of things, a real is understoood as an integer (a0) plus a
binary fraction in [0,1) (the rest of some "binary" formal power series,
meaning one with a_i = 0 or 1 for i > 0 and infinitely many 0s).  A general
formal power series without this restriction to 0 and 1 then constitutes
a redundant representation of a real, which can be made irredundant when
needed (e.g. when comparing with <) by quotienting by I.

An intuitively clear but less constructive view is to evaluate each series at
x = 1/2, the root of 1-2x, noting that any series bounded as above converges
absolutely there.  Series identified by I are those that evaluate to the
same real at x = 1/2.

What is nonconstructive about this is that direct evaluation of an infinite
series at a point requires infinite time, no matter how large and parallel
the infinite circuit computing it may be.

In contrast, P and P/I are more constructive in the following sense.
Addition and subtraction in P require circuit depth O(1) using an infinite
circuit whose gates perform integer addition and subtraction (just do it
coordinatewise).  Reduction mod I takes longer, but there is a variant of
the above in which it is fast enough.  Instead of the field R we settle
for just the group R, and instead of |a_i| < c (3/2)^i / i^(3/2) we settle
for simply |a_i| < c.  In this case any given series can be reduced (same
generator 1-2x) to the above normal form in circuit depth log_2(c) (nice
exercise), a finite quantity despite the series itself being of infinite
length and fluctuating arbitrarily within ±c.

Multiplication is problematic for two reasons.  First it obliges the weaker
bound, complicating reduction.  Secondly it is a convolution, complicating
arithmetic even when carry propagation is deferred.  I don't see obvious
solutions to either of these problems.  On the other hand I have no a priori
reason to suppose that these circuit-theoretic complications of passing
from R as a group to R as a ring or field would be reflected in suitably
constructive topos-theoretic developments of these notions.

Vaughan Pratt