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

ONT Re: Program Semantics




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

Note 23

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

| 1.  An Introduction to Denotational Semantics
|
| 1.5.  A Preview of Partially Additive Semantics (cont.)
|
| We now introduce the fundamental operation of sum,
| first for Mfn and then for Pfn.
|
| 9.  Definition.  Let X and Y be sets.  Let I be a set and for each i in I
|     let f_i be in Mfn(X, Y).  (We say (f_i : i in I) is an I-indexed family
|     in Mfn(X, Y).)  Then the 'sum' Sum(f_i : i in I), alternatively written
|     as Sum_(i in I) f_i, or as Sum_i,I f_i, is the multifunction in Mfn(X, Y)
|     defined by:
|
|     (Sum_i,I f_i)(x)  =  |_|^i,I f_i (x)
|
|                       =  {y in Y : y in f_i (x) for some i in I}.
|
| Hence, for one-element families (meaning that I has one element)
| Sum(f) = f, and in the case where I is empty the sum maps x
| to the empty set for all x in X (see Exercise 1).
|
| If I = {1, 2, ..., n} with n >= 2, so that the family (f_i : i in I)
| has the form (f_1, ..., f_n), we write f_1 + ... + f_n as a synonym
| for Sum(f_i : i in I).  In general, we may write Sum f_i instead
| of  Sum(f_i : i in I) when I is clear from context.
|
| An intuitive flowscheme notation for summing is exemplified by the following.
|
| 10.  f + g is written:
|
|                          |
|                          |
|                          |
|                          v
|        o-----------------o-----------------o
|        |                                   |
|        |                                   |
|        |                                   |
|     o-----o                             o-----o
|     |     |                             |     |
|     |  f  |                             |  g  |
|     |     |                             |     |
|     o-----o                             o-----o
|        |                                   |
|        |                                   |
|        |                                   |
|        o-----------------o-----------------o
|                          |
|                          |
|                          |
|                          v
|
| and similarly for other families (f_i : i in I).
|
| This notation conveys the idea of (9) since an output
| from (f + g)(x) is an output from either f(x) or g(x).
|
| Manes & Arbib, AAPS, pages 28-29.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.

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