It could well be that Vaughan and I are defining the midpoint structure in the same way. Here's how I described it (using the conventions from my last posting). 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. 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(g(dx,uy>) else if ux = B and dy = T then h(g<ux,dy>) 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.
From: Peter Freyd <pjf@saul.cis.upenn.edu>
It could well be that Vaughan and I are defining the midpoint structure in the same way.
Yes, after changing g(dx,uy) to g(ux,dy) in line 2 of Peter's definition of g and similarly for line 3 (otherwise g(dx,uy) simplifies to the nonsensical g(T,B)) Peter and I have essentially the same coalgebra on IxI, and exactly the same after some inessential permutations within that definition. While I rather like Peter's nonrecursive definition 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 of the halving map h:I --> I sending x to x/2, it should be remarked that the effect of this map as an operation on sequences is to preserve the empty sequence, and for nonempty sequences simply to prepend a copy of the leading digit, e.g. -++-+000... becomes --++-+000.... (This takes the 3-symbol alphabet for Peter's number system to be {-,0,+}.) In other words, right shift by one with sign extension, a well-known realization of halving. Along the same lines, Peter's d and u maps shift the sequence left. If d (resp. u) shifts a + (resp. -) off the left end, the result is replaced by the constantly + (resp. -) sequence, i.e. "clamp overflow to +1 (resp. -1)". Although the interval [-1,1] goes naturally with Peter's final coalgebra, it occurrs to me that a fragment of Conway's surreal numbers is perfectly matched to it, namely the interval [-\omega,\omega] consisting of the real line plus two endpoints. With respect to the Conway story this can be described as what Conway produces by day omega, modulo infinitesimals (identify those surreals that are only infinitesimally far apart). At no day does exactly the real line appear in Conway's scenario. Prior to day omega only the finite binary rationals have appeared. Day omega sees the sudden emergence of all the reals along with 1/omega added to and subtracted from each rational, as well as -omega and omega. Except for -omega and omega, the quotienting eliminates the 1/omega perturbations, yielding exactly the real line plus endpoints. Exactly the same quotienting happens with Peter's final coalgebra, whose elements are representable as finite and infinite strings over {-,+} (the 0 is eliminated by allowing strings to be finite; if you want all strings to be infinite, put 0 back in the alphabet and use it to pad the infinite strings to infinity). For example ---+++++... and --+----... are identified by both Conway and Freyd. Using Peter's choice of [-1,1] as the represented interval, these are both -1/4. Using Conway's number system, these are respectively -2 - 1/omega and -2 + 1/omega, which with the identification I described above become -2. In Conway's setup the finite constant sequences are the integers, with the empty sequence being 0 and counting being done in unary. At the first sign reversal the bits jump mysteriously from unary to binary, not by fiat but as a surprising consequence of a definition of addition that on the face of is so natural that you would not dream it could cause a radix jump like that. So both [-1,1] and [-omega,omega] each admit a natural final coalgebra structure for Peter's functor, namely Peter's and Conway's respectively, and I would be surprised to see a different final coalgebra in either case that was as natural. In contrast, Dusko and I exhibited a number of more or less equally convincing final coalgebra structures on [0,1) and [0,omega) for the functor product-with-omega, no one of which I would be willing to call *the* right one. Vaughan
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
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.
what exactly do you mean by corecursive? (it's guarded, and guarded equations do have unique fixpoints.) -- dusko
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
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
participants (4)
-
Dusko Pavlovic -
Peter Freyd -
Peter Selinger -
Vaughan Pratt