ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 29
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| Repetitive constructs may be defined using infinite sums. For example:
|
| 27. Definition. For A c X and f in SC(X, X) define:
|
| while A do f
|
| = Sum_(n=0,OO) inc_A’ (f inc_A)^n
|
| in SC(X, X)
|
| (where, for g in SC(Y, Y), g^n is defined by g^0 = id_Y, g^(n+1) = g^n g)
| with one summand for each number n of traversals of the loop in either of
| these two variant flowschemes:
|
| |
| |
| o-------------------------->| X
| | |
| | v
| | o
| | / \
| | / \
| | T / \ F
| | o-------------o A o-------------o
| | | \ / |
| | X | \ / | X
| | | \ / |
| | v o v
| | o---------o
| | | |
| | | f |
| | | |
| | o---------o
| | |
| | |
| | |
| o---------o
|
|
| |
| |
| o-------------------------->| X
| | |
| | v
| | o-----------------o-----------------o
| | | |
| | | |
| | v v
| | o---------o o---------o
| | | | | |
| | | inc_A | | inc_A’ |
| | | | | |
| | o---------o o---------o
| | | |
| | X | | X
| | v v
| | o---------o
| | | |
| | | f |
| | | |
| | o---------o
| | |
| | |
| o---------o
|
| That the sum exists when the semantic category is Pfn
| is clear from the fact that:
|
| 28. DD(inc_A’ (f inc_A)^n)
|
| = {x in X : x, f(x), ..., f^(n-1)(x) in A, and f^n (x) not in A},
|
| which ensures that x is in DD(inc_A’ (f inc_A)^n) for at most one n.
|
| Manes & Arbib, AAPS, page 34.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤