| Thread Links | Date Links | ||||
|---|---|---|---|---|---|
| Thread Prev | Thread Next | Thread Index | Date Prev | Date Next | Date Index |
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 27
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| 21. Definition. For n >= 1, an 'n-way test' on X
|
| is (p_1, ..., p_n),
|
| with each p_i an inclusion function in Pfn(X, X)
|
| and DD(p_i) |^| DD(p_j) = Ø if i =/= j.
|
| 22. Definition. Let (p_1, ..., p_n) be an n-way test on X and let
| f_1, ..., f_n be in SC(X, Y). Then a natural generalization of
| the case statement in Pascal is:
|
| case(p_1, ..., p_n) of (f_1, ..., f_n) = f_1 p_1 + ... + f_n p_n
|
| with flowscheme:
|
| |
| |
| | X
| |
| v
| o-----------------o-----------------o
| | |
| | |
| | |
| o-----o o-----o
| | | | |
| | p_1 | | p_n |
| | | | |
| o-----o o-----o
| | |
| X | . . . | X
| | |
| o-----o o-----o
| | | | |
| | f_1 | | f_n |
| | | | |
| o-----o o-----o
| | |
| | |
| | |
| o-----------------o-----------------o
| |
| |
| | Y
| |
| v
|
| The sum is defined by Proposition 18.
|
| A related construction in multifunction semantics is the following:
|
| 23. Definition. Let p_1, ..., p_n be guard functions
| in Pfn(X, X) and let f_1, ..., f_n be in Mfn(X, Y).
| Then the 'alternative construct' is:
|
| if p_1 -> f_1 [] ... [] p_n -> f_n fi
|
| = f_1 p_1 + ... + f_n p_n in Mfn(X, Y).
|
| We emphasize that the guards here are not required to have disjoint
| domains. The intended meaning is "pick any i for which the guard p_i
| is true and execute f_i". The flowscheme is the same as in (22).
|
| The Pascal if-then-else construction is a special case of (22) as follows.
|
| 24. Definition. Let A be a subset of X.
| Define A’ to be the complement of A,
| that is, A’ = {x in X : x not in A}.
| Then (inc_A, inc_A’) is a two-way
| test on X. For f, g in SC(X, Y)
| define:
|
| if A then f else g = f inc_A + g inc_A’
|
| in SC(X, Y).
|
| Two suitable flowschemes are:
|
| |
| |
| | X
| |
| v
| o
| / \
| / \
| T / \ F
| o-------------o A o-------------o
| | \ / |
| | \ / |
| | \ / |
| v o v
| o---------o o---------o
| | | | |
| | f | | g |
| | | | |
| o---------o o---------o
| | |
| | |
| | |
| o-----------------o-----------------o
| |
| |
| | Y
| |
| v
|
|
| |
| |
| | X
| |
| v
| o-----------------o-----------------o
| | |
| | |
| | |
| o---------o o---------o
| | | | |
| | inc_A | | inc_A’ |
| | | | |
| o---------o o---------o
| | |
| X | | X
| | |
| o---------o o---------o
| | | | |
| | f | | g |
| | | | |
| o---------o o---------o
| | |
| | |
| | |
| o-----------------o-----------------o
| |
| |
| | Y
| |
| v
|
| Manes & Arbib, AAPS, pages 32-33.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤