Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

ONT Re: Program Semantics




¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

Note 34

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

| 2.  An Introduction to Category Theory
|
| 2.1.  The Definition of a Category (cont.)
|
| 6.  Definitions.  A 'partially ordered set', or 'poset' for short,
|     is a pair (P, =<) where P is a set and =< is a binary relation
|     on P which is a 'partial order' on P.  This is defined to mean
|     that the following three axioms hold for all x, y, z in P.
|
|     'Reflexivity'.   x =< x.
|
|     'Transitivity'.  If x =< y and y =< z, then x =< z.
|
|     'Antisymmetry'.  If x =< y and y =< x, then x = y.
|
| We emphasize that the symbol =< has no à priori meaning.
| 'Any' relation satisfying the three axioms is a partial order,
| and many different partial orders may be of interest on one set.
|
| While other symbols could be used, for example,
| xRy instead of x =< y, the =< symbol gives rise
| to the following associated definitions.  In a
| poset (P, =<) we say that:
|
|     x  <  y    if x =< y but x =/= y,
|
|     x  >= y    if y =< x,
|
|     x  >  y    if y  < x,
|
|     x =/< y    if it is false that x =< y,
|
|                warning:  not equivalent to x > y,
|                e.g., see the Hasse diagram below.
|
| x /< y,  x /> y,  x >/= y are defined similarly.  It is not
| so clear how to obtain similar conventions with the symbol R.
|
| A useful device for drawing finite posets galore
| is the 'Hasse diagram', an example of which is:
|
|     d        e
|      o       o
|       \     / \
|        \   /   \
|         \ /     \
|        b o       o c
|           \     /
|            \   /
|             \ /
|              o
|              a
|
| Here P is the set of nodes (= o's);  P = {a, b, c, d, e} in this example.
| The partial order is defined by x =< y if and only if x = y or x is below y
| and there exists an upward path from x to y.  It is easy to see that (P, =<)
| is always a poset.  In the above example, a =< b, a =< d, while b and c are
| 'incomparable' because b =/< c and c =/< b.
|
| A 'totally ordered' set is a partially ordered set (P, =<) in which every two
| elements are comparable -- given x, y at least one of x =< y or y =< x holds.
| The term 'partially' ordered set refers to the possibility that incomparable
| pairs may exist.
|
| Posets are fundamental structures arising frequently in
| mathematics and theoretical computer science.  They play
| several roles in this book.  Here are some examples of
| posets:
|
| 7.  Example.  If N = {0, 1, 2, ...} is the set of natural numbers and
|     =< has its usual meaning, then (N, =<) is a totally ordered set.
|
| 8.  Example.  If Y is any set and !P!(Y) is the set of subsets of Y,
|     then (!P!(Y), c) is a poset where A c B is the subset inclusion.
|     Notice that we may have:
|
|     o-----------------------------o
|     |              Y              |
|     |      o-----o   o-----o      |
|     |     /       \ /       \     |
|     |    /         o         \    |
|     |   /         / \         \   |
|     |  o         o   o         o  |
|     |  |    A    |   |    B    |  |
|     |  |         |   |         |  |
|     |  o         o   o         o  |
|     |   \         \ /         /   |
|     |    \         o         /    |
|     |     \       / \       /     |
|     |      o-----o   o-----o      |
|     |                             |
|     o-----------------------------o
|
| that is, A, B in !P!(Y) but neither A c B nor B c A holds.  Thus,
| if Y has two or more elements, (!P!(Y), c) is not totally ordered.
|
| 9.  Example.  For any two sets X, Y and f, g in Pfn(X, Y) define
|     f =< g to mean 'g extends f', that is, "for x in X where f(x)
|     is defined, there g(x) is also defined and then g(x) = f(x)".
|     Then (Pfn(X, Y), =<) is a poset which is not totally ordered.
|     This example is important in Section 5.1.
|
| Manes & Arbib, AAPS, pages 41-42.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤