ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 33
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.1. The Definition of a Category (cont.)
|
| 2. Example. 'Set', the category of 'sets and total functions'.
| Here objects are sets, a morphism f : X -> Y is a total function
| from X to Y, composition is the usual one, (gf)(x) = g(f(x)), and
| id_X (x) = x.
|
| 3. Example. 'Pfn', the category of 'sets and partial functions'.
| Here objects are sets, but a morphism f : X -> Y is a partial function
| from X to Y. Composition is as in 1.3.7. The identity (total) function
| still provides id_X. Notice that Pfn(X, Y) in the sense of definition (1)
| is exactly Pfn(X, Y) as in 1.3.4.
|
| 4. Example. 'Mfn', the category of 'sets and multivalued functions'.
| Here objects are sets, Mfn(X, Y) is as in 1.4.3 with composition
| given by 1.4.4, and id_X (x) = {x}.
|
| 5. Example. 'ANMfn', the category of sets and multivalued functions
| with "all or nothing" composition. In this example, objects are
| sets and ANMfn(X, Y) = Mfn(X, Y) but composition gf : X -> Z for
| f : X -> Y and g : Y -> Z is defined by:
|
| ( Ø if g(y) = Ø for some y in f(x),
| gf(x) = <
| ( {z in Z : there exists y in f(x) with z in g(y)} else.
|
| This is "all or nothing" in the sense that scenario 1.4.5 has been
| modified so that no output is defined if 'any' computation fails to
| terminate. The identity morphism id_X is the same as in Mfn. Thus,
| the only difference between ANMfn and Mfn is composition.
|
| Examples (2-5) are categories. For all but ANMfn, axiom (b)
| has been established in Section 1.4, (we leave the modification
| of properties 1.4.6 to ANMfn as an exercise). Axiom (c) is routine.
| Axiom (a) holds by definition -- we consider the domain and codomain
| as part of the definition of a function. In the student's likely
| first encounter with functions, elementary calculus, axiom (a) is
| not made explicit. Formulas such as x^2 are confused with functions
| and one speaks one moment of "x^2 for -1 =< x =< 10" and the next
| moment of "x^2 for 2 =< x =< 3". According to our conventions
| these are different functions. This is reasonable since these
| functions have different properties -- for example, the second
| is monotone increasing where the first is not.
|
| We again avoid a formal proof that repeated use of the associative law
| axiom (b) establishes that all n-fold compositions are equal regardless of
| parenthesization, and so can be written without parentheses as f_n ... f_1.
| The commutative designation such as 1.5.4 is useful in any category.
|
| Thus, in the diagram:
|
| A g B
| o---->o
| ^ \
| f / \ h
| / v
| X o o Y
| \ ^
| \ /
| \ /
| a \ / b
| \ /
| v /
| o
| D
|
| we understand that "ba = hgf" is asserted
| and we may emphasize this assertion by
| saying "the diagram commutes".
|
| When one regards a category as "the semantic category"
| generalizing 1.5.1, with (3), (4), (5) being examples,
| the flowscheme notation of 1.5.2 -- clearly a workable
| synonym for f : X -> Y in any category -- is useful.
| In practice, however, many other types of category
| arise. Experience dictates that virtually any class
| of structures can be made the objects of a category
| in a "natural" way. Some of the possibilities are
| explored in the exercises. We turn now to examples
| of categories that are useful in this book but not
| necessarily as "semantic" categories.
|
| Manes & Arbib, AAPS, pages 40-41.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤