In an earlier posting I showed how to define co-inductively the closed interval, in particular I showed that its elements are named by sequences of 0s and 1s with the usual binary-expansion equivalence relation. There is a well-known computational problem with this approach, already in the definition of the midpoint operation: at what point can you determine the first digit of the midpoint of .0000... and .1111...? At the Como meeting I learned from Andrej Bauer about a better approach. Take the elements of [-1,1] to be named by infinite sequences of _signed_ binary digits, that is -1, 0, +1. [Just to confuse matters, Scedrov and I once used signed _ternary_ digits (n Cats and Allegators for the "Freyd curve"). The signed binary expansions .+1 -1 and .0 +1 describe the same number, to wit, 1/4.] Using signed binary expansions one can compute midpoints with a little 3-state machine that takes as input the sequence of pairs of signed binary digits of the given numbers x and y, and produces as output a sequence of signed binary digits for the midpoint x|y. (There may, indeed, be momentary delays in the output, but there will not be an indefinite delay -- indeed, the number of output digits will never be more than one less than the number of pairs of input digits). The challenge is to revise the co-induction so that it is this better version that emerges. In the previous version I worked in the category of posets with _distinct_ top and bottom, that is, those posets for which not[(B = x) and (x = T)]. In the revised version I'll strengthen the condition by working in the category of posets with _separated_ top and bottom: [(B < x) or (x < T)]. (The conditions are equivalent in the presence of De Morgan's law. In a topos the top and bottom of omega are always distinct but they are separated only when De Morgan's law is satisfied throughout.) In the previous setting I defined what I'll now call the _thin_ version of the ordered-wedge of X and Y, to wit, the set of pairs, <x,y> satisfying the condition: (x = T) or (B = y). The _thick_ version is the set of pairs, <x,y> satisfying the two weaker conditions: (x < T) => (B = y) (B < y) => (x = T) (each of which is classically equivalent to the single condition used in the thin version). Easy exercise: if top and bottom are separated in X and Y, then they are separated in the thick version of the ordered-wedge XvY. (Indeed, it's enough for top and bottom to be separated in just one of X and Y . No, it is not enough to assume just that they are distinct in each.) A map X -> XvX is thus given by a pair d,u: X -> X such that for all x: (dx < T) => (B = ux) (B < ux) => (dx = T) The final coalgebra for XvX is still the closed interval, but now in the better computational sense. Let me explain. Given an arbitrary coalgebra d,u : X -> X, I need to describe a coalgebra homomorphism f: X -> I. where I is the set of equivalence types of infinite sequences of signed binary digits. The first step is to work not with elements of X but elements of XvX. Consider a machine that given <x,y>:XvX asks in parallel the questions: "B < y?" "B < ux and dy < T?" "x < T?" Exercise: If the top and bottom of X are separated and d,u describe a map to the thick ordered-wedge XvX, then at least one of these questions has a positive answer. Given z:X obtain a sequence of signed binary digits by starting with the pair <x,y> = <dz,uz> and iterating the non-deterministic procedure: If B < y then emit +1 as output and replace <x,y> with <dy,uy>; If B < ux and dy < T then emit 0 as output and replace <x,y> with <ux,dy>; If x < B then emit -1 as output and replace <x,y> with <dx,ux>. Not-so-easy exercises: regardless of the non-determinism, the element fz:[-1,+1] named by the resulting sequence is determined. Moreover, f(uz) = u(fz) and f(dz) = df(z). PS. There is some geometry behind this stuff. Let me here mention just this: given a pair <x,y> in XvX map it into the four-fold ordered-wedge XvXvXvX. Think of each of the four copies of X as one "quarter" of the whole. If B < y then the point lies inside the "top half" (the 3rd and 4th quarters). If B < ux and dy < T then the point lies inside the "middle half" (the 2nd and 3rd quarters). If x < B then the point lies inside the bottom half" (the 1st and 2nd quarters). Clearly any point is inside at least one of these three halves. The output-digit registers which of the three halves is moved to and the corresponding pair-replacement effects that move. PPS. On 22 Dec I gave a Dedekind-cut proof that the interval [0,1] constructed in the standard fashion from (unsigned) binary sequences is the final coalgebra for the functor that sends X (with distinct top and bottom) to the thin version of XvX. That proof should be replaced. First note that the midpoint-algebra homomorphism from [0,1] to [-1,1] can be effected simply by replacing each 0 with -1 and keeping each 1 as +1. Given d,u:X -> X such that for all x it is the case that either dx = T or ux = B , consider a machine that upon given x:X asks in parallel the questions "dx = T?" and "ux = B?". If dx = T then emit +1 as output and replace x with ux, If ux = B then emit -1 as output and replace x with dx. Given x:X one may iterate this (non-deterministic) procedure to obtain a sequence of +1s and -1s. Pretty-easy exercises: regardless of the non-determinism, the element fx:[-1,+1] named by the resulting sequence is determined; f(ux) = u(fx); f(dx) = df(x).
Here are a comment and a question regarding the interesting reality check. Peter Freyd wrote, among other things:
Take the elements of [-1,1] to be named by infinite sequences of _signed_ binary digits, that is -1, 0, +1.
[...]
The signed binary expansions .+1 -1 and .0 +1 describe the same number, to wit, 1/4.
In a way, the finitary identities +1 -1 == 0 +1 together with their symmetric versions -1 +1 == 0 -1 capture *all* identifications made by the quotient map 3^N -->> [-1, 1] s |--> [[s]] = s1 / 2 + s2 / 4 + ... + sn / 2^n + ... that takes a signed-digit binary expansion s to the number [[s]] that it denotes. Here 3 = {-1,0,+1}, and I am supposing initially that [-1,1] is already given. Let === be the kernel of the quotient map: s === t iff [[s]] = [[t]]. Let == be the least equivalence relation on 3^N such that s +1 -1 t == s 0 +1 t and s -1 +1 t == s 0 -1 t, where s ranges over 3^* and t over 3^N. It is easy to see that == is coarser than ===. It is *strictly* coarser as, for example, we have that -1 1 1 1 1 1 1 1 1 ... === 1 -1 -1 -1 -1 -1 -1 ..., because both sequences denote the number zero, but === cannot be replaced by ==, because these two sequences cannot be made equal by finitely many applications of the identities. HOWEVER, if one endows 3^N with the Cantor topology (the product of the discrete topology of 3), then the relation === is the topological closure of the relation == in the product space 3^N x 3^N. That is, all we need to do in order to get === from == is to add limits. Thus, === can be defined in a topologico-combinatorial way *without* reference to a previously existing interval [-1,1]. Therefore we have a simple direct (classical) construction of the Euclidean interval [-1,1] as a topological quotient of 3^N by an easily defined equivalence relation of finite character. (NB. Of course, === has to be closed, because [-1,1] is Hausdorff and the semantic map is continuous (and hence a topological quotient map, as it is a surjection of compact Hausdorff spaces). Thus, another way of putting the above is to say that == fails to be === only by failing to be closed.) Moreover, there is a *computable* idempotent function f : 3^N x 3^N --> 3^N x 3^N with the property that if f(s,t)=(s',t') then (1) s===s', t===t' and (2) if s===t then s' = t' (Yes, I mean this; s' and t' are the *same* sequence.) As this may sound puzzling at first sight, let me observe that it doesn't help in effectively deciding equality, nor does it show that numbers would have canonical representatives, because norm(s,s)=(s,s) is consistent with the above specification. Such a function f(s,t) is computed by a finite automaton that tries to apply the two identities to make s and t equal, by scanning longer and longer finite prefixes of s and t, where this attempt fails at some finite stage if and only if s and t denote distinct numbers. At most n+2 digits of input have to be scanned in order to produce n digits of output. (Reference: "Effective and sequential definition by cases on the reals via infinite signed-digit numerals", Volume 13 of Electronic Notes in Theoretical Computer Science, 1998.) --------- Question: --------- Can we replace topology by coinduction in the formulations (and proofs) of the above properties? Martin Escardo
participants (2)
-
Martin Escardo -
Peter Freyd