ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 21
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics
|
| In this section we consider partial functions and multifunctions
| as frameworks for denotational semantics without reference to
| any particular programming language. Basic constructions
| such as chaining, conditional testing, and looping
| are described at the function level. The term
| "partially additive" refers to a kind of
| sum operation which can be defined on
| the sets Pfn(X, Y), Mfn(X, Y), (and
| more generally in Section 3.2).
|
| To fix the context we must choose just one of "partial function" or
| "multifunction", that is, we must specify the "semantic category" in
| the sense of the following definition (which will be generalized in the
| next chapter.
|
| 1. Definition. The 'semantic category' is either Pfn (for partial functions)
| or Mfn (for multifunctions). We adopt the noncommittal notation SC(X, Y)
| to mean "Pfn(X, Y) if the semantic category is Pfn and Mfn if the semantic
| category is Mfn".
|
| 2. Notation. We will use all the notations:
|
| f : X -> Y
|
| f
| X ---> Y
|
|
| X o-----o Y
| ----->| f |----->
| o-----o
|
| as synonyms for f in SC(X, Y). These may appear geometrically reoriented
| in diagrams, for example, right-to-left, vertically, diagonally, and so on.
| The last notation is "flowscheme" notation.
|
| The important operation of iterated composition has already been
| introduced (in 1.4.4, 1.4.6-8 for Mfn, 1.3.7, 1.4.11 for Pfn).
| If f_i in SC(X_i-1, X_i) for i = 1, ..., n, suitable flowscheme
| notation for the composition f_n ... f_1 in SC(X_0, X_n) is:
|
| 3.
|
| X_0 o---------o X_1 X_n-1 o---------o X_n
| --------->| f_1 |---------> . . . --------->| f_n |--------->
| o---------o o---------o
|
| f
| The labeled arrow notation X -----> Y is
| useful in "commutative diagrams" such as:
|
| 4.
| f_1 f_2
| X_0 o-------->o-------->o X_2
| |\ X_1 / \
| | \ / \
| | \ / \
| | \ / \
| | g \ / f_3 \ h
| | \ / \
| | \ / \
| | \ / \
| | v v f_4 v
| \ o------------------>o X_4
| \ X_3 |
| \ |
| f \ | f_5
| \ |
| \ v
| ---------------------->o X_5
|
| in which our convention is the following:
|
| 5. In a diagram such as (4), if two paths of arrows begin at the same place
| and end at the same place, then, unless the contrary is indicated, the
| compositions of these paths are asserted to be equal. To emphasize
| this assertion we say "the diagram commutes".
|
| Thus, in (4), we have the following equations:
|
| g = f_3 f_2 f_1 in SC(X_0, X_3),
|
| h = f_4 f_3 in SC(X_2, X_4),
|
| h f_2 f_1 = f_4 g in SC(X_0, X_4),
|
| f = f_5 f_4 f_3 f_2 f_1 in SC(X_0, X_5),
|
| and so on. Notation such as:
|
| 6.
| f
| X o------------------>o Y
| \ /
| \ /
| \ ? /
| \ /
| h \ / g
| \ /
| \ /
| \ /
| v v
| o
| Z
|
| could be used to indicate that h is not
| necessarily the same as gf in SC(X, Z).
|
| Manes & Arbib, AAPS, pages 26-27.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤