Re: Real midpoints

[Peter Selinger <selinger@math.lsa.umich.edu>]

> > 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.

Dusko Pavlovic wrote:
> what exactly do you mean by corecursive? (it's guarded, and guarded equations
> 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