categories: Re: Real midpoints

[Dusko Pavlovic <dusko@kestrel.edu>]

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

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