* Re: Real midpoints
1999-12-26 18:45 Real midpoints Peter Freyd
@ 1999-12-29 8:03 ` Vaughan Pratt
2000-01-17 1:23 ` Peter Selinger
1 sibling, 0 replies; 6+ messages in thread
From: Vaughan Pratt @ 1999-12-29 8:03 UTC (permalink / raw)
To: categories
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
^ permalink raw reply [flat|nested] 6+ messages in thread* Re: Real midpoints
1999-12-26 18:45 Real midpoints Peter Freyd
1999-12-29 8:03 ` Vaughan Pratt
@ 2000-01-17 1:23 ` Peter Selinger
2000-01-18 4:07 ` Dusko Pavlovic
1 sibling, 1 reply; 6+ messages in thread
From: Peter Selinger @ 2000-01-17 1:23 UTC (permalink / raw)
To: Categories List
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
^ permalink raw reply [flat|nested] 6+ messages in thread