ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 28
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 1. An Introduction to Denotational Semantics
|
| 1.5. A Preview of Partially Additive Semantics (cont.)
|
| The sum operation and composition lead to a calculus to
| manipulate functions. We begin with two basic properties
| of inclusion functions whose proof is obvious and follow this
| with an example that simplifies a compound conditional statement.
|
| 25. Proposition. Let A and B be subsets of X. Then:
|
| a. inc_A inc_B = inc_(A |^| B) = inc_B inc_A.
|
| b. If A |^| B = Ø,
|
| then inc_A + inc_B exists,
|
| and inc_A + inc_B = inc_(A |_| B).
|
| 26. Example. If A, B c X, and f, g, h in SC(X, Y), then:
|
| if A then (if B then f else g) else (if A’ then f else h)
|
| = (f inc_B + g inc_B’)inc_A + (f inc_A’ + h inc_A)inc_A’
|
| <since A’’ = A>
|
| = f inc_B inc_A + g inc_B’ inc_A + f inc_A’ inc_A’ + h inc_A inc_A’
|
| <by (15)>
|
| = f inc_(A |^| B) + g inc_(A |^| B’) + f inc_A’
|
| <by (25)>
|
| = f(inc_(A |^| B) + inc_A’) + g inc_(A |^| B’)
|
| <by (15) since the sum in parentheses is defined by (25)>
|
| = f(inc_((A |^| B) |_| A’)) + g inc_(A |^| B’)
|
| <by (25)>
|
| = f inc_(A |^| B’)’ + g inc_(A |^| B’)
|
| = if A |^| B’ then g else f.
|
| Manes & Arbib, AAPS, pages 33-34.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤