ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 44
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.2. Isomorphism, Duality, and Zero Objects (cont.)
|
| Returning to the definition of Srd, composition is defined to be the usual
| composition q’ o q of total functions. That this is well defined is best
| seen from "diagram pasting":
|
| X f X
| o<----------------------------o
| ^| |
| / | |
| / | |
| / | |
| x_0 / | q | q
| / | |
| / | |
| / | |
| / y_0 v h v
| 1 o-------->o<----------------------------o
| \ | Y | Y
| \ | |
| \ | |
| \ | |
| z_0 \ | q’ | q’
| \ | |
| \ | |
| \ | |
| vv k v
| o<----------------------------o
| Z Z
|
| For example,
|
| k(q’q) = (q’q)f,
|
| because
|
| k(q’q) = (kq’)q = (q’h)q = q’(hq) = q’(qf) = (q’q)f.
|
| Axiom (b) of 2.1.1 [the associative property] is obvious since the
| composition of total functions is associative. The identities for
| axiom (c) are the obvious ones:
|
| X f X
| o<----------------------------o
| ^| |
| / | |
| x_0 / | |
| / | |
| / | |
| 1 o | id_X | id_X
| \ | |
| \ | |
| x_0 \ | |
| \ | |
| vv v
| o<----------------------------o
| X f X
|
| Now claim: If q : (X, x_0, f) -> (Y, y_0, h) is a Srd-morphism, then q
| is an isomorphism in Srd if and only if q is bijective. On the one hand,
| if q is an isomorphism then there exists p : (Y, y_0, h) -> (X, x_0, f)
| with q o p = id_Y and p o q = id_X, so q is bijective. Conversely, if q
| is bijective then there exists a function p : Y -> X with q o p = id_Y and
| p o q = id_X. Is such p a morphism : (Y, y_0, h) -> (X, x_0, f)? Consider
| the diagram below -- the ?'s indicate places where commutativity is yet to
| be proved.
|
| X f X
| o<----------------------------o
| ^| |
| / | |
| / | |
| / | |
| x_0 / | q | q
| / | |
| / | |
| / | |
| / y_0 v h v
| 1 o-------->o<----------------------------o
| \ | Y | Y
| \ ? | |
| \ | |
| \ | |
| x_0 \ | p ? | p
| \ | |
| \ | |
| \ | |
| vv v
| o<----------------------------o
| X f X
|
| Well, reading from the diagram above:
|
| (ph)q = p(hq) = p(qf) = (pq)f
|
| = id_X f = f = f id_X
|
| = f(pq) = (fp)q.
|
| Thus:
|
| ph = (ph)(q q^-1) = ((ph)q) q^-1
|
| = ((fp)q) q^-1 = (fp)(q q^-1) = fp.
|
| Similarly:
|
| p(y_0) = p(q(x_0)) = (pq)(x_0) = id_X (x_0) = x_0.
|
| We reiterate the desire that objects in a category should be isomorphic
| just in case they are "abstractly the same". This works out well for the
| category of recursion data above where if q : (X, x_0, f) -> (Y, y_0, g)
| is an isomorphism, the bijection q transports x_0 to y_0 and f to g, so
| thinking of q as a "relabelling", the abstract structure is "the same".
| When designing new categories, one of the aesthetic criteria to keep
| in mind is that this technical sense of isomorphism should relate to
| intuitive ones. For example, if when defining the category of simple
| recursion data we dropped the requirement that q(x_0) = y_0 and that
| qf = gq, we would get a category whose isomorphisms were bijections,
| but here if s : N -> N is s(n) = n + 1, whereas for z : N -> N one
| has z(n) = 0, then (N, 0, s) and (N, 0, z) would be isomorphic,
| which is not desirable.
|
| Manes & Arbib, AAPS, pages 54-55.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤