Reality check

Reality check

[Peter Freyd]

In an earlier posting I showed how to define co-inductively the closed
interval, in particular I showed that its elements are named by 
sequences of  0s  and  1s  with the usual binary-expansion equivalence
relation. There is a well-known computational problem with this 
approach, already in the definition of the midpoint operation: at what
point can you determine the first digit of the midpoint of .0000...  
and  .1111...? 

At the Como meeting I learned from Andrej Bauer about a  better
approach. Take the elements of  [-1,1]  to be named by infinite
sequences of _signed_ binary digits, that is -1, 0, +1.

[Just to confuse matters, Scedrov and I once used signed _ternary_ 
digits (n Cats and Allegators for the "Freyd curve"). The signed binary
expansions  .+1 -1  and  .0 +1  describe the same number, to wit, 1/4.]

Using signed binary expansions one can compute midpoints with a little
3-state machine that takes as input the sequence of pairs of signed 
binary digits of the given numbers  x  and  y, and produces as output
a sequence of signed binary digits for the midpoint  x|y. (There may,
indeed, be momentary delays in the output, but there will not be an
indefinite delay -- indeed, the number of output digits will never be
more than one less than the number of pairs of input digits).

The challenge is to revise the co-induction so that it is this better 
version that emerges.

In the previous version I worked in the category of posets with
_distinct_ top and bottom, that is, those posets for which

                      not[(B = x) and (x = T)].

In the revised version I'll strengthen the condition by working in the
category of posets with _separated_ top and bottom:

                         [(B < x) or (x < T)].

(The conditions are equivalent in the presence of De Morgan's law. In
a topos the top and bottom of omega are always distinct but they are
separated only when De Morgan's law is satisfied throughout.)

In the previous setting I defined what I'll now call the _thin_ 
version of the ordered-wedge of  X  and  Y, to wit, the set of pairs,
<x,y>  satisfying the condition:

                          (x = T) or (B = y).

The _thick_ version is the set of pairs, <x,y>  satisfying the two 
weaker conditions:
                          (x < T) => (B = y)
                          (B < y) => (x = T)

(each of which is classically equivalent to the single condition used 
in the thin version).

Easy exercise: if top and bottom are separated in  X  and  Y, then 
they are separated in the thick version of the ordered-wedge  XvY.
(Indeed, it's enough for top and bottom to be separated in just one of
X  and  Y . No, it is not enough to assume just that they are distinct
in each.)

A map  X -> XvX  is thus given by a pair  d,u: X -> X  such that for
all  x:
                         (dx < T) => (B = ux)
                         (B < ux) => (dx = T)

The final coalgebra for  XvX  is still the closed interval, but now in 
the better computational sense. Let me explain.

Given an arbitrary coalgebra  d,u : X -> X, I need to describe a 
coalgebra homomorphism  f: X -> I. where  I  is the set of equivalence
types of infinite sequences of signed binary digits.

The first step is to work not with elements of  X  but elements of 
XvX. Consider a machine that given  <x,y>:XvX  asks in parallel the
questions:
                         "B < y?"
                         "B < ux  and  dy < T?"
                         "x < T?"

Exercise: If the top and bottom of  X  are separated and  d,u 
describe a map to the thick ordered-wedge  XvX, then at least one of
these questions has a positive answer.

Given  z:X  obtain a sequence of signed binary digits by starting with
the pair  <x,y> = <dz,uz>  and iterating the  non-deterministic 
procedure:

  If  B < y               
    then emit  +1  as output and replace  <x,y>  with  <dy,uy>;
  If  B < ux  and  dy < T  
    then emit   0  as output and replace  <x,y>  with  <ux,dy>;
  If  x < B      
    then emit  -1  as output and replace  <x,y>  with  <dx,ux>.

Not-so-easy exercises: regardless of the non-determinism, the element 
fz:[-1,+1]  named by the resulting sequence is determined. Moreover,
f(uz) = u(fz)  and  f(dz) = df(z).


PS. There is some geometry behind this stuff. Let me here mention just
this: given a pair  <x,y>  in  XvX  map it into the four-fold 
ordered-wedge  XvXvXvX. Think of each of the four copies of  X  as one
"quarter" of the whole. If  B < y  then the point lies inside the "top
half" (the 3rd and 4th quarters). If  B < ux  and  dy < T  then the 
point lies inside the "middle half" (the 2nd and 3rd quarters). If 
x < B  then the  point lies inside the bottom half" (the 1st and 2nd
quarters). Clearly any point is inside at least one of these three 
halves. The output-digit registers which of the three halves is moved
to and the corresponding pair-replacement effects that move.


PPS. On 22 Dec I gave a Dedekind-cut proof that the interval  [0,1]  
constructed in the standard fashion from (unsigned) binary sequences 
is the final coalgebra for the functor that sends  X  (with distinct 
top and bottom) to the thin version of  XvX. That proof should be 
replaced. First note that the midpoint-algebra homomorphism from  [0,1]
to  [-1,1]  can be effected simply by replacing each  0  with  -1  and
keeping each  1  as  +1. Given  d,u:X -> X  such that for all  x  it is
the case that either  dx = T  or  ux = B , consider a machine that upon
given  x:X  asks in parallel the questions  "dx = T?"  and  "ux = B?".
 
 If  dx = T  then emit  +1  as output and replace  x  with  ux, 
 If  ux = B  then emit  -1  as output and replace  x  with  dx. 

Given  x:X  one may iterate this (non-deterministic) procedure to
obtain a sequence of  +1s  and  -1s. Pretty-easy exercises: regardless
of the non-determinism, the element  fx:[-1,+1]  named by the
resulting sequence is determined; f(ux) = u(fx); f(dx) = df(x).

Re: Reality check

[Martin Escardo]

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 

Re: Reality check

[Andrej.Bauer]

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 <konecny@rect.muni.cz>, 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.

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.


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

Re: Reality check

[Martin Escardo]

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.

Re: Reality check

[Alex Simpson]

Martin writes:

>  > [Discussion about intuitionistic versions of Freyd's construction
>  > deleted.]

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: Alex.Simpson@dcs.ed.ac.uk             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