ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 45
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.3. Products and Coproducts
|
| In this section we show that two constructions of set theory which
| play an important role in program semantics -- Cartesian products
| and disjoint unions -- can be described in category-theoretic terms
| and so generalize to a wide class of categories. While the original
| constructions seem unrelated, their category-theoretic descriptions are
| seen to be dual. Cartesian products abstract to products in a category
| whereas disjoint unions abstract to coproducts, it being common to indicate
| duality by the prefix "co" as discussed earlier in 2.2.13. Coproducts are
| an important structural aspect of the partially additive categories in the
| next chapter.
|
| We begin by describing Cartesian products of sets. The term "Cartesian" honors
| the mathematician René Descartes who developed plane analytic geometry whereby
| the plane is represented as the set of all ordered pairs (x, y) with x and y
| in the set R of real numbers. Thus, the plane is R x R where, in general,
| for any two sets X, Y their 'Cartesian product' is the set:
|
| X x Y = {(x, y) : x in X, y in Y}
|
| of all ordered pairs with x in X and y in Y. If a program fragment had two
| variables x and y taking values in the sets X and Y, respectively, then X x Y
| would comprise all possible values which could be taken by the two variables
| taken together. Turning to a formal analysis, we offer the following precise
| description of an ordered pair (x, y) in X x Y which, if somewhat pedantic, is
| useful for generalizing to the product of infinitely many sets. If we invent
| a convenient two-element set, say {i, j}, an ordered pair in X and Y amounts
| to a total function f : {i, j} -> X |_| Y with f(i) in X and f(j) in Y.
| The relationship between (x, y) and f is that f(i) = x and f(j) = y, and
| this formula defines (x, y) in terms of f, and f in terms of (x, y), and,
| indeed, establishes a bijective correspondence between the f and the (x, y).
| We could then regard X x Y as the set of all functions f : {i, j} -> X |_| Y
| with f(i) in X and f(j) in Y. This leads to the following general definition:
|
| 1. Definition. Let (X_i : i in I) be any family of sets.
| Their 'Cartesian product' is the set of all functions:
|
| f
| I ---> |_|^(i in I) X_i
|
| such that f(i) is in X_i for each i in I.
| We denote this set of functions by:
|
| ]¯[_(i in I) X_i or ]¯[ {X_i : i in I}.
|
| Often family notation is used so we write (x_i : i in I) instead of f,
| where f(i) = x_i. This directly generalizes the motivating comments
| above where I has two elements.
|
| 2. Example. If I = {p, a, s} and if X_p is a set of persons, X_a is a set
| of age values, say {16, 17, ..., 80}, and X_s = {male, female}, then
|
| ]¯[_(i in I) X_i
|
| is a suitable value object for a data base "record"
| for a person's age and sex.
|
| Manes & Arbib, AAPS, pages 57-58.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤