hi. almost a year after peter freyd posted his version of the coalgebra of real numbers (henceforth coreals), i finally tried to cash in on my initial excitement with it, and spec out the coinductive programs for addition and multiplication. however, i must report that i am a bit stuck. since i am also guilty of not having tried to work this out in time, i'll try to refresh things (at least for myself) by reporting in some detail. the reason why i was excited, as i think i explained at the time, was that peter seemed to be able to define the algebraic operations on his coreals by a relatively simple *stream* coinduction. for the coreals vaughan pratt and i had previously constructed, i only knew how to do this using the *conway games*, ie cuts, which appeared to be the most inefficient way imaginable. let me clarify the context a little, and why any of this matters. first of all, why another presentation of reals, when there are already so many deep and beautiful presentations, left behind the centuries of analysis? well, in spite of all that math, the CS students still learn that real numbers must be truncated, because they are infinite, whereas the computers are finite. as if computers are more finite than our heads, or smaller than our calculus textbooks. so the task is to find a presentation of the "real reals" suitable for computers. and the hypothesis is that coinduction allows such presentations. and indeed, we have several different coinductive implementations of the datatype of reals, and it has also been shown that a lot of what people do in differential calculus yields to coinduction. but the problem is that coalgebraically implemented reals offer some resistance to algebra: adding and multiplying computable reals may not be computable. if each real number is represented irredundantly, say by a unique stream of digits, then there will be numbers for which the entire infinite streams of digits will need to be consumed before the first digit of their sum, or product, can be determined. this observation is due to brouwer, and has been mentioned in this thread several times, in one form or another. in any case, in order to implement coreal algebra, besides a real coalgebra R, we also need a *redundant numeration system*, a surjection D^N --->> R mapping to each number the streams of D-digits representing it (plus some structure saying this). the coalgebras vaughan and i had constructed represent each number by a unique stream, and didn't seem to have good numeration systems. (now i think at least two of them have decent *generalized* numerations --- later more.) in contrast, peter's coalgebra represented reals as equivalence classes of streams, and thus came equipped with natural numerations! true, they were never mentioned explicitly, probably because XvX was viewed as a subobject of XxX, in order to allow splitting X--->XvX as a pair <d,u>. but viewing XvX as the quotient of X+X = 2xX displays the final coalgebra I of XvX as the quotient of the final coalgebra 2^N of 2xX. hence the numeration 2^N --->> I corresponding to the standard binary expansion. of course, this system is not fully redundant (i think andrej bauer pointed this out), but the transition to the signed binary expansion 3^N --->> I where 3 = {-1,0,1}, is almost as well known... (ok, i only learned of it from martin escardo's thesis, but the real aritmeticists surely know all about it.) in any case, it seemed reasonable to expect that freyd's elegant derivations lift to the redundant numerations, viz the streams lurking at the intuitive background of all constructions. and indeed, the midpoint operation lifts to a coinductive definition on 3^N. but nothing beyond that point works for me. in particular, i don't know how to construct from the closed interval *with a numeration system* a *coalgebra* of all reals, *with the corresponding numeration*. neither of the reflection of midpoint algebras in abelian groups, nor the extension of the "yoneda" embedding of the interval in its endomorphism monoid extends to the numeration systems. how do you enrich the structure of abelian group by a numeration system? what should the midpoint algebra homomorphisms lift on the attached numerations? the alternative that i keep pushing are the conway coreals. the finite and infinite lists of 1 and -1 yield an irredundant representation of the real line, extended with the infinity on both ends. to get the real number corresponding to a list, sum up the initial 1s or -1s, until the sign changes. this is the integer part of the number. after that point, sum up the entries of the list divided by increasing powers of 2. this is, of course, gonshor's version of surreal numbers. it is a retract of the conway's version. but conway's games can be viewed as {L,R}-labelled hypersets. so they form a final coalgebra. the addition, and the multiplication arise as *eminently* coinductive operations. the addition happens to be defined by a coalgebra similar to the one defining the product of analytic functions, and the asynchronous product of processes. conway's definitions of all algebraic operations are very nice examples of coinductive programming. the idea is now to use gonshor's version as the real coalgebra, and conway's version as a generalized numeration system: instead of streams of digits, use {L,R}-labelled graphs, viz hypersets. gonshor's numbers correspond to the minimal representatives of conway's numbers, so they embed canonically; whereas conway's *simplicity theorem* yields the retraction. in practice, given two real numbers, say to add, and the desired precision of the result, you replace them by sufficiently small binary intervals, ie the simplest binary numbers contained. these lift to finite conway games, and easily add. finding the simplest form is trivial. i am not sure whether i am missing something, but with this approximation part, the algorithm does not seem inefficient at all any more. originally, this story was invented for the coalgebra of alternating dyadics, which has appeared in my paper with vaughan pratt. but alternating dyadics are easily seen to be just a version of gonshor's representation. and just like alternating dyadics/gonshor reals embed in conway's games, our coalgebra of continued fractions embeds in contorted fractions, mentioned by peter johnstone... one would expect that that numeration system might be still a bit more efficient, or less inefficient, though i didn't look at the details at all... happy halloween, -- dusko