ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 30
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| 29. Definition. For A c X and f in SC(X, X) define:
|
| repeat f until A = (while A’ do f) f.
|
| It is easy to use the laws for manipulating sums to
| deduce a formula like that of (27), (see Exercise 7).
|
| A companion to the multivalued alternative construct
| of (23) is the multivalued repetitive construct:
|
| do p_1 -> f_1 [] ... [] p_n -> f_n od
|
| which is intended to mean "pick any i for which guard p_i is true and
| execute f_i; repeat until no such i exists and then exit". Since
| the choice of i is multivalued, many successful computation paths
| are possible. A suitable formal definition of the semantics
| is the following:
|
| 30. Definition. Let p_1, ..., p_n be guard functions
| in Pfn(X, X) and let f_1, ..., f_n be in Mfn(X, X).
| Then the 'multivalued repetitive construct' is:
|
| do p_1 -> f_1 [] ... [] p_n -> f_n od
|
| = while A do if p_1 -> f_1 [] ... [] p_n -> f_n fi,
|
| where if p_i = inc_A_i, then A = A_1 |_| ... |_| A_n.
|
| This may be expressed as an infinite sum (see Exercise 8).
|
| 31. Example. For A c X, f in SC(X, X), g in SC(X, Y) we have the
| identity [of the constructs in the following two flowschemes]:
|
| |
| |
| o-------------------------->| X
| | |
| | v
| | o
| | / \
| | / \
| | T / \ F
| | o-------------o A o-------------o
| | | \ / |
| | | \ / |
| | | \ / |
| | v o v
| | o-------o o-------o
| | | | | |
| | | f | | g |
| | | | | |
| | o-------o o-------o
| | | |
| | | | Y
| | | |
| o---------o v
|
| =============================================================
|
| |
| |
| | X
| |
| v
| o
| / \
| / \
| T / \ F
| o---------o A o---------o
| | \ / |
| o--------------------->| \ / |
| | | \ / |
| | v o v
| | o o-------o
| | / \ | |
| | / \ | g |
| | T / \ F | |
| | o---------o A o---------o o-------o
| | | \ / | |
| | | \ / | |
| | | \ / | |
| | v o v |
| | o-------o o-------o |
| | | | | | |
| | | f | | g | |
| | | | | | |
| | o-------o o-------o |
| | | | |
| | | | |
| | | | |
| o--------o o-------------o
| |
| | Y
| |
| v
|
| that is,
|
| g (while A do f) = if A then g (while A do f) else g.
|
| A formal proof is as follows, where we make use of (15), (16), (25).
|
| if A then g (while A do f) else g
|
| 0/0
| = { g Sum inc_A’ (f inc_A)^n } inc_A + g inc_A’
| n=0
|
| 0/0
| = g { Sum inc_A’ (f inc_A)^n } + g inc_A’
| n=1
|
| <since inc_A’ inc_A = 0, while inc_A inc_A = inc_A>
|
| 0/0
| = g { Sum inc_A’ (f inc_A)^n }
| n=0
|
| <since the sum in parentheses 'is' defined>
|
| = g (while A do f).
|
| Manes & Arbib, AAPS, pages 34-36.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤