Subject: categories: Re: Reality check

From: Martin Escardo <[email-masked]>
Date: Tue, 1 Aug 2000 12:56:37 +0100 (BST)

Here are a comment and a question regarding the interesting reality
check.

Peter Freyd wrote, among other things:
 > Take the elements of  [-1,1]  to be named by infinite
 > sequences of _signed_ binary digits, that is -1, 0, +1.
 > 
 > [...]
 > 
 > The signed binary
 > expansions  .+1 -1  and  .0 +1  describe the same number, to wit, 1/4.

In a way, the finitary identities

      +1 -1  ==  0 +1  

together with their symmetric versions

      -1 +1  ==  0 -1  

capture *all* identifications made by the quotient map

     3^N  -->>  [-1, 1]

      s  |-->    [[s]] = s1 / 2  +  s2 / 4  + ... +  sn / 2^n + ... 

that takes a signed-digit binary expansion s to the number [[s]] that
it denotes. Here 3 = {-1,0,+1}, and I am supposing initially that
[-1,1] is already given.

Let === be the kernel of the quotient map:

     s === t  iff [[s]] = [[t]].

Let == be the least equivalence relation on 3^N such that

     s +1 -1 t == s 0 +1 t
and
     s -1 +1 t == s 0 -1 t,

where s ranges over 3^* and t over 3^N. 

It is easy to see that == is coarser than ===.  It is *strictly*
coarser as, for example, we have that

	-1 1 1 1 1 1 1 1 1 ... === 1 -1 -1 -1 -1 -1 -1 ..., 

because both sequences denote the number zero, but === cannot be
replaced by ==, because these two sequences cannot be made equal by
finitely many applications of the identities.

HOWEVER, if one endows 3^N with the Cantor topology (the product of
the discrete topology of 3), then the relation === is the topological
closure of the relation == in the product space 3^N x 3^N. 
That is, all we need to do in order to get === from == is to add
limits. 

Thus, === can be defined in a topologico-combinatorial way *without*
reference to a previously existing interval [-1,1]. Therefore we have
a simple direct (classical) construction of the Euclidean interval
[-1,1] as a topological quotient of 3^N by an easily defined
equivalence relation of finite character.

(NB. Of course, === has to be closed, because [-1,1] is Hausdorff and
the semantic map is continuous (and hence a topological quotient map,
as it is a surjection of compact Hausdorff spaces). Thus, another way
of putting the above is to say that == fails to be === only by failing
to be closed.)

Moreover, there is a *computable* idempotent function 

	  f : 3^N x 3^N --> 3^N x 3^N 

with the property that if f(s,t)=(s',t') then 

     (1) s===s', t===t' and

     (2) if s===t then s' = t' 

            (Yes, I mean this; s' and t' are the *same* sequence.)

As this may sound puzzling at first sight, let me observe that it
doesn't help in effectively deciding equality, nor does it show that
numbers would have canonical representatives, because norm(s,s)=(s,s)
is consistent with the above specification.

Such a function f(s,t) is computed by a finite automaton that tries to
apply the two identities to make s and t equal, by scanning longer and
longer finite prefixes of s and t, where this attempt fails at some
finite stage if and only if s and t denote distinct numbers.  At most
n+2 digits of input have to be scanned in order to produce n digits of
output.

(Reference: "Effective and sequential definition by cases on the reals
via infinite signed-digit numerals", Volume 13 of Electronic Notes in
Theoretical Computer Science, 1998.)

---------
Question: 
---------

Can we replace topology by coinduction in the formulations (and
proofs) of the above properties?

Martin Escardo

---

From: Martin Escardo <[email-masked]>
Date: Fri, 4 Aug 2000 11:23:36 +0100 (BST)

I can't answer Andrej's questions, but I can make a few
observations. 

 > It would be interesting to simplify this presentation even further by
 > using a signed representation with digits -1 and 1 only, in base B
 > strictly between 1 and 2. For example, the golden ratio base B = (1 +
 > sqrt(5))/2 seems to be very popular among exact real arithmetic
 > people. But it's unclear how to make a finite state automaton for
 > negation of === in this case.

In base Golden Ratio with digits 0 and 1 (proposed by Pietro Di
Gianantonio), the family of identities that generates === is

   ... 100 ... === ... 011 ... 

It corresponds to the fact that the Golden Ratio is the positive
solution of the equation x^2 = x + 1.

    (i.e. 1 x^2 + 0 x^1 + 0 x^0 = 0 x^2 + 1 x^1 + 1 x^0)
          =       =       =       =       =       =

What I have reported about signed-digit binary notation has also been
developed for Golden-Ratio notation by David McGaw in his Honours
project ( http://www.dcs.st-and.ac.uk/~mhe/macgaw.ps.gz ).  You may be
able to get a finite automaton from his algorithm for solving the word
problem. It should be even simpler than the one for signed binary,
because there are fewer cases to consider.

 > [Discussion about intuitionistic versions of Freyd's construction
 > deleted.]
 > This [discussion] leads to the idea that we should think of
 > the closed interval I as being glued like this:
 > 
 >              I
 >       |------------|--R--|
 >                    |--L--|------------|
 >                             I

This is precisely what the Golden-Ratio notation achieves.

The interval I is now [0,phi], where phi is the Golden Ratio.

Then the "digit maps" are l(x)=(x+0)/phi and r(x)=(x+1)/phi.

The intersection of the images of l and r is a closed interval with
non-empty interior, as in your picture. 

The above family of identities is equivalent to the single equation
l o r o r = r o l o l.

One could try to consider algebras with two operations and this
equation in order to get the interval in a more constructive way.

---

From: [email-masked]
Date: 03 Aug 2000 16:28:59 -0400

I just returned from an idyllic island in the Adriatic sea, so I am
joining the discussion on the reals a bit late.

Jesse Hughes and I have thought about some of the questions that have
been discussed so far in February, and I would like to report on what
we had come up with.

1.

Martin Escardo asked whether it is possible to define the signed
binary digit representation of [-1,1] in purely coinductive form. This
can be done as follows (I am using Martin's notation for === and [[s]]).

Let 3 = 1 + 1 + 1 = {-1, 0, 1}, and let C be the final coalgebra for
the functor X |--> 3 x X. If the ambient category is nice enough C is
the Cantor space 3^N, but we stick to purely coinductive language and
think of elements of C as streams. Since C is the final coalgebra for
X |--> 3 x X, every stream in C can be written uniquely in the form
h::t where h is the "head" digit and t is the "tail" of the stream.

The question is how to define the coincidence relation === on C
without reference to the closed interval. The right person to ask this
was Michal Konecny <[email-masked]>, a student of Achim Jung's,
who studied what functions on real numbers can be computed by finite
state automata (he also knows very well what exactly can be computed
with finite state automata---there seems to be a close relation to
f.s.a. and coinductive definitions). He immediately came up with a
finite state automaton that accepts the negation of ===, from which a
coinductive definition of === can be obtained easily. Michal produced
pretty pictures that you can see at http://andrej.com/michal.ps

The trick is to define === together with an auxiliary relation ~==.
The intended meaning of s ~== t is [[s]] = 1/2 + [[t]]. It goes as
follows:

 x::a === y::b  <==>    (x=y, a === b) or
                        (x=1, y=-1, a=-1-1-1..., b=111...) or
                        (x=-1, y=1, a=111..., b=-1-1-1...) or
                        (x=0, y=1, a ~== b) or
                        (x=-1,y=0, a ~== b) or
                        (x=1, y=0, b ~== a) or
                        (x=0, y=-1, b ~== a)

 and

 x::a ~== y::b  <==>    (x=1, y=-1, a ~== b) or
                        (x=0, y=-1, a ~== b) or
                        (x=1, y=0, a ~== b) or

Now let I be the quotient of C by ===. If the category is rich enough
we can show that I is the closed interval of Cauchy reals.

2.

Alex Simpson suggested that we should look for what he calls
"pseudo-ordering" instead of the classical "linear ordering". I
definitely agree with that. I would just like to say that in my view
it is better to say "(intuitionistic) linear order" than
"pseudo-order" since the three axioms (by the way, there is no need to
explicitly quantify over z in the second axiom, is there?)

  1. not (x < y and y < x)

  2. x < y ==> (x < z or z < y)

  3. (not (x < y or y < x)) ==> x = y

are classically equivalent to the usual axioms for linear order, as
far as I can tell. So there is nothing "pseudo-" about the axioms,
unless intuitionistic logic is "pseudo-logic"...

I also agree with Alex that gluing along a point is not the right
thing to do, from a constructive/intuitionistic point of view.

3.

Lastly, let me suggest another construction which Jesse and I have
come up with, but we are unable to verify whether it works. Perhaps
someone who does not get confused so quickly by too many arrows can
tell us if it is worth anything.

We were thinking like this. Consider the construction described by
Peter Freyd, where we take objects with distinguished elements 0 and 1.
We require that not (0 = 1) and then we define a "gluing functor"
X |--> X v X which identifies 0 from one copy of X with 1 in the other
copy of X. Then it turns out that (classically) the final coalgebra
for the gluing functor is the closed interval I. This construction
does not work in the intuitionistic case because gluing along a single
point is a very classical construction. For an intuitionistic
construction we should glue along an interval so that we have some
"numerical tolerance". This leads to the idea that we should think of
the closed interval I as being glued like this:

             I
      |------------|--R--|
                   |--L--|------------|
                            I

That is, we replace the notion of "bottom 0" and "top 1" with "left
part L" and "right part R". In categorical language, the global points
0: * ---> I and 1: * ---> I are replaced with regular subspaces
L: I >--> I and R: I >--> I. So the obvious thing to attempt is to
consider objects X with distinguished "right part R: X >--> X" and
"left part L: X >--> X". However, this doesn't work because when we form 
the pushout

          R
      X >----> X
      V        V
    L |        |
      |       _|
      V      | V
      X -----> Y

we are stuck since we don't know how to obtain the left and right
parts of Y (they should be regular monos Y >--> Y). But we can fix
this by removing the condition that the left and the right part be
isomorphic to the whole, which gives us the following construction:

As objects we take pairs of parallel regular monos

    >--R-->
  X >--L--> Y

We think of R as the "right part of Y" and L as the "left part of Y".
There is an obvious notion of morphism between such objects
R,L: X >--> Y and R',L': X' >--> Y', namely a pair of arrows x: X ---> X'
and y: Y ---> Y' such that the following two diagrams, folded into a single
picture, commute:

      >--R-->
    X >--L--> Y
    |         |
  x |         | y
    |         |
    V         V
    X'>--R'-> Y'
      >--L'->

Define the gluing functor which maps such an object R,L: X ---> Y to the
object R',L': Y ---> Z where Z, L', and R' appear in the pushout diagram:

          R
      X >----> Y
      V        V
    L |        | L'
      |       _|
      V      | V
      Y -----> Z
          R'

We probably have to require that R and L are distinct regular monos
(just like we required that 0 and 1 are distinct, and they were
regular monos for free). We also have to assume that pushouts of
regular monos along regular monos are regular monos.

Question: does this functor have a final coalgebra, say in the
category of sets? How about in a topos with natural numbers object?

Observe that if there is a final coalgebra, then it is necessarily of
the form R, L: I >--> I, the left and the right parts are isomorphic
to the whole, because the structure map of a final coalgebra is an
isomorphism. So this much at least works out fine.

I have a feeling that the construction won't work, which is not bad
anyway, since the midpoint construction together with the completness
axiom of Alex's and Martin's works beautifully. I am just curious to
see what the final coalgebra might be.

Andrej

---

From: Alex Simpson <[email-masked]>
Date: Fri, 04 Aug 2000 12:16:52 +0100

>  > [Discussion about intuitionistic versions of Freyd's construction

So, in response to that aspect:

Peter's motivation was to capture the signed binary interval rather 
than the binary one, a distinction that only exists in an 
intuitionistic setting. For (at least) this reason, his original 
definition was already intuitionistic (indeed his axioms were 
explicitly formulated in an intuitionistically appropriate form). 
The point I was making was that, given that one is already being 
sensitive to intuitionistic formulations, one also needs to be
equally careful about other aspects of the axiomatization (e.g. 
the definition of a suitable category of ordered sets). I was
curious to know which of the (apparently many) possible alternative 
definitions Peter had in mind.

It seems to me eminently plausible that Peter's construction works 
perfectly for the previously discussed intuitionistic linear orderings 
(I agree with Andrej about terminology - I took my terminology 
"pseudo ordering" from Peter Aczel). In fact, I would expect it to give 
the closed interval of Dedekind reals in any elementary topos with nno.
(Peter's proof that one obtains the signed-binary = Cauchy interval does 
indeed appear to use number-number choice.) I think that would be
a very nice result.

Peter, is this the sort of thing you're aiming at?

Alex

-- 
Alex Simpson, LFCS, Division of Informatics, University of Edinburgh
Email: [email-masked]             Tel: +44 (0)131 650 5113
FTP: ftp.dcs.ed.ac.uk/pub/als                Fax: +44 (0)131 667 7209  
URL: http://www.dcs.ed.ac.uk/home/als