Subject: categories: Re: Real midpoints

From: Peter Selinger <[email-masked]>
Date: Sun, 16 Jan 2000 20:23:36 -0500 (EST)

Dusko Pavlovic wrote on Jan 15:
> peter's bipointed approach, however, induces a *redundant*
> representation. this allows him to extract the algebraic operations
> coinductively.

Sorry for lagging a few weeks behind in this discussion. Something has
been bothering me about Peter's definition of the midpoint operation
(Dec 26). How can it be coinductive, but the resulting function is not
computable? After mulling it over, I realized that Peter's definition
is *not* coinductive: He gives an equation which has a unique
fixpoint, but it is not a coinductive fixpoint. I believe that Peter's
representation has not enough redundancy to define the algebraic
operations in a purely coinductive manner. Note however that Peter
really only wanted to define the algebraic structure from the final
coalgebra structure on  I = [-1,1];  he did not claim to do it purely
coinductively.

Recall Peter's definition of the midpoint operation (where  h:I-->I  is
the "halfing" map  h(x) = x|0).  I have corrected some typos in lines
4+5:

> Let  g  be the endo-function on  I x I  defined recursively by:
>
>     g<x,y> = if  dx = T  and  dy = T  then             <x,y>    else
>              if  dx = T  and  uy = B  then  (h x h) (g<ux,dy>)  else
>              if  ux = B  and  dy = T  then  (h x h) (g<dx,uy>)  else
>              if  ux = B  and  uy = B  then             <x,y>.
>
> The values of  g  lie in the first and third quadrants, that is, those
> points such that either  dx = dy = T  or  ux = uy = B.  The two maps
>
>            g       d x d                   g       u x u
>     I x I --> I x I --> I x I  and  I x I --> I x I --> I x I
>
> give a coalgebra structure on  I x I.  The midpoint operation may be
> defined as the induced map to the final coalgebra.

I think Vaughan has already pointed out that this is not well-defined,
because the four cases in the definition of g are not mutually
disjoint and the right-hand sides do not match; thus let us assume we
write  "dx != T"  instead of  "ux = B",  and similarly for  y.  Note that
the resulting map is neither continuous nor monotone; thus, we are
definitely forced to work with bipointed sets, not posets, for this
construction.

My point is that the definition of  g  is neither recursive nor
co-recursive. The definition of  g  is merely expressed as a fixpoint
equation, and Peter has set up things so that there is indeed a unique
solution to this equation. However, the reason the fixpoint is unique
is because the  "h"  part is contracting, and not because the equation
is co-recursive.

If we write  g  as a pair  <g1, g2>: I x I --> I,  we can separate the
equation for  g  into two equations about  g1  and  g2.  A priori, these two
equations are mutually dependent, but interestingly, it turns out that
they are independent, so we need not worry about simultaneous
fixpoints.  The equation for  g1  can be written as

           s x s                      dist
    I x I -------> (I + I) x (I + I) ------> IxI + IxI + IxI + IxI

      |                                                |
(1)   | g1                                             | pi1 + g1 + g1 + pi1
      |                                                |
                      [h-,h,h,h+]                       
      I  <----------------------------------  I  +  I  +  I  +  I

(add downward arrow heads), where  s: I --> I v I --> I + I  is the
composition of the coalgebra morphism  F  for  I  with one of the two
obvious maps  I v I --> I + I  (the one that sends the midpoint to the
second component, say).  "dist" is distributivity, and  h-  and  h+  are
the maps defined by  h-(x) = x|-1  and  h+(x) = x|1  (these have explicit
definitions similar to that of the halfing map  h).

The equation for  g2  is similar. One obtains it by replacing  pi1
with  pi2.

For this diagram to be considered a co-recursive definition of  g1,  it
would have to be equivalent to a diagram of the form

                    G
    I x I ---------------> (I x I) v (I x I)

      |                            |
(2)   | g1                         | g1 v g1
      |                            |
                    F
      I  --------------------->  I v I

for some suitable coalgebra  G  on  I x I.  This, however, is not the
case, unless (in a suitable sense)  G  is just as complex as  g1  is. For
instance, the first bit (trit?) of  G(x,y)  is the same as that of
g(x,y),  which is the same as the first bit of  midpoint(x,y).  But
the first bit of the midpoint cannot be computed with finite lookahead
(consider  x = 1/3 = +-+-+-...  and  y = -1/3 = -+-+-+...).  Thus, the
first bit of  g  or  G  can't be computed either, and no matter through
how many levels of co-recursion we go, we never arrive at an
elementary function.  Thus, there is no chance of defining the
midpoint operation from elementary functions through a finite chain of
co-recursions.

It ought to be possible to formalize this argument.  Intuitively, note
that in diagram (2),  g1  appears in something like a "tail recursive"
position, whereas in diagram (1) it does not. Thus, if  G  is computable
with finite lookahead (as a function on pairs of streams), and  g1  is
defined like in (2), then  g1  is also computable with finite lookahead:
namely,  G  will tell us the first trit, plus a continuation, and the tail
recursive call will compute the rest. Thus computable functions on
streams are closed under co-recursion (as they should).

Finally, Peter's definition of the midpoint function utilizes the
function  g  and then lifts it through one level of co-recursion. It
is, however, possible, to define the midpoint function directly
without going through this  g:  It is the unique morphism  m: I x I --> I
that makes the following diagram commute:

           s x s                      dist
    I x I -------> (I + I) x (I + I) ------> IxI + IxI + IxI + IxI

      |                                                |
(1)   | m                                              | m + m + m + m
      |                                                |
                      [h-,h,h,h+]                       
      I  <----------------------------------  I  +  I  +  I  +  I.

Or, if you prefer, it is the unique solution of

     m<x,y> = if  dx =  T  and  dy =  T  then  h+ (m<ux,uy>)  else
              if  dx =  T  and  dy != T  then  h  (m<ux,dy>)  else
              if  dx != T  and  dy =  T  then  h  (m<dx,uy>)  else
              if  dx != T  and  dy != T  then  h- (m<dx,dy>)

This definition, of course, is not co-recursive either.  If I am not
mistaken, it is more or less what Vaughan defined in his mail on 
Dec 24, except he separated the case for  dx = T  into two cases 
ux != B  and  (dx=T and ux=B)  (and similarly for  y).

Best wishes, -- Peter Selinger

---

From: Dusko Pavlovic <[email-masked]>
Date: Mon, 17 Jan 2000 20:07:28 -0800

> is because the  "h"  part is contracting, and not because the equation

what exactly do you mean by corecursive? (it's guarded, and guarded equations
do have unique fixpoints.)

-- dusko

---

From: Peter Selinger <[email-masked]>
Date: Tue, 18 Jan 2000 11:16:22 -0500 (EST)

> do have unique fixpoints.)

The definition I had in mind is that an arrow g is defined from G by
co-recursion "in a single step" if it arises as the unique coalgebra
homomorphism from a coalgebra G to the terminal coalgebra.  It is
defined by co-recusion "in multiple steps" if it is obtained from
certain basic morphisms by repeated applications of the above single
step, together with basic operations on morphisms. I am not so sure
what I mean by "basic"; but I have in mind morphisms and operations
that are defined by ordinary equations (as opposed to fixpoint
equations) from the structure of the category at hand (such as
composition, pairing, the functor "X v Y", etc).

What's the exact definition of "guarded" in this context? I assume
that h x h would be the guard. The fact that Peter's equation has a
unique fixpoint relies on the fact that h x h is contracting. It
follows, for instance, from Banach's fixpoint theorem. If one omits
the "h x h", there are multiple fixpoints.  It seems that the proof
that Peter's equation has a unique fixpoint is independent of the
underlying representation of [0,1], whereas my proposed definition of
"co-recursive" is not.

By the way, Peter's definition of the "halfing" map does not quite fit
my idea of a "basic" map above: 

> Let  F:I --> I v I  be a final coalgebra. We will denote the top of  I
> as  T  and the bottom as  B.  Construct the "halving" map,  h:I --> I,
> (on  [-1,1]  it will send  x  to  x/2)  as:  
> 
>                    T v F v B             F'v F'        F'
>     I --> 1 v I v 1 ------> I v I v I v I ---> I v I  --> I
> 
> where  F' denotes the inverse of  F, and, by a little overloading, T
> and  B  denote the maps constantly equal to  T  and  B.  The leftmost
> map records the fact that the terminator is a unit for the 
> ordered-wedge functor.

The problem is that "X v Y" is only functorial on morphisms that
preserve top and bottom, and neither T nor B are of that form. Thus it
seems one needs to briefly step outside the category to justify this
particular definition of h.

-- Peter

---

From: Dusko Pavlovic <[email-masked]>
Date: Wed, 19 Jan 2000 12:23:09 -0800

> composition, pairing, the functor "X v Y", etc).

i think such class of corecursive functions would be too narrow: eg, it
seems that only a small part of the elements of the final coalgebra (the
"rationals") can be captured as corecursive constants, at least as long as
your basic operations are finitary. while the class of recursive functions
is countable, the class of corecursive functions should not be, if
constants are to be included.

> What's the exact definition of "guarded" in this context?

in stream and list coalgebra, a fairly obvious semantic condition covers
not only the usual syntactical guard conditions, but also the convergence
criteria for power series solutions of, say, diff eqns. it's in my CMCS98
paper

@article{PavlovicD:GIFC
  author =       "Dusko Pavlovi\'c",
  title =        "Guarded induction on final coalgebras",
  journal =      "E. Notes in Theor. Comp. Sci.",
  pages =        "143--160",
  year =         "1998",
  volume =       "11",
  url =          "http://www.elsevier.nl/locate/entcs",
}

saying "categorically" which operations are guarded wrt an arbitrary functor is
less straightforward... or at least less easy to justify. i worked on this, but
never managed to get a really convincing formulation. (a clumsy one is on my web
page.)

-- dusko