ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 35
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.1. The Definition of a Category (cont.)
|
| Partially ordered sets form a category.
|
| 10. Example. Define 'Poset' to be the category whose objects are posets
| and with Poset((P, =<), (P', =<')) the set of all total functions
| f : P -> P' which are 'monotone' in the sense that:
|
| if x_1 =< x_2 then f(x_1) =<' f(x_2).
|
| Composition and identity morphisms are as in Set.
|
| The reader should check that Poset does then satisfy the category axioms.
|
| We next introduce another important mathematical structure.
|
| 11. Definition. A 'monoid' is a triple (M, o, e),
| where M is a set, o : M x M -> M is a function,
| and e is in M, all subject to the axioms:
|
| o is 'associative'. (x o y) o z = x o (y o z) for all x, y, z in M.
|
| e is the 'identity'. e o x = x o e = x for all x in M.
|
| As for categories, the composition
| of x_1, ..., x_n is written without
| parentheses as x_1 o ... o x_n.
|
| 12. Example. For any category C and any object X in ob(C),
| the set C(X, X) of all morphisms of X to itself forms
| a monoid under composition, with identity id_X.
|
| 13. Example. An example of a monoid familiar from
| formal language theory is (X*, conc, !e!), where
| X* is the set of all finite strings (x_1, ..., x_m),
| m >= 0, with each x_i in the given "alphabet" X.
| Here 'conc' is the operation of 'concatenation':
|
| conc((x_1, ..., x_m), (y_1, ..., y_n))
|
| = (x_1, ..., x_m, y_1, ..., y_n),
|
| and !e! = () is the 'empty string',
| namely, (x_1, ..., x_m) with m = 0.
|
| 14. Example. The category 'Mon' has monoids as objects and
| monoid homomorphisms as morphisms. Here, given two monoids
| (M, o, e) and (M', *, e'), we say that a function f : M -> M'
| is a 'monoid homomorphism' f : (M, o, e) -> (M', *, e') if and
| only if f(e) = e' and f(x o y) = f(x) * f(y) for all x, y in M.
| We define composition and identity as for functions. The reader
| should check that Mon does indeed satisfy the category axioms.
|
| Manes & Arbib, AAPS, page 43.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤