ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 22
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| The identity function id : !DTN! --> !DTN! was introduced
| with FPF in 1.3.8. More generally, we have the following:
|
| 7. Definition. For each set X, the 'identity function' of X,
| id_X : X -> X is the total function defined by id_X (x) = x.
| This function is in Pfn(X, X) and so may be considered in
| Mfn(X, X) as in 1.4.9-10, so that always id_X in SC(X, X).
|
| We clearly have the following:
|
| 8. For f in SC(X, Y),
|
| id_Y f = f = f id_X.
|
| We may express this by a commutative diagram:
|
| f
| X o------------------>o Y
| \ ^ \
| \ / \
| \ / \
| \ f / \
| id_X \ / \ id_Y
| \ / \
| \ / \
| \ / \
| v / f v
| X o------------------>o Y
|
| Alternatively, inventing the "through box":
|
| X o-----o X
| ----->|-----|----->
| o-----o
|
| as a flowscheme notation for id_X,
| (8) may be expressed in flowscheme
| terms by:
|
| | |
| | X | X
| v v
| o-----o | o-----o
| | | | | | |
| | f | | X | | |
| | | v | | |
| o-----o o-----o o-----o
| | | | |
| | Y = | f | = | X
| v | | v
| o-----o o-----o o-----o
| | | | | | |
| | | | | Y | f |
| | | | | | |
| o-----o v o-----o
| | |
| | Y | Y
| v v
|
| Manes & Arbib, AAPS, pages 27-28.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤