Re: "Kantor dust"

[Vaughan Pratt <pratt@cs.stanford.edu>]

Prof. Peter Johnstone wrote:
> On Mon, 9 Feb 2009, Dusko Pavlovic wrote:
>> QUESTION 2: is there a branch of constructivism that would reject as
>> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N
>> as the coefficients of continued fractions?
>>
> I don't think there is any doubt that the map exists. The problem is that,
> for most if not all schools of constructivism, it's wildly non-surjective.

There is more than one notion of continued fraction.  I suspect you're
thinking of one of the more commonly used ones, but in the light of
Dusko and my CMCS'99 paper, which talks about a number of notions of
continued fraction, I imagine Dusko had one in mind for which the map is
classically a bijection, and surely should continue to be so for at
least some schools of constructivism.  Let me give a (hopefully) careful
proof of this here.

As I observed in a previous post, the pathological definitions of
"continued fraction" giving the behaviour you may be thinking of are
those whose coinductive step is antimonotone, e.g. via a function from
[0,oo) to (0,1] such as 1/(1+x).  These appear in the literature not
from any desire to be pathological but merely because they tend to be
the first ones that come to mind, and their non-surjectivity is simply
not noticed by the naive programmer.

In contrast, monotone functions from [0,oo) to [0,1) such as x/(1+x) or
2*atan(x)/pi, with respective inverses x/(1-x) and tan(pi*x/2), do not
create this pathology in the continued fractions based on them, and give
rise to maps from N^N to [0,1) and [0,oo) that are not only surjective
but bijective, as well as monotone increasing with respect to the
lexicographic order on N^N.

Let R: N^N --> [0,oo) be the strictly monotone increasing function (with
respect to the lexicographic order on N^N) defined coinductively as

   R(s) = s(0) + f(R(s o succ))

where s: N --> N is a sequence in N^N (a function on N),
f: [0,oo) --> [0,1) is a strictly monotone increasing function, for
example f(x) = x/(1+x), and succ: N --> N is the successor operation of
the NNO N.

As a (surely constructive!) witness to the surjectivity, indeed
bijectivity, of R,  define the inverse S: [0,oo) --> N^N  of R as
follows.  (R converts sequences to Reals, which S turns back into
Sequences.)

   S(x)(0) = floor(x)
   S(x)(n+1) = S(g(x mod 1))(n)

where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is
the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition
of R.

As an aside for any visual thinkers reading this, the picture

   [0,oo)  ~  [0,1)[1,2)[2,3)...

may help.  This splits [0,oo) into N unit intervals each identifiable
with [0,1), each of which is blown back up to [0,oo) (under this
identification) by g(x) = x/(1-x).  The function S: [0,oo) --> N^N
converts nonnegative reals x to sequences of natural numbers by taking
the first element of the sequence to be floor(x), thereby selecting one
of the unit intervals, leaving x mod 1 to be accounted for within that
interval, of type [0,1), which is blown back up to type [0,oo) using g
and then inductively converted to the rest of the sequence by S.  In
this way we drill down into [0,oo) cranking out natural numbers as we
drill progressively deeper.

For the typing N^N --> [0,1) that Dusko asked about, the codomain of R
is easily converted from [0,oo) to [0,1) by composing the monotone
bijection  f : [0,oo) --> [0,1)  with the monotone bijection R : N^N -->
[0,oo) to give a monotone bijection from N^N to [0,1).

In the topos of sheaves on either R itself or the subcategory of Top you
prefer, I am not a topos hacker and have no idea whether there are more
than two functions from N^N to 2 = 1+1 when N^N is defined coinductively
as a final coalgebra (as distinct from being defined simply by
exponentiation, where surely there are more than two such functions).
Toby Bartels claims it's obvious, in which case there should be a short
construction of a nonconstant function from N^N (as a final coalgebra)
to 2 (or to N, the codomain Toby spoke of) in the topos of sheaves on R.
  Toby, what is it?

Vaughan Pratt

PS.  None of this contradicts the point you (PTJ) and Freyd have been
making, since around 2002 apparently, concerning the constructive merits
of apartness as an implementation of the glue used in the Freyd
coalgebra, which I only very belatedly came to appreciate, namely within
the past two days.  In view of this I retract my "The choice of poisons
is therefore manual glue vs. double induction" of last Wednesday.  I am
willing to believe that the Freyd coalgebra with manual glue implemented
via apartness produces the "real reals" in these toposes of sheaves, but
would like eventually to understand why of course.  That said, I would
still like to know whether our final coalgebra, for FX = N x X where x
is "lexicographic product" suitably defined for an NNO N in a topos, is
or is not equally real in these toposes.  If it is then this would be a
situation where apartness is not needed to produce the reals
constructively, presumably contradicting Brouwer.