Re: squares and cubes

Re: squares and cubes

[Dusko Pavlovic]

hi.

i somehow managed to unsubscribe from this list at some point, and almost
missed the thread about coalgebra of reals. i am not sure that i have seen
all the relevant postings, but here are my 2p of thoughts.

if i am not misunderstanding anything, peter freyd's closed interval
coalgebra achieves something that vaughan pratt's and mine do not. we work
with lists and streams and get *irredundant* representations of reals.
however, without redundancy, the algebraic operations on reals are
undecidable. peter's bipointed approach, however, induces a *redundant*
representation. this allows him to extract the algebraic operations
coinductively.

in the talk at the 1998 lisbon workshop on coalgebra (and later in some
seminar talks), i described a redundant coalgebra of conway reals, where
conway's definitions of the field operations were derivable as coalgebra
homomoprhisms. however, the setting seemed too complicated, probably due
to me. peter's definition of the midpoint algebra is considerably simpler,
although the resulting operations are probably still computationally quite
inefficient.

the coalgebra of alternating dyadics, described in the paper with vaughan,
was derived from this 'conway' coalgebra. as explained in sec 3.4, it
provides the best dyadic approximation, while the continued fraction
coalgebra, provides the best rational approximation. presumably, it can be
derived from the 'norton' coalgebra (contorted fractions), mentioned by
peter johnstone. there are as many redundant coalgebras of reals, as there
are corresponding irredundant ones (one for every interval partition), for
fast outputs.

i think that some of the mentioned *mysteries* about the maps between
these various representations boil down to the fact that they are
coalgebra isomorphisms, that do not preserve the derived structure, but
rather *transform* it. eg, the laplace transform is a coalgebra
isomorphism between the coalgebra of analytic functions and a dual
coalgebra of meromorphic functions --- whereby the convolution ring gets
transformed into a multiplicative domain, etcetc.

in any case, when you are done with reals, you may be interested to have a
look int my paper with martin escardo "calculus in coinductive form",
LICS98, or
ftp://ftp.kestrel.edu/pub/papers/pavlovic/LAPL.ps.gz

all the best,
-- dusko

PS along the lines of peter's bipointed construction (and also to check
whether i understood it):

* bipointed sets are the algebras for the functor 2+(-) :
Set -> Set.

* bipointed sets with two _distinct_ points are the free such algebras. so
lets work in the kleisli category *K* for 2+(-). write 2 = {0,1}

* the bifunctor (-) v (-) : *K* --> *K* maps

    * the objects X, Y to X + {m} + Y
    * the arrows X --f-->2+U and Y--g-->2+V to

        h : X+{m}+Y ---> 2 + U+{m}+V

        h(x) = f(x) if f(x) = 0  or f(x) in U
        h(x) = m if f(x) = 1
        h(M) = m
        h(y) = g(y) if g(y) = 1 or g(y) in V
        h(y) = m if g(y) = 0

* now (0,1) is the final coalgebra for the functor X v X on *K*. the
coalgebra structure

        (0,1) ---> 2+(0,1) +{m}+(0,1)

maps 1/2 to m, x<1/2 to 2x and x>1/2 to 2x-1.

* the finality is now easy to prove directly, by displaying the
anamorphism for any given coalgebra X -r-> 2+X+{m}+X. ditto for the
algebraic structure.

Re: squares and cubes

[Vaughan Pratt]

From: Dusko Pavlovic <dusko@kestrel.edu>
>if i am not misunderstanding anything, peter freyd's closed interval
>coalgebra achieves something that vaughan pratt's and mine do not. we work
>with lists and streams and get *irredundant* representations of reals.
>however, without redundancy, the algebraic operations on reals are
>undecidable. peter's bipointed approach, however, induces a *redundant*
>representation. this allows him to extract the algebraic operations
>coinductively.

I am deeply embarrassed at not drawing this inference myself.  I noticed
the felicitous identification of 0111... and 1000... but the importance of
the resulting redundancy didn't click.  That the whole process happened
in one step led me to think that the representation was as irredundant
as all extant one-step constructions.  The fact that addition is easier
to define with Peter's functor than with ours should have been a big hint.

Redundant representations for fast computer arithmetic have been in wide
use since the 1960's.  The Wallace tree, long available in chip form,
leverages the idea to multiply n bit integers with log n circuit delay.
(Chris Wallace is an Australian computer scientist who came up with
this idea while working on Illiac 2 at the University of Illinois.)
The actual multiplication takes half the time, the other half is spent
performing the identification step at the end, namely by putting the
result into canonical form.

All redundant representations of the reals that are or could be used
in computer architecture require a separate step to identify the
redundant representations.  For example Schanuel's recently discussed
almost-additive sequences of integers redundantly represent the reals,
and must be quotiented in order to represent them irredundantly.  By the
same token the group of bounded sequences that I mentioned does the
same, and it too must be quotiented in a separate step, in this case by
a subgroup expressing 2(x/2) = x.

Peter's final coalgebra performs the identification in the same step in
which the reals are created.  I am fairly confident there is no precedent
for such a one-step construction of the reals in which the representation
is redundant.

Vaughan Pratt

Re: squares and cubes

[Vaughan Pratt]

>I am deeply embarrassed at not drawing this inference myself.  I noticed
>the felicitous identification of 0111... and 1000... but the importance of
>the resulting redundancy didn't click.  That the whole process happened
>in one step led me to think that the representation was as irredundant
>as all extant one-step constructions.  The fact that addition is easier
>to define with Peter's functor than with ours should have been a big hint.

Well, maybe not so embarrassed after all.  Although there is some
redundancy, as Peter Selinger pointed out to me (in the same message where
he pointed out the problem with 1->3) there isn't enough redundancy to
make the function constituting Peter F.'s midpoint coalgebra computable,
at least not corecursively.

Given say -++---+-++... and +--+++-+--... (two complementary reals x and
-x, which must therefore sum to zero), if they stay complementary forever
one can output either of +---------... or -+++++++++... forever, with
one output bit per input bit.  These two infinite sequences redundantly
represent zero (as does the empty sequence).  Furthermore if one pictures
oneself as outputting both infinite sequences (justified by the idea that
in the limit they become the same real), then one can discard the "wrong"
one when it is discovered that the two inputs aren't complementary.
Addition defined corecursively in this way is effective.

But while this is computationally appealing, technically speaking it
isn't quite coinduction, which makes no provision for hedging one's bets
by carrying along both possibilities when you can't make up your mind.
To make traditional redundant computer arithmetic work coinductively,
more redundancy is needed.

To that end I tried tripointed sets, calling the constants -,0,+, along
with a functor 3(X) that makes not two but three copies of X and pastes
their constants together as follows:

	-  0  +
	   -  0  +
	      -  0  +
	-------------
	-  .  0  .  +

The idea is that the constants denote -1, 0, and 1 respectively and that
3(I) somehow is isomorphic to I, with the two dots becoming -1/2 and 1/2
respectively.  But for that to work 3(-) would have to paste a lot more
points than it does.

So this seems like a nice question: is there a category C and a functor
F:C->C whose final coalgebra is the continuum with sufficiently redundant
coalgebraic structure to permit addition to be defined coinductively?

Vaughan

squares and cubes

[Peter Freyd]

About an associative bifunctor I wrote

  There's a general theorem that says that a final coalgebra for 
  X v X  is automatically a final coalgebra for  X v X v X v X,
  indeed, for any such ordered-wedge where the number of copies of  X
  is a power of two. I haven't been able to find the proof for a 
  general theorem that specializes to  X v X v X.

Well, the proof is just a modification of an old one (of mine). And
once in hand, it makes clear the nonsensical nature of the
construction for the thirding map that appeared in my "Derivatives"
posting. (I'll replace it with a better construction in a later
posting.)

The general theorem is that if  T  is an endo-functor on a category 
with coproducts and if  f:F --> TF  is a final coalgebra then

   f     Tfn
F --> TF --> TTF  is a final  TT-coalgebra. (Citation below, albeit
for the dual case -- it appears that not everyone has noticed that
just by replacing the category in question with its dual one can
transfer any theorem about initial algebras to one about final
coalgebras.)

Let  X*Y  denote the values of a bifunctor (not necessarily 
associative) on a category with binary coproducts.

    If  f:F --> F*F  is a final "square coalgebra" then

        f       f*1
     F --> F*F ----> (F*F)*F  is a final "cubical coalgebra".

Given a cubical coalgebra  a:A --> (A*A)*A  consider the square 
coalgebra  A + A*A  --> (A + A*A)*(A + A*A)   whose left coordinate 

            a           r*l
map  is  A --> (A*A)*A ----> (A + A*A)*(A + A*A)  and whose right

                        l*l
coordinate map is  A*A ----> (A + A*A)*(A + A*A)  where  l  and  r  
denote the left and right coprojections for the coproduct.  Let  
A + A*A  --> F  be the induced map to the final square coalgebra and
let  a'  and  a'' be its coordinate maps. Then

           a'                            a''
     A --------> F        and      A*A ------> F
                                                       (add downward
   a |           | f              1 |          | f      arrowheads)

 (A*A)*A -----> F*F                A*A -----> F*F          
         a''*a'                        a'*a'

Consequently:
                             a'
                    A  --------------> F

                  a |                  | f
                            a''*a'
                (A*A)*A ------------> F*F

                  1 |                  | f*1

                (A*A)*A ---------> (F*F)*F
                        (a'*a')*a'

For the uniqueness, suppose that  a'  is as in the last diagram with
the middle arrow removed. Define  a'' so that the penultimate diagram
commutes (f, by Lambek, is an isomorphism). Then the map from  A + A*A
to  F  whose coordinate maps are  a'  and  a''  is a map of square 
coalgebras, hence  a'  is as already described.

For a counterexample for arbitrary categories, consider the discrete
category with two objects and bifunctor that turns it into the
two-element group. On discrete categories coalgebras are, of course,
the same as fixed points, and the only way a functor can have a final
coalgebra is if it has a unique fixed point. The object that serves
as the identity element for the group structure is thus the final
square coalgebra. But both objects are cubical coalgebras, hence 
there is no final cubical coalgebra.

There's nothing special about the number three. Given any iteration
obtainable from the bifunctor, the constructions above can be 
modified to provide proofs and counterexamples. Indeed, we needn't
restrict to bifunctors. For example, if  TXYZ  is a trifunctor on a 
category with binary coproducts, then a final coalgebra for  TXXX
gives rise to a final coalgebra for  TX(T(TXXX)X)(TXX(TXXX)).

But what I can't find a proof for is the analogue of this theorem,
good for any category (same citation):

  If  T  is an endo-functor and if  TT  has a final coalgebra
  then so does  T.

The analogue would be: if  X*Y  is a bifunctor and if  (X*X)*X  has
a final coalgebra then so does  X*X.  All my counterexamples --  here
and in the citation below -- are on discrete categories. For what it's 
worth, if an associative bifunctor on a discrete category is such that
X*X*X  has a final coalgebra, then so does  X*X.


Algebraically Complete Categories, Como Conference, Category Theory, 
     Proceedings of the International Conference held in Como, Italy,
     1990, Lecture Notes in Mathematics, 1488, Springer-Verlag, 1991